mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-12 09:03:27 +00:00
Code Activity

Fixed "sat -initsteps" off-by-one bug

Browse source
This commit is contained in:
Clifford Wolf 2015-02-22 12:42:05 +01:00
parent fae0e75ace
commit 39d25b212c
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
passes/sat/sat.cc
View file

@ -1436,7 +1436,7 @@ struct SatPass : public Pass {
if (inductlen > 1) if (inductlen > 1)
inductstep.force_unique_state(1, inductlen + 1); inductstep.force_unique_state(1, inductlen + 1);
if (inductlen < tempinduct_skip || inductlen < initsteps || inductlen % stepsize != 0) if (inductlen <= tempinduct_skip || inductlen <= initsteps || inductlen % stepsize != 0)
{ {
if (inductlen < tempinduct_skip) if (inductlen < tempinduct_skip)
log("\n[induction step %d] Skipping prove for this step (-tempinduct-skip %d).", log("\n[induction step %d] Skipping prove for this step (-tempinduct-skip %d).",