diff options
| author | Clifford Wolf <clifford@clifford.at> | 2015-08-12 12:56:20 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2015-08-12 12:56:20 +0200 |
| commit | f81bf9bdea7f99602bc2c7f0d43f1058a716508e (patch) | |
| tree | 16ff66d3734b4793ad765d29f0cba3e3c7a55154 /backends | |
| parent | 667b0150185d53578b002a00df9c4f347a35fed2 (diff) | |
| download | yosys-f81bf9bdea7f99602bc2c7f0d43f1058a716508e.tar.gz yosys-f81bf9bdea7f99602bc2c7f0d43f1058a716508e.tar.bz2 yosys-f81bf9bdea7f99602bc2c7f0d43f1058a716508e.zip | |
Added SMV back-end 'test_cells.sh' script
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smv/test_cells.sh | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/backends/smv/test_cells.sh b/backends/smv/test_cells.sh new file mode 100644 index 000000000..63de465c0 --- /dev/null +++ b/backends/smv/test_cells.sh @@ -0,0 +1,33 @@ +#!/bin/bash + +set -ex + +rm -rf test_cells.tmp +mkdir -p test_cells.tmp +cd test_cells.tmp + +# don't test $mul to reduce runtime +# don't test $div and $mod to reduce runtime and avoid "div by zero" message +../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$macc /$mul /$div /$mod' + +cat > template.txt << "EOT" +%module main + INVARSPEC ! bool(_trigger); +EOT + +for fn in test_*.il; do + ../../../yosys -p " + read_ilang $fn + rename gold gate + synth + + read_ilang $fn + miter -equiv -flatten gold gate main + hierarchy -top main + write_smv -tpl template.txt ${fn#.il}.smv + " + nuXmv -dynamic ${fn#.il}.smv > ${fn#.il}.out +done + +grep '^-- invariant .* is false' *.out || echo 'All OK.' + |