From 56b593b91cc693849e3b3b3de0666f6ec9a597f6 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 7 Jun 2013 14:37:33 +0200
Subject: Improved sat generator and sat_solve pass

---
 passes/sat/example.ys   | 2 +-
 passes/sat/sat_solve.cc | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'passes')

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");
-- 
cgit v1.2.3