From dcbd00c101465323d173fac9bc5efb4f0d19f377 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 21 Feb 2015 17:43:49 +0100 Subject: [PATCH] Fixed basecase init for "sat -tempinduct" --- passes/sat/sat.cc | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index ad680b6a2..4ca95a71a 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);