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

Fixed basecase init for "sat -tempinduct"

This commit is contained in:
Clifford Wolf 2015-02-21 17:43:49 +01:00
parent 49dd9c713f
commit dcbd00c101
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
passes/sat/sat.cc
View File

@ -1281,6 +1281,7 @@ struct SatPass : public Pass {
SatHelper basecase(design, module, enable_undef); SatHelper basecase(design, module, enable_undef);
SatHelper inductstep(design, module, enable_undef); SatHelper inductstep(design, module, enable_undef);
bool basecase_setup_init = true;
basecase.sets = sets; basecase.sets = sets;
basecase.prove = prove; basecase.prove = prove;
@ -1305,7 +1306,6 @@ struct SatPass : public Pass {
for (int timestep = 1; timestep <= seq_len; timestep++) for (int timestep = 1; timestep <= seq_len; timestep++)
basecase.setup(timestep); basecase.setup(timestep);
basecase.setup_init();
inductstep.sets = sets; inductstep.sets = sets;
inductstep.prove = prove; inductstep.prove = prove;
@ -1337,6 +1337,11 @@ struct SatPass : public Pass {
int property = basecase.setup_proof(seq_len + inductlen); int property = basecase.setup_proof(seq_len + inductlen);
basecase.generate_model(); basecase.generate_model();
if (basecase_setup_init) {
basecase.setup_init();
basecase_setup_init = false;
}
if (inductlen > 1) if (inductlen > 1)
basecase.force_unique_state(seq_len + 1, seq_len + inductlen); basecase.force_unique_state(seq_len + 1, seq_len + inductlen);