aboutsummaryrefslogtreecommitdiffstats
path: root/tests/smv/run-single.sh
blob: a261f4ea6532c1840e2d625181b4b37fd8c008ae (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
#!/bin/bash

cat > $1.tpl <<EOT
%module main
  INVARSPEC ! bool(_trigger)
EOT

cat > $1.ys <<EOT
echo on

read_ilang $1.il
hierarchy; proc; opt
rename -top uut
design -save gold

synth
design -stash gate

design -copy-from gold -as gold uut
design -copy-from gate -as gate uut
miter -equiv -flatten gold gate main
hierarchy -top main

dump
write_smv -tpl $1.tpl $1.smv
EOT

set -ex

../../yosys -l $1.log -q $1.ys
NuSMV -bmc $1.smv >> $1.log
grep "^-- invariant .* is true" $1.log