diff options
Diffstat (limited to 'passes')
| -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 b7798ab2..e2eb1749 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 1644eaaa..0f826fc9 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"); |