diff options
| author | Clifford Wolf <clifford@clifford.at> | 2015-02-21 20:05:16 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2015-02-21 20:05:16 +0100 |
| commit | 9237fb924e74a0ed687992df6988b4aa2105614e (patch) | |
| tree | b33ad51476c492af1960dc29c3293f4435847b61 /passes/sat | |
| parent | 1688b9b464fd5f594e5bf506dc0e859eaee305de (diff) | |
| download | yosys-9237fb924e74a0ed687992df6988b4aa2105614e.tar.gz yosys-9237fb924e74a0ed687992df6988b4aa2105614e.tar.bz2 yosys-9237fb924e74a0ed687992df6988b4aa2105614e.zip | |
When "sat -tempinduct-baseonly -maxsteps N" reaches maxsteps it is a good thing.
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/sat.cc | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index d89c75506..9404a0d77 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -1438,6 +1438,11 @@ struct SatPass : public Pass { } } + if (tempinduct_baseonly) { + log("\nReached maximum number of time steps -> proved base case for %d steps: SUCCESS!\n", maxsteps); + goto tip_success; + } + log("\nReached maximum number of time steps -> proof failed.\n"); if(!vcd_file_name.empty()) inductstep.dump_model_to_vcd(vcd_file_name); |