Various improvements in sat_solve pass and SAT generator

3 files changed, 74 insertions, 10 deletions

diff --git a/passes/sat/example.v b/passes/sat/example.v
index 45011f70..9e8c94b7 100644
--- a/passes/sat/example.v
+++ b/passes/sat/example.v
@@ -1,5 +1,5 @@
 
-module example(a, y);
+module example001(a, y);
 
 input [15:0] a;
 output y;
@@ -10,3 +10,63 @@ assign y = !gt && !lt;
 
 endmodule
 
+// ------------------------------------
+
+module example002(a, y);
+
+input [3:0] a;
+output y;
+reg [1:0] t1, t2;
+
+always @* begin
+	casex (a)
+		16'b1xxx:
+			t1 <= 1;
+		16'bx1xx:
+			t1 <= 2;
+		16'bxx1x:
+			t1 <= 3;
+		16'bxxx1:
+			t1 <= 4;
+		default:
+			t1 <= 0;
+	endcase
+	casex (a)
+		16'b1xxx:
+			t2 <= 1;
+		16'b01xx:
+			t2 <= 2;
+		16'b001x:
+			t2 <= 3;
+		16'b0001:
+			t2 <= 4;
+		default:
+			t2 <= 0;
+	endcase
+end
+
+assign y = t1 != t2;
+
+endmodule
+
+// ------------------------------------
+
+module example003(clk, rst, y);
+
+input clk, rst;
+output y;
+
+reg [3:0] counter;
+
+always @(posedge clk)
+	case (1)
+		rst, counter == 9:
+			counter <= 0;
+		default:
+			counter <= counter+1;
+	endcase
+
+assign y = counter == 12;
+
+endmodule
+
diff --git a/passes/sat/example.ys b/passes/sat/example.ys
index b6d131c9..d4037f78 100644
--- a/passes/sat/example.ys
+++ b/passes/sat/example.ys
@@ -1,3 +1,5 @@
 read_verilog example.v
-techmap; opt; abc; opt
-sat_solve -set y 1'b1
+proc; opt_clean
+sat_solve -set y 1'b1 example001
+sat_solve -set y 1'b1 example002
+sat_solve -set y 1'b1 example003
diff --git a/passes/sat/sat_solve.cc b/passes/sat/sat_solve.cc
index a7605b44..b71d0507 100644
--- a/passes/sat/sat_solve.cc
+++ b/passes/sat/sat_solve.cc
@@ -211,14 +211,16 @@ struct SatSolvePass : public Pass {
 		int import_cell_counter = 0;
 		for (auto &c : module->cells)
 			if (design->selected(module, c.second) && ct.cell_known(c.second->type)) {
-				for (auto &p : c.second->connections)
-					if (ct.cell_output(c.second->type, p.first))
-						show_drivers.insert(sigmap(p.second), c.second);
-					else
-						show_driven[c.second].append(sigmap(p.second));
 				// log("Import cell: %s\n", RTLIL::id2cstr(c.first));
-				satgen.importCell(c.second);
-				import_cell_counter++;
+				if (satgen.importCell(c.second)) {
+					for (auto &p : c.second->connections)
+						if (ct.cell_output(c.second->type, p.first))
+							show_drivers.insert(sigmap(p.second), c.second);
+						else
+							show_driven[c.second].append(sigmap(p.second));
+					import_cell_counter++;
+				} else
+					log("Warning: failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
 			}
 		log("Imported %d cells to SAT database.\n", import_cell_counter);