mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-26 13:06:12 +00:00
Code Activity

Various fixes and improvements in "write_smt2 -bv"

Browse source
This commit is contained in:
Clifford Wolf 2014-12-25 20:28:16 +01:00
parent b748622a7f
commit e8c12e5f0c
3 changed files with 43 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

18
backends/smt2/test_cells.sh
View file

@ -6,7 +6,7 @@ rm -rf test_cells
mkdir test_cells
cd test_cells
../../../yosys -p 'test_cell -n 2 -w test all /$alu /$macc /$fa /$lcu /$lut /$shift /$shiftx /$div /$mod'
../../../yosys -p 'test_cell -muxdiv -w test all /$alu /$macc /$fa /$lcu /$lut /$shift /$shiftx'
cat > miter.tpl <<- EOT
; #model# (set-option :produce-models true)
@ -18,7 +18,7 @@ cat > miter.tpl <<- EOT
; #model# (get-value ((|miter_n in_A| s) (|miter_n in_B| s) (|miter_n gold_Y| s) (|miter_n gate_Y| s) (|miter_n trigger| s)))
EOT
for x in test_*.il; do
for x in $(set +x; ls test_*.il | sort -R); do
x=${x%.il}
cat > $x.ys <<- EOT
read_ilang $x.il
@ -34,8 +34,11 @@ for x in test_*.il; do
dump
write_smt2 -bv -tpl miter.tpl $x.smt2
EOT
../../../yosys $x.ys
cvc4 $x.smt2 > $x.result
../../../yosys -q $x.ys
if ! cvc4 $x.smt2 > $x.result; then
cat $x.result
exit 1
fi
if ! grep unsat $x.result; then
echo "Proof failed! Extracting model..."
sed -i 's/^; #model# //' $x.smt2
@ -43,3 +46,10 @@ for x in test_*.il; do
exit 1
fi
done
set +x
echo ""
echo " All tests passed."
echo ""
exit 0