backends/btor/test_cells.sh

   1 #!/bin/bash
   2
   3 set -ex
   4
   5 rm -rf test_cells.tmp
   6 mkdir -p test_cells.tmp
   7 cd test_cells.tmp
   8
   9 ../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod'
  10
  11 for fn in test_*.il; do
  12         ../../../yosys -p "
  13                 read_ilang $fn
  14                 rename gold gate
  15                 synth
  16
  17                 read_ilang $fn
  18                 miter -equiv -make_assert -flatten gold gate main
  19                 hierarchy -top main
  20                 write_btor ${fn%.il}.btor
  21         "
  22         boolectormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out
  23         if grep " SATISFIABLE" ${fn%.il}.out; then
  24                 echo "Check failed for ${fn%.il}."
  25                 exit 1
  26         fi
  27 done
  28
  29 echo "OK."
  30