backends/smv/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 # don't test $mul to reduce runtime
  10 # don't test $div and $mod to reduce runtime and avoid "div by zero" message
  11 ../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$macc /$mul /$div /$mod'
  12
  13 cat > template.txt << "EOT"
  14 %module main
  15   INVARSPEC ! bool(_trigger);
  16 EOT
  17
  18 for fn in test_*.il; do
  19         ../../../yosys -p "
  20                 read_ilang $fn
  21                 rename gold gate
  22                 synth
  23
  24                 read_ilang $fn
  25                 miter -equiv -flatten gold gate main
  26                 hierarchy -top main
  27                 write_smv -tpl template.txt ${fn#.il}.smv
  28         "
  29         nuXmv -dynamic ${fn#.il}.smv > ${fn#.il}.out
  30 done
  31
  32 grep '^-- invariant .* is false' *.out || echo 'All OK.'
  33