From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 3 Oct 2019 18:11:50 +0000 (-0700)
Subject: Use `sat -tempinduct` and comments for why equiv_opt not sufficient
X-Git-Tag: working-ls180~1000^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=045f34403889b69f3ac3ac08d96e5cf1fae787d1;p=yosys.git

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

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 4b130578b..ee5ad8a1a 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -188,6 +188,13 @@ endmodule
 EOT
 
 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
 
 design -save gold
@@ -197,7 +204,7 @@ design -stash gate
 design -import gold -as gold
 design -import gate -as gate
 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
 select -assert-count 1 t:$dff r:WIDTH=4 %i