6 mkdir
-p test_cells.tmp
9 # don't test $mul to reduce runtime
10 # don't test $div/$mod/$modfloor 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 /$modfloor'
13 cat > template.txt
<< "EOT"
15 INVARSPEC
! bool
(_trigger
);
18 for fn
in test_
*.il
; do
25 miter -equiv -flatten gold gate main
27 write_smv -tpl template.txt ${fn#.il}.smv
29 nuXmv
-dynamic ${fn#.il}.smv
> ${fn#.il}.out
32 grep '^-- invariant .* is false' *.out ||
echo 'All OK.'