diff options
| author | Clifford Wolf <clifford@clifford.at> | 2013-06-10 16:09:29 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2013-06-10 16:09:29 +0200 |
| commit | 7d790febb040ae153a4db9be725f4d9709a49843 (patch) | |
| tree | d4a808d5918258197038a433dd143ed5e59dfefa /passes/sat | |
| parent | 15ff4cc63b95dde4c0445610586b4d80097a5681 (diff) | |
| download | yosys-7d790febb040ae153a4db9be725f4d9709a49843.tar.gz yosys-7d790febb040ae153a4db9be725f4d9709a49843.tar.bz2 yosys-7d790febb040ae153a4db9be725f4d9709a49843.zip | |
Improvements and fixes in SAT code
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/sat.cc | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index a13f83183..e5f678820 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -41,6 +41,11 @@ static void split(std::vector<std::string> &tokens, const std::string &text, cha tokens.push_back(text.substr(start)); } +static int get_dummy_line_num() +{ + return 0; +} + static bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str) { std::vector<std::string> tokens; @@ -56,6 +61,7 @@ static bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string continue; if ('0' <= netname[0] && netname[0] <= '9') { + AST::get_line_num = get_dummy_line_num; AST::AstNode *ast = VERILOG_FRONTEND::const2ast(netname); if (ast == NULL) return false; @@ -320,7 +326,7 @@ struct SatHelper continue; if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C") continue; - queued_signals.add(handled_signals.remove(p.second)); + queued_signals.add(handled_signals.remove(sigmap(p.second))); } } } @@ -712,6 +718,8 @@ struct SatPass : public Pass { sathelper.ez.printDIMACS(stdout, true); #endif + bool did_rerun = false; + rerun_solver: log("\nSolving problem with %d variables and %d clauses..\n", sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses()); @@ -733,16 +741,18 @@ struct SatPass : public Pass { } if (loopcount != 0) { - loopcount--; + loopcount--, did_rerun = true; sathelper.invalidate_model(); goto rerun_solver; } } else { - if (prove.size() == 0) { + if (did_rerun) + log("SAT solving finished - no more models found.\n"); + else if (prove.size() == 0) log("SAT solving finished - no model found.\n"); - } else { + else { log("SAT proof finished - no model found: SUCCESS!\n"); print_qed(); } |