diff options
| author | Clifford Wolf <clifford@clifford.at> | 2015-02-21 17:43:49 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2015-02-21 17:43:49 +0100 |
| commit | dcbd00c101465323d173fac9bc5efb4f0d19f377 (patch) | |
| tree | 437f06c002bb65b9541c488ac502377d18bc637e | |
| parent | 49dd9c713f008173100e159782223aede631b510 (diff) | |
| download | yosys-dcbd00c101465323d173fac9bc5efb4f0d19f377.tar.gz yosys-dcbd00c101465323d173fac9bc5efb4f0d19f377.tar.bz2 yosys-dcbd00c101465323d173fac9bc5efb4f0d19f377.zip | |
Fixed basecase init for "sat -tempinduct"
| -rw-r--r-- | passes/sat/sat.cc | 7 |
1 files changed, 6 insertions, 1 deletions
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); |