tests/smv/run-single.sh

   1 #!/bin/bash
   2
   3 cat > $1.tpl <<EOT
   4 %module main
   5   INVARSPEC ! bool(_trigger)
   6 EOT
   7
   8 cat > $1.ys <<EOT
   9 echo on
  10
  11 read_ilang $1.il
  12 hierarchy; proc; opt
  13 rename -top uut
  14 design -save gold
  15
  16 synth
  17 design -stash gate
  18
  19 design -copy-from gold -as gold uut
  20 design -copy-from gate -as gate uut
  21 miter -equiv -flatten gold gate main
  22 hierarchy -top main
  23
  24 dump
  25 write_smv -tpl $1.tpl $1.smv
  26 EOT
  27
  28 set -ex
  29
  30 ../../yosys -l $1.log -q $1.ys
  31 NuSMV -bmc $1.smv >> $1.log
  32 grep "^-- invariant .* is true" $1.log
  33