blob: 63de465c05c1c0ec972c22af644b0b6351539d93 (
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
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.'
|
