summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2015-02-21 17:43:49 +0100
committerClifford Wolf <clifford@clifford.at>2015-02-21 17:43:49 +0100
commitdcbd00c101465323d173fac9bc5efb4f0d19f377 (patch)
tree437f06c002bb65b9541c488ac502377d18bc637e /passes
parent49dd9c713f008173100e159782223aede631b510 (diff)
Fixed basecase init for "sat -tempinduct"
Diffstat (limited to 'passes')
-rw-r--r--passes/sat/sat.cc7
1 files changed, 6 insertions, 1 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index ad680b6a..4ca95a71 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -1281,6 +1281,7 @@ struct SatPass : public Pass {
SatHelper basecase(design, module, enable_undef);
SatHelper inductstep(design, module, enable_undef);
+ bool basecase_setup_init = true;
basecase.sets = sets;
basecase.prove = prove;
@@ -1305,7 +1306,6 @@ struct SatPass : public Pass {
for (int timestep = 1; timestep <= seq_len; timestep++)
basecase.setup(timestep);
- basecase.setup_init();
inductstep.sets = sets;
inductstep.prove = prove;
@@ -1337,6 +1337,11 @@ struct SatPass : public Pass {
int property = basecase.setup_proof(seq_len + inductlen);
basecase.generate_model();
+ if (basecase_setup_init) {
+ basecase.setup_init();
+ basecase_setup_init = false;
+ }
+
if (inductlen > 1)
basecase.force_unique_state(seq_len + 1, seq_len + inductlen);