riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Use `sat -tempinduct` and comments for why equiv_opt not sufficient

This commit is contained in:
Eddie Hung 2019-10-03 11:11:50 -07:00
parent e9645c7fa7
commit 045f344038
1 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
tests/various/peepopt.ys
View File

@ -188,6 +188,13 @@ endmodule
EOT EOT
proc proc
# NB: equiv_opt uses equiv_induct which covers
# only the induction half of temporal induction
# --- missing the base-case half
# This makes it akin to `sat -tempinduct-inductonly`
# instead of `sat -tempinduct-baseonly` or
# `sat -tempinduct` which is necessary for this
# testcase
#equiv_opt -assert peepopt #equiv_opt -assert peepopt
design -save gold design -save gold
@ -197,7 +204,7 @@ design -stash gate
design -import gold -as gold design -import gold -as gold
design -import gate -as gate design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -seq 1 -verify -prove-asserts -show-ports miter sat -tempinduct -verify -prove-asserts -show-ports miter
design -load gate design -load gate
select -assert-count 1 t:$dff r:WIDTH=4 %i select -assert-count 1 t:$dff r:WIDTH=4 %i