diff options
| author | Clifford Wolf <clifford@clifford.at> | 2013-06-07 14:37:33 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2013-06-07 14:37:33 +0200 |
| commit | 56b593b91cc693849e3b3b3de0666f6ec9a597f6 (patch) | |
| tree | ccaa7c501a228f4056b887370682f054c81aea48 /passes/sat | |
| parent | 46fbe9d26299a7b6197463b3056d778f525658fb (diff) | |
| download | yosys-56b593b91cc693849e3b3b3de0666f6ec9a597f6.tar.gz yosys-56b593b91cc693849e3b3b3de0666f6ec9a597f6.tar.bz2 yosys-56b593b91cc693849e3b3b3de0666f6ec9a597f6.zip | |
Improved sat generator and sat_solve pass
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/example.ys | 2 | ||||
| -rw-r--r-- | passes/sat/sat_solve.cc | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/passes/sat/example.ys b/passes/sat/example.ys index b7798ab2e..e2eb17497 100644 --- a/passes/sat/example.ys +++ b/passes/sat/example.ys @@ -1,3 +1,3 @@ read_verilog example.v -techmap; opt +techmap; opt; abc; opt sat_solve -show a -set y 1'b1 diff --git a/passes/sat/sat_solve.cc b/passes/sat/sat_solve.cc index 1644eaaa1..0f826fc94 100644 --- a/passes/sat/sat_solve.cc +++ b/passes/sat/sat_solve.cc @@ -129,7 +129,7 @@ struct SatSolvePass : public Pass { std::vector<std::pair<std::string, std::string>> sets; std::vector<std::string> shows; - log_header("Executing SAT_SOLVE pass (detecting logic loops).\n"); + log_header("Executing SAT_SOLVE pass (solving SAT problems in the circuit).\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -189,7 +189,7 @@ struct SatSolvePass : public Pass { satgen.importCell(c.second); import_cell_counter++; } - log("Imported %d cells.\n", import_cell_counter); + log("Imported %d cells to SAT database.\n", import_cell_counter); std::vector<int> modelExpressions; std::vector<bool> modelValues; @@ -227,7 +227,7 @@ struct SatSolvePass : public Pass { } } - log("Solving problem with %d variables and %d clauses..\n", ez.numCnfVariables(), int(ez.cnf().size())); + log("Solving problem with %d variables and %d clauses..\n", ez.numCnfVariables(), ez.numCnfClauses()); if (ez.solve(modelExpressions, modelValues)) { log("SAT solving finished - model found:\n"); |