From 921064c20044f72a64bec12dbd73103bdd3f45e3 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 18 Dec 2013 13:21:02 +0100
Subject: [PATCH 01/49] Added support for macro arguments

---
 frontends/verilog/preproc.cc | 98 +++++++++++++++++++++++++++---------
 tests/simple/macros.v        |  9 ++++
 2 files changed, 84 insertions(+), 23 deletions(-)
 create mode 100644 tests/simple/macros.v

diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index 8d435d94..e17531be 100644
--- a/frontends/verilog/preproc.cc
+++ b/frontends/verilog/preproc.cc
@@ -76,8 +76,9 @@ static char next_char()
 	return ch == '\r' ? next_char() : ch;
 }
 
-static void skip_spaces()
+static std::string skip_spaces()
 {
+	std::string spaces;
 	while (1) {
 		char ch = next_char();
 		if (ch == 0)
@@ -86,7 +87,9 @@ static void skip_spaces()
 			return_char(ch);
 			break;
 		}
+		spaces += ch;
 	}
+	return spaces;
 }
 
 static std::string next_token(bool pass_newline = false)
@@ -170,13 +173,14 @@ static std::string next_token(bool pass_newline = false)
 	else
 	{
 		const char *ok = "abcdefghijklmnopqrstuvwxyz_ABCDEFGHIJKLMNOPQRSTUVWXYZ$0123456789";
-		while ((ch = next_char()) != 0) {
-			if (strchr(ok, ch) == NULL) {
-				return_char(ch);
-				break;
+		if (ch == '`' || strchr(ok, ch) != NULL)
+			while ((ch = next_char()) != 0) {
+				if (strchr(ok, ch) == NULL) {
+					return_char(ch);
+					break;
+				}
+				token += ch;
 			}
-			token += ch;
-		}
 	}
 
 	return token;
@@ -289,27 +293,48 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
 
 		if (tok == "`define") {
 			std::string name, value;
+			std::map<std::string, int> args;
 			skip_spaces();
 			name = next_token(true);
 			skip_spaces();
 			int newline_count = 0;
+			int state = 0;
 			while (!tok.empty()) {
 				tok = next_token();
-				if (tok == "\n") {
-					return_char('\n');
-					break;
-				}
-				if (tok == "\\") {
-					char ch = next_char();
-					if (ch == '\n') {
-						value += " ";
-						newline_count++;
-					} else {
-						value += std::string("\\");
-						return_char(ch);
-					}
+				if (state == 0 && tok == "(") {
+					state = 1;
+					skip_spaces();
 				} else
-					value += tok;
+				if (state == 1) {
+					if (tok == ")")
+						state = 2;
+					else if (tok != ",") {
+						int arg_idx = args.size()+1;
+						args[tok] = arg_idx;
+					}
+					skip_spaces();
+				} else {
+					if (state != 2)
+						state = 3;
+					if (tok == "\n") {
+						return_char('\n');
+						break;
+					}
+					if (tok == "\\") {
+						char ch = next_char();
+						if (ch == '\n') {
+							value += " ";
+							newline_count++;
+						} else {
+							value += std::string("\\");
+							return_char(ch);
+						}
+					} else
+					if (args.count(tok) > 0)
+						value += stringf("`macro_%s_arg%d", name.c_str(), args.at(tok));
+					else
+						value += tok;
+				}
 			}
 			while (newline_count-- > 0)
 				return_char('\n');
@@ -338,8 +363,35 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
 		}
 
 		if (tok.size() > 1 && tok[0] == '`' && defines_map.count(tok.substr(1)) > 0) {
-			// printf("expand: >>%s<< -> >>%s<<\n", tok.c_str(), defines_map[tok.substr(1)].c_str());
-			insert_input(defines_map[tok.substr(1)]);
+			std::string name = tok.substr(1);
+			// printf("expand: >>%s<< -> >>%s<<\n", name.c_str(), defines_map[name].c_str());
+			std::string skipped_spaces = skip_spaces();
+			tok = next_token(true);
+			if (tok == "(") {
+				int level = 1;
+				std::vector<std::string> args;
+				args.push_back(std::string());
+				while (1)
+				{
+					tok = next_token(true);
+					if (tok == ")" || tok == "}" || tok == "]")
+						level--;
+					if (level == 0)
+						break;
+					if (level == 1 && tok == ",")
+						args.push_back(std::string());
+					else
+						args.back() += tok;
+					if (tok == "(" || tok == "{" || tok == "[")
+						level++;
+				}
+				for (size_t i = 0; i < args.size(); i++)
+					defines_map[stringf("macro_%s_arg%d", name.c_str(), i+1)] = args[i];
+			} else {
+				insert_input(tok);
+				insert_input(skipped_spaces);
+			}
+			insert_input(defines_map[name]);
 			continue;
 		}
 
diff --git a/tests/simple/macros.v b/tests/simple/macros.v
new file mode 100644
index 00000000..e2025717
--- /dev/null
+++ b/tests/simple/macros.v
@@ -0,0 +1,9 @@
+module test(a, y);
+`define MSB_LSB_SEP :
+`define get_msb(off, len) ((off)+(len)-1)
+`define get_lsb(off, len) (off)
+`define sel_bits(offset, len) `get_msb(offset, len) `MSB_LSB_SEP `get_lsb(offset, len)
+input [31:0] a;
+output [7:0] y;
+assign y = a[`sel_bits(16, 8)];
+endmodule

From fbd06a1afcef77e32b1fbe6405f1e639995d2fa5 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 18 Dec 2013 13:41:36 +0100
Subject: [PATCH 02/49] Added elsif preproc support

---
 frontends/verilog/preproc.cc |  15 ++-
 tests/simple/macros.v        | 230 ++++++++++++++++++++++++++++++++++-
 2 files changed, 243 insertions(+), 2 deletions(-)

diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index e17531be..023c4dbc 100644
--- a/frontends/verilog/preproc.cc
+++ b/frontends/verilog/preproc.cc
@@ -206,6 +206,7 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
 {
 	std::map<std::string, std::string> defines_map(pre_defines_map);
 	int ifdef_fail_level = 0;
+	bool in_elseif = false;
 
 	output_code.clear();
 	input_buffer.clear();
@@ -222,17 +223,29 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
 		if (tok == "`endif") {
 			if (ifdef_fail_level > 0)
 				ifdef_fail_level--;
+			if (ifdef_fail_level == 0)
+				in_elseif = false;
 			continue;
 		}
 
 		if (tok == "`else") {
 			if (ifdef_fail_level == 0)
 				ifdef_fail_level = 1;
-			else if (ifdef_fail_level == 1)
+			else if (ifdef_fail_level == 1 && !in_elseif)
 				ifdef_fail_level = 0;
 			continue;
 		}
 
+		if (tok == "`elsif") {
+			skip_spaces();
+			std::string name = next_token(true);
+			if (ifdef_fail_level == 0)
+				ifdef_fail_level = 1, in_elseif = true;
+			else if (ifdef_fail_level == 1 && defines_map.count(name) != 0)
+				ifdef_fail_level = 0, in_elseif = true;
+			continue;
+		}
+
 		if (tok == "`ifdef") {
 			skip_spaces();
 			std::string name = next_token(true);
diff --git a/tests/simple/macros.v b/tests/simple/macros.v
index e2025717..cda46cb4 100644
--- a/tests/simple/macros.v
+++ b/tests/simple/macros.v
@@ -1,9 +1,237 @@
-module test(a, y);
+
+module test_def(a, y);
+
 `define MSB_LSB_SEP :
 `define get_msb(off, len) ((off)+(len)-1)
 `define get_lsb(off, len) (off)
 `define sel_bits(offset, len) `get_msb(offset, len) `MSB_LSB_SEP `get_lsb(offset, len)
+
 input [31:0] a;
 output [7:0] y;
+
 assign y = a[`sel_bits(16, 8)];
+
+endmodule
+
+// ---------------------------------------------------
+
+module test_ifdef(a, y);
+
+input [2:0] a;
+output reg [31:0] y;
+
+always @* begin
+	y = 0;
+
+	`undef X
+	`ifdef X
+		y = y + 42;
+	`else
+		`undef  A
+		`undef  B
+		`ifdef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`undef  A
+		`define B
+		`ifdef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`undef  B
+		`ifdef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`define B
+		`ifdef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		// ------------------------------------
+		`undef  A
+		`undef  B
+		`ifndef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`undef  A
+		`define B
+		`ifndef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`undef  B
+		`ifndef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`define B
+		`ifndef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		// ------------------------------------
+		`undef A
+		`ifdef A
+			y = (y << 1) | a[0];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`ifdef A
+			y = (y << 1) | a[0];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		// ------------------------------------
+		`undef A
+		`ifndef A
+			y = (y << 1) | a[0];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`ifndef A
+			y = (y << 1) | a[0];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+	`endif
+
+	`define X
+	`ifdef X
+		`undef  A
+		`undef  B
+		`ifdef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`undef  A
+		`define B
+		`ifdef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`undef  B
+		`ifdef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`define B
+		`ifdef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		// ------------------------------------
+		`undef  A
+		`undef  B
+		`ifndef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`undef  A
+		`define B
+		`ifndef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`undef  B
+		`ifndef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`define B
+		`ifndef A
+			y = (y << 1) | a[0];
+		`elsif B
+			y = (y << 1) | a[1];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		// ------------------------------------
+		`undef A
+		`ifdef A
+			y = (y << 1) | a[0];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`ifdef A
+			y = (y << 1) | a[0];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		// ------------------------------------
+		`undef A
+		`ifndef A
+			y = (y << 1) | a[0];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+		`define A
+		`ifndef A
+			y = (y << 1) | a[0];
+		`else
+			y = (y << 1) | a[2];
+		`endif
+	`else
+		y = y + 42;
+	`endif
+end
+
 endmodule

From 994c83db0143f5d86e1442577e0efcf0c2c57cda Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 18 Dec 2013 13:43:53 +0100
Subject: [PATCH 03/49] Added multiplier test case from eda playground

---
 tests/simple/multiplier.v | 132 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 132 insertions(+)
 create mode 100644 tests/simple/multiplier.v

diff --git a/tests/simple/multiplier.v b/tests/simple/multiplier.v
new file mode 100644
index 00000000..3c0aa1fc
--- /dev/null
+++ b/tests/simple/multiplier.v
@@ -0,0 +1,132 @@
+
+// Via http://www.edaplayground.com/s/6/591
+// stackoverflow 20556634
+// http://stackoverflow.com/questions/20556634/how-can-i-iteratively-create-buses-of-parameterized-size-to-connect-modules-also
+
+// Code your design here
+`define macro_args
+`define indexed_part_select
+
+module Multiplier_flat #(parameter M = 4, parameter N = 4)(
+input [M-1:0] A, //Input A, size M
+input [N-1:0] B, //Input B, size N
+output [M+N-1:0] P );  //Output P (product), size M+N
+
+/* Calculate LSB using Wolfram Alpha
+ N==3 : http://www.wolframalpha.com/input/?i=0%2C+4%2C+9%2C+15%2C+...
+ N==4 : http://www.wolframalpha.com/input/?i=0%2C+5%2C+11%2C+18%2C+26%2C+35%2C+...
+ N==5 : http://www.wolframalpha.com/input/?i=0%2C+6%2C+13%2C+21%2C+30%2C+...
+ */
+`ifdef macro_args
+// initial $display("Use Macro Args");
+`define calc_pp_lsb(n) (((n)-1)*((n)+2*M)/2)
+//`define calc_pp_msb(n) (`calc_pp_lsb(n+1)-1)
+`define calc_pp_msb(n) ((n**2+(2*M+1)*n-2)/2)
+//`define calc_range(n) `calc_pp_msb(n):`calc_pp_lsb(n)
+`define calc_pp_range(n) `calc_pp_lsb(n) +: (M+n)
+
+wire [`calc_pp_msb(N):0] PP;
+assign PP[`calc_pp_range(1)] = { 1'b0 , { A & {M{B[0]}} } };
+assign P = PP[`calc_pp_range(N)];
+`elsif indexed_part_select
+// initial $display("Use Indexed Part Select");
+localparam MSB = (N**2+(2*M+1)*N-2)/2;
+wire [MSB:0] PP;
+assign PP[M:0] = { 1'b0 , { A & {M{B[0]}} } };
+assign P = PP[MSB -: M+N];
+`else
+// initial $display("Use Worst Case");
+localparam MSB = (N**2+(2*M+1)*N-2)/2;
+wire [MSB:0] PP;
+assign PP[M:0] = { 1'b0 , { A & {M{B[0]}} } };
+assign P = PP[MSB : MSB+1-M-N];
+`endif
+
+genvar i;
+generate
+for (i=1; i < N; i=i+1)
+begin: addPartialProduct
+    wire [M+i-1:0] gA,gB,gS;
+    wire Cout;
+    assign gA = { A & {M{B[i]}} , {i{1'b0}} };
+    `ifdef macro_args
+    assign gB = PP[`calc_pp_range(i)];
+    assign PP[`calc_pp_range(i+1)] = {Cout,gS};
+    `elsif indexed_part_select
+    assign gB = PP[(i-1)*(i+2*M)/2 +: M+i];
+    assign PP[i*((i+1)+2*M)/2 +: M+i+1] = {Cout,gS};
+    `else
+    localparam LSB = (i-1)*(i+2*M)/2;
+    localparam MSB = (i**2+(2*M+1)*i-2)/2;
+    localparam MSB2 = ((i+1)**2+(2*M+1)*(i+1)-2)/2;
+    assign gB = PP[MSB : LSB];
+    assign PP[ MSB2 : MSB+1] = {Cout,gS};
+    `endif
+    RippleCarryAdder#(M+i) adder( .A(gA), .B(gB), .S(gS), .Cin (1'b0), .Cout(Cout) );
+end
+endgenerate
+
+`ifdef macro_args
+// Cleanup global space
+`undef calc_pp_range
+`undef calc_pp_msb
+`undef calc_pp_lsb
+`endif
+endmodule
+
+module Multiplier_2D #(parameter M = 4, parameter N = 4)(
+input [M-1:0] A, //Input A, size M
+input [N-1:0] B, //Input B, size N
+output [M+N-1:0] P );  //Output P (product), size M+N
+
+wire [M+N-1:0] PP [N-1:0];
+
+// Note: bits PP[0][M+N-1:M+1] are never used. Unused bits are optimized out during synthesis
+//assign PP[0][M:0] = { {1'b0} , { A & {M{B[0]}} } };
+//assign PP[0][M+N-1:M+1] = {(N-1){1'b0}}; // uncomment to make probing readable
+assign PP[0] = { {N{1'b0}} , { A & {M{B[0]}} } };
+assign P = PP[N-1];
+
+genvar i;
+generate
+for (i=1; i < N; i=i+1)
+begin: addPartialProduct
+    wire [M+i-1:0] gA,gB,gS; wire Cout;
+    assign gA = { A & {M{B[i]}} , {i{1'b0}} };
+    assign gB = PP[i-1][M+i-1:0];
+    //assign PP[i][M+i:0] = {Cout,gS};
+    //if (i+1<N) assign PP[i][M+N-1:M+i+1] = {(N-i){1'b0}}; // uncomment to make probing readable
+    assign PP[i] = { {(N-i){1'b0}}, Cout, gS};
+    RippleCarryAdder#(M+i) adder(
+    	.A(gA), .B(gB), .S(gS), .Cin(1'b0), .Cout(Cout) );
+end
+endgenerate
+
+//always@* foreach(S[i]) $display("S[%0d]:%b",i,S[i]);
+
+endmodule
+
+module RippleCarryAdder#(parameter N = 4)(A,B,Cin,S,Cout);
+
+input [N-1:0] A;
+input [N-1:0] B;
+input Cin;
+output [N-1:0] S;
+output Cout;
+wire [N:0] CC;
+
+assign CC[0] = Cin;
+assign Cout = CC[N];
+genvar i;
+generate
+for (i=0; i < N; i=i+1)
+begin: addbit
+    FullAdder unit(A[i],B[i],CC[i],S[i],CC[i+1]);
+end
+endgenerate
+
+endmodule
+
+module FullAdder(input A,B,Cin, output wire S,Cout);
+assign {Cout,S} = A+B+Cin;
+endmodule

From c904f5e197470b14ae7951010444edc8309b7807 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 19 Dec 2013 13:21:57 +0100
Subject: [PATCH 04/49] Prefer non-inverted clocks in dfflibmap

---
 passes/techmap/dfflibmap.cc | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index 0324afa8..49b98059 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -473,17 +473,19 @@ struct DfflibmapPass : public Pass {
 		find_cell_sr(libparser.ast, "$_DFFSR_PPN_", true, true, false);
 		find_cell_sr(libparser.ast, "$_DFFSR_PPP_", true, true, true);
 
-		bool keep_running = true;
-		while (keep_running) {
+		bool keep_running;
+		do {
 			keep_running = false;
-			keep_running |= expand_cellmap("$_DFF_*_", "C");
-			keep_running |= expand_cellmap("$_DFF_*??_", "C");
 			keep_running |= expand_cellmap("$_DFF_?*?_", "R");
 			keep_running |= expand_cellmap("$_DFF_??*_", "DQ");
-			keep_running |= expand_cellmap("$_DFFSR_*??_", "C");
 			keep_running |= expand_cellmap("$_DFFSR_?*?_", "S");
 			keep_running |= expand_cellmap("$_DFFSR_??*_", "R");
-		}
+		} while (keep_running);
+		do {
+			keep_running |= expand_cellmap("$_DFF_*_", "C");
+			keep_running |= expand_cellmap("$_DFF_*??_", "C");
+			keep_running |= expand_cellmap("$_DFFSR_*??_", "C");
+		} while (keep_running);
 
 		map_sr_to_arst("$_DFFSR_NNN_", "$_DFF_NN0_");
 		map_sr_to_arst("$_DFFSR_NNN_", "$_DFF_NN1_");

From 2ee3ac4ba39cda4de82de53cac96826103851cd8 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 20 Dec 2013 12:11:58 +0100
Subject: [PATCH 05/49] Added log_dump() API

---
 kernel/log.h | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

diff --git a/kernel/log.h b/kernel/log.h
index d88dda88..5ee6b565 100644
--- a/kernel/log.h
+++ b/kernel/log.h
@@ -93,4 +93,58 @@ struct PerformanceTimer
 #endif
 };
 
+// simple API for quickly dumping values when debugging
+
+static inline void log_dump_val_worker(int v) { log("%d", v); }
+static inline void log_dump_val_worker(size_t v) { log("%zd", v); }
+static inline void log_dump_val_worker(long int v) { log("%ld", v); }
+static inline void log_dump_val_worker(long long int v) { log("%lld", v); }
+static inline void log_dump_val_worker(char c) { log(c >= 32 && c < 127 ? "'%c'" : "'\\x%02x'", c); }
+static inline void log_dump_val_worker(bool v) { log("%s", v ? "true" : "false"); }
+static inline void log_dump_val_worker(double v) { log("%f", v); }
+static inline void log_dump_val_worker(const char *v) { log("%s", v); }
+static inline void log_dump_val_worker(std::string v) { log("%s", v.c_str()); }
+static inline void log_dump_val_worker(RTLIL::SigSpec v) { log("%s", log_signal(v)); }
+static inline void log_dump_args_worker(const char *p) { log_assert(*p == 0); }
+
+template <typename T, typename ... Args>
+void log_dump_args_worker(const char *p, T first, Args ... args)
+{
+	int next_p_state = 0;
+	const char *next_p = p;
+	while (*next_p && (next_p_state != 0 || *next_p != ',')) {
+		if (*next_p == '"')
+			do {
+				next_p++;
+				while (*next_p == '\\' && *(next_p + 1))
+					next_p += 2;
+			} while (*next_p && *next_p != '"');
+		if (*next_p == '\'') {
+			next_p++;
+			if (*next_p == '\\')
+				next_p++;
+			if (*next_p)
+				next_p++;
+		}
+		if (*next_p == '(' || *next_p == '[' || *next_p == '{')
+			next_p_state++;
+		if ((*next_p == ')' || *next_p == ']' || *next_p == '}') && next_p_state > 0)
+			next_p_state--;
+		next_p++;
+	}
+	log("\n\t%.*s => ", int(next_p - p), p);
+	if (*next_p == ',')
+		next_p++;
+	while (*next_p == ' ' || *next_p == '\t' || *next_p == '\r' || *next_p == '\n')
+		next_p++;
+	log_dump_val_worker(first);
+	log_dump_args_worker(next_p, args ...);
+}
+
+#define log_dump(...) do { \
+	log("DEBUG DUMP IN %s AT %s:%d:", __PRETTY_FUNCTION__, __FILE__, __LINE__); \
+	log_dump_args_worker(#__VA_ARGS__, __VA_ARGS__); \
+	log("\n"); \
+} while (0)
+
 #endif

From 404bcc2d1ed64dffa92b9891d930c6c53c192c1c Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 20 Dec 2013 12:13:51 +0100
Subject: [PATCH 06/49] Fixed dfflibmap endless-loop bug

---
 passes/techmap/dfflibmap.cc | 1 +
 1 file changed, 1 insertion(+)

diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index 49b98059..c35a09c2 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -482,6 +482,7 @@ struct DfflibmapPass : public Pass {
 			keep_running |= expand_cellmap("$_DFFSR_??*_", "R");
 		} while (keep_running);
 		do {
+			keep_running = false;
 			keep_running |= expand_cellmap("$_DFF_*_", "C");
 			keep_running |= expand_cellmap("$_DFF_*??_", "C");
 			keep_running |= expand_cellmap("$_DFFSR_*??_", "C");

From eaf7d9675de7e54ef55b5cd45784c2ea7556e8cf Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 20 Dec 2013 12:34:34 +0100
Subject: [PATCH 07/49] Further improved dfflibmap cellmap exploration

---
 passes/techmap/dfflibmap.cc | 32 ++++++++++++++++++--------------
 1 file changed, 18 insertions(+), 14 deletions(-)

diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index c35a09c2..a38ec66b 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -473,20 +473,24 @@ struct DfflibmapPass : public Pass {
 		find_cell_sr(libparser.ast, "$_DFFSR_PPN_", true, true, false);
 		find_cell_sr(libparser.ast, "$_DFFSR_PPP_", true, true, true);
 
-		bool keep_running;
-		do {
-			keep_running = false;
-			keep_running |= expand_cellmap("$_DFF_?*?_", "R");
-			keep_running |= expand_cellmap("$_DFF_??*_", "DQ");
-			keep_running |= expand_cellmap("$_DFFSR_?*?_", "S");
-			keep_running |= expand_cellmap("$_DFFSR_??*_", "R");
-		} while (keep_running);
-		do {
-			keep_running = false;
-			keep_running |= expand_cellmap("$_DFF_*_", "C");
-			keep_running |= expand_cellmap("$_DFF_*??_", "C");
-			keep_running |= expand_cellmap("$_DFFSR_*??_", "C");
-		} while (keep_running);
+		int level = 0;
+		while (level < 3) {
+			bool did_something = false;
+			switch (level) {
+			case 2:
+				did_something |= expand_cellmap("$_DFF_*_", "C");
+				did_something |= expand_cellmap("$_DFF_*??_", "C");
+				did_something |= expand_cellmap("$_DFFSR_*??_", "C");
+			case 1:
+				did_something |= expand_cellmap("$_DFF_??*_", "DQ");
+			case 0:
+				did_something |= expand_cellmap("$_DFF_?*?_", "R");
+				did_something |= expand_cellmap("$_DFFSR_?*?_", "S");
+				did_something |= expand_cellmap("$_DFFSR_??*_", "R");
+			}
+			if (!did_something)
+				level++;
+		}
 
 		map_sr_to_arst("$_DFFSR_NNN_", "$_DFF_NN0_");
 		map_sr_to_arst("$_DFFSR_NNN_", "$_DFF_NN1_");

From 1fb29050e57b99822db3b111647a87491f935ee9 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 20 Dec 2013 14:21:18 +0100
Subject: [PATCH 08/49] Cleanup of dfflibmap cellmap exploration code

---
 passes/techmap/dfflibmap.cc | 37 ++++++++++++++++++++-----------------
 1 file changed, 20 insertions(+), 17 deletions(-)

diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index a38ec66b..765a606c 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -473,23 +473,26 @@ struct DfflibmapPass : public Pass {
 		find_cell_sr(libparser.ast, "$_DFFSR_PPN_", true, true, false);
 		find_cell_sr(libparser.ast, "$_DFFSR_PPP_", true, true, true);
 
-		int level = 0;
-		while (level < 3) {
-			bool did_something = false;
-			switch (level) {
-			case 2:
-				did_something |= expand_cellmap("$_DFF_*_", "C");
-				did_something |= expand_cellmap("$_DFF_*??_", "C");
-				did_something |= expand_cellmap("$_DFFSR_*??_", "C");
-			case 1:
-				did_something |= expand_cellmap("$_DFF_??*_", "DQ");
-			case 0:
-				did_something |= expand_cellmap("$_DFF_?*?_", "R");
-				did_something |= expand_cellmap("$_DFFSR_?*?_", "S");
-				did_something |= expand_cellmap("$_DFFSR_??*_", "R");
-			}
-			if (!did_something)
-				level++;
+		// try to implement as many cells as possible just by inverting
+		// the SET and RESET pins. If necessary, implement cell types
+		// by inverting both D and Q. Only invert clock pins if there
+		// is no other way of implementing the cell.
+		while (1)
+		{
+			if (expand_cellmap("$_DFF_?*?_", "R") ||
+					expand_cellmap("$_DFFSR_?*?_", "S") ||
+					expand_cellmap("$_DFFSR_??*_", "R"))
+				continue;
+
+			if (expand_cellmap("$_DFF_??*_", "DQ"))
+				continue;
+
+			if (expand_cellmap("$_DFF_*_", "C") ||
+					expand_cellmap("$_DFF_*??_", "C") ||
+					expand_cellmap("$_DFFSR_*??_", "C"))
+				continue;
+
+			break;
 		}
 
 		map_sr_to_arst("$_DFFSR_NNN_", "$_DFF_NN0_");

From 8856cec308932d224da2061ca59d0eacf90f4793 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 21 Dec 2013 08:42:37 +0100
Subject: [PATCH 09/49] Now prefer smallest cells in dfflibmap

---
 passes/techmap/dfflibmap.cc | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index 765a606c..6fbd5210 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -106,6 +106,7 @@ static void find_cell(LibertyAst *ast, std::string cell_type, bool clkpol, bool
 	LibertyAst *best_cell = NULL;
 	std::map<std::string, char> best_cell_ports;
 	int best_cell_pins = 0;
+	float best_cell_area = 0;
 
 	if (ast->id != "library")
 		log_error("Format error in liberty file.\n");
@@ -141,6 +142,11 @@ static void find_cell(LibertyAst *ast, std::string cell_type, bool clkpol, bool
 			this_cell_ports[cell_rst_pin] = 'R';
 		this_cell_ports[cell_next_pin] = 'D';
 
+		float area = 0;
+		LibertyAst *ar = cell->find("area");
+		if (ar != NULL && !ar->value.empty())
+			area = atof(ar->value.c_str());
+
 		int num_pins = 0;
 		bool found_output = false;
 		for (auto pin : cell->children)
@@ -174,14 +180,18 @@ static void find_cell(LibertyAst *ast, std::string cell_type, bool clkpol, bool
 		if (!found_output || (best_cell != NULL && num_pins > best_cell_pins))
 			continue;
 
+		if (best_cell != NULL && num_pins == best_cell_pins && area > best_cell_area)
+			continue;
+
 		best_cell = cell;
 		best_cell_pins = num_pins;
+		best_cell_area = area;
 		best_cell_ports.swap(this_cell_ports);
 	continue_cell_loop:;
 	}
 
 	if (best_cell != NULL) {
-		log("  cell %s is a direct match for cell type %s.\n", best_cell->args[0].c_str(), cell_type.substr(1).c_str());
+		log("  cell %s (pins=%d, area=%.2f) is a direct match for cell type %s.\n", best_cell->args[0].c_str(), best_cell_pins, best_cell_area, cell_type.substr(1).c_str());
 		cell_mappings[cell_type].cell_name = best_cell->args[0];
 		cell_mappings[cell_type].ports = best_cell_ports;
 	}
@@ -192,6 +202,7 @@ static void find_cell_sr(LibertyAst *ast, std::string cell_type, bool clkpol, bo
 	LibertyAst *best_cell = NULL;
 	std::map<std::string, char> best_cell_ports;
 	int best_cell_pins = 0;
+	float best_cell_area = 0;
 
 	if (ast->id != "library")
 		log_error("Format error in liberty file.\n");
@@ -223,6 +234,11 @@ static void find_cell_sr(LibertyAst *ast, std::string cell_type, bool clkpol, bo
 		this_cell_ports[cell_clr_pin] = 'R';
 		this_cell_ports[cell_next_pin] = 'D';
 
+		float area = 0;
+		LibertyAst *ar = cell->find("area");
+		if (ar != NULL && !ar->value.empty())
+			area = atof(ar->value.c_str());
+
 		int num_pins = 0;
 		bool found_output = false;
 		for (auto pin : cell->children)
@@ -256,14 +272,18 @@ static void find_cell_sr(LibertyAst *ast, std::string cell_type, bool clkpol, bo
 		if (!found_output || (best_cell != NULL && num_pins > best_cell_pins))
 			continue;
 
+		if (best_cell != NULL && num_pins == best_cell_pins && area > best_cell_area)
+			continue;
+
 		best_cell = cell;
 		best_cell_pins = num_pins;
+		best_cell_area = area;
 		best_cell_ports.swap(this_cell_ports);
 	continue_cell_loop:;
 	}
 
 	if (best_cell != NULL) {
-		log("  cell %s is a direct match for cell type %s.\n", best_cell->args[0].c_str(), cell_type.substr(1).c_str());
+		log("  cell %s (pins=%d, area=%.2f) is a direct match for cell type %s.\n", best_cell->args[0].c_str(), best_cell_pins, best_cell_area, cell_type.substr(1).c_str());
 		cell_mappings[cell_type].cell_name = best_cell->args[0];
 		cell_mappings[cell_type].ports = best_cell_ports;
 	}

From 334b0cc8033490de29b4ac896d0dcc2ecab0e59b Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 21 Dec 2013 20:47:22 +0100
Subject: [PATCH 10/49] Fixed dfflibmap for unused output ports

---
 passes/techmap/dfflibmap.cc | 1 +
 1 file changed, 1 insertion(+)

diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index 6fbd5210..40caf780 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -419,6 +419,7 @@ static void dfflibmap(RTLIL::Design *design, RTLIL::Module *module)
 			if (port.second == '0' || port.second == '1') {
 				sig = RTLIL::SigSpec(port.second == '0' ? 0 : 1, 1);
 			} else
+			if (port.second != 0)
 				log_abort();
 			new_cell->connections["\\" + port.first] = sig;
 		}

From fb31d10236635bf098210aa42327fbe2c8f3d08d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 13:02:46 +0100
Subject: [PATCH 11/49] Renamed sat -set-undef to -set-any-undef

---
 passes/sat/sat.cc | 40 ++++++++++++++++++++--------------------
 1 file changed, 20 insertions(+), 20 deletions(-)

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index e330dfa6..e3b941f5 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -50,8 +50,8 @@ struct SatHelper
 
 	// undef constraints
 	bool enable_undef, set_init_undef;
-	std::vector<std::string> sets_def, sets_undef, sets_all_undef;
-	std::map<int, std::vector<std::string>> sets_def_at, sets_undef_at, sets_all_undef_at;
+	std::vector<std::string> sets_def, sets_any_undef, sets_all_undef;
+	std::map<int, std::vector<std::string>> sets_def_at, sets_any_undef_at, sets_all_undef_at;
 
 	// model variables
 	std::vector<std::string> shows;
@@ -571,7 +571,7 @@ struct SatPass : public Pass {
 		log("    -set-def <signal>\n");
 		log("        add a constraint that all bits of the given signal must be defined\n");
 		log("\n");
-		log("    -set-undef <signal>\n");
+		log("    -set-any-undef <signal>\n");
 		log("        add a constraint that at least one bit of the given signal is undefined\n");
 		log("\n");
 		log("    -set-all-undef <signal>\n");
@@ -597,9 +597,9 @@ struct SatPass : public Pass {
 		log("        given timestep. this has priority over a -set for the same signal.\n");
 		log("\n");
 	#if 0
-		log("    -set-def <N> <signal>\n");
-		log("    -set-undef <N> <signal>\n");
-		log("    -set-all-undef <N> <signal>\n");
+		log("    -set-def-at <N> <signal>\n");
+		log("    -set-any-undef-at <N> <signal>\n");
+		log("    -set-all-undef-at <N> <signal>\n");
 		log("        add undef contraints in the given timestep.\n");
 		log("\n");
 	#endif
@@ -634,8 +634,8 @@ struct SatPass : public Pass {
 	{
 		std::vector<std::pair<std::string, std::string>> sets, sets_init, prove;
 		std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
-		std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_undef_at, sets_all_undef_at;
-		std::vector<std::string> shows, sets_def, sets_undef, sets_all_undef;
+		std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
+		std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
 		int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
 		bool verify = false, fail_on_timeout = false, enable_undef = false;
 		bool ignore_div_by_zero = false, set_init_undef = false, max_undef = true;
@@ -688,17 +688,17 @@ struct SatPass : public Pass {
 				sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
 				continue;
 			}
-			if (args[argidx] == "-set-def" && argidx+2 < args.size()) {
+			if (args[argidx] == "-set-def" && argidx+1 < args.size()) {
 				sets_def.push_back(args[++argidx]);
 				enable_undef = true;
 				continue;
 			}
-			if (args[argidx] == "-set-undef" && argidx+2 < args.size()) {
-				sets_undef.push_back(args[++argidx]);
+			if (args[argidx] == "-set-any-undef" && argidx+1 < args.size()) {
+				sets_any_undef.push_back(args[++argidx]);
 				enable_undef = true;
 				continue;
 			}
-			if (args[argidx] == "-set-all-undef" && argidx+2 < args.size()) {
+			if (args[argidx] == "-set-all-undef" && argidx+1 < args.size()) {
 				sets_all_undef.push_back(args[++argidx]);
 				enable_undef = true;
 				continue;
@@ -731,9 +731,9 @@ struct SatPass : public Pass {
 				enable_undef = true;
 				continue;
 			}
-			if (args[argidx] == "-set-undef-at" && argidx+2 < args.size()) {
+			if (args[argidx] == "-set-any-undef-at" && argidx+2 < args.size()) {
 				int timestep = atoi(args[++argidx].c_str());
-				sets_undef_at[timestep].push_back(args[++argidx]);
+				sets_any_undef_at[timestep].push_back(args[++argidx]);
 				enable_undef = true;
 				continue;
 			}
@@ -791,10 +791,10 @@ struct SatPass : public Pass {
 			basecase.shows = shows;
 			basecase.timeout = timeout;
 			basecase.sets_def = sets_def;
-			basecase.sets_undef = sets_undef;
+			basecase.sets_any_undef = sets_any_undef;
 			basecase.sets_all_undef = sets_all_undef;
 			basecase.sets_def_at = sets_def_at;
-			basecase.sets_undef_at = sets_undef_at;
+			basecase.sets_any_undef_at = sets_any_undef_at;
 			basecase.sets_all_undef_at = sets_all_undef_at;
 			basecase.sets_init = sets_init;
 			basecase.set_init_undef = set_init_undef;
@@ -809,10 +809,10 @@ struct SatPass : public Pass {
 			inductstep.shows = shows;
 			inductstep.timeout = timeout;
 			inductstep.sets_def = sets_def;
-			inductstep.sets_undef = sets_undef;
+			inductstep.sets_any_undef = sets_any_undef;
 			inductstep.sets_all_undef = sets_all_undef;
 			inductstep.sets_def_at = sets_def_at;
-			inductstep.sets_undef_at = sets_undef_at;
+			inductstep.sets_any_undef_at = sets_any_undef_at;
 			inductstep.sets_all_undef_at = sets_all_undef_at;
 			inductstep.sets_init = sets_init;
 			inductstep.set_init_undef = set_init_undef;
@@ -901,10 +901,10 @@ struct SatPass : public Pass {
 			sathelper.shows = shows;
 			sathelper.timeout = timeout;
 			sathelper.sets_def = sets_def;
-			sathelper.sets_undef = sets_undef;
+			sathelper.sets_any_undef = sets_any_undef;
 			sathelper.sets_all_undef = sets_all_undef;
 			sathelper.sets_def_at = sets_def_at;
-			sathelper.sets_undef_at = sets_undef_at;
+			sathelper.sets_any_undef_at = sets_any_undef_at;
 			sathelper.sets_all_undef_at = sets_all_undef_at;
 			sathelper.sets_init = sets_init;
 			sathelper.set_init_undef = set_init_undef;

From 11ffa7867794ee5bda2742830bda64976ad4f549 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 13:27:21 +0100
Subject: [PATCH 12/49] Added sat -set-def/-set-*-undef support

---
 passes/sat/sat.cc | 71 +++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 66 insertions(+), 5 deletions(-)

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index e3b941f5..0a8006eb 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -202,6 +202,71 @@ struct SatHelper
 		check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
 		ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
 
+		// 0 = sets_def
+		// 1 = sets_any_undef
+		// 2 = sets_all_undef
+		std::set<RTLIL::SigSpec> sets_def_undef[3];
+
+		for (auto &s : sets_def) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[0].insert(sig);
+		}
+
+		for (auto &s : sets_any_undef) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[1].insert(sig);
+		}
+
+		for (auto &s : sets_all_undef) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[2].insert(sig);
+		}
+
+		for (auto &s : sets_def_at[timestep]) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[0].insert(sig);
+			sets_def_undef[1].erase(sig);
+			sets_def_undef[2].erase(sig);
+		}
+
+		for (auto &s : sets_any_undef_at[timestep]) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[0].erase(sig);
+			sets_def_undef[1].insert(sig);
+			sets_def_undef[2].erase(sig);
+		}
+
+		for (auto &s : sets_all_undef_at[timestep]) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[0].erase(sig);
+			sets_def_undef[1].erase(sig);
+			sets_def_undef[2].insert(sig);
+		}
+
+		for (int t = 0; t < 3; t++)
+		for (auto &sig : sets_def_undef[t]) {
+			log("Import %s constraint for timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
+			std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
+			if (t == 0)
+				ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
+			if (t == 1)
+				ez.assume(ez.expression(ezSAT::OpOr, undef_sig));
+			if (t == 2)
+				ez.assume(ez.expression(ezSAT::OpAnd, undef_sig));
+		}
+
 		int import_cell_counter = 0;
 		for (auto &c : module->cells)
 			if (design->selected(module, c.second)) {
@@ -567,7 +632,6 @@ struct SatPass : public Pass {
 		log("    -set <signal> <value>\n");
 		log("        set the specified signal to the specified value.\n");
 		log("\n");
-	#if 0
 		log("    -set-def <signal>\n");
 		log("        add a constraint that all bits of the given signal must be defined\n");
 		log("\n");
@@ -577,7 +641,6 @@ struct SatPass : public Pass {
 		log("    -set-all-undef <signal>\n");
 		log("        add a constraint that all bits of the given signal are undefined\n");
 		log("\n");
-	#endif
 		log("    -show <signal>\n");
 		log("        show the model for the specified signal. if no -show option is\n");
 		log("        passed then a set of signals to be shown is automatically selected.\n");
@@ -596,13 +659,11 @@ struct SatPass : public Pass {
 		log("        set or unset the specified signal to the specified value in the\n");
 		log("        given timestep. this has priority over a -set for the same signal.\n");
 		log("\n");
-	#if 0
 		log("    -set-def-at <N> <signal>\n");
 		log("    -set-any-undef-at <N> <signal>\n");
 		log("    -set-all-undef-at <N> <signal>\n");
 		log("        add undef contraints in the given timestep.\n");
 		log("\n");
-	#endif
 		log("    -set-init <signal> <value>\n");
 		log("        set the initial value for the register driving the signal to the value\n");
 		log("\n");
@@ -638,7 +699,7 @@ struct SatPass : public Pass {
 		std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
 		int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
 		bool verify = false, fail_on_timeout = false, enable_undef = false;
-		bool ignore_div_by_zero = false, set_init_undef = false, max_undef = true;
+		bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 

From ecc30255ba70910777a4586f5bd6abc818073293 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 13:50:08 +0100
Subject: [PATCH 13/49] Added proper === and !== support in constant
 expressions

---
 frontends/ast/ast.cc         |  4 ++++
 frontends/ast/ast.h          |  2 ++
 frontends/ast/genrtlil.cc    | 16 ++++++++++------
 frontends/ast/simplify.cc    | 16 ++++++++++------
 frontends/verilog/lexer.l    |  4 ++--
 frontends/verilog/parser.y   | 10 +++++++++-
 kernel/calc.cc               | 29 +++++++++++++++++++++++++++++
 kernel/rtlil.h               |  2 ++
 tests/simple/undef_eqx_nex.v | 11 +++++++++++
 9 files changed, 79 insertions(+), 15 deletions(-)
 create mode 100644 tests/simple/undef_eqx_nex.v

diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 0e65f1cb..20158488 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -103,6 +103,8 @@ std::string AST::type2str(AstNodeType type)
 	X(AST_LE)
 	X(AST_EQ)
 	X(AST_NE)
+	X(AST_EQX)
+	X(AST_NEX)
 	X(AST_GE)
 	X(AST_GT)
 	X(AST_ADD)
@@ -539,6 +541,8 @@ void AstNode::dumpVlog(FILE *f, std::string indent)
 	if (0) { case AST_LE:           txt = "<=";  }
 	if (0) { case AST_EQ:           txt = "==";  }
 	if (0) { case AST_NE:           txt = "!=";  }
+	if (0) { case AST_EQX:          txt = "===";  }
+	if (0) { case AST_NEX:          txt = "!==";  }
 	if (0) { case AST_GE:           txt = ">=";  }
 	if (0) { case AST_GT:           txt = ">";   }
 	if (0) { case AST_ADD:          txt = "+";   }
diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h
index f8e27927..22853d0f 100644
--- a/frontends/ast/ast.h
+++ b/frontends/ast/ast.h
@@ -82,6 +82,8 @@ namespace AST
 		AST_LE,
 		AST_EQ,
 		AST_NE,
+		AST_EQX,
+		AST_NEX,
 		AST_GE,
 		AST_GT,
 		AST_ADD,
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 269752df..36ca1432 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -728,6 +728,8 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint)
 	case AST_LE:
 	case AST_EQ:
 	case AST_NE:
+	case AST_EQX:
+	case AST_NEX:
 	case AST_GE:
 	case AST_GT:
 		width_hint = std::max(width_hint, 1);
@@ -1113,12 +1115,14 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 		}
 
 	// generate cells for binary operations: $lt, $le, $eq, $ne, $ge, $gt
-	if (0) { case AST_LT: type_name = "$lt"; }
-	if (0) { case AST_LE: type_name = "$le"; }
-	if (0) { case AST_EQ: type_name = "$eq"; }
-	if (0) { case AST_NE: type_name = "$ne"; }
-	if (0) { case AST_GE: type_name = "$ge"; }
-	if (0) { case AST_GT: type_name = "$gt"; }
+	if (0) { case AST_LT:  type_name = "$lt"; }
+	if (0) { case AST_LE:  type_name = "$le"; }
+	if (0) { case AST_EQ:  type_name = "$eq"; }
+	if (0) { case AST_NE:  type_name = "$ne"; }
+	if (0) { case AST_EQX: type_name = "$eq"; }
+	if (0) { case AST_NEX: type_name = "$ne"; }
+	if (0) { case AST_GE:  type_name = "$ge"; }
+	if (0) { case AST_GT:  type_name = "$gt"; }
 		{
 			int width = std::max(width_hint, 1);
 			width_hint = -1, sign_hint = true;
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index f6df0c17..982d1ae3 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -299,6 +299,8 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 	case AST_LE:
 	case AST_EQ:
 	case AST_NE:
+	case AST_EQX:
+	case AST_NEX:
 	case AST_GE:
 	case AST_GT:
 		width_hint = -1;
@@ -1258,12 +1260,14 @@ skip_dynamic_range_lvalue_expansion:;
 				newNode = mkconst_bits(y.bits, sign_hint);
 			}
 			break;
-		if (0) { case AST_LT: const_func = RTLIL::const_lt; }
-		if (0) { case AST_LE: const_func = RTLIL::const_le; }
-		if (0) { case AST_EQ: const_func = RTLIL::const_eq; }
-		if (0) { case AST_NE: const_func = RTLIL::const_ne; }
-		if (0) { case AST_GE: const_func = RTLIL::const_ge; }
-		if (0) { case AST_GT: const_func = RTLIL::const_gt; }
+		if (0) { case AST_LT:  const_func = RTLIL::const_lt; }
+		if (0) { case AST_LE:  const_func = RTLIL::const_le; }
+		if (0) { case AST_EQ:  const_func = RTLIL::const_eq; }
+		if (0) { case AST_NE:  const_func = RTLIL::const_ne; }
+		if (0) { case AST_EQX: const_func = RTLIL::const_eqx; }
+		if (0) { case AST_NEX: const_func = RTLIL::const_nex; }
+		if (0) { case AST_GE:  const_func = RTLIL::const_ge; }
+		if (0) { case AST_GT:  const_func = RTLIL::const_gt; }
 			if (children[0]->type == AST_CONSTANT && children[1]->type == AST_CONSTANT) {
 				int cmp_width = std::max(children[0]->bits.size(), children[1]->bits.size());
 				bool cmp_signed = children[0]->is_signed && children[1]->is_signed;
diff --git a/frontends/verilog/lexer.l b/frontends/verilog/lexer.l
index a0deb755..9e606d90 100644
--- a/frontends/verilog/lexer.l
+++ b/frontends/verilog/lexer.l
@@ -232,8 +232,8 @@ supply1 { return TOK_SUPPLY1; }
 "<=" { return OP_LE; }
 ">=" { return OP_GE; }
 
-"===" { return OP_EQ; }
-"!==" { return OP_NE; }
+"===" { return OP_EQX; }
+"!==" { return OP_NEX; }
 
 "~&" { return OP_NAND; }
 "~|" { return OP_NOR;  }
diff --git a/frontends/verilog/parser.y b/frontends/verilog/parser.y
index f47d1785..874482d6 100644
--- a/frontends/verilog/parser.y
+++ b/frontends/verilog/parser.y
@@ -117,7 +117,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %left '|' OP_NOR
 %left '^' OP_XNOR
 %left '&' OP_NAND
-%left OP_EQ OP_NE
+%left OP_EQ OP_NE OP_EQX OP_NEX
 %left '<' OP_LE OP_GE '>'
 %left OP_SHL OP_SHR OP_SSHL OP_SSHR
 %left '+' '-'
@@ -1161,6 +1161,14 @@ basic_expr:
 		$$ = new AstNode(AST_NE, $1, $4);
 		append_attr($$, $3);
 	} |
+	basic_expr OP_EQX attr basic_expr {
+		$$ = new AstNode(AST_EQX, $1, $4);
+		append_attr($$, $3);
+	} |
+	basic_expr OP_NEX attr basic_expr {
+		$$ = new AstNode(AST_NEX, $1, $4);
+		append_attr($$, $3);
+	} |
 	basic_expr OP_GE attr basic_expr {
 		$$ = new AstNode(AST_GE, $1, $4);
 		append_attr($$, $3);
diff --git a/kernel/calc.cc b/kernel/calc.cc
index 61025104..fc978c11 100644
--- a/kernel/calc.cc
+++ b/kernel/calc.cc
@@ -386,6 +386,35 @@ RTLIL::Const RTLIL::const_ne(const RTLIL::Const &arg1, const RTLIL::Const &arg2,
 	return result;
 }
 
+RTLIL::Const RTLIL::const_eqx(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+{
+	RTLIL::Const arg1_ext = arg1;
+	RTLIL::Const arg2_ext = arg2;
+	RTLIL::Const result(RTLIL::State::S0, result_len);
+
+	int width = std::max(arg1_ext.bits.size(), arg2_ext.bits.size());
+	extend_u0(arg1_ext, width, signed1 && signed2);
+	extend_u0(arg2_ext, width, signed1 && signed2);
+
+	for (size_t i = 0; i < arg1_ext.bits.size(); i++) {
+		if (arg1_ext.bits.at(i) != arg2_ext.bits.at(i))
+			return result;
+	}
+
+	result.bits.front() = RTLIL::State::S1;
+	return result;
+}
+
+RTLIL::Const RTLIL::const_nex(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+{
+	RTLIL::Const result = RTLIL::const_eqx(arg1, arg2, signed1, signed2, result_len);
+	if (result.bits.front() == RTLIL::State::S0)
+		result.bits.front() = RTLIL::State::S1;
+	else if (result.bits.front() == RTLIL::State::S1)
+		result.bits.front() = RTLIL::State::S0;
+	return result;
+}
+
 RTLIL::Const RTLIL::const_ge(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
 {
 	int undef_bit_pos = -1;
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index fbdab53e..91dd9d44 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -174,6 +174,8 @@ namespace RTLIL
 	RTLIL::Const const_le          (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 	RTLIL::Const const_eq          (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 	RTLIL::Const const_ne          (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+	RTLIL::Const const_eqx         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+	RTLIL::Const const_nex         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 	RTLIL::Const const_ge          (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 	RTLIL::Const const_gt          (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 
diff --git a/tests/simple/undef_eqx_nex.v b/tests/simple/undef_eqx_nex.v
new file mode 100644
index 00000000..63912a2f
--- /dev/null
+++ b/tests/simple/undef_eqx_nex.v
@@ -0,0 +1,11 @@
+module test(y);
+output [7:0] y;
+assign y[0] = 0/0;
+assign y[1] = 0/1;
+assign y[2] = 0/0 ==  32'bx;
+assign y[3] = 0/0 !=  32'bx;
+assign y[4] = 0/0 === 32'bx;
+assign y[5] = 0/0 !== 32'bx;
+assign y[6] = 0/1 === 32'bx;
+assign y[7] = 0/1 !== 32'bx;
+endmodule

From 369bf81a7049c96f62af084bb5007fbf45e36ab4 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 14:20:15 +0100
Subject: [PATCH 14/49] Added support for non-const === and !== (for miter
 circuits)

---
 backends/verilog/verilog_backend.cc | 14 ++++----
 frontends/ast/genrtlil.cc           |  4 +--
 kernel/celltypes.h                  |  4 +++
 kernel/rtlil.cc                     |  2 +-
 kernel/satgen.h                     | 20 +++++++++---
 passes/extract/extract.cc           |  2 ++
 passes/opt/opt_const.cc             | 12 ++++---
 passes/proc/proc_arst.cc            |  4 +--
 techlibs/common/simlib.v            | 36 +++++++++++++++++++++
 techlibs/common/stdcells.v          | 50 +++++++++++++++++++++++++++++
 10 files changed, 128 insertions(+), 20 deletions(-)

diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index ff41c2e3..d8160c97 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -506,12 +506,14 @@ bool dump_cell_expr(FILE *f, std::string indent, RTLIL::Cell *cell)
 	HANDLE_BINOP("$sshl", "<<<")
 	HANDLE_BINOP("$sshr", ">>>")
 
-	HANDLE_BINOP("$lt", "<")
-	HANDLE_BINOP("$le", "<=")
-	HANDLE_BINOP("$eq", "==")
-	HANDLE_BINOP("$ne", "!=")
-	HANDLE_BINOP("$ge", ">=")
-	HANDLE_BINOP("$gt", ">")
+	HANDLE_BINOP("$lt",  "<")
+	HANDLE_BINOP("$le",  "<=")
+	HANDLE_BINOP("$eq",  "==")
+	HANDLE_BINOP("$ne",  "!=")
+	HANDLE_BINOP("$eqx", "===")
+	HANDLE_BINOP("$nex", "!==")
+	HANDLE_BINOP("$ge",  ">=")
+	HANDLE_BINOP("$gt",  ">")
 
 	HANDLE_BINOP("$add", "+")
 	HANDLE_BINOP("$sub", "-")
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 36ca1432..1b6fc1d8 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -1119,8 +1119,8 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 	if (0) { case AST_LE:  type_name = "$le"; }
 	if (0) { case AST_EQ:  type_name = "$eq"; }
 	if (0) { case AST_NE:  type_name = "$ne"; }
-	if (0) { case AST_EQX: type_name = "$eq"; }
-	if (0) { case AST_NEX: type_name = "$ne"; }
+	if (0) { case AST_EQX: type_name = "$eqx"; }
+	if (0) { case AST_NEX: type_name = "$nex"; }
 	if (0) { case AST_GE:  type_name = "$ge"; }
 	if (0) { case AST_GT:  type_name = "$gt"; }
 		{
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index e59f74d6..29eb490f 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -78,6 +78,8 @@ struct CellTypes
 		cell_types.insert("$le");
 		cell_types.insert("$eq");
 		cell_types.insert("$ne");
+		cell_types.insert("$eqx");
+		cell_types.insert("$nex");
 		cell_types.insert("$ge");
 		cell_types.insert("$gt");
 		cell_types.insert("$add");
@@ -237,6 +239,8 @@ struct CellTypes
 		HANDLE_CELL_TYPE(le)
 		HANDLE_CELL_TYPE(eq)
 		HANDLE_CELL_TYPE(ne)
+		HANDLE_CELL_TYPE(eqx)
+		HANDLE_CELL_TYPE(nex)
 		HANDLE_CELL_TYPE(ge)
 		HANDLE_CELL_TYPE(gt)
 		HANDLE_CELL_TYPE(add)
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 9dfe196d..47dc098a 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -408,7 +408,7 @@ namespace {
 			}
 
 			if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" ||
-					cell->type == "$ge" || cell->type == "$gt") {
+					cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt") {
 				param("\\A_SIGNED");
 				param("\\B_SIGNED");
 				port("\\A", param("\\A_WIDTH"));
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 35e15aa6..c0807f55 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -451,7 +451,7 @@ struct SatGen
 			return true;
 		}
 
-		if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt")
+		if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt")
 		{
 			bool is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
 			std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
@@ -465,9 +465,9 @@ struct SatGen
 				ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
 			if (cell->type == "$le")
 				ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), yy.at(0));
-			if (cell->type == "$eq")
+			if (cell->type == "$eq" || cell->type == "$eqx")
 				ez->SET(ez->vec_eq(a, b), yy.at(0));
-			if (cell->type == "$ne")
+			if (cell->type == "$ne" || cell->type == "$nex")
 				ez->SET(ez->vec_ne(a, b), yy.at(0));
 			if (cell->type == "$ge")
 				ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), yy.at(0));
@@ -476,7 +476,19 @@ struct SatGen
 			for (size_t i = 1; i < y.size(); i++)
 				ez->SET(ez->FALSE, yy.at(i));
 
-			if (model_undef && (cell->type == "$eq" || cell->type == "$ne"))
+			if (model_undef && (cell->type == "$eqx" || cell->type == "$nex"))
+			{
+				std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
+				std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
+				std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
+				yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
+
+				for (size_t i = 0; i < y.size(); i++)
+					ez->SET(ez->FALSE, undef_y.at(i));
+
+				ez->assume(ez->vec_eq(y, yy));
+			}
+			else if (model_undef && (cell->type == "$eq" || cell->type == "$ne"))
 			{
 				std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 				std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
diff --git a/passes/extract/extract.cc b/passes/extract/extract.cc
index 0c639aed..aa21e573 100644
--- a/passes/extract/extract.cc
+++ b/passes/extract/extract.cc
@@ -499,6 +499,8 @@ struct ExtractPass : public Pass {
 			solver.addSwappablePorts("$xnor",      "\\A", "\\B");
 			solver.addSwappablePorts("$eq",        "\\A", "\\B");
 			solver.addSwappablePorts("$ne",        "\\A", "\\B");
+			solver.addSwappablePorts("$eqx",       "\\A", "\\B");
+			solver.addSwappablePorts("$nex",       "\\A", "\\B");
 			solver.addSwappablePorts("$add",       "\\A", "\\B");
 			solver.addSwappablePorts("$mul",       "\\A", "\\B");
 			solver.addSwappablePorts("$logic_and", "\\A", "\\B");
diff --git a/passes/opt/opt_const.cc b/passes/opt/opt_const.cc
index b7b361e9..30d85588 100644
--- a/passes/opt/opt_const.cc
+++ b/passes/opt/opt_const.cc
@@ -144,7 +144,7 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 #endif
 		}
 
-		if (cell->type == "$eq" || cell->type == "$ne")
+		if (cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex")
 		{
 			RTLIL::SigSpec a = cell->connections["\\A"];
 			RTLIL::SigSpec b = cell->connections["\\B"];
@@ -160,10 +160,12 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 
 			assert(a.chunks.size() == b.chunks.size());
 			for (size_t i = 0; i < a.chunks.size(); i++) {
-				if (a.chunks[i].wire == NULL && a.chunks[i].data.bits[0] > RTLIL::State::S1)
-					continue;
-				if (b.chunks[i].wire == NULL && b.chunks[i].data.bits[0] > RTLIL::State::S1)
-					continue;
+				if (cell->type == "$eq" || cell->type == "$ne") {
+					if (a.chunks[i].wire == NULL && a.chunks[i].data.bits[0] > RTLIL::State::S1)
+						continue;
+					if (b.chunks[i].wire == NULL && b.chunks[i].data.bits[0] > RTLIL::State::S1)
+						continue;
+				}
 				new_a.append(a.chunks[i]);
 				new_b.append(b.chunks[i]);
 			}
diff --git a/passes/proc/proc_arst.cc b/passes/proc/proc_arst.cc
index 65dc97bd..57194657 100644
--- a/passes/proc/proc_arst.cc
+++ b/passes/proc/proc_arst.cc
@@ -47,7 +47,7 @@ static bool check_signal(RTLIL::Module *mod, RTLIL::SigSpec signal, RTLIL::SigSp
 			polarity = !polarity;
 			return check_signal(mod, cell->connections["\\A"], ref, polarity);
 		}
-		if (cell->type == "$eq" && cell->connections["\\Y"] == signal) {
+		if ((cell->type == "$eq" || cell->type == "$eqx") && cell->connections["\\Y"] == signal) {
 			if (cell->connections["\\A"].is_fully_const()) {
 				if (!cell->connections["\\A"].as_bool())
 					polarity = !polarity;
@@ -59,7 +59,7 @@ static bool check_signal(RTLIL::Module *mod, RTLIL::SigSpec signal, RTLIL::SigSp
 				return check_signal(mod, cell->connections["\\A"], ref, polarity);
 			}
 		}
-		if (cell->type == "$ne" && cell->connections["\\Y"] == signal) {
+		if ((cell->type == "$ne" || cell->type == "$nex") && cell->connections["\\Y"] == signal) {
 			if (cell->connections["\\A"].is_fully_const()) {
 				if (cell->connections["\\A"].as_bool())
 					polarity = !polarity;
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index b4440ea8..034244ca 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -376,6 +376,42 @@ endmodule
 
 // --------------------------------------------------------
 
+module \$eqx (A, B, Y);
+
+parameter A_SIGNED = 0;
+parameter B_SIGNED = 0;
+parameter A_WIDTH = 0;
+parameter B_WIDTH = 0;
+parameter Y_WIDTH = 0;
+
+`INPUT_A
+`INPUT_B
+output [Y_WIDTH-1:0] Y;
+
+assign Y = A_BUF.val === B_BUF.val;
+
+endmodule
+
+// --------------------------------------------------------
+
+module \$nex (A, B, Y);
+
+parameter A_SIGNED = 0;
+parameter B_SIGNED = 0;
+parameter A_WIDTH = 0;
+parameter B_WIDTH = 0;
+parameter Y_WIDTH = 0;
+
+`INPUT_A
+`INPUT_B
+output [Y_WIDTH-1:0] Y;
+
+assign Y = A_BUF.val !== B_BUF.val;
+
+endmodule
+
+// --------------------------------------------------------
+
 module \$ge (A, B, Y);
 
 parameter A_SIGNED = 0;
diff --git a/techlibs/common/stdcells.v b/techlibs/common/stdcells.v
index ef4b96f7..c7efa240 100644
--- a/techlibs/common/stdcells.v
+++ b/techlibs/common/stdcells.v
@@ -572,6 +572,56 @@ endmodule
 
 // --------------------------------------------------------
 
+module \$eqx (A, B, Y);
+
+parameter A_SIGNED = 0;
+parameter B_SIGNED = 0;
+parameter A_WIDTH = 1;
+parameter B_WIDTH = 1;
+parameter Y_WIDTH = 1;
+
+parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+
+input [A_WIDTH-1:0] A;
+input [B_WIDTH-1:0] B;
+output [Y_WIDTH-1:0] Y;
+
+wire carry, carry_sign;
+wire [WIDTH-1:0] A_buf, B_buf;
+\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+
+assign Y = ~|(A_buf ^ B_buf);
+
+endmodule
+
+// --------------------------------------------------------
+
+module \$nex (A, B, Y);
+
+parameter A_SIGNED = 0;
+parameter B_SIGNED = 0;
+parameter A_WIDTH = 1;
+parameter B_WIDTH = 1;
+parameter Y_WIDTH = 1;
+
+parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+
+input [A_WIDTH-1:0] A;
+input [B_WIDTH-1:0] B;
+output [Y_WIDTH-1:0] Y;
+
+wire carry, carry_sign;
+wire [WIDTH-1:0] A_buf, B_buf;
+\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+
+assign Y = |(A_buf ^ B_buf);
+
+endmodule
+
+// --------------------------------------------------------
+
 module \$ge (A, B, Y);
 
 parameter A_SIGNED = 0;

From 7b02a44efbb81ce2c97dcb87f1d8ca016c14ba76 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 14:21:24 +0100
Subject: [PATCH 15/49] Fixed/improved opt_const $eq/$ne/$eqx/$nex handling

---
 passes/opt/opt_const.cc | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/passes/opt/opt_const.cc b/passes/opt/opt_const.cc
index 30d85588..d84910ee 100644
--- a/passes/opt/opt_const.cc
+++ b/passes/opt/opt_const.cc
@@ -166,6 +166,8 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 					if (b.chunks[i].wire == NULL && b.chunks[i].data.bits[0] > RTLIL::State::S1)
 						continue;
 				}
+				if (a.chunks[i] == b.chunks[i])
+					continue;
 				new_a.append(a.chunks[i]);
 				new_b.append(b.chunks[i]);
 			}
@@ -177,7 +179,7 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 				goto next_cell;
 			}
 
-			if (new_a.width != a.width) {
+			if (new_a.width < a.width || new_b.width < b.width) {
 				new_a.optimize();
 				new_b.optimize();
 				cell->connections["\\A"] = new_a;

From ebf9abfeb6c65821ee4f1ef0f4ab16660348c45f Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 14:32:42 +0100
Subject: [PATCH 16/49] Fixed sat handling of $eqx and $nex cells

---
 kernel/satgen.h | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/kernel/satgen.h b/kernel/satgen.h
index c0807f55..8fb8e818 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -461,6 +461,13 @@ struct SatGen
 
 			std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 
+			if (model_undef && (cell->type == "$eqx" || cell->type == "$nex")) {
+				std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
+				std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
+				a = ez->vec_or(a, undef_a);
+				b = ez->vec_or(b, undef_b);
+			}
+
 			if (cell->type == "$lt")
 				ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
 			if (cell->type == "$le")
@@ -481,7 +488,11 @@ struct SatGen
 				std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 				std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 				std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
-				yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
+
+				if (cell->type == "$eqx")
+					yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
+				else
+					yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
 
 				for (size_t i = 0; i < y.size(); i++)
 					ez->SET(ez->FALSE, undef_y.at(i));

From 72026a934ecfd072b2e0964a12ba4fdafc0f276e Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 15:05:52 +0100
Subject: [PATCH 17/49] Fixed parsing of macros with no arguments and expansion
 text starting with "("

---
 frontends/verilog/preproc.cc | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index 023c4dbc..501adf05 100644
--- a/frontends/verilog/preproc.cc
+++ b/frontends/verilog/preproc.cc
@@ -309,9 +309,10 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
 			std::map<std::string, int> args;
 			skip_spaces();
 			name = next_token(true);
-			skip_spaces();
 			int newline_count = 0;
 			int state = 0;
+			if (skip_spaces() != "")
+				state = 3;
 			while (!tok.empty()) {
 				tok = next_token();
 				if (state == 0 && tok == "(") {

From c9699fe76deb13209d61af461d9ce850a5113c8d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 15:10:07 +0100
Subject: [PATCH 18/49] More $eq/$ne/$eqx/$nex fixes in opt_const

---
 passes/opt/opt_const.cc | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/passes/opt/opt_const.cc b/passes/opt/opt_const.cc
index d84910ee..a3f3ee41 100644
--- a/passes/opt/opt_const.cc
+++ b/passes/opt/opt_const.cc
@@ -160,6 +160,13 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 
 			assert(a.chunks.size() == b.chunks.size());
 			for (size_t i = 0; i < a.chunks.size(); i++) {
+				if (a.chunks[i].wire == NULL && b.chunks[i].wire == NULL &&
+						a.chunks[i].data.bits[0] != b.chunks[i].data.bits[0]) {
+					RTLIL::SigSpec new_y = RTLIL::SigSpec((cell->type == "$eq" || cell->type == "$eqx") ?  RTLIL::State::S0 : RTLIL::State::S1);
+					new_y.extend(cell->parameters["\\Y_WIDTH"].as_int(), false);
+					replace_cell(module, cell, "empty", "\\Y", new_y);
+					goto next_cell;
+				}
 				if (cell->type == "$eq" || cell->type == "$ne") {
 					if (a.chunks[i].wire == NULL && a.chunks[i].data.bits[0] > RTLIL::State::S1)
 						continue;
@@ -173,7 +180,7 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 			}
 
 			if (new_a.width == 0) {
-				RTLIL::SigSpec new_y = RTLIL::SigSpec(cell->type == "$eq" ?  RTLIL::State::S1 : RTLIL::State::S0);
+				RTLIL::SigSpec new_y = RTLIL::SigSpec((cell->type == "$eq" || cell->type == "$eqx") ?  RTLIL::State::S1 : RTLIL::State::S0);
 				new_y.extend(cell->parameters["\\Y_WIDTH"].as_int(), false);
 				replace_cell(module, cell, "empty", "\\Y", new_y);
 				goto next_cell;

From 0f5ab7649e4496b1923cad6f093c735a2350fdc8 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 15:15:20 +0100
Subject: [PATCH 19/49] Small cleanup in SatGen

---
 kernel/satgen.h | 2 --
 1 file changed, 2 deletions(-)

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 8fb8e818..67312f44 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -161,7 +161,6 @@ struct SatGen
 	{
 		bool arith_undef_handled = false;
 		bool is_arith_compare = cell->type == "$lt" || cell->type == "$le" || cell->type == "$ge" || cell->type == "$gt";
-		int arith_undef_result = ez->FALSE;
 
 		if (model_undef && (cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" || cell->type == "$mod" || is_arith_compare))
 		{
@@ -191,7 +190,6 @@ struct SatGen
 				ez->assume(ez->vec_eq(undef_y_bits, undef_y));
 			}
 
-			arith_undef_result = undef_y_bit;
 			arith_undef_handled = true;
 		}
 

From 1dcbba1abf28afae846bd42f49d716892ffd685c Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 16:25:27 +0100
Subject: [PATCH 20/49] Fixed parsing of non-arg macro calls followed by "("

---
 frontends/verilog/preproc.cc | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index 501adf05..5cfa0f24 100644
--- a/frontends/verilog/preproc.cc
+++ b/frontends/verilog/preproc.cc
@@ -204,6 +204,7 @@ static void input_file(FILE *f, std::string filename)
 
 std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::map<std::string, std::string> pre_defines_map, const std::list<std::string> include_dirs)
 {
+	std::set<std::string> defines_with_args;
 	std::map<std::string, std::string> defines_map(pre_defines_map);
 	int ifdef_fail_level = 0;
 	bool in_elseif = false;
@@ -354,6 +355,10 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
 				return_char('\n');
 			// printf("define: >>%s<< -> >>%s<<\n", name.c_str(), value.c_str());
 			defines_map[name] = value;
+			if (state == 2)
+				defines_with_args.insert(name);
+			else
+				defines_with_args.erase(name);
 			continue;
 		}
 
@@ -363,6 +368,7 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
 			name = next_token(true);
 			// printf("undef: >>%s<<\n", name.c_str());
 			defines_map.erase(name);
+			defines_with_args.erase(name);
 			continue;
 		}
 
@@ -381,7 +387,7 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
 			// printf("expand: >>%s<< -> >>%s<<\n", name.c_str(), defines_map[name].c_str());
 			std::string skipped_spaces = skip_spaces();
 			tok = next_token(true);
-			if (tok == "(") {
+			if (tok == "(" && defines_with_args.count(name) > 0) {
 				int level = 1;
 				std::vector<std::string> args;
 				args.push_back(std::string());

From 122b3c067b87464bd362ccce96fdeb84fa476653 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 18:11:05 +0100
Subject: [PATCH 21/49] Fixed sat handling of $eqx and $nex with unequal port
 widths

---
 kernel/satgen.h | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 67312f44..05f3310c 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -462,6 +462,7 @@ struct SatGen
 			if (model_undef && (cell->type == "$eqx" || cell->type == "$nex")) {
 				std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 				std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
+				extendSignalWidth(undef_a, undef_b, cell, true);
 				a = ez->vec_or(a, undef_a);
 				b = ez->vec_or(b, undef_b);
 			}
@@ -486,6 +487,7 @@ struct SatGen
 				std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 				std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 				std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
+				extendSignalWidth(undef_a, undef_b, cell, true);
 
 				if (cell->type == "$eqx")
 					yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));

From d81e3ed3aeca4b517736b8c95b20b2e8b1e0c860 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 28 Dec 2013 10:29:22 +0100
Subject: [PATCH 22/49] More conservastive $eq/$ne/$eqx/$nex opt_const code

---
 passes/opt/opt_const.cc | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/passes/opt/opt_const.cc b/passes/opt/opt_const.cc
index a3f3ee41..84285567 100644
--- a/passes/opt/opt_const.cc
+++ b/passes/opt/opt_const.cc
@@ -160,19 +160,13 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 
 			assert(a.chunks.size() == b.chunks.size());
 			for (size_t i = 0; i < a.chunks.size(); i++) {
-				if (a.chunks[i].wire == NULL && b.chunks[i].wire == NULL &&
-						a.chunks[i].data.bits[0] != b.chunks[i].data.bits[0]) {
+				if (a.chunks[i].wire == NULL && b.chunks[i].wire == NULL && a.chunks[i].data.bits[0] != b.chunks[i].data.bits[0] &&
+						a.chunks[i].data.bits[0] <= RTLIL::State::S1 && b.chunks[i].data.bits[0] <= RTLIL::State::S1) {
 					RTLIL::SigSpec new_y = RTLIL::SigSpec((cell->type == "$eq" || cell->type == "$eqx") ?  RTLIL::State::S0 : RTLIL::State::S1);
 					new_y.extend(cell->parameters["\\Y_WIDTH"].as_int(), false);
 					replace_cell(module, cell, "empty", "\\Y", new_y);
 					goto next_cell;
 				}
-				if (cell->type == "$eq" || cell->type == "$ne") {
-					if (a.chunks[i].wire == NULL && a.chunks[i].data.bits[0] > RTLIL::State::S1)
-						continue;
-					if (b.chunks[i].wire == NULL && b.chunks[i].data.bits[0] > RTLIL::State::S1)
-						continue;
-				}
 				if (a.chunks[i] == b.chunks[i])
 					continue;
 				new_a.append(a.chunks[i]);

From bd39263796fdf4f1c747a4a8449a0a484fdb3026 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 28 Dec 2013 10:30:31 +0100
Subject: [PATCH 23/49] Improved $_MUX_ handling in opt_const

---
 passes/opt/opt_const.cc | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/passes/opt/opt_const.cc b/passes/opt/opt_const.cc
index 84285567..0ead97b4 100644
--- a/passes/opt/opt_const.cc
+++ b/passes/opt/opt_const.cc
@@ -17,8 +17,6 @@
  *
  */
 
-#undef MUX_UNDEF_SEL_TO_UNDEF_RESULTS
-
 #include "opt_status.h"
 #include "kernel/register.h"
 #include "kernel/sigtools.h"
@@ -133,15 +131,16 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 				ACTION_DO("\\Y", input.extract(2, 1));
 			if (input.match("  0")) ACTION_DO("\\Y", input.extract(2, 1));
 			if (input.match("  1")) ACTION_DO("\\Y", input.extract(1, 1));
-#ifdef MUX_UNDEF_SEL_TO_UNDEF_RESULTS
 			if (input.match("01 ")) ACTION_DO("\\Y", input.extract(0, 1));
-			// TODO: "10 " -> replace with "!S" gate
-			// TODO: "0  " -> replace with "B AND S" gate
-			// TODO: " 1 " -> replace with "A OR S" gate
-			// TODO: "1  " -> replace with "B OR !S" gate (?)
-			// TODO: " 0 " -> replace with "A AND !S" gate (?)
-			if (input.match("  *")) ACTION_DO_Y(x);
-#endif
+			if (input.match("10 ")) {
+				cell->type = "$_INV_";
+				cell->connections["\\A"] = input.extract(0, 1);
+				cell->connections.erase("\\B");
+				cell->connections.erase("\\S");
+				goto next_cell;
+			}
+			if (input.match("01*")) ACTION_DO_Y(x);
+			if (input.match("10*")) ACTION_DO_Y(x);
 		}
 
 		if (cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex")

From 7f717875999f18065a69934db2075fd1508d3a7d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 28 Dec 2013 11:24:36 +0100
Subject: [PATCH 24/49] Added sat -prove-x and -set-def-inputs

---
 passes/sat/sat.cc | 128 ++++++++++++++++++++++++++++++++++------------
 1 file changed, 96 insertions(+), 32 deletions(-)

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 0a8006eb..21202199 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -44,7 +44,7 @@ struct SatHelper
 	SatGen satgen;
 
 	// additional constraints
-	std::vector<std::pair<std::string, std::string>> sets, prove, sets_init;
+	std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
 	std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
 	std::map<int, std::vector<std::string>> unsets_at;
 
@@ -284,34 +284,75 @@ struct SatHelper
 
 	int setup_proof(int timestep = -1)
 	{
-		assert(prove.size() > 0);
+		assert(prove.size() + prove_x.size() > 0);
 
 		RTLIL::SigSpec big_lhs, big_rhs;
+		std::vector<int> prove_bits;
 
-		for (auto &s : prove)
+		if (prove.size() > 0)
 		{
-			RTLIL::SigSpec lhs, rhs;
+			for (auto &s : prove)
+			{
+				RTLIL::SigSpec lhs, rhs;
 
-			if (!RTLIL::SigSpec::parse(lhs, module, s.first))
-				log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
-			if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
-				log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
-			show_signal_pool.add(sigmap(lhs));
-			show_signal_pool.add(sigmap(rhs));
+				if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+					log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
+				if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+					log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
+				show_signal_pool.add(sigmap(lhs));
+				show_signal_pool.add(sigmap(rhs));
 
-			if (lhs.width != rhs.width)
-				log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
-					s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+				if (lhs.width != rhs.width)
+					log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+						s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
 
-			log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
-			big_lhs.remove2(lhs, &big_rhs);
-			big_lhs.append(lhs);
-			big_rhs.append(rhs);
+				log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+				big_lhs.remove2(lhs, &big_rhs);
+				big_lhs.append(lhs);
+				big_rhs.append(rhs);
+			}
+
+			log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+			check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
+			prove_bits.push_back(satgen.signals_eq(big_lhs, big_rhs, timestep));
 		}
 
-		log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
-		check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
-		return satgen.signals_eq(big_lhs, big_rhs, timestep);
+		if (prove_x.size() > 0)
+		{
+			for (auto &s : prove_x)
+			{
+				RTLIL::SigSpec lhs, rhs;
+
+				if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+					log_cmd_error("Failed to parse lhs proof-x expression `%s'.\n", s.first.c_str());
+				if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+					log_cmd_error("Failed to parse rhs proof-x expression `%s'.\n", s.second.c_str());
+				show_signal_pool.add(sigmap(lhs));
+				show_signal_pool.add(sigmap(rhs));
+
+				if (lhs.width != rhs.width)
+					log_cmd_error("Proof-x expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+						s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+
+				log("Import proof-x-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+				big_lhs.remove2(lhs, &big_rhs);
+				big_lhs.append(lhs);
+				big_rhs.append(rhs);
+			}
+
+			log("Final proof-x equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+
+			std::vector<int> value_lhs = satgen.importDefSigSpec(big_lhs, timestep);
+			std::vector<int> value_rhs = satgen.importDefSigSpec(big_rhs, timestep);
+
+			std::vector<int> undef_lhs = satgen.importUndefSigSpec(big_lhs, timestep);
+			std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep);
+
+			for (size_t i = 0; i < value_lhs.size(); i++)
+				prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i))))));
+		}
+
+		return ez.expression(ezSAT::OpAnd, prove_bits);
 	}
 
 	void force_unique_state(int timestep_from, int timestep_to)
@@ -641,6 +682,9 @@ struct SatPass : public Pass {
 		log("    -set-all-undef <signal>\n");
 		log("        add a constraint that all bits of the given signal are undefined\n");
 		log("\n");
+		log("    -set-def-inputs\n");
+		log("        add -set-def constraints for all module inputs\n");
+		log("\n");
 		log("    -show <signal>\n");
 		log("        show the model for the specified signal. if no -show option is\n");
 		log("        passed then a set of signals to be shown is automatically selected.\n");
@@ -678,6 +722,10 @@ struct SatPass : public Pass {
 		log("        induction proof it is proven that the condition holds forever after\n");
 		log("        the number of time steps passed using -seq.\n");
 		log("\n");
+		log("    -prove-x <signal> <value>\n");
+		log("        Like -prove, but an undef (x) bit in the lhs matches any value on\n");
+		log("        the right hand side. Useful for equivialence checking.\n");
+		log("\n");
 		log("    -maxsteps <N>\n");
 		log("        Set a maximum length for the induction.\n");
 		log("\n");
@@ -693,12 +741,12 @@ struct SatPass : public Pass {
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
-		std::vector<std::pair<std::string, std::string>> sets, sets_init, prove;
+		std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x;
 		std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
 		std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
 		std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
 		int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
-		bool verify = false, fail_on_timeout = false, enable_undef = false;
+		bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
 		bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@@ -743,6 +791,11 @@ struct SatPass : public Pass {
 				max_undef = true;
 				continue;
 			}
+			if (args[argidx] == "-set-def-inputs") {
+				enable_undef = true;
+				set_def_inputs = true;
+				continue;
+			}
 			if (args[argidx] == "-set" && argidx+2 < args.size()) {
 				std::string lhs = args[++argidx];
 				std::string rhs = args[++argidx];
@@ -770,6 +823,13 @@ struct SatPass : public Pass {
 				prove.push_back(std::pair<std::string, std::string>(lhs, rhs));
 				continue;
 			}
+			if (args[argidx] == "-prove-x" && argidx+2 < args.size()) {
+				std::string lhs = args[++argidx];
+				std::string rhs = args[++argidx];
+				prove_x.push_back(std::pair<std::string, std::string>(lhs, rhs));
+				enable_undef = true;
+				continue;
+			}
 			if (args[argidx] == "-seq" && argidx+1 < args.size()) {
 				seq_len = atoi(args[++argidx].c_str());
 				continue;
@@ -834,10 +894,16 @@ struct SatPass : public Pass {
 		if (module == NULL) 
 			log_cmd_error("Can't perform SAT on an empty selection!\n");
 
-		if (prove.size() == 0 && verify)
+		if (prove.size() + prove_x.size() == 0 && verify)
 			log_cmd_error("Got -verify but nothing to prove!\n");
 
-		if (prove.size() > 0 && seq_len > 0)
+		if (set_def_inputs) {
+			for (auto &it : module->wires)
+				if (it.second->port_input)
+					sets_def.push_back(it.second->name);
+		}
+
+		if (prove.size() + prove_x.size() > 0 && seq_len > 0)
 		{
 			if (loopcount > 0 || max_undef)
 				log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
@@ -847,6 +913,7 @@ struct SatPass : public Pass {
 
 			basecase.sets = sets;
 			basecase.prove = prove;
+			basecase.prove_x = prove_x;
 			basecase.sets_at = sets_at;
 			basecase.unsets_at = unsets_at;
 			basecase.shows = shows;
@@ -867,16 +934,12 @@ struct SatPass : public Pass {
 
 			inductstep.sets = sets;
 			inductstep.prove = prove;
+			inductstep.prove_x = prove_x;
 			inductstep.shows = shows;
 			inductstep.timeout = timeout;
 			inductstep.sets_def = sets_def;
 			inductstep.sets_any_undef = sets_any_undef;
 			inductstep.sets_all_undef = sets_all_undef;
-			inductstep.sets_def_at = sets_def_at;
-			inductstep.sets_any_undef_at = sets_any_undef_at;
-			inductstep.sets_all_undef_at = sets_all_undef_at;
-			inductstep.sets_init = sets_init;
-			inductstep.set_init_undef = set_init_undef;
 			inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
 
 			inductstep.setup(1);
@@ -957,6 +1020,7 @@ struct SatPass : public Pass {
 
 			sathelper.sets = sets;
 			sathelper.prove = prove;
+			sathelper.prove_x = prove_x;
 			sathelper.sets_at = sets_at;
 			sathelper.unsets_at = unsets_at;
 			sathelper.shows = shows;
@@ -973,7 +1037,7 @@ struct SatPass : public Pass {
 
 			if (seq_len == 0) {
 				sathelper.setup();
-				if (sathelper.prove.size() > 0)
+				if (sathelper.prove.size() + sathelper.prove_x.size() > 0)
 					sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
 			} else {
 				for (int timestep = 1; timestep <= seq_len; timestep++)
@@ -1000,7 +1064,7 @@ struct SatPass : public Pass {
 					sathelper.maximize_undefs();
 				}
 
-				if (prove.size() == 0) {
+				if (prove.size() + prove_x.size() == 0) {
 					log("SAT solving finished - model found:\n");
 				} else {
 					log("SAT proof finished - model found: FAIL!\n");
@@ -1026,7 +1090,7 @@ struct SatPass : public Pass {
 					goto timeout;
 				if (rerun_counter)
 					log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
-				else if (prove.size() == 0)
+				else if (prove.size() + prove_x.size() == 0)
 					log("SAT solving finished - no model found.\n");
 				else {
 					log("SAT proof finished - no model found: SUCCESS!\n");

From c69c416d28015e496045d1b4529c465fbaad42e2 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 28 Dec 2013 11:54:40 +0100
Subject: [PATCH 25/49] Added $bu0 cell (for easy correct $eq/$ne mapping)

---
 kernel/calc.cc              |  8 ++++++++
 kernel/celltypes.h          |  2 ++
 kernel/rtlil.cc             |  2 +-
 kernel/rtlil.h              |  1 +
 passes/techmap/simplemap.cc | 13 +++++++++++++
 techlibs/common/stdcells.v  | 14 ++++++++++----
 6 files changed, 35 insertions(+), 5 deletions(-)

diff --git a/kernel/calc.cc b/kernel/calc.cc
index fc978c11..a56db93a 100644
--- a/kernel/calc.cc
+++ b/kernel/calc.cc
@@ -543,6 +543,14 @@ RTLIL::Const RTLIL::const_pos(const RTLIL::Const &arg1, const RTLIL::Const&, boo
 	return arg1_ext;
 }
 
+RTLIL::Const RTLIL::const_bu0(const RTLIL::Const &arg1, const RTLIL::Const&, bool signed1, bool, int result_len)
+{
+	RTLIL::Const arg1_ext = arg1;
+	extend_u0(arg1_ext, result_len, signed1);
+
+	return arg1_ext;
+}
+
 RTLIL::Const RTLIL::const_neg(const RTLIL::Const &arg1, const RTLIL::Const&, bool signed1, bool, int result_len)
 {
 	RTLIL::Const arg1_ext = arg1;
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 29eb490f..2f311c82 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -60,6 +60,7 @@ struct CellTypes
 	{
 		cell_types.insert("$not");
 		cell_types.insert("$pos");
+		cell_types.insert("$bu0");
 		cell_types.insert("$neg");
 		cell_types.insert("$and");
 		cell_types.insert("$or");
@@ -250,6 +251,7 @@ struct CellTypes
 		HANDLE_CELL_TYPE(mod)
 		HANDLE_CELL_TYPE(pow)
 		HANDLE_CELL_TYPE(pos)
+		HANDLE_CELL_TYPE(bu0)
 		HANDLE_CELL_TYPE(neg)
 #undef HANDLE_CELL_TYPE
 
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 47dc098a..b8c9e21a 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -370,7 +370,7 @@ namespace {
 
 		void check()
 		{
-			if (cell->type == "$not" || cell->type == "$pos" || cell->type == "$neg") {
+			if (cell->type == "$not" || cell->type == "$pos" || cell->type == "$bu0" || cell->type == "$neg") {
 				param("\\A_SIGNED");
 				port("\\A", param("\\A_WIDTH"));
 				port("\\Y", param("\\Y_WIDTH"));
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index 91dd9d44..8e3b78ee 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -187,6 +187,7 @@ namespace RTLIL
 	RTLIL::Const const_pow         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 
 	RTLIL::Const const_pos         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+	RTLIL::Const const_bu0         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 	RTLIL::Const const_neg         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 };
 
diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc
index fbd86d59..6b25eb9b 100644
--- a/passes/techmap/simplemap.cc
+++ b/passes/techmap/simplemap.cc
@@ -60,6 +60,18 @@ static void simplemap_pos(RTLIL::Module *module, RTLIL::Cell *cell)
 	module->connections.push_back(RTLIL::SigSig(sig_y, sig_a));
 }
 
+static void simplemap_bu0(RTLIL::Module *module, RTLIL::Cell *cell)
+{
+	int width = cell->parameters.at("\\Y_WIDTH").as_int();
+
+	RTLIL::SigSpec sig_a = cell->connections.at("\\A");
+	sig_a.extend_u0(width, cell->parameters.at("\\A_SIGNED").as_bool());
+
+	RTLIL::SigSpec sig_y = cell->connections.at("\\Y");
+
+	module->connections.push_back(RTLIL::SigSig(sig_y, sig_a));
+}
+
 static void simplemap_bitop(RTLIL::Module *module, RTLIL::Cell *cell)
 {
 	int width = cell->parameters.at("\\Y_WIDTH").as_int();
@@ -454,6 +466,7 @@ void simplemap_get_mappers(std::map<std::string, void(*)(RTLIL::Module*, RTLIL::
 {
 	mappers["$not"]         = simplemap_not;
 	mappers["$pos"]         = simplemap_pos;
+	mappers["$bu0"]         = simplemap_bu0;
 	mappers["$and"]         = simplemap_bitop;
 	mappers["$or"]          = simplemap_bitop;
 	mappers["$xor"]         = simplemap_bitop;
diff --git a/techlibs/common/stdcells.v b/techlibs/common/stdcells.v
index c7efa240..5482d380 100644
--- a/techlibs/common/stdcells.v
+++ b/techlibs/common/stdcells.v
@@ -44,6 +44,12 @@ endmodule
 
 // --------------------------------------------------------
 
+(* techmap_simplemap *)
+module \$bu0 ;
+endmodule
+
+// --------------------------------------------------------
+
 module \$neg (A, Y);
 
 parameter A_SIGNED = 0;
@@ -538,8 +544,8 @@ output [Y_WIDTH-1:0] Y;
 
 wire carry, carry_sign;
 wire [WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$bu0 #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$bu0 #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 assign Y = ~|(A_buf ^ B_buf);
 
@@ -563,8 +569,8 @@ output [Y_WIDTH-1:0] Y;
 
 wire carry, carry_sign;
 wire [WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$bu0 #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$bu0 #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 assign Y = |(A_buf ^ B_buf);
 

From fe8ec32a1c401f54e0791d8d241ef583e09257dc Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 28 Dec 2013 12:10:32 +0100
Subject: [PATCH 26/49] Added new cell types to manual

---
 manual/CHAPTER_CellLib.tex  | 9 +++++++++
 passes/techmap/simplemap.cc | 2 +-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index 09be0870..61713e74 100644
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -97,6 +97,12 @@ The width of the output port \B{Y}.
 
 Table~\ref{tab:CellLib_binary} lists all cells for binary RTL operators.
 
+The additional cell type {\tt \$bu0} is similar to {\tt \$pos}, but always
+extends unsigned arguments with zeros. ({\tt \$pos} extends unsigned arguments
+with {\tt x}-bits if the most significant bit is {\tt x}.) This is used
+internally to correctly implement the {\tt ==} and {\tt !=} operators for
+constant arguments.
+
 \subsection{Multiplexers}
 
 Multiplexers are generated by the Verilog HDL frontend for {\tt
@@ -147,6 +153,9 @@ Verilog & Cell Type \\
 \hline
 \lstinline[language=Verilog]; Y = A && B; & {\tt \$logic\_and} \\
 \lstinline[language=Verilog]; Y = A || B; & {\tt \$logic\_or} \\
+\hline
+\lstinline[language=Verilog]; Y = A === B; & {\tt \$eqx} \\
+\lstinline[language=Verilog]; Y = A !== B; & {\tt \$nex} \\
 \end{tabular}
 \hfil
 \begin{tabular}[t]{ll}
diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc
index 6b25eb9b..2480cf28 100644
--- a/passes/techmap/simplemap.cc
+++ b/passes/techmap/simplemap.cc
@@ -498,7 +498,7 @@ struct SimplemapPass : public Pass {
 		log("This pass maps a small selection of simple coarse-grain cells to yosys gate\n");
 		log("primitives. The following internal cell types are mapped by this pass:\n");
 		log("\n");
-		log("  $not, $pos, $and, $or, $xor, $xnor\n");
+		log("  $not, $pos, $bu0, $and, $or, $xor, $xnor\n");
 		log("  $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool\n");
 		log("  $logic_not, $logic_and, $logic_or, $mux\n");
 		log("  $sr, $dff, $dffsr, $adff, $dlatch\n");

From 74d0de3b74cdf5d41eacd588d69488290549fd7e Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 28 Dec 2013 12:14:47 +0100
Subject: [PATCH 27/49] Updated manual/command-reference-manual.tex

---
 backends/ilang/ilang_backend.cc     |   2 +-
 manual/command-reference-manual.tex | 142 ++++++++++++++++++++++++++--
 2 files changed, 137 insertions(+), 7 deletions(-)

diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index 66775b2a..924e316b 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -402,7 +402,7 @@ struct DumpPass : public Pass {
 		log("ilang format.\n");
 		log("\n");
 		log("    -m\n");
-		log("        also dump the module headers, even if only parts of a single");
+		log("        also dump the module headers, even if only parts of a single\n");
 		log("        module is selected\n");
 		log("\n");
 		log("    -n\n");
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex
index 1c91cb66..54fec542 100644
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@@ -131,6 +131,13 @@ first run this pass and then map the logic paths to the target technology.
 Write the selected parts of the design to the console or specified file in
 ilang format.
 
+    -m
+        also dump the module headers, even if only parts of a single
+        module is selected
+
+    -n
+        only dump the module headers if the entire module is selected
+
     -outfile <filename>
         Write to the specified file.
 \end{lstlisting}
@@ -146,6 +153,12 @@ inputs.
     -set <signal> <value>
         set the specified signal to the specified value.
 
+    -set-undef
+        set all unspecified source signals to undef (x)
+
+    -table <signal>
+        create a truth table using the specified input signals
+
     -show <signal>
         show the value for the specified signal. if no -show option is passed
         then all output ports of the current module are used.
@@ -423,6 +436,10 @@ needed.
         use the specified top module to built a design hierarchy. modules
         outside this tree (unused modules) are removed.
 
+        when the -top option is used, the 'top' attribute will be set on the
+        specified top module. otherwise a module with the 'top' attribute set
+        will implicitly be used as top module, if such a module exists.
+
 In -generate mode this pass generates blackbox modules for the given cell
 types (wildcards supported). For this the design is searched for cells that
 match the given types and then the given port declarations are used to
@@ -440,6 +457,16 @@ This pass ignores the current selection and always operates on all modules
 in the current design.
 \end{lstlisting}
 
+\section{history -- show last interactive commands}
+\label{cmd:history}
+\begin{lstlisting}[numbers=left,frame=single]
+    history
+
+This command prints all commands in the shell history buffer. This are
+all commands executed in an interactive session, but not the commands
+from executed scripts.
+\end{lstlisting}
+
 \section{iopadmap -- technology mapping of i/o pads (or buffers)}
 \label{cmd:iopadmap}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -469,11 +496,17 @@ the resulting cells to more sophisticated PAD cells.
 \section{ls -- list modules or objects in modules}
 \label{cmd:ls}
 \begin{lstlisting}[numbers=left,frame=single]
-    ls
+    ls [pattern]
 
-When no active module is selected, this prints a list of all module.
+When no active module is selected, this prints a list of all modules.
 
 When an active module is selected, this prints a list of objects in the module.
+
+If a pattern is given, the objects matching the pattern are printed
+
+Note that this command does not use the selection mechanism and always operates
+on the whole design or whole active module. Use 'select -list' to show a list
+of currently selected objects.
 \end{lstlisting}
 
 \section{memory -- translate memories to basic cells}
@@ -761,6 +794,10 @@ Verilog-2005 is supported.
         don't perform basic optimizations (such as const folding) in the
         high-level front-end.
 
+    -ignore_redef
+        ignore re-definitions of modules. (the default behavior is to
+        create an error message.)
+
     -Dname[=definition]
         define the preprocessor symbol 'name' and set its optional value
         'definition'
@@ -800,9 +837,29 @@ and additional constraints passed as parameters.
     -max <N>
         like -all, but limit number of solutions to <N>
 
+    -enable_undef
+        enable modeling of undef value (aka 'x-bits')
+        this option is implied by -set-def, -set-undef et. cetera
+
+    -max_undef
+        maximize the number of undef bits in solutions, giving a better
+        picture of which input bits are actually vital to the solution.
+
     -set <signal> <value>
         set the specified signal to the specified value.
 
+    -set-def <signal>
+        add a constraint that all bits of the given signal must be defined
+
+    -set-any-undef <signal>
+        add a constraint that at least one bit of the given signal is undefined
+
+    -set-all-undef <signal>
+        add a constraint that all bits of the given signal are undefined
+
+    -set-def-inputs
+        add -set-def constraints for all module inputs
+
     -show <signal>
         show the model for the specified signal. if no -show option is
         passed then a set of signals to be shown is automatically selected.
@@ -821,6 +878,17 @@ The following options can be used to set up a sequential problem:
         set or unset the specified signal to the specified value in the
         given timestep. this has priority over a -set for the same signal.
 
+    -set-def-at <N> <signal>
+    -set-any-undef-at <N> <signal>
+    -set-all-undef-at <N> <signal>
+        add undef contraints in the given timestep.
+
+    -set-init <signal> <value>
+        set the initial value for the register driving the signal to the value
+
+    -set-init-undef
+        set all initial states (not set using -set-init) to undef
+
 The following additional options can be used to set up a proof. If also -seq
 is passed, a temporal induction proof is performed.
 
@@ -829,6 +897,10 @@ is passed, a temporal induction proof is performed.
         induction proof it is proven that the condition holds forever after
         the number of time steps passed using -seq.
 
+    -prove-x <signal> <value>
+        Like -prove, but an undef (x) bit in the lhs matches any value on
+        the right hand side. Useful for equivialence checking.
+
     -maxsteps <N>
         Set a maximum length for the induction.
 
@@ -1108,6 +1180,15 @@ to a graphics file (usually SVG or PostScript).
         stretch the graph so all inputs are on the left side and all outputs
         (including inout ports) are on the right side.
 
+    -pause
+        wait for the use to press enter to before returning
+
+    -enum
+        enumerate objects with internal ($-prefixed) names
+
+    -long
+        do not abbeviate objects with internal ($-prefixed) names
+
 When no <format> is specified, SVG is used. When no <format> and <viewer> is
 specified, 'yosys-svgviewer' is used to display the schematic.
 
@@ -1115,6 +1196,20 @@ The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>',
 unless another prefix is specified using -prefix <prefix>.
 \end{lstlisting}
 
+\section{simplemap -- mapping simple coarse-grain cells}
+\label{cmd:simplemap}
+\begin{lstlisting}[numbers=left,frame=single]
+    simplemap [selection]
+
+This pass maps a small selection of simple coarse-grain cells to yosys gate
+primitives. The following internal cell types are mapped by this pass:
+
+  $not, $pos, $bu0, $and, $or, $xor, $xnor
+  $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool
+  $logic_not, $logic_and, $logic_or, $mux
+  $sr, $dff, $dffsr, $adff, $dlatch
+\end{lstlisting}
+
 \section{splitnets -- split up multi-bit nets}
 \label{cmd:splitnets}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1131,6 +1226,20 @@ This command splits multi-bit nets into single-bit nets.
         also split module ports. per default only internal signals are split.
 \end{lstlisting}
 
+\section{stat -- print some statistics}
+\label{cmd:stat}
+\begin{lstlisting}[numbers=left,frame=single]
+    stat [options] [selection]
+
+Print some statistics (number of objects) on the selected portion of the
+design.
+
+    -top <module>
+        print design hierarchy with this module as top. if the design is fully
+        selected and a module has the 'top' attribute set, this module is used
+        default value for this option.
+\end{lstlisting}
+
 \section{submod -- moving part of a module to a new submodule}
 \label{cmd:submod}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1202,7 +1311,7 @@ The following commands are executed by this synthesis command:
         clean
 
     map_cells:
-        techmap -map <share_dir>/xilinx/cells.v
+        techmap -share_map xilinx/cells.v
         clean
 
     clkbuf:
@@ -1214,7 +1323,7 @@ The following commands are executed by this synthesis command:
         iopadmap -outpad OBUF I:O -inpad IBUF O:I @xilinx_nonclocks
 
     edif:
-        write_edif -top <top> synth.edif
+        write_edif synth.edif
 \end{lstlisting}
 
 \section{tcl -- execute a TCL script file}
@@ -1246,12 +1355,26 @@ file.
         transforms the internal RTL cells to the internal gate
         library.
 
+    -share_map filename
+        like -map, but look for the file in the share directory (where the
+        yosys data files are). this is mainly used internally when techmap
+        is called from other commands.
+
+    -D <define>, -I <incdir>
+        this options are passed as-is to the verilog frontend for loading the
+        map file. Note that the verilog frontend is also called with the
+        '-ignore_redef' option set.
+
 When a module in the map file has the 'techmap_celltype' attribute set, it will
-match cells with a type that match the text value of this attribute.
+match cells with a type that match the text value of this attribute. Otherwise
+the module name will be used to match the cell.
+
+When a module in the map file has the 'techmap_simplemap' attribute set, techmap
+will use 'simplemap' (see 'help simplemap') to map cells matching the module.
 
 All wires in the modules from the map file matching the pattern _TECHMAP_*
 or *._TECHMAP_* are special wires that are used to pass instructions from
-the mapping module to the techmap command. At the moment the following spoecial
+the mapping module to the techmap command. At the moment the following special
 wires are supported:
 
     _TECHMAP_FAIL_
@@ -1273,6 +1396,13 @@ wires are supported:
         wire to start out as non-constant and evaluate to a constant value
         during processing of other _TECHMAP_DO_* commands.
 
+In addition to this special wires, techmap also supports special parameters in
+modules in the map file:
+
+    _TECHMAP_CELLTYPE_
+        When a parameter with this name exists, it will be set to the type name
+        of the cell that matches the module.
+
 When a module in the map file has a parameter where the according cell in the
 design has a port, the module from the map file is only used if the port in
 the design is connected to a constant value. The parameter is then set to the

From bf607df6d57c3976880004192129eff8b1c0d0a9 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 29 Dec 2013 17:39:49 +0100
Subject: [PATCH 28/49] Fixed undef extend for bitwise binary ops (bugs in
 simplemap and satgen)

---
 kernel/satgen.h             | 19 ++++++++-----------
 passes/techmap/simplemap.cc |  4 ++--
 2 files changed, 10 insertions(+), 13 deletions(-)

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 05f3310c..b04bd619 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -121,11 +121,10 @@ struct SatGen
 		return ez->expression(ezSAT::OpAnd, eq_bits);
 	}
 
-	void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0, bool undef_mode = false)
+	void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0, bool forced_signed = false)
 	{
-		log_assert(!undef_mode || model_undef);
-		bool is_signed = undef_mode;
-		if (!undef_mode && cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
+		bool is_signed = forced_signed;
+		if (!forced_signed && cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
 			is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
 		while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
 			vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
@@ -133,18 +132,16 @@ struct SatGen
 			vec_b.push_back(is_signed && vec_b.size() > 0 ? vec_b.back() : ez->FALSE);
 	}
 
-	void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell, bool undef_mode = false)
+	void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
 	{
-		log_assert(!undef_mode || model_undef);
-		extendSignalWidth(vec_a, vec_b, cell, vec_y.size(), undef_mode);
+		extendSignalWidth(vec_a, vec_b, cell, vec_y.size(), forced_signed);
 		while (vec_y.size() < vec_a.size())
 			vec_y.push_back(ez->literal());
 	}
 
-	void extendSignalWidthUnary(std::vector<int> &vec_a, std::vector<int> &vec_y, RTLIL::Cell *cell, bool undef_mode = false)
+	void extendSignalWidthUnary(std::vector<int> &vec_a, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
 	{
-		log_assert(!undef_mode || model_undef);
-		bool is_signed = undef_mode || (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool());
+		bool is_signed = forced_signed || (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool());
 		while (vec_a.size() < vec_y.size())
 			vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
 		while (vec_y.size() < vec_a.size())
@@ -222,7 +219,7 @@ struct SatGen
 				std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 				std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 				std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
-				extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
+				extendSignalWidth(undef_a, undef_b, undef_y, cell, false);
 
 				if (cell->type == "$and" || cell->type == "$_AND_") {
 					std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc
index 2480cf28..e06a80bb 100644
--- a/passes/techmap/simplemap.cc
+++ b/passes/techmap/simplemap.cc
@@ -77,11 +77,11 @@ static void simplemap_bitop(RTLIL::Module *module, RTLIL::Cell *cell)
 	int width = cell->parameters.at("\\Y_WIDTH").as_int();
 
 	RTLIL::SigSpec sig_a = cell->connections.at("\\A");
-	sig_a.extend(width, cell->parameters.at("\\A_SIGNED").as_bool());
+	sig_a.extend_u0(width, cell->parameters.at("\\A_SIGNED").as_bool());
 	sig_a.expand();
 
 	RTLIL::SigSpec sig_b = cell->connections.at("\\B");
-	sig_b.extend(width, cell->parameters.at("\\B_SIGNED").as_bool());
+	sig_b.extend_u0(width, cell->parameters.at("\\B_SIGNED").as_bool());
 	sig_b.expand();
 
 	RTLIL::SigSpec sig_y = cell->connections.at("\\Y");

From 364f277afba815029be8b4bf67e68547080df859 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 29 Dec 2013 20:18:22 +0100
Subject: [PATCH 29/49] Fixed a stupid access after delete bug

---
 frontends/ast/simplify.cc | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 982d1ae3..9b8ed760 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -497,8 +497,9 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 		if (width != int(children[0]->bits.size())) {
 			RTLIL::SigSpec sig(children[0]->bits);
 			sig.extend_u0(width, children[0]->is_signed);
-			delete children[0];
+			AstNode *old_child_0 = children[0];
 			children[0] = mkconst_bits(sig.as_const().bits, children[0]->is_signed);
+			delete old_child_0;
 		}
 		children[0]->is_signed = is_signed;
 	}

From c616802ac717fd029a32714f18f26dc8c90a6723 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Dec 2013 13:41:16 +0100
Subject: [PATCH 30/49] Always use BLIF as ABC output format

---
 passes/abc/Makefile.inc |   1 -
 passes/abc/abc.cc       |  17 +--
 passes/abc/blifparse.cc |  26 +++++
 passes/abc/vlparse.cc   | 227 ----------------------------------------
 passes/abc/vlparse.h    |  28 -----
 5 files changed, 31 insertions(+), 268 deletions(-)
 delete mode 100644 passes/abc/vlparse.cc
 delete mode 100644 passes/abc/vlparse.h

diff --git a/passes/abc/Makefile.inc b/passes/abc/Makefile.inc
index dbb7496c..a7c5b02c 100644
--- a/passes/abc/Makefile.inc
+++ b/passes/abc/Makefile.inc
@@ -1,7 +1,6 @@
 
 ifeq ($(ENABLE_ABC),1)
 OBJS += passes/abc/abc.o
-OBJS += passes/abc/vlparse.o
 OBJS += passes/abc/blifparse.o
 endif
 
diff --git a/passes/abc/abc.cc b/passes/abc/abc.cc
index e37f896f..5965ffa1 100644
--- a/passes/abc/abc.cc
+++ b/passes/abc/abc.cc
@@ -36,7 +36,6 @@
 #include <dirent.h>
 #include <sstream>
 
-#include "vlparse.h"
 #include "blifparse.h"
 
 struct gate_t
@@ -481,10 +480,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 			buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
 					"%s -s -c 'read_verilog %s/input.v; read_library %s/stdcells.genlib; strash; balance; dch; map; ",
 					exe_file.c_str(), tempdir_name, tempdir_name);
-		if (lut_mode)
-			buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos, "write_blif %s/output.blif' 2>&1", tempdir_name);
-		else                                                             
-			buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos, "write_verilog %s/output.v' 2>&1", tempdir_name);
+		buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos, "write_blif %s/output.blif' 2>&1", tempdir_name);
 
 		errno = ENOMEM;  // popen does not set errno if memory allocation fails, therefore set it by hand
 		f = popen(buffer, "r");
@@ -504,16 +500,13 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 			}
 		}
 
-		if (asprintf(&p, "%s/%s", tempdir_name, lut_mode ? "output.blif" : "output.v") < 0) abort();
+		if (asprintf(&p, "%s/%s", tempdir_name, "output.blif") < 0) log_abort();
 		f = fopen(p, "rt");
 		if (f == NULL)
 			log_error("Can't open ABC output file `%s'.\n", p);
-#if 0
-		RTLIL::Design *mapped_design = new RTLIL::Design;
-		frontend_register["verilog"]->execute(f, p, std::vector<std::string>(), mapped_design);
-#else
-		RTLIL::Design *mapped_design = lut_mode ? abc_parse_blif(f) : abc_parse_verilog(f);
-#endif
+
+		RTLIL::Design *mapped_design = abc_parse_blif(f);
+
 		fclose(f);
 		free(p);
 
diff --git a/passes/abc/blifparse.cc b/passes/abc/blifparse.cc
index 17acc843..825d5eab 100644
--- a/passes/abc/blifparse.cc
+++ b/passes/abc/blifparse.cc
@@ -101,6 +101,32 @@ RTLIL::Design *abc_parse_blif(FILE *f)
 				continue;
 			}
 
+			if (!strcmp(cmd, ".gate"))
+			{
+				RTLIL::Cell *cell = new RTLIL::Cell;
+				cell->name = NEW_ID;
+				module->add(cell);
+
+				char *p = strtok(NULL, " \t\r\n");
+				if (p == NULL)
+					goto error;
+				cell->type = RTLIL::escape_id(p);
+
+				while ((p = strtok(NULL, " \t\r\n")) != NULL) {
+					char *q = strchr(p, '=');
+					if (q == NULL || !q[0] || !q[1])
+						goto error;
+					*(q++) = 0;
+					if (module->wires.count(RTLIL::escape_id(q)) == 0) {
+						RTLIL::Wire *wire = new RTLIL::Wire;
+						wire->name = RTLIL::escape_id(q);
+						module->add(wire);
+					}
+					cell->connections[RTLIL::escape_id(p)] = module->wires.at(RTLIL::escape_id(q));
+				}
+				continue;
+			}
+
 			if (!strcmp(cmd, ".names"))
 			{
 				char *p;
diff --git a/passes/abc/vlparse.cc b/passes/abc/vlparse.cc
deleted file mode 100644
index fe10f57b..00000000
--- a/passes/abc/vlparse.cc
+++ /dev/null
@@ -1,227 +0,0 @@
-/*
- *  yosys -- Yosys Open SYnthesis Suite
- *
- *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *  
- *  Permission to use, copy, modify, and/or distribute this software for any
- *  purpose with or without fee is hereby granted, provided that the above
- *  copyright notice and this permission notice appear in all copies.
- *  
- *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- */
-
-#include "vlparse.h"
-#include "kernel/log.h"
-#include <stdio.h>
-#include <string>
-
-static int lex_line, lex_tok;
-static std::string lex_str;
-
-static int token(int tok)
-{
-	lex_tok = tok;
-#if 0
-	if (lex_tok == 256)
-		fprintf(stderr, "STR in line %d: >>%s<<\n", lex_line, lex_str.c_str());
-	else if (tok >= 32 && tok < 255)
-		fprintf(stderr, "CHAR in line %d: >>%c<<\n", lex_line, lex_tok);
-	else
-		fprintf(stderr, "CHAR in line %d: %d\n", lex_line, lex_tok);
-#endif
-	return tok;
-}
-
-static int lex(FILE *f)
-{
-	int ch = getc(f);
-
-	while (ch == ' ' || ch == '\t' || ch == '\n') {
-		if (ch == '\n')
-			lex_line++;
-		ch = getc(f);
-	}
-
-	if (ch <= 0 || 255 < ch)
-		return token(lex_tok);
-	
-	if (('a' <= ch && ch <= 'z') || ('A' <= ch && ch <= 'Z') ||
-			('0' <= ch && ch <= '9') || ch == '_' || ch == '\'') {
-		lex_str = char(ch);
-		while (1) {
-			ch = getc(f);
-			if (('a' <= ch && ch <= 'z') || ('A' <= ch && ch <= 'Z') ||
-					('0' <= ch && ch <= '9') || ch == '_' || ch == '\'') {
-				lex_str += char(ch);
-				continue;
-			}
-			break;
-		}
-		ungetc(ch, f);
-		return token(256);
-	}
-
-	if (ch == '/') {
-		ch = getc(f);
-		if (ch == '/') {
-			while (ch != '\n')
-				ch = getc(f);
-			ungetc(ch, f);
-			return lex(f);
-		}
-		ungetc(ch, f);
-		return token('/');
-	}
-
-	return token(ch);
-}
-
-RTLIL::Design *abc_parse_verilog(FILE *f)
-{
-	RTLIL::Design *design = new RTLIL::Design;
-	RTLIL::Module *module;
-	RTLIL::Wire *wire;
-	RTLIL::Cell *cell;
-
-	int port_count = 1;
-	lex_line = 1;
-
-	// parse module header
-	if (lex(f) != 256 || lex_str != "module")
-		goto error;
-	if (lex(f) != 256)
-		goto error;
-
-	module = new RTLIL::Module;
-	module->name = "\\" + lex_str;
-	design->modules[module->name] = module;
-
-	if (lex(f) != '(')
-		goto error;
-	while (lex(f) != ')') {
-		if (lex_tok != 256 && lex_tok != ',')
-			goto error;
-	}
-	if (lex(f) != ';')
-		goto error;
-
-	// parse module body
-	while (1)
-	{
-		if (lex(f) != 256)
-			goto error;
-
-		if (lex_str == "endmodule")
-			return design;
-
-		if (lex_str == "input" || lex_str == "output" || lex_str == "wire")
-		{
-			std::string mode = lex_str;
-			while (lex(f) != ';') {
-				if (lex_tok != 256 && lex_tok != ',')
-					goto error;
-				if (lex_tok == 256) {
-					// printf("%s [%s]\n", mode.c_str(), lex_str.c_str());
-					wire = new RTLIL::Wire;
-					wire->name = "\\" + lex_str;
-					if (mode == "input") {
-						wire->port_id = port_count++;
-						wire->port_input = true;
-					}
-					if (mode == "output") {
-						wire->port_id = port_count++;
-						wire->port_output = true;
-					}
-					module->wires[wire->name] = wire;
-				}
-			}
-		}
-		else if (lex_str == "assign")
-		{
-			std::string lhs, rhs;
-
-			if (lex(f) != 256)
-				goto error;
-			lhs = lex_str;
-
-			if (lex(f) != '=')
-				goto error;
-			if (lex(f) != 256)
-				goto error;
-			rhs = lex_str;
-
-			if (lex(f) != ';')
-				goto error;
-
-			if (module->wires.count(RTLIL::escape_id(lhs)) == 0)
-				goto error;
-
-			if (rhs == "1'b0")
-				module->connections.push_back(RTLIL::SigSig(module->wires.at(RTLIL::escape_id(lhs)), RTLIL::SigSpec(0, 1)));
-			else if (rhs == "1'b1")
-				module->connections.push_back(RTLIL::SigSig(module->wires.at(RTLIL::escape_id(lhs)), RTLIL::SigSpec(1, 1)));
-			else if (module->wires.count(RTLIL::escape_id(rhs)) > 0)
-				module->connections.push_back(RTLIL::SigSig(module->wires.at(RTLIL::escape_id(lhs)), module->wires.at(RTLIL::escape_id(rhs))));
-			else
-				goto error;
-		}
-		else
-		{
-			std::string cell_type = lex_str;
-
-			if (lex(f) != 256)
-				goto error;
-
-			std::string cell_name = lex_str;
-
-			if (lex(f) != '(')
-				goto error;
-
-			// printf("cell [%s] [%s]\n", cell_type.c_str(), cell_name.c_str());
-			cell = new RTLIL::Cell;
-			cell->type = "\\" + cell_type;
-			cell->name = "\\" + cell_name;
-			module->cells[cell->name] = cell;
-
-			lex(f);
-			while (lex_tok != ')')
-			{
-				if (lex_tok != '.' || lex(f) != 256)
-					goto error;
-
-				std::string cell_port = lex_str;
-
-				if (lex(f) != '(' || lex(f) != 256)
-					goto error;
-
-				std::string wire_name = lex_str;
-
-				// printf("  [%s] <- [%s]\n", cell_port.c_str(), wire_name.c_str());
-				if (module->wires.count("\\" + wire_name) == 0)
-					goto error;
-				cell->connections["\\" + cell_port] = RTLIL::SigSpec(module->wires["\\" + wire_name]);
-
-				if (lex(f) != ')' || (lex(f) != ',' && lex_tok != ')'))
-					goto error;
-				while (lex_tok == ',')
-					lex(f);
-			}
-
-			if (lex(f) != ';')
-				goto error;
-		}
-	}
-
-error:
-	log_error("Syntax error in line %d!\n", lex_line);
-	// delete design;
-	// return NULL;
-}
-
diff --git a/passes/abc/vlparse.h b/passes/abc/vlparse.h
deleted file mode 100644
index 9514c419..00000000
--- a/passes/abc/vlparse.h
+++ /dev/null
@@ -1,28 +0,0 @@
-/*
- *  yosys -- Yosys Open SYnthesis Suite
- *
- *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *  
- *  Permission to use, copy, modify, and/or distribute this software for any
- *  purpose with or without fee is hereby granted, provided that the above
- *  copyright notice and this permission notice appear in all copies.
- *  
- *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- */
-
-#ifndef ABC_VLPARSE
-#define ABC_VLPARSE
-
-#include "kernel/rtlil.h"
-
-extern RTLIL::Design *abc_parse_verilog(FILE *f);
-
-#endif
-

From a582b9d1849a9cb1f13323d8894de3fdb0bc6c90 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Dec 2013 13:51:25 +0100
Subject: [PATCH 31/49] Fixed commented out techmap call in
 tests/tools/autotest.sh

---
 tests/tools/autotest.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index 5a302bcd..e5376809 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -150,7 +150,7 @@ do
 		else
 			test_passes -p "hierarchy; proc; memory; opt; fsm; opt"
 			test_passes -p "hierarchy; proc; memory; opt; fsm; opt; techmap; opt"
-			# test_passes -p "hierarchy; proc; memory; opt; fsm; opt; techmap -opt; opt; abc; opt"
+			# test_passes -p "hierarchy; proc; memory; opt; fsm; opt; techmap; opt; abc; opt"
 		fi
 		touch ../${bn}.log
 	}

From be5dab87fd49f0095678d7b69d35a8456a641178 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Dec 2013 14:29:29 +0100
Subject: [PATCH 32/49] Now using BLIF as ABC input format

---
 passes/abc/abc.cc | 97 ++++++++++++++++++++++++++++-------------------
 1 file changed, 57 insertions(+), 40 deletions(-)

diff --git a/passes/abc/abc.cc b/passes/abc/abc.cc
index 5965ffa1..1e7c66e1 100644
--- a/passes/abc/abc.cc
+++ b/passes/abc/abc.cc
@@ -21,6 +21,10 @@
 // Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification
 // http://www.eecs.berkeley.edu/~alanmi/abc/
 
+// [[CITE]] Berkeley Logic Interchange Format (BLIF)
+// University of California. Berkeley. July 28, 1992
+// http://www.ece.cmu.edu/~ee760/760docs/blif.pdf
+
 // [[CITE]] Kahn's Topological sorting algorithm
 // Kahn, Arthur B. (1962), "Topological sorting of large networks", Communications of the ACM 5 (11): 558–562, doi:10.1145/368996.369025
 // http://en.wikipedia.org/wiki/Topological_sorting
@@ -339,7 +343,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 	if (!cleanup)
 		tempdir_name[0] = tempdir_name[4] = '_';
 	char *p = mkdtemp(tempdir_name);
-	log_header("Extracting gate netlist of module `%s' to `%s/input.v'..\n", module->name.c_str(), tempdir_name);
+	log_header("Extracting gate netlist of module `%s' to `%s/input.blif'..\n", module->name.c_str(), tempdir_name);
 	if (p == NULL)
 		log_error("For some reason mkdtemp() failed!\n");
 
@@ -362,60 +366,73 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 	
 	handle_loops();
 
-	if (asprintf(&p, "%s/input.v", tempdir_name) < 0) abort();
+	if (asprintf(&p, "%s/input.blif", tempdir_name) < 0) abort();
 	FILE *f = fopen(p, "wt");
 	if (f == NULL)
 		log_error("Opening %s for writing failed: %s\n", p, strerror(errno));
 	free(p);
 
-	fprintf(f, "module netlist (");
-	bool first = true;
-	for (auto &si : signal_list) {
-		if (!si.is_port)
-			continue;
-		if (!first)
-			fprintf(f, ", ");
-		fprintf(f, "n%d", si.id);
-		first = false;
-	}
-	fprintf(f, "); // %s\n", module->name.c_str());
+	fprintf(f, ".model netlist\n");
 
-	int count_input = 0, count_output = 0;
+	int count_input = 0;
+	fprintf(f, ".inputs");
 	for (auto &si : signal_list) {
-		if (si.is_port) {
-			if (si.type >= 0)
-				count_output++;
-			else
-				count_input++;
-		}
-		fprintf(f, "%s n%d; // %s\n", si.is_port ? si.type >= 0 ?
-				"output" : "input" : "wire", si.id, log_signal(si.sig));
+		if (!si.is_port || si.type >= 0)
+			continue;
+		fprintf(f, " n%d", si.id);
+		count_input++;
 	}
+	fprintf(f, "\n");
+
+	int count_output = 0;
+	fprintf(f, ".outputs");
+	for (auto &si : signal_list) {
+		if (!si.is_port || si.type < 0)
+			continue;
+		fprintf(f, " n%d", si.id);
+		count_output++;
+	}
+	fprintf(f, "\n");
+
+	for (auto &si : signal_list)
+		fprintf(f, "# n%-5d %s\n", si.id, log_signal(si.sig));
+
 	for (auto &si : signal_list) {
 		assert(si.sig.width == 1 && si.sig.chunks.size() == 1);
-		if (si.sig.chunks[0].wire == NULL)
-			fprintf(f, "assign n%d = %c;\n", si.id, si.sig.chunks[0].data.bits[0] == RTLIL::State::S1 ? '1' : '0');
+		if (si.sig.chunks[0].wire == NULL) {
+			fprintf(f, ".names n%d\n", si.id);
+			if (si.sig.chunks[0].data.bits[0] == RTLIL::State::S1)
+				fprintf(f, "1\n");
+		}
 	}
 
 	int count_gates = 0;
 	for (auto &si : signal_list) {
-		if (si.type == 'n')
-			fprintf(f, "not (n%d, n%d);\n", si.id, si.in1);
-		else if (si.type == 'a')
-			fprintf(f, "and (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
-		else if (si.type == 'o')
-			fprintf(f, "or (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
-		else if (si.type == 'x')
-			fprintf(f, "xor (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
-		else if (si.type == 'm')
-			fprintf(f, "assign n%d = n%d ? n%d : n%d;\n", si.id, si.in3, si.in2, si.in1);
-		else if (si.type >= 0)
+		if (si.type == 'n') {
+			fprintf(f, ".names n%d n%d\n", si.in1, si.id);
+			fprintf(f, "0 1\n");
+		} else if (si.type == 'a') {
+			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, "11 1\n");
+		} else if (si.type == 'o') {
+			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, "-1 1\n");
+			fprintf(f, "1- 1\n");
+		} else if (si.type == 'x') {
+			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, "01 1\n");
+			fprintf(f, "10 1\n");
+		} else if (si.type == 'm') {
+			fprintf(f, ".names n%d n%d n%d n%d\n", si.in1, si.in2, si.in3, si.id);
+			fprintf(f, "1-0 1\n");
+			fprintf(f, "-11 1\n");
+		} else if (si.type >= 0)
 			abort();
 		if (si.type >= 0)
 			count_gates++;
 	}
 
-	fprintf(f, "endmodule\n");
+	fprintf(f, ".end\n");
 	fclose(f);
 
 	log("Extracted %d gates and %zd wires to a netlist network with %d inputs and %d outputs.\n",
@@ -456,7 +473,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 		int buffer_pos = 0;
 		if (!liberty_file.empty()) {
 			buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
-					"%s -s -c 'read_verilog %s/input.v; read_lib %s; ",
+					"%s -s -c 'read_blif %s/input.blif; read_lib %s; ",
 					exe_file.c_str(), tempdir_name, liberty_file.c_str());
 			if (!constr_file.empty())
 				buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
@@ -469,16 +486,16 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 		} else
 		if (!script_file.empty())
 			buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
-					"%s -s -c 'read_verilog %s/input.v; source %s; ",
+					"%s -s -c 'read_blif %s/input.blif; source %s; ",
 					exe_file.c_str(), tempdir_name, script_file.c_str());
 		else
 		if (lut_mode)
 			buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
-					"%s -s -c 'read_verilog %s/input.v; read_lut %s/lutdefs.txt; strash; balance; dch; if; ",
+					"%s -s -c 'read_blif %s/input.blif; read_lut %s/lutdefs.txt; strash; balance; dch; if; ",
 					exe_file.c_str(), tempdir_name, tempdir_name);
 		else
 			buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
-					"%s -s -c 'read_verilog %s/input.v; read_library %s/stdcells.genlib; strash; balance; dch; map; ",
+					"%s -s -c 'read_blif %s/input.blif; read_library %s/stdcells.genlib; strash; balance; dch; map; ",
 					exe_file.c_str(), tempdir_name, tempdir_name);
 		buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos, "write_blif %s/output.blif' 2>&1", tempdir_name);
 

From 1cd975ef8de889bf7f51ea108fcb8df878c906df Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Dec 2013 14:39:02 +0100
Subject: [PATCH 33/49] Updated ABC to hg rev 57517e81666b

---
 Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 2590033a..525d8513 100644
--- a/Makefile
+++ b/Makefile
@@ -31,13 +31,13 @@ YOSYS_VER := 0.1.0+
 GIT_REV := $(shell git rev-parse --short HEAD || echo UNKOWN)
 OBJS = kernel/version_$(GIT_REV).o
 
-# set 'ABC = default' to use abc/ as it is
+# set 'ABCREV = default' to use abc/ as it is
 #
 # Note: If you do ABC development, make sure that 'abc' in this directory
 # is just a symlink to your actual ABC working directory, as 'make mrproper'
 # will remove the 'abc' directory and you do not want to accidentally
 # delete your work on ABC..
-ABCREV = 9241719523f6
+ABCREV = 57517e81666b
 ABCPULL = 1
 
 -include Makefile.conf

From 15acf593e707c6666459c0cfd121a5f0fc996571 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Dec 2013 14:54:06 +0100
Subject: [PATCH 34/49] Added additional checks for A_SIGNED == B_SIGNED for
 cells with that constraint

---
 kernel/rtlil.cc | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index b8c9e21a..4916ca72 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -337,7 +337,7 @@ namespace {
 			expected_ports.insert(name);
 		}
 
-		void check_expected()
+		void check_expected(bool check_matched_sign = true)
 		{
 			for (auto &para : cell->parameters)
 				if (expected_params.count(para.first) == 0)
@@ -345,6 +345,13 @@ namespace {
 			for (auto &conn : cell->connections)
 				if (expected_ports.count(conn.first) == 0)
 					error(__LINE__);
+
+			if (expected_params.count("\\A_SIGNED") != 0 && expected_params.count("\\B_SIGNED") && check_matched_sign) {
+				bool a_is_signed = param("\\A_SIGNED") != 0;
+				bool b_is_signed = param("\\B_SIGNED") != 0;
+				if (a_is_signed != b_is_signed)
+					error(__LINE__);
+			}
 		}
 
 		void check_gate(const char *ports)
@@ -403,7 +410,7 @@ namespace {
 				port("\\A", param("\\A_WIDTH"));
 				port("\\B", param("\\B_WIDTH"));
 				port("\\Y", param("\\Y_WIDTH"));
-				check_expected();
+				check_expected(false);
 				return;
 			}
 
@@ -425,7 +432,7 @@ namespace {
 				port("\\A", param("\\A_WIDTH"));
 				port("\\B", param("\\B_WIDTH"));
 				port("\\Y", param("\\Y_WIDTH"));
-				check_expected();
+				check_expected(cell->type != "$pow");
 				return;
 			}
 
@@ -443,7 +450,7 @@ namespace {
 				port("\\A", param("\\A_WIDTH"));
 				port("\\B", param("\\B_WIDTH"));
 				port("\\Y", param("\\Y_WIDTH"));
-				check_expected();
+				check_expected(false);
 				return;
 			}
 

From b3b00f1bf442cee0a2db6cc846cf9b866172496d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Dec 2013 15:41:40 +0100
Subject: [PATCH 35/49] Various small cleanups in stdcells.v techmap code

---
 techlibs/common/stdcells.v | 106 +++++++++++++------------------------
 1 file changed, 38 insertions(+), 68 deletions(-)

diff --git a/techlibs/common/stdcells.v b/techlibs/common/stdcells.v
index 5482d380..4e764078 100644
--- a/techlibs/common/stdcells.v
+++ b/techlibs/common/stdcells.v
@@ -115,7 +115,6 @@ endmodule
 module \$reduce_xor ;
 endmodule
 
-
 // --------------------------------------------------------
 
 (* techmap_simplemap *)
@@ -218,7 +217,7 @@ parameter A_WIDTH = 1;
 parameter B_WIDTH = 1;
 parameter Y_WIDTH = 1;
 
-parameter WIDTH = A_WIDTH > Y_WIDTH ? A_WIDTH : Y_WIDTH;
+localparam WIDTH = A_WIDTH > Y_WIDTH ? A_WIDTH : Y_WIDTH;
 
 input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
@@ -271,7 +270,7 @@ parameter A_WIDTH = 1;
 parameter B_WIDTH = 1;
 parameter Y_WIDTH = 1;
 
-parameter WIDTH = Y_WIDTH;
+localparam WIDTH = Y_WIDTH;
 
 input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
@@ -324,7 +323,7 @@ parameter A_WIDTH = 1;
 parameter B_WIDTH = 1;
 parameter Y_WIDTH = 1;
 
-parameter WIDTH = A_WIDTH > Y_WIDTH ? A_WIDTH : Y_WIDTH;
+localparam WIDTH = A_WIDTH > Y_WIDTH ? A_WIDTH : Y_WIDTH;
 
 input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
@@ -387,11 +386,11 @@ output X, Y;
 // {t1, t2} = A + B
 wire t1, t2, t3;
 
- \$_AND_ gate1 ( .A(A),  .B(B),  .Y(t1) );
- \$_XOR_ gate2 ( .A(A),  .B(B),  .Y(t2) );
- \$_AND_ gate3 ( .A(t2), .B(C),  .Y(t3) ); 
- \$_XOR_ gate4 ( .A(t2), .B(C),  .Y(Y)  );
- \$_OR_  gate5 ( .A(t1), .B(t3), .Y(X)  );
+\$_AND_ gate1 ( .A(A),  .B(B),  .Y(t1) );
+\$_XOR_ gate2 ( .A(A),  .B(B),  .Y(t2) );
+\$_AND_ gate3 ( .A(t2), .B(C),  .Y(t3) ); 
+\$_XOR_ gate4 ( .A(t2), .B(C),  .Y(Y)  );
+\$_OR_  gate5 ( .A(t1), .B(t3), .Y(X)  );
 
 endmodule
 
@@ -438,7 +437,7 @@ parameter A_WIDTH = 1;
 parameter B_WIDTH = 1;
 parameter Y_WIDTH = 1;
 
-parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
 
 input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
@@ -446,8 +445,8 @@ output [Y_WIDTH-1:0] Y;
 
 wire carry, carry_sign;
 wire [WIDTH-1:0] A_buf, B_buf, Y_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 \$__alu #(
 	.WIDTH(WIDTH)
@@ -487,7 +486,7 @@ parameter A_WIDTH = 1;
 parameter B_WIDTH = 1;
 parameter Y_WIDTH = 1;
 
-parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
 
 input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
@@ -495,8 +494,8 @@ output [Y_WIDTH-1:0] Y;
 
 wire carry, carry_sign;
 wire [WIDTH-1:0] A_buf, B_buf, Y_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 \$__alu #(
 	.WIDTH(WIDTH)
@@ -536,7 +535,7 @@ parameter A_WIDTH = 1;
 parameter B_WIDTH = 1;
 parameter Y_WIDTH = 1;
 
-parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
 
 input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
@@ -544,8 +543,8 @@ output [Y_WIDTH-1:0] Y;
 
 wire carry, carry_sign;
 wire [WIDTH-1:0] A_buf, B_buf;
-\$bu0 #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$bu0 #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$bu0 #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$bu0 #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 assign Y = ~|(A_buf ^ B_buf);
 
@@ -561,7 +560,7 @@ parameter A_WIDTH = 1;
 parameter B_WIDTH = 1;
 parameter Y_WIDTH = 1;
 
-parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
 
 input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
@@ -569,8 +568,8 @@ output [Y_WIDTH-1:0] Y;
 
 wire carry, carry_sign;
 wire [WIDTH-1:0] A_buf, B_buf;
-\$bu0 #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$bu0 #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$bu0 #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$bu0 #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 assign Y = |(A_buf ^ B_buf);
 
@@ -586,7 +585,7 @@ parameter A_WIDTH = 1;
 parameter B_WIDTH = 1;
 parameter Y_WIDTH = 1;
 
-parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
 
 input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
@@ -594,8 +593,8 @@ output [Y_WIDTH-1:0] Y;
 
 wire carry, carry_sign;
 wire [WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 assign Y = ~|(A_buf ^ B_buf);
 
@@ -611,7 +610,7 @@ parameter A_WIDTH = 1;
 parameter B_WIDTH = 1;
 parameter Y_WIDTH = 1;
 
-parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
 
 input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
@@ -619,8 +618,8 @@ output [Y_WIDTH-1:0] Y;
 
 wire carry, carry_sign;
 wire [WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 assign Y = |(A_buf ^ B_buf);
 
@@ -697,8 +696,8 @@ input [B_WIDTH-1:0] B;
 output [Y_WIDTH-1:0] Y;
 
 wire [Y_WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 \$__alu #(
 	.WIDTH(Y_WIDTH)
@@ -726,8 +725,8 @@ input [B_WIDTH-1:0] B;
 output [Y_WIDTH-1:0] Y;
 
 wire [Y_WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 \$__alu #(
 	.WIDTH(Y_WIDTH)
@@ -775,8 +774,8 @@ input [B_WIDTH-1:0] B;
 output [Y_WIDTH-1:0] Y;
 
 wire [Y_WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 \$__arraymul #(
 	.WIDTH(Y_WIDTH)
@@ -837,12 +836,12 @@ input [B_WIDTH-1:0] B;
 output [Y_WIDTH-1:0] Y, R;
 
 wire [WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
 
 wire [WIDTH-1:0] A_buf_u, B_buf_u, Y_u, R_u;
-assign A_buf_u = A_SIGNED && B_SIGNED && A_buf[WIDTH-1] ? -A_buf : A_buf;
-assign B_buf_u = A_SIGNED && B_SIGNED && B_buf[WIDTH-1] ? -B_buf : B_buf;
+assign A_buf_u = A_SIGNED && A_buf[WIDTH-1] ? -A_buf : A_buf;
+assign B_buf_u = B_SIGNED && B_buf[WIDTH-1] ? -B_buf : B_buf;
 
 \$__div_mod_u #(
 	.WIDTH(WIDTH)
@@ -872,9 +871,6 @@ input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
 output [Y_WIDTH-1:0] Y;
 
-wire [Y_WIDTH-1:0] Y_buf;
-wire [Y_WIDTH-1:0] Y_div_zero;
-
 \$__div_mod #(
 	.A_SIGNED(A_SIGNED),
 	.B_SIGNED(B_SIGNED),
@@ -884,20 +880,9 @@ wire [Y_WIDTH-1:0] Y_div_zero;
 ) div_mod (
 	.A(A),
 	.B(B),
-	.Y(Y_buf)
+	.Y(Y)
 );
 
-// explicitly force the division-by-zero behavior found in other synthesis tools 
-generate begin
-	if (A_SIGNED && B_SIGNED) begin:make_div_zero
-		assign Y_div_zero = A[A_WIDTH-1] ? {Y_WIDTH{1'b0}} | 1'b1 : {Y_WIDTH{1'b1}};
-	end else begin:make_div_zero
-		assign Y_div_zero = {A_WIDTH{1'b1}};
-	end
-end endgenerate
-
-assign Y = B ? Y_buf : Y_div_zero;
-
 endmodule
 
 // --------------------------------------------------------
@@ -914,9 +899,6 @@ input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
 output [Y_WIDTH-1:0] Y;
 
-wire [Y_WIDTH-1:0] Y_buf;
-wire [Y_WIDTH-1:0] Y_div_zero;
-
 \$__div_mod #(
 	.A_SIGNED(A_SIGNED),
 	.B_SIGNED(B_SIGNED),
@@ -926,21 +908,9 @@ wire [Y_WIDTH-1:0] Y_div_zero;
 ) div_mod (
 	.A(A),
 	.B(B),
-	.R(Y_buf)
+	.R(Y)
 );
 
-// explicitly force the division-by-zero behavior found in other synthesis tools 
-localparam div_zero_copy_a_bits = A_WIDTH < B_WIDTH ? A_WIDTH : B_WIDTH;
-generate begin
-	if (A_SIGNED && B_SIGNED) begin:make_div_zero
-		assign Y_div_zero = $signed(A[div_zero_copy_a_bits-1:0]);
-	end else begin:make_div_zero
-		assign Y_div_zero = $unsigned(A[div_zero_copy_a_bits-1:0]);
-	end
-end endgenerate
-
-assign Y = B ? Y_buf : Y_div_zero;
-
 endmodule
 
 /****

From 4892a3ce6dd6b7432ef1855707d656afd4878fcc Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Dec 2013 21:25:09 +0100
Subject: [PATCH 36/49] Added abc -dff and -clk support

---
 passes/abc/abc.cc       | 177 ++++++++++++++++++++++++++++++++--------
 passes/abc/blifparse.cc |  28 ++++++-
 passes/abc/blifparse.h  |   2 +-
 3 files changed, 173 insertions(+), 34 deletions(-)

diff --git a/passes/abc/abc.cc b/passes/abc/abc.cc
index 1e7c66e1..efba4359 100644
--- a/passes/abc/abc.cc
+++ b/passes/abc/abc.cc
@@ -57,6 +57,9 @@ static RTLIL::Module *module;
 static std::vector<gate_t> signal_list;
 static std::map<RTLIL::SigSpec, int> signal_map;
 
+static bool clk_polarity;
+static RTLIL::SigSpec clk_sig;
+
 static int map_signal(RTLIL::SigSpec sig, char gate_type = -1, int in1 = -1, int in2 = -1, int in3 = -1)
 {
 	assert(sig.width == 1);
@@ -103,6 +106,26 @@ static void mark_port(RTLIL::SigSpec sig)
 
 static void extract_cell(RTLIL::Cell *cell)
 {
+	if (cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")
+	{
+		if (clk_polarity != (cell->type == "$_DFF_P_"))
+			return;
+		if (clk_sig != assign_map(cell->connections["\\C"]))
+			return;
+
+		RTLIL::SigSpec sig_d = cell->connections["\\D"];
+		RTLIL::SigSpec sig_q = cell->connections["\\Q"];
+
+		assign_map.apply(sig_d);
+		assign_map.apply(sig_q);
+
+		map_signal(sig_q, 'f', map_signal(sig_d));
+
+		module->cells.erase(cell->name);
+		delete cell;
+		return;
+	}
+
 	if (cell->type == "$_INV_")
 	{
 		RTLIL::SigSpec sig_a = cell->connections["\\A"];
@@ -138,7 +161,7 @@ static void extract_cell(RTLIL::Cell *cell)
 		else if (cell->type == "$_XOR_")
 			map_signal(sig_y, 'x', mapped_a, mapped_b);
 		else
-			abort();
+			log_abort();
 
 		module->cells.erase(cell->name);
 		delete cell;
@@ -220,20 +243,21 @@ static void handle_loops()
 	// dot_f = fopen("test.dot", "w");
 
 	for (auto &g : signal_list) {
-		if (g.type == -1) {
+		if (g.type == -1 || g.type == 'f') {
 			workpool.insert(g.id);
-		}
-		if (g.in1 >= 0) {
-			edges[g.in1].insert(g.id);
-			in_edges_count[g.id]++;
-		}
-		if (g.in2 >= 0 && g.in2 != g.in1) {
-			edges[g.in2].insert(g.id);
-			in_edges_count[g.id]++;
-		}
-		if (g.in3 >= 0 && g.in3 != g.in2 && g.in3 != g.in1) {
-			edges[g.in3].insert(g.id);
-			in_edges_count[g.id]++;
+		} else {
+			if (g.in1 >= 0) {
+				edges[g.in1].insert(g.id);
+				in_edges_count[g.id]++;
+			}
+			if (g.in2 >= 0 && g.in2 != g.in1) {
+				edges[g.in2].insert(g.id);
+				in_edges_count[g.id]++;
+			}
+			if (g.in3 >= 0 && g.in3 != g.in2 && g.in3 != g.in1) {
+				edges[g.in3].insert(g.id);
+				in_edges_count[g.id]++;
+			}
 		}
 	}
 
@@ -330,7 +354,8 @@ static void handle_loops()
 		fclose(dot_f);
 }
 
-static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file, std::string liberty_file, std::string constr_file, bool cleanup, int lut_mode)
+static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file,
+		std::string liberty_file, std::string constr_file, bool cleanup, int lut_mode, bool dff_mode, std::string clk_str)
 {
 	module = current_module;
 	map_autoidx = RTLIL::autoidx++;
@@ -339,6 +364,9 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 	signal_list.clear();
 	assign_map.set(module);
 
+	clk_polarity = true;
+	clk_sig = RTLIL::SigSpec();
+
 	char tempdir_name[] = "/tmp/yosys-abc-XXXXXX";
 	if (!cleanup)
 		tempdir_name[0] = tempdir_name[4] = '_';
@@ -347,6 +375,45 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 	if (p == NULL)
 		log_error("For some reason mkdtemp() failed!\n");
 
+	if (clk_str.empty()) {
+		if (clk_str[0] == '!') {
+			clk_polarity = false;
+			clk_str = clk_str.substr(1);
+		}
+		if (module->wires.count(RTLIL::escape_id(clk_str)) != 0)
+			clk_sig = assign_map(RTLIL::SigSpec(module->wires.at(RTLIL::escape_id(clk_str)), 1));
+	}
+
+	if (dff_mode && clk_sig.width == 0)
+	{
+		int best_dff_counter = 0;
+		std::map<std::pair<bool, RTLIL::SigSpec>, int> dff_counters;
+
+		for (auto &it : module->cells)
+		{
+			RTLIL::Cell *cell = it.second;
+			if (cell->type != "$_DFF_N_" && cell->type != "$_DFF_P_")
+				continue;
+
+			std::pair<bool, RTLIL::SigSpec> key(cell->type == "$_DFF_P_", assign_map(cell->connections.at("\\C")));
+			if (++dff_counters[key] > best_dff_counter) {
+				best_dff_counter = dff_counters[key];
+				clk_polarity = key.first;
+				clk_sig = key.second;
+			}
+		}
+	}
+
+	if (dff_mode || !clk_str.empty()) {
+		if (clk_sig.width == 0)
+			log("No (matching) clock domain found. Not extracting any FF cells.\n");
+		else
+			log("Found (matching) %s clock domain: %s\n", clk_polarity ? "posedge" : "negedge", log_signal(clk_sig));
+	}
+
+	if (clk_sig.width != 0)
+		mark_port(clk_sig);
+
 	std::vector<RTLIL::Cell*> cells;
 	cells.reserve(module->cells.size());
 	for (auto &it : module->cells)
@@ -366,7 +433,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 	
 	handle_loops();
 
-	if (asprintf(&p, "%s/input.blif", tempdir_name) < 0) abort();
+	if (asprintf(&p, "%s/input.blif", tempdir_name) < 0) log_abort();
 	FILE *f = fopen(p, "wt");
 	if (f == NULL)
 		log_error("Opening %s for writing failed: %s\n", p, strerror(errno));
@@ -426,8 +493,10 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 			fprintf(f, ".names n%d n%d n%d n%d\n", si.in1, si.in2, si.in3, si.id);
 			fprintf(f, "1-0 1\n");
 			fprintf(f, "-11 1\n");
+		} else if (si.type == 'f') {
+			fprintf(f, ".latch n%d n%d\n", si.in1, si.id);
 		} else if (si.type >= 0)
-			abort();
+			log_abort();
 		if (si.type >= 0)
 			count_gates++;
 	}
@@ -443,7 +512,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 	{
 		log_header("Executing ABC.\n");
 
-		if (asprintf(&p, "%s/stdcells.genlib", tempdir_name) < 0) abort();
+		if (asprintf(&p, "%s/stdcells.genlib", tempdir_name) < 0) log_abort();
 		f = fopen(p, "wt");
 		if (f == NULL)
 			log_error("Opening %s for writing failed: %s\n", p, strerror(errno));
@@ -459,7 +528,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 		free(p);
 
 		if (lut_mode) {
-			if (asprintf(&p, "%s/lutdefs.txt", tempdir_name) < 0) abort();
+			if (asprintf(&p, "%s/lutdefs.txt", tempdir_name) < 0) log_abort();
 			f = fopen(p, "wt");
 			if (f == NULL)
 				log_error("Opening %s for writing failed: %s\n", p, strerror(errno));
@@ -522,7 +591,8 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 		if (f == NULL)
 			log_error("Can't open ABC output file `%s'.\n", p);
 
-		RTLIL::Design *mapped_design = abc_parse_blif(f);
+		bool builtin_lib = liberty_file.empty() && script_file.empty() && !lut_mode;
+		RTLIL::Design *mapped_design = abc_parse_blif(f, builtin_lib ? "\\DFF" : "\\_dff_");
 
 		fclose(f);
 		free(p);
@@ -540,11 +610,11 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 		}
 
 		std::map<std::string, int> cell_stats;
-		if (liberty_file.empty() && script_file.empty() && !lut_mode)
+		if (builtin_lib)
 		{
 			for (auto &it : mapped_mod->cells) {
 				RTLIL::Cell *c = it.second;
-				cell_stats[c->type.substr(1)]++;
+				cell_stats[RTLIL::unescape_id(c->type)]++;
 				if (c->type == "\\ZERO" || c->type == "\\ONE") {
 					RTLIL::SigSig conn;
 					conn.first = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Y"].chunks[0].wire->name)]);
@@ -592,21 +662,46 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 					design->select(module, cell);
 					continue;
 				}
-				assert(0);
+				if (c->type == "\\DFF") {
+					log_assert(clk_sig.width == 1);
+					RTLIL::Cell *cell = new RTLIL::Cell;
+					cell->type = clk_polarity ? "$_DFF_P_" : "$_DFF_N_";
+					cell->name = remap_name(c->name);
+					cell->connections["\\D"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\D"].chunks[0].wire->name)]);
+					cell->connections["\\Q"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Q"].chunks[0].wire->name)]);
+					cell->connections["\\C"] = clk_sig;
+					module->cells[cell->name] = cell;
+					design->select(module, cell);
+					continue;
+				}
+				log_abort();
 			}
 		}
 		else
 		{
-			for (auto &it : mapped_mod->cells) {
+			for (auto &it : mapped_mod->cells)
+			{
 				RTLIL::Cell *c = it.second;
-				cell_stats[c->type.substr(1)]++;
-				if (c->type == "$_const0_" || c->type == "$_const1_") {
+				cell_stats[RTLIL::unescape_id(c->type)]++;
+				if (c->type == "\\_const0_" || c->type == "\\_const1_") {
 					RTLIL::SigSig conn;
-					conn.first = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Y"].chunks[0].wire->name)]);
-					conn.second = RTLIL::SigSpec(c->type == "$_const0_" ? 0 : 1, 1);
+					conn.first = RTLIL::SigSpec(module->wires[remap_name(c->connections.begin()->second.chunks[0].wire->name)]);
+					conn.second = RTLIL::SigSpec(c->type == "\\_const0_" ? 0 : 1, 1);
 					module->connections.push_back(conn);
 					continue;
 				}
+				if (c->type == "\\_dff_") {
+					log_assert(clk_sig.width == 1);
+					RTLIL::Cell *cell = new RTLIL::Cell;
+					cell->type = clk_polarity ? "$_DFF_P_" : "$_DFF_N_";
+					cell->name = remap_name(c->name);
+					cell->connections["\\D"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\D"].chunks[0].wire->name)]);
+					cell->connections["\\Q"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Q"].chunks[0].wire->name)]);
+					cell->connections["\\C"] = clk_sig;
+					module->cells[cell->name] = cell;
+					design->select(module, cell);
+					continue;
+				}
 				RTLIL::Cell *cell = new RTLIL::Cell;
 				cell->type = c->type;
 				cell->parameters = c->parameters;
@@ -673,7 +768,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
 		assert(n >= 0);
 		for (int i = 0; i < n; i++) {
 			if (strcmp(namelist[i]->d_name, ".") && strcmp(namelist[i]->d_name, "..")) {
-				if (asprintf(&p, "%s/%s", tempdir_name, namelist[i]->d_name) < 0) abort();
+				if (asprintf(&p, "%s/%s", tempdir_name, namelist[i]->d_name) < 0) log_abort();
 				log("Removing `%s'.\n", p);
 				remove(p);
 				free(p);
@@ -718,6 +813,16 @@ struct AbcPass : public Pass {
 		log("    -lut <width>\n");
 		log("        generate netlist using luts of (max) the specified width.\n");
 		log("\n");
+		log("    -dff\n");
+		log("        also pass $_DFF_?_ cells through ABC (only one clock domain, if many\n");
+		log("        clock domains are present in a module, the one with the largest number\n");
+		log("        of $dff cells in it is used)\n");
+		log("\n");
+		log("    -clk [!]<signal-name>\n");
+		log("        use the specified clock domain. (when this option is used in combination\n");
+		log("        with -dff, then it falls back to the automatic dection of clock domain\n");
+		log("        if the specified clock is not found in a module.)\n");
+		log("\n");
 		log("    -nocleanup\n");
 		log("        when this option is used, the temporary files created by this pass\n");
 		log("        are not removed. this is useful for debugging.\n");
@@ -734,8 +839,8 @@ struct AbcPass : public Pass {
 		log_push();
 
 		std::string exe_file = rewrite_yosys_exe("yosys-abc");
-		std::string script_file, liberty_file, constr_file;
-		bool cleanup = true;
+		std::string script_file, liberty_file, constr_file, clk_str;
+		bool dff_mode = false, cleanup = true;
 		int lut_mode = 0;
 
 		size_t argidx;
@@ -768,6 +873,14 @@ struct AbcPass : public Pass {
 				lut_mode = atoi(args[++argidx].c_str());
 				continue;
 			}
+			if (arg == "-dff") {
+				dff_mode = true;
+				continue;
+			}
+			if (arg == "-clk" && argidx+1 < args.size() && lut_mode == 0) {
+				clk_str = args[++argidx];
+				continue;
+			}
 			if (arg == "-nocleanup") {
 				cleanup = false;
 				continue;
@@ -782,7 +895,7 @@ struct AbcPass : public Pass {
 				if (mod_it.second->processes.size() > 0)
 					log("Skipping module %s as it contains processes.\n", mod_it.second->name.c_str());
 				else
-					abc_module(design, mod_it.second, script_file, exe_file, liberty_file, constr_file, cleanup, lut_mode);
+					abc_module(design, mod_it.second, script_file, exe_file, liberty_file, constr_file, cleanup, lut_mode, dff_mode, clk_str);
 			}
 
 		assign_map.clear();
diff --git a/passes/abc/blifparse.cc b/passes/abc/blifparse.cc
index 825d5eab..a630405c 100644
--- a/passes/abc/blifparse.cc
+++ b/passes/abc/blifparse.cc
@@ -44,7 +44,7 @@ static bool read_next_line(char *buffer, int &line_count, FILE *f)
 	}
 }
 
-RTLIL::Design *abc_parse_blif(FILE *f)
+RTLIL::Design *abc_parse_blif(FILE *f, std::string dff_name)
 {
 	RTLIL::Design *design = new RTLIL::Design;
 	RTLIL::Module *module = new RTLIL::Module;
@@ -101,6 +101,32 @@ RTLIL::Design *abc_parse_blif(FILE *f)
 				continue;
 			}
 
+			if (!strcmp(cmd, ".latch"))
+			{
+				char *d = strtok(NULL, " \t\r\n");
+				char *q = strtok(NULL, " \t\r\n");
+
+				if (module->wires.count(RTLIL::escape_id(d)) == 0) {
+					RTLIL::Wire *wire = new RTLIL::Wire;
+					wire->name = RTLIL::escape_id(d);
+					module->add(wire);
+				}
+
+				if (module->wires.count(RTLIL::escape_id(q)) == 0) {
+					RTLIL::Wire *wire = new RTLIL::Wire;
+					wire->name = RTLIL::escape_id(q);
+					module->add(wire);
+				}
+
+				RTLIL::Cell *cell = new RTLIL::Cell;
+				cell->name = NEW_ID;
+				cell->type = dff_name;
+				cell->connections["\\D"] = module->wires.at(RTLIL::escape_id(d));
+				cell->connections["\\Q"] = module->wires.at(RTLIL::escape_id(q));
+				module->add(cell);
+				continue;
+			}
+
 			if (!strcmp(cmd, ".gate"))
 			{
 				RTLIL::Cell *cell = new RTLIL::Cell;
diff --git a/passes/abc/blifparse.h b/passes/abc/blifparse.h
index 98afedac..272e4e64 100644
--- a/passes/abc/blifparse.h
+++ b/passes/abc/blifparse.h
@@ -22,7 +22,7 @@
 
 #include "kernel/rtlil.h"
 
-extern RTLIL::Design *abc_parse_blif(FILE *f);
+extern RTLIL::Design *abc_parse_blif(FILE *f, std::string dff_name);
 
 #endif
 

From ab3f6266ad732e0fc3e02e2addc0c5486293702a Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Dec 2013 21:25:34 +0100
Subject: [PATCH 37/49] Use "abc -dff" in "make test"

---
 tests/tools/autotest.sh | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index e5376809..fcc21237 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -148,9 +148,8 @@ do
 		if [ -n "$scriptfiles" ]; then
 			test_passes
 		else
-			test_passes -p "hierarchy; proc; memory; opt; fsm; opt"
-			test_passes -p "hierarchy; proc; memory; opt; fsm; opt; techmap; opt"
-			# test_passes -p "hierarchy; proc; memory; opt; fsm; opt; techmap; opt; abc; opt"
+			test_passes -p "hierarchy; proc; opt; memory; opt; fsm; opt"
+			test_passes -p "hierarchy; proc; opt; memory; opt; fsm; opt; techmap; opt; abc -dff; opt"
 		fi
 		touch ../${bn}.log
 	}

From e09ebf475c0056ab37a58d6242e79c230e88b1c4 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Dec 2013 21:58:35 +0100
Subject: [PATCH 38/49] Fixed use of limited length buffer in ABC blif parser

---
 passes/abc/blifparse.cc | 23 ++++++++++++++++-------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/passes/abc/blifparse.cc b/passes/abc/blifparse.cc
index a630405c..2d46d1a8 100644
--- a/passes/abc/blifparse.cc
+++ b/passes/abc/blifparse.cc
@@ -22,22 +22,28 @@
 #include <stdio.h>
 #include <string.h>
 
-static bool read_next_line(char *buffer, int &line_count, FILE *f)
+static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count, FILE *f)
 {
+	int buffer_len = 0;
 	buffer[0] = 0;
 
 	while (1)
 	{
-		int buffer_len = strlen(buffer);
+		buffer_len += strlen(buffer + buffer_len);
 		while (buffer_len > 0 && (buffer[buffer_len-1] == ' ' || buffer[buffer_len-1] == '\t' ||
 				buffer[buffer_len-1] == '\r' || buffer[buffer_len-1] == '\n'))
 			buffer[--buffer_len] = 0;
 
+		if (buffer_size-buffer_len < 4096) {
+			buffer_size *= 2;
+			buffer = (char*)realloc(buffer, buffer_size);
+		}
+
 		if (buffer_len == 0 || buffer[buffer_len-1] == '\\') {
 			if (buffer[buffer_len-1] == '\\')
 				buffer[--buffer_len] = 0;
 			line_count++;
-			if (fgets(buffer+buffer_len, 4096-buffer_len, f) == NULL)
+			if (fgets(buffer+buffer_len, buffer_size-buffer_len, f) == NULL)
 				return false;
 		} else
 			return true;
@@ -56,12 +62,13 @@ RTLIL::Design *abc_parse_blif(FILE *f, std::string dff_name)
 	module->name = "\\netlist";
 	design->modules[module->name] = module;
 
-	char buffer[4096];
+	size_t buffer_size = 4096;
+	char *buffer = (char*)malloc(buffer_size);
 	int line_count = 0;
 
 	while (1)
 	{
-		if (!read_next_line(buffer, line_count, f))
+		if (!read_next_line(buffer, buffer_size, line_count, f))
 			goto error;
 
 	continue_without_read:
@@ -83,8 +90,10 @@ RTLIL::Design *abc_parse_blif(FILE *f, std::string dff_name)
 			if (!strcmp(cmd, ".model"))
 				continue;
 
-			if (!strcmp(cmd, ".end"))
+			if (!strcmp(cmd, ".end")) {
+				free(buffer);
 				return design;
+			}
 
 			if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs")) {
 				char *p;
@@ -174,7 +183,7 @@ RTLIL::Design *abc_parse_blif(FILE *f, std::string dff_name)
 				if (input_sig.width == 0) {
 					RTLIL::State state = RTLIL::State::Sa;
 					while (1) {
-						if (!read_next_line(buffer, line_count, f))
+						if (!read_next_line(buffer, buffer_size, line_count, f))
 							goto error;
 						for (int i = 0; buffer[i]; i++) {
 							if (buffer[i] == ' ' || buffer[i] == '\t')

From e501b8e5c79328095b694ee3f4432f3024ffa598 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 1 Jan 2014 18:55:21 +0100
Subject: [PATCH 39/49] Updated CHANGELOG

---
 CHANGELOG | 38 ++++++++++++++++++++++++++++++++++++--
 1 file changed, 36 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG b/CHANGELOG
index fe0534c0..fa2c9b08 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -6,6 +6,40 @@ List of incompatible changes and major milestones between releases
 Yosys 0.1.0 .. Yoys 0.1.0+
 --------------------------
 
- - Tighter integration of ABC build with Yosys build. The make
-   targets 'make abc' and 'make install-abc' are now obsolete.
+ * Improvements in Verilog frontend:
+     - Added support for local registers in named blocks
+     - Added support for "case" in "generate" blocks
+     - Added support for $clog2 system function
+     - Added preprocessor support for macro arguments
+     - Added preprocessor support for `elsif statement
+
+ * Improvements in technology mapping:
+     - The "dfflibmap" command now strongly prefers solutions with
+           no inverters in clock paths
+     - The "dfflibmap" command now prefers cells with smaller area
+
+ * Integration with ABC:
+     - Updated ABC to hg rev 57517e81666b
+     - Tighter integration of ABC build with Yosys build. The make
+           targets 'make abc' and 'make install-abc' are now obsolete.
+     - Added support for passing FFs from one clock domain through ABC
+     - Now always use BLIF as exchange format with ABC
+
+ * Improvements to "eval" and "sat" framework:
+     - Added support for "0" and "~0" in right-hand side -set expressions
+     - Added "eval -set-undef" and "eval -table"
+     - Added "sat -set-init" support for sequential problems
+     - Added undef support to SAT solver, incl. various new "sat" options
+     - Added correct support for === and !== for "eval" and "sat"
+
+ * Added "abbreviated IDs":
+     - Now $<something>$foo can be abbriviated as $foo.
+     - Usually this last part is a unique id (from RTLIL::autoidx)
+     - This abbreviated IDs are now also used in "show" output
+
+ * Various other changes to commands and options:
+     - The "ls" command now supports wildcards
+     - Added "show -pause" and "show -format dot"
+     - Added "dump -m" and "dump -n"
+     - Added "history" command
 

From 249ef8695a77c266434c1716707cf15c061290ab Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 2 Jan 2014 16:52:33 +0100
Subject: [PATCH 40/49] Major rewrite of "freduce" command

---
 kernel/satgen.h       |   8 +-
 passes/sat/eval.cc    |   2 +-
 passes/sat/freduce.cc | 682 +++++++++++++++++++++++-------------------
 passes/sat/sat.cc     |   2 +-
 4 files changed, 373 insertions(+), 321 deletions(-)

diff --git a/kernel/satgen.h b/kernel/satgen.h
index b04bd619..510240f5 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -35,21 +35,19 @@ typedef ezSAT ezDefaultSAT;
 struct SatGen
 {
 	ezSAT *ez;
-	RTLIL::Design *design;
 	SigMap *sigmap;
 	std::string prefix;
 	SigPool initial_state;
 	bool ignore_div_by_zero;
 	bool model_undef;
 
-	SatGen(ezSAT *ez, RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) :
-			ez(ez), design(design), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
+	SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) :
+			ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
 	{
 	}
 
-	void setContext(RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string())
+	void setContext(SigMap *sigmap, std::string prefix = std::string())
 	{
-		this->design = design;
 		this->sigmap = sigmap;
 		this->prefix = prefix;
 	}
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index 5d0d35b6..5d36b474 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -148,7 +148,7 @@ struct VlogHammerReporter
 
 		ezDefaultSAT ez;
 		SigMap sigmap(module);
-		SatGen satgen(&ez, design, &sigmap);
+		SatGen satgen(&ez, &sigmap);
 		satgen.model_undef = model_undef;
 
 		for (auto &c : module->cells)
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index d57fdd32..04d9e20d 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -28,337 +28,386 @@
 #include <string.h>
 #include <algorithm>
 
-#define NUM_INITIAL_RANDOM_TEST_VECTORS 10
-
 namespace {
 
+bool noinv_mode;
+int verbose_level;
+typedef std::map<RTLIL::SigBit, std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>>> drivers_t;
+
+struct equiv_bit_t
+{
+	int depth;
+	bool inverted;
+	RTLIL::SigBit bit;
+
+	bool operator<(const equiv_bit_t &other) const {
+		if (depth != other.depth)
+			return depth < other.depth;
+		if (inverted != other.inverted)
+			return inverted < other.inverted;
+		return bit < other.bit;
+	}
+};
+
+struct FindReducedInputs
+{
+	SigMap &sigmap;
+	drivers_t &drivers;
+
+	ezDefaultSAT ez;
+	std::set<RTLIL::Cell*> ez_cells;
+	SatGen satgen;
+
+	FindReducedInputs(SigMap &sigmap, drivers_t &drivers) :
+			sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap)
+	{
+		satgen.model_undef = true;
+	}
+
+	void register_cone_worker(std::set<RTLIL::SigBit> &pi, std::set<RTLIL::SigBit> &sigdone, RTLIL::SigBit out)
+	{
+		if (out.wire == NULL)
+			return;
+		if (sigdone.count(out) != 0)
+			return;
+		sigdone.insert(out);
+
+		if (drivers.count(out) != 0) {
+			std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
+			if (ez_cells.count(drv.first) == 0) {
+				satgen.setContext(&sigmap, "A");
+				if (!satgen.importCell(drv.first))
+					log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
+				satgen.setContext(&sigmap, "B");
+				if (!satgen.importCell(drv.first))
+					log_abort();
+				ez_cells.insert(drv.first);
+			}
+			for (auto &bit : drv.second)
+				register_cone_worker(pi, sigdone, bit);
+		} else
+			pi.insert(out);
+	}
+
+	void register_cone(std::vector<RTLIL::SigBit> &pi, RTLIL::SigBit out)
+	{
+		std::set<RTLIL::SigBit> pi_set, sigdone;
+		register_cone_worker(pi_set, sigdone, out);
+		pi.clear();
+		pi.insert(pi.end(), pi_set.begin(), pi_set.end());
+	}
+
+	void analyze(std::vector<RTLIL::SigBit> &reduced_inputs, RTLIL::SigBit output)
+	{
+		if (verbose_level >= 1)
+			log("    Analyzing input cone for signal %s:\n", log_signal(output));
+
+		std::vector<RTLIL::SigBit> pi;
+		register_cone(pi, output);
+
+		if (verbose_level >= 1)
+			log("      Found %d input signals and %d cells.\n", int(pi.size()), int(ez_cells.size()));
+
+		satgen.setContext(&sigmap, "A");
+		int output_a = satgen.importSigSpec(output).front();
+		int output_undef_a = satgen.importUndefSigSpec(output).front();
+		ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi))));
+
+		satgen.setContext(&sigmap, "B");
+		int output_b = satgen.importSigSpec(output).front();
+		int output_undef_b = satgen.importUndefSigSpec(output).front();
+		ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi))));
+
+		for (size_t i = 0; i < pi.size(); i++)
+		{
+			RTLIL::SigSpec test_sig(pi[i]);
+			RTLIL::SigSpec rest_sig(pi);
+			rest_sig.remove(i, 1);
+
+			int test_sig_a, test_sig_b;
+			std::vector<int> rest_sig_a, rest_sig_b;
+
+			satgen.setContext(&sigmap, "A");
+			test_sig_a = satgen.importSigSpec(test_sig).front();
+			rest_sig_a = satgen.importSigSpec(rest_sig);
+
+			satgen.setContext(&sigmap, "B");
+			test_sig_b = satgen.importSigSpec(test_sig).front();
+			rest_sig_b = satgen.importSigSpec(rest_sig);
+
+			if (ez.solve(ez.vec_eq(rest_sig_a, rest_sig_b), ez.XOR(output_a, output_b), ez.XOR(test_sig_a, test_sig_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b))) {
+				if (verbose_level >= 2)
+					log("      Result for input %s: pass\n", log_signal(test_sig));
+				reduced_inputs.push_back(pi[i]);
+			} else {
+				if (verbose_level >= 2)
+					log("      Result for input %s: strip\n", log_signal(test_sig));
+			}
+		}
+
+		if (verbose_level >= 1)
+			log("      Reduced input cone contains %d inputs.\n", int(reduced_inputs.size()));
+	}
+};
+
+struct PerformReduction
+{
+	SigMap &sigmap;
+	drivers_t &drivers;
+
+	ezDefaultSAT ez;
+	SatGen satgen;
+
+	std::vector<int> sat_pi, sat_out, sat_def;
+	std::vector<RTLIL::SigBit> out_bits, pi_bits;
+	std::vector<bool> out_inverted;
+	std::vector<int> out_depth;
+
+	int register_cone_worker(std::set<RTLIL::Cell*> &celldone, std::map<RTLIL::SigBit, int> &sigdepth, RTLIL::SigBit out)
+	{
+		if (out.wire == NULL)
+			return 0;
+		if (sigdepth.count(out) != 0)
+			return sigdepth.at(out);
+		sigdepth[out] = 0;
+
+		if (drivers.count(out) != 0) {
+			std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
+			if (celldone.count(drv.first) == 0) {
+				if (!satgen.importCell(drv.first))
+					log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
+				celldone.insert(drv.first);
+			}
+			int max_child_dept = 0;
+			for (auto &bit : drv.second)
+				max_child_dept = std::max(register_cone_worker(celldone, sigdepth, bit), max_child_dept);
+			sigdepth[out] = max_child_dept + 1;
+		} else {
+			pi_bits.push_back(out);
+			sat_pi.push_back(satgen.importSigSpec(out).front());
+			ez.assume(ez.NOT(satgen.importUndefSigSpec(out).front()));
+		}
+
+		return sigdepth[out];
+	}
+
+	PerformReduction(SigMap &sigmap, drivers_t &drivers, std::vector<RTLIL::SigBit> &bits) :
+			sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap), out_bits(bits)
+	{
+		satgen.model_undef = true;
+
+		std::set<RTLIL::Cell*> celldone;
+		std::map<RTLIL::SigBit, int> sigdepth;
+
+		for (auto &bit : bits) {
+			out_depth.push_back(register_cone_worker(celldone, sigdepth, bit));
+			sat_out.push_back(satgen.importSigSpec(bit).front());
+			sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front()));
+		}
+
+		if (noinv_mode) {
+			out_inverted = std::vector<bool>(sat_out.size(), false);
+		} else {
+			if (!ez.solve(sat_out, out_inverted, ez.expression(ezSAT::OpAnd, sat_def)))
+				log_error("Solving for initial model failed!\n");
+			for (size_t i = 0; i < sat_out.size(); i++)
+				if (out_inverted.at(i))
+					sat_out[i] = ez.NOT(sat_out[i]);
+		}
+	}
+
+	void analyze(std::vector<std::vector<equiv_bit_t>> &results, std::vector<int> &bucket, int level)
+	{
+		if (bucket.size() <= 1)
+			return;
+
+		if (verbose_level >= 1)
+			log("%*s  Trying to shatter bucket with %d signals.\n", 2*level, "", int(bucket.size()));
+
+		std::vector<int> sat_list, sat_inv_list;
+		for (int idx : bucket) {
+			sat_list.push_back(ez.AND(sat_out[idx], sat_def[idx]));
+			sat_inv_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
+		}
+
+		std::vector<int> modelVars = sat_out;
+		std::vector<bool> model;
+
+		if (verbose_level >= 2) {
+			modelVars.insert(modelVars.end(), sat_def.begin(), sat_def.end());
+			modelVars.insert(modelVars.end(), sat_pi.begin(), sat_pi.end());
+		}
+
+		if (ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_list), ez.expression(ezSAT::OpOr, sat_inv_list)))
+		{
+			if (verbose_level >= 2) {
+				for (size_t i = 0; i < pi_bits.size(); i++)
+					log("%*s       -> PI  %c == %s\n", 2*level, "", model[2*sat_out.size() + i] ? '1' : '0', log_signal(pi_bits[i]));
+				for (int idx : bucket)
+					log("%*s       -> OUT %c == %s%s\n", 2*level, "", model[sat_out.size() + idx] ? model[idx] ? '1' : '0' : 'x',
+							out_inverted.at(idx) ? "~" : "", log_signal(out_bits[idx]));
+			}
+
+			std::vector<int> buckets[2];
+			for (int idx : bucket)
+				buckets[model[idx] ? 1 : 0].push_back(idx);
+			analyze(results, buckets[0], level+1);
+			analyze(results, buckets[1], level+1);
+		}
+		else
+		{
+			if (verbose_level >= 1) {
+				log("%*s    Found %d equivialent signals:", 2*level, "", int(bucket.size()));
+				for (int idx : bucket)
+					log("%s%s%s", idx == bucket.front() ? " " : ", ", out_inverted[idx] ? "~" : "", log_signal(out_bits[idx]));
+				log("\n");
+			}
+
+			std::vector<equiv_bit_t> result;
+			for (int idx : bucket) {
+				equiv_bit_t bit;
+				bit.depth = out_depth[idx];
+				bit.inverted = out_inverted[idx];
+				bit.bit = out_bits[idx];
+				result.push_back(bit);
+			}
+
+			std::sort(result.begin(), result.end());
+			if (result.front().inverted)
+				for (auto &bit : result)
+					bit.inverted = !bit.inverted;
+
+			results.push_back(result);
+		}
+	}
+
+	void analyze(std::vector<std::vector<equiv_bit_t>> &results)
+	{
+		std::vector<int> bucket;
+		for (size_t i = 0; i < sat_out.size(); i++)
+			bucket.push_back(i);
+		analyze(results, bucket, 1);
+	}
+};
+
 struct FreduceHelper
 {
-	RTLIL::Design *design;
 	RTLIL::Module *module;
-	bool try_mode;
 
-	ezDefaultSAT ez;
 	SigMap sigmap;
-	CellTypes ct;
-	SatGen satgen;
-	ConstEval ce;
+	drivers_t drivers;
 
-	SigPool inputs, nodes;
-	RTLIL::SigSpec input_sigs;
-
-	SigSet<RTLIL::SigSpec> source_signals;
-	std::vector<RTLIL::Const> test_vectors;
-	std::map<RTLIL::SigSpec, RTLIL::Const> node_to_data;
-	std::map<RTLIL::SigSpec, RTLIL::SigSpec> node_result;
-
-	uint32_t xorshift32_state;
-
-        uint32_t xorshift32() {
-		xorshift32_state ^= xorshift32_state << 13;
-		xorshift32_state ^= xorshift32_state >> 17;
-		xorshift32_state ^= xorshift32_state << 5;
-		return xorshift32_state;
+	FreduceHelper(RTLIL::Module *module) : module(module), sigmap(module)
+	{
 	}
 
-	FreduceHelper(RTLIL::Design *design, RTLIL::Module *module, bool try_mode) :
-			design(design), module(module), try_mode(try_mode),
-			sigmap(module), satgen(&ez, design, &sigmap), ce(module)
+	int run()
 	{
+		log("Running functional reduction on module %s:\n", RTLIL::id2cstr(module->name));
+
+		CellTypes ct;
 		ct.setup_internals();
 		ct.setup_stdcells();
 
-		xorshift32_state = 123456789;
-		xorshift32();
-		xorshift32();
-		xorshift32();
-	}
-
-	bool run_test(RTLIL::SigSpec test_vec)
-	{
-		ce.clear();
-		ce.set(input_sigs, test_vec.as_const());
-
-		for (auto &bit : nodes.bits) {
-			RTLIL::SigSpec nodesig(bit.first, 1, bit.second), nodeval = nodesig;
-			if (!ce.eval(nodeval)) {
-				if (!try_mode)
-					log_error("Evaluation of node %s failed!\n", log_signal(nodesig));
-				log("FAILED: Evaluation of node %s failed!\n", log_signal(nodesig));
-				return false;
+		std::vector<std::set<RTLIL::SigBit>> batches;
+		for (auto &it : module->cells)
+			if (ct.cell_known(it.second->type)) {
+				std::set<RTLIL::SigBit> inputs, outputs;
+				for (auto &port : it.second->connections) {
+					std::vector<RTLIL::SigBit> bits = sigmap(port.second).to_sigbit_vector();
+					if (ct.cell_output(it.second->type, port.first))
+						outputs.insert(bits.begin(), bits.end());
+					else
+						inputs.insert(bits.begin(), bits.end());
+				}
+				std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> drv(it.second, inputs);
+				for (auto &bit : outputs)
+					drivers[bit] = drv;
+				batches.push_back(outputs);
 			}
-			node_to_data[nodesig].bits.push_back(nodeval.as_const().bits.at(0));
-		}
 
-		return true;
-	}
-
-	void dump_node_data()
-	{
-		int max_node_len = 20;
-		for (auto &it : node_to_data)
-			max_node_len = std::max(max_node_len, int(strlen(log_signal(it.first))));
-		log("  full node fingerprints:\n");
-		for (auto &it : node_to_data)
-			log("    %-*s %s\n", max_node_len+5, log_signal(it.first), log_signal(it.second));
-	}
-
-	bool check(RTLIL::SigSpec sig1, RTLIL::SigSpec sig2)
-	{
-		log("  performing SAT proof:  %s == %s  ->", log_signal(sig1), log_signal(sig2));
-
-		std::vector<int> vec1 = satgen.importSigSpec(sig1);
-		std::vector<int> vec2 = satgen.importSigSpec(sig2);
-		std::vector<int> model = satgen.importSigSpec(input_sigs);
-		std::vector<bool> testvect;
-
-		if (ez.solve(model, testvect, ez.vec_ne(vec1, vec2))) {
-			RTLIL::SigSpec testvect_sig;
-			for (int i = 0; i < input_sigs.width; i++)
-				testvect_sig.append(testvect.at(i) ? RTLIL::State::S1 : RTLIL::State::S0);
-			testvect_sig.optimize();
-			log(" failed: %s\n", log_signal(testvect_sig));
-			test_vectors.push_back(testvect_sig.as_const());
-			if (!run_test(testvect_sig))
-				return false;
-		} else {
-			log(" success.\n");
-			if (!sig1.is_fully_const())
-				node_result[sig1].append(sig2);
-			if (!sig2.is_fully_const())
-				node_result[sig2].append(sig1);
-		}
-		return true;
-	}
-
-	bool analyze_const()
-	{
-		for (auto &it : node_to_data)
+		int bits_count = 0;
+		std::map<std::vector<RTLIL::SigBit>, std::vector<RTLIL::SigBit>> buckets;
+		for (auto &batch : batches)
 		{
-			if (node_result.count(it.first))
-				continue;
-			if (it.second == RTLIL::Const(RTLIL::State::S0, it.second.bits.size()))
-				if (!check(it.first, RTLIL::SigSpec(RTLIL::State::S0)))
-					return false;
-			if (it.second == RTLIL::Const(RTLIL::State::S1, it.second.bits.size()))
-				if (!check(it.first, RTLIL::SigSpec(RTLIL::State::S1)))
-					return false;
+			RTLIL::SigSpec batch_sig(std::vector<RTLIL::SigBit>(batch.begin(), batch.end()));
+			batch_sig.optimize();
+
+			log("  Finding reduced input cone for signal batch %s%c\n", log_signal(batch_sig), verbose_level ? ':' : '.');
+
+			FindReducedInputs infinder(sigmap, drivers);
+			for (auto &bit : batch) {
+				std::vector<RTLIL::SigBit> inputs;
+				infinder.analyze(inputs, bit);
+				buckets[inputs].push_back(bit);
+				bits_count++;
+			}
 		}
-		return true;
-	}
+		log("  Sorted %d signal bits into %d buckets.\n", bits_count, int(buckets.size()));
 
-	bool analyze_alias()
-	{
-	restart:
-		std::map<RTLIL::Const, RTLIL::SigSpec> reverse_map;
-
-		for (auto &it : node_to_data) {
-			if (node_result.count(it.first) && node_result.at(it.first).is_fully_const())
-				continue;
-			reverse_map[it.second].append(it.first);
-		}
-
-		for (auto &it : reverse_map)
+		std::vector<std::vector<equiv_bit_t>> equiv;
+		for (auto &bucket : buckets)
 		{
-			if (it.second.width <= 1)
+			if (bucket.second.size() == 1)
 				continue;
 
-			it.second.expand();
-			for (int i = 0; i < it.second.width; i++)
-			for (int j = i+1; j < it.second.width; j++) {
-				RTLIL::SigSpec sig1 = it.second.chunks.at(i), sig2 = it.second.chunks.at(j);
-				if (node_result.count(sig1) && node_result.count(sig2))
+			RTLIL::SigSpec bucket_sig(bucket.second);
+			bucket_sig.optimize();
+
+			log("  Trying to shatter bucket %s%c\n", log_signal(bucket_sig), verbose_level ? ':' : '.');
+			PerformReduction worker(sigmap, drivers, bucket.second);
+			worker.analyze(equiv);
+		}
+
+		log("  Rewiring %d equivialent groups:\n", int(equiv.size()));
+		int rewired_sigbits = 0;
+		for (auto &grp : equiv)
+		{
+			log("    Using as master for group: %s\n", log_signal(grp.front().bit));
+
+			RTLIL::SigSpec inv_sig;
+			for (size_t i = 1; i < grp.size(); i++)
+			{
+				RTLIL::Cell *drv = drivers.at(grp[i].bit).first;
+
+				if (grp[i].inverted && drv->type == "$_INV_" && sigmap(drv->connections.at("\\A")) == grp[0].bit) {
+					log("      Skipping inverted slave %s: already in reduced form\n", log_signal(grp[i].bit));
 					continue;
-				if (node_to_data.at(sig1) != node_to_data.at(sig2))
-					goto restart;
-				if (!check(it.second.chunks.at(i), it.second.chunks.at(j)))
-					return false;
-			}
-		}
-		return true;
-	}
+				}
 
-	bool toproot_helper(RTLIL::SigSpec cursor, RTLIL::SigSpec stoplist, RTLIL::SigSpec &donelist, int level)
-	{
-		// log("    %*schecking %s: %s\n", level*2, "", log_signal(cursor), log_signal(stoplist));
+				log("      Connect slave%s: %s\n", grp[i].inverted ? " using inverter" : "", log_signal(grp[i].bit));
 
-		if (stoplist.extract(cursor).width != 0) {
-			// log("    %*s  STOP\n", level*2, "");
-			return false;
-		}
+				RTLIL::Wire *dummy_wire = module->new_wire(1, NEW_ID);
+				for (auto &port : drv->connections) {
+					RTLIL::SigSpec mapped = sigmap(port.second);
+					mapped.replace(grp[i].bit, dummy_wire, &port.second);
+				}
 
-		if (donelist.extract(cursor).width != 0)
-			return true;
+				if (grp[i].inverted)
+				{
+					if (inv_sig.width == 0)
+					{
+						inv_sig = module->new_wire(1, NEW_ID);
 
-		stoplist.append(cursor);
-		std::set<RTLIL::SigSpec> next = source_signals.find(cursor);
-
-		for (auto &it : next)
-			if (!toproot_helper(it, stoplist, donelist, level+1))
-				return false;
-
-		donelist.append(cursor);
-		return true;
-	}
-
-	// KISS topological sort of bits in signal. return one element of sig
-	// without dependencies to the others (or empty if input is not a DAG).
-	RTLIL::SigSpec toproot(RTLIL::SigSpec sig)
-	{
-		sig.expand();
-		// log("  finding topological root in %s:\n", log_signal(sig));
-		for (auto &c : sig.chunks) {
-			RTLIL::SigSpec stoplist = sig, donelist;
-			stoplist.remove(c);
-			// log("    testing %s as root:\n", log_signal(c));
-			if (toproot_helper(c, stoplist, donelist, 0))
-				return c;
-		}
-		return RTLIL::SigSpec();
-	}
-
-	void update_design_for_group(RTLIL::SigSpec root, RTLIL::SigSpec rest)
-	{
-		SigPool unlink;
-		unlink.add(rest);
-
-		for (auto &cell_it : module->cells) {
-			RTLIL::Cell *cell = cell_it.second;
-			if (!ct.cell_known(cell->type))
-				continue;
-			for (auto &conn : cell->connections)
-				if (ct.cell_output(cell->type, conn.first)) {
-					RTLIL::SigSpec sig = sigmap(conn.second);
-					sig.expand();
-					bool did_something = false;
-					for (auto &c : sig.chunks) {
-						if (c.wire == NULL || !unlink.check_any(c))
-							continue;
-						c.wire = new RTLIL::Wire;
-						c.wire->name = NEW_ID;
-						module->add(c.wire);
-						assert(c.width == 1);
-						c.offset = 0;
-						did_something = true;
+						RTLIL::Cell *inv_cell = new RTLIL::Cell;
+						inv_cell->name = NEW_ID;
+						inv_cell->type = "$_INV_";
+						inv_cell->connections["\\A"] = grp[0].bit;
+						inv_cell->connections["\\Y"] = inv_sig;
+						module->add(inv_cell);
 					}
-					if (did_something) {
-						sig.optimize();
-						conn.second = sig;
-					}
-				}
-		}
 
-		rest.expand();
-		for (auto &c : rest.chunks) {
-			if (c.wire != NULL && !root.is_fully_const()) {
-				source_signals.erase(c);
-				source_signals.insert(c, root);
+					module->connections.push_back(RTLIL::SigSig(grp[i].bit, inv_sig));
+				}
+				else
+					module->connections.push_back(RTLIL::SigSig(grp[i].bit, grp[0].bit));
+
+				rewired_sigbits++;
 			}
-			module->connections.push_back(RTLIL::SigSig(c, root));
-		}
-	}
-
-	void analyze_groups()
-	{
-		SigMap to_group_major;
-		for (auto &it : node_result) {
-			it.second.expand();
-			for (auto &c : it.second.chunks)
-				to_group_major.add(it.first, c);
 		}
 
-		std::map<RTLIL::SigSpec, RTLIL::SigSpec> major_to_rest;
-		for (auto &it : node_result)
-			major_to_rest[to_group_major(it.first)].append(it.first);
-
-		for (auto &it : major_to_rest)
-		{
-			RTLIL::SigSig group = it;
-
-			if (!it.first.is_fully_const()) {
-				group.first = toproot(it.second);
-				if (group.first.width == 0) {
-					log("Operating on non-DAG input: failed to find topological root for `%s'.\n", log_signal(it.second));
-					return;
-				}
-				group.second.remove(group.first);
-			}
-
-			group.first.optimize();
-			group.second.sort_and_unify();
-
-			log("  found group: %s -> %s\n", log_signal(group.first), log_signal(group.second));
-			update_design_for_group(group.first, group.second);
-		}
-	}
-
-	void run()
-	{
-		log("\nFunctionally reduce module %s:\n", RTLIL::id2cstr(module->name));
-		
-		// find inputs and nodes (nets driven by internal cells)
-		// add all internal cells to sat solver
-
-		for (auto &cell_it : module->cells) {
-			RTLIL::Cell *cell = cell_it.second;
-			if (!ct.cell_known(cell->type))
-				continue;
-			RTLIL::SigSpec cell_inputs, cell_outputs;
-			for (auto &conn : cell->connections)
-				if (ct.cell_output(cell->type, conn.first)) {
-					nodes.add(sigmap(conn.second));
-					cell_outputs.append(sigmap(conn.second));
-				} else {
-					inputs.add(sigmap(conn.second));
-					cell_inputs.append(sigmap(conn.second));
-				}
-			cell_inputs.sort_and_unify();
-			cell_outputs.sort_and_unify();
-			cell_inputs.expand();
-			for (auto &c : cell_inputs.chunks)
-				if (c.wire != NULL)
-					source_signals.insert(cell_outputs, c);
-			if (!satgen.importCell(cell))
-				log_error("Failed to import cell to SAT solver: %s (%s)\n",
-						RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
-		}
-		inputs.del(nodes);
-		nodes.add(inputs);
-		log("  found %d nodes (%d inputs).\n", int(nodes.size()), int(inputs.size()));
-
-		// initialise input_sigs and add all-zero, all-one and a few random test vectors
-
-		input_sigs = inputs.export_all();
-		test_vectors.push_back(RTLIL::SigSpec(RTLIL::State::S0, input_sigs.width).as_const());
-		test_vectors.push_back(RTLIL::SigSpec(RTLIL::State::S1, input_sigs.width).as_const());
-
-		for (int i = 0; i < NUM_INITIAL_RANDOM_TEST_VECTORS; i++) {
-			RTLIL::SigSpec sig;
-			for (int j = 0; j < input_sigs.width; j++)
-				sig.append(xorshift32() % 2 ? RTLIL::State::S1 : RTLIL::State::S0);
-			sig.optimize();
-			assert(sig.width == input_sigs.width);
-			test_vectors.push_back(sig.as_const());
-		}
-
-		for (auto &test_vec : test_vectors)
-			if (!run_test(test_vec))
-				return;
-
-		// run the analysis and update design
-
-		if (!analyze_const())
-			return;
-
-		if (!analyze_alias())
-			return;
-
-		log("  input vector: %s\n", log_signal(input_sigs));
-		for (auto &test_vec : test_vectors)
-			log("  test vector: %s\n", log_signal(test_vec));
-
-		dump_node_data();
-		analyze_groups();
+		log("  Rewired a total of %d signal bits in module %s.\n", rewired_sigbits, RTLIL::id2cstr(module->name));
+		return rewired_sigbits;
 	}
 };
 
@@ -376,41 +425,46 @@ struct FreducePass : public Pass {
 		log("equivialent, they are merged to one node and one of the redundant drivers is\n");
 		log("removed.\n");
 		log("\n");
-		log("    -try\n");
-		log("        do not issue an error when the analysis fails.\n");
-		log("        (usually beacause of logic loops in the design)\n");
+		log("    -v, -vv\n");
+		log("        enable verbose or very verbose output\n");
+		log("\n");
+		log("    -noinv\n");
+		log("        do not consolidate inverted signals\n");
 		log("\n");
-		// log("    -enable_invert\n");
-		// log("        also detect nodes that are inverse to each other.\n");
-		// log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
-		bool enable_invert = false;
-		bool try_mode = false;
+		verbose_level = 0;
+		noinv_mode = false;
 
 		log_header("Executing FREDUCE pass (perform functional reduction).\n");
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++) {
-			if (args[argidx] == "-enable_invert") {
-				enable_invert = true;
+			if (args[argidx] == "-v") {
+				verbose_level = 1;
 				continue;
 			}
-			if (args[argidx] == "-try") {
-				try_mode = true;
+			if (args[argidx] == "-vv") {
+				verbose_level = 2;
+				continue;
+			}
+			if (args[argidx] == "-noinv") {
+				noinv_mode = true;
 				continue;
 			}
 			break;
 		}
 		extra_args(args, argidx, design);
 
-		for (auto &mod_it : design->modules)
-		{
+		int bitcount = 0;
+		for (auto &mod_it : design->modules) {
 			RTLIL::Module *module = mod_it.second;
 			if (design->selected(module))
-				FreduceHelper(design, module, try_mode).run();
+				bitcount += FreduceHelper(module).run();
 		}
+
+		log("Rewired a total of %d signal bits.\n", bitcount);
 	}
 } FreducePass;
  
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 21202199..fef99dfc 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -61,7 +61,7 @@ struct SatHelper
 	bool gotTimeout;
 
 	SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
-		design(design), module(module), sigmap(module), ct(design), satgen(&ez, design, &sigmap)
+		design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap)
 	{
 		this->enable_undef = enable_undef;
 		satgen.model_undef = enable_undef;

From 6dec0e0b3ef3aa42dec4a505896042fe7a2276c6 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 2 Jan 2014 17:51:30 +0100
Subject: [PATCH 41/49] Added autotest.sh -p option

---
 tests/tools/autotest.sh | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index fcc21237..b1c330d8 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -9,13 +9,14 @@ keeprunning=false
 backend_opts="-noattr -noexpr"
 kompare_xst=false
 scriptfiles=""
+scriptopt=""
 toolsdir="$(cd $(dirname $0); pwd)"
 
 if [ ! -f $toolsdir/cmp_tbdata -o $toolsdir/cmp_tbdata.c -nt $toolsdir/cmp_tbdata ]; then
 	( set -ex;  gcc -Wall -o $toolsdir/cmp_tbdata $toolsdir/cmp_tbdata.c; ) || exit 1
 fi
 
-while getopts iml:wkvrxs: opt; do
+while getopts iml:wkvrxs:p: opt; do
 	case "$opt" in
 		i)
 			use_isim=true ;;
@@ -30,14 +31,16 @@ while getopts iml:wkvrxs: opt; do
 		v)
 			verbose=true ;;
 		r)
-			backend_opts="$backend_opts norename" ;;
+			backend_opts="$backend_opts -norename" ;;
 		x)
 			kompare_xst=true ;;
 		s)
 			[[ "$OPTARG" == /* ]] || OPTARG="$PWD/$OPTARG"
 			scriptfiles="$scriptfiles $OPTARG" ;;
+		p)
+			scriptopt="$OPTARG" ;;
 		*)
-			echo "Usage: $0 [-i] [-w] [-k] [-v] [-r] [-x] [-l libs] [-s script] verilog-files\n" >&2
+			echo "Usage: $0 [-i] [-w] [-k] [-v] [-r] [-x] [-l libs] [-s script] [-p cmdstring] verilog-files\n" >&2
 			exit 1
 	esac
 done
@@ -147,6 +150,8 @@ do
 
 		if [ -n "$scriptfiles" ]; then
 			test_passes
+		elif [ -n "$scriptopt" ]; then
+			test_passes -p "$scriptopt"
 		else
 			test_passes -p "hierarchy; proc; opt; memory; opt; fsm; opt"
 			test_passes -p "hierarchy; proc; opt; memory; opt; fsm; opt; techmap; opt; abc -dff; opt"

From c6b33f81eb458233be15e1f53882b3684449f3b7 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 2 Jan 2014 18:11:01 +0100
Subject: [PATCH 42/49] Some cleanups in freduce -inv mode (and switched from
 -noinv to -inv)

---
 passes/sat/freduce.cc | 55 +++++++++++++++++++++++--------------------
 1 file changed, 29 insertions(+), 26 deletions(-)

diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 04d9e20d..9f822100 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -30,7 +30,7 @@
 
 namespace {
 
-bool noinv_mode;
+bool inv_mode;
 int verbose_level;
 typedef std::map<RTLIL::SigBit, std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>>> drivers_t;
 
@@ -154,6 +154,7 @@ struct PerformReduction
 {
 	SigMap &sigmap;
 	drivers_t &drivers;
+	std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs;
 
 	ezDefaultSAT ez;
 	SatGen satgen;
@@ -191,8 +192,8 @@ struct PerformReduction
 		return sigdepth[out];
 	}
 
-	PerformReduction(SigMap &sigmap, drivers_t &drivers, std::vector<RTLIL::SigBit> &bits) :
-			sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap), out_bits(bits)
+	PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs, std::vector<RTLIL::SigBit> &bits) :
+			sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(&ez, &sigmap), out_bits(bits)
 	{
 		satgen.model_undef = true;
 
@@ -205,15 +206,14 @@ struct PerformReduction
 			sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front()));
 		}
 
-		if (noinv_mode) {
-			out_inverted = std::vector<bool>(sat_out.size(), false);
-		} else {
+		if (inv_mode) {
 			if (!ez.solve(sat_out, out_inverted, ez.expression(ezSAT::OpAnd, sat_def)))
 				log_error("Solving for initial model failed!\n");
 			for (size_t i = 0; i < sat_out.size(); i++)
 				if (out_inverted.at(i))
 					sat_out[i] = ez.NOT(sat_out[i]);
-		}
+		} else
+			out_inverted = std::vector<bool>(sat_out.size(), false);
 	}
 
 	void analyze(std::vector<std::vector<equiv_bit_t>> &results, std::vector<int> &bucket, int level)
@@ -277,7 +277,14 @@ struct PerformReduction
 				for (auto &bit : result)
 					bit.inverted = !bit.inverted;
 
-			results.push_back(result);
+			for (size_t i = 1; i < result.size(); i++) {
+				std::pair<RTLIL::SigBit, RTLIL::SigBit> p(result[0].bit, result[i].bit);
+				if (inv_pairs.count(p) != 0)
+					result.erase(result.begin() + i);
+			}
+
+			if (result.size() > 1)
+				results.push_back(result);
 		}
 	}
 
@@ -296,6 +303,7 @@ struct FreduceHelper
 
 	SigMap sigmap;
 	drivers_t drivers;
+	std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> inv_pairs;
 
 	FreduceHelper(RTLIL::Module *module) : module(module), sigmap(module)
 	{
@@ -310,7 +318,7 @@ struct FreduceHelper
 		ct.setup_stdcells();
 
 		std::vector<std::set<RTLIL::SigBit>> batches;
-		for (auto &it : module->cells)
+		for (auto &it : module->cells) {
 			if (ct.cell_known(it.second->type)) {
 				std::set<RTLIL::SigBit> inputs, outputs;
 				for (auto &port : it.second->connections) {
@@ -325,6 +333,9 @@ struct FreduceHelper
 					drivers[bit] = drv;
 				batches.push_back(outputs);
 			}
+			if (inv_mode && it.second->type == "$_INV_")
+				inv_pairs.insert(std::pair<RTLIL::SigBit, RTLIL::SigBit>(sigmap(it.second->connections.at("\\A")), sigmap(it.second->connections.at("\\Y"))));
+		}
 
 		int bits_count = 0;
 		std::map<std::vector<RTLIL::SigBit>, std::vector<RTLIL::SigBit>> buckets;
@@ -355,7 +366,7 @@ struct FreduceHelper
 			bucket_sig.optimize();
 
 			log("  Trying to shatter bucket %s%c\n", log_signal(bucket_sig), verbose_level ? ':' : '.');
-			PerformReduction worker(sigmap, drivers, bucket.second);
+			PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second);
 			worker.analyze(equiv);
 		}
 
@@ -368,20 +379,12 @@ struct FreduceHelper
 			RTLIL::SigSpec inv_sig;
 			for (size_t i = 1; i < grp.size(); i++)
 			{
-				RTLIL::Cell *drv = drivers.at(grp[i].bit).first;
-
-				if (grp[i].inverted && drv->type == "$_INV_" && sigmap(drv->connections.at("\\A")) == grp[0].bit) {
-					log("      Skipping inverted slave %s: already in reduced form\n", log_signal(grp[i].bit));
-					continue;
-				}
-
 				log("      Connect slave%s: %s\n", grp[i].inverted ? " using inverter" : "", log_signal(grp[i].bit));
 
+				RTLIL::Cell *drv = drivers.at(grp[i].bit).first;
 				RTLIL::Wire *dummy_wire = module->new_wire(1, NEW_ID);
-				for (auto &port : drv->connections) {
-					RTLIL::SigSpec mapped = sigmap(port.second);
-					mapped.replace(grp[i].bit, dummy_wire, &port.second);
-				}
+				for (auto &port : drv->connections)
+					sigmap(port.second).replace(grp[i].bit, dummy_wire, &port.second);
 
 				if (grp[i].inverted)
 				{
@@ -428,14 +431,14 @@ struct FreducePass : public Pass {
 		log("    -v, -vv\n");
 		log("        enable verbose or very verbose output\n");
 		log("\n");
-		log("    -noinv\n");
-		log("        do not consolidate inverted signals\n");
+		log("    -inv\n");
+		log("        enable explicit handling of inverted signals\n");
 		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
 		verbose_level = 0;
-		noinv_mode = false;
+		inv_mode = false;
 
 		log_header("Executing FREDUCE pass (perform functional reduction).\n");
 
@@ -449,8 +452,8 @@ struct FreducePass : public Pass {
 				verbose_level = 2;
 				continue;
 			}
-			if (args[argidx] == "-noinv") {
-				noinv_mode = true;
+			if (args[argidx] == "-inv") {
+				inv_mode = true;
 				continue;
 			}
 			break;

From ced4d7b321f01571e6746d2a3ff21efa270795a1 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 2 Jan 2014 18:44:24 +0100
Subject: [PATCH 43/49] Added support for module->connections to select %ci,
 %co and %x handling

---
 passes/cmds/select.cc | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/passes/cmds/select.cc b/passes/cmds/select.cc
index 137f8618..5712a023 100644
--- a/passes/cmds/select.cc
+++ b/passes/cmds/select.cc
@@ -272,6 +272,21 @@ static int select_op_expand(RTLIL::Design *design, RTLIL::Selection &lhs, std::v
 			if (lhs.selected_member(mod_it.first, it.first) && limits.count(it.first) == 0)
 				selected_wires.insert(it.second);
 
+		for (auto &conn : mod->connections)
+		{
+			std::vector<RTLIL::SigBit> conn_lhs = conn.first.to_sigbit_vector();
+			std::vector<RTLIL::SigBit> conn_rhs = conn.second.to_sigbit_vector();
+
+			for (size_t i = 0; i < conn_lhs.size(); i++) {
+				if (conn_lhs[i].wire == NULL || conn_rhs[i].wire == NULL)
+					continue;
+				if (mode != 'i' && selected_wires.count(conn_rhs[i].wire) && lhs.selected_members[mod->name].count(conn_lhs[i].wire->name) == 0)
+					lhs.selected_members[mod->name].insert(conn_lhs[i].wire->name), sel_objects++, max_objects--;
+				if (mode != 'o' && selected_wires.count(conn_lhs[i].wire) && lhs.selected_members[mod->name].count(conn_rhs[i].wire->name) == 0)
+					lhs.selected_members[mod->name].insert(conn_rhs[i].wire->name), sel_objects++, max_objects--;
+			}
+		}
+
 		for (auto &cell : mod->cells)
 		for (auto &conn : cell.second->connections)
 		{

From 0759c97748dc159bacc4a25fd83b6fddfe618bc6 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 2 Jan 2014 19:37:34 +0100
Subject: [PATCH 44/49] More "freduce" related fixes and improvements

---
 passes/sat/freduce.cc | 86 +++++++++++++++++++++++++++++++++----------
 1 file changed, 67 insertions(+), 19 deletions(-)

diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 9f822100..9974f935 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -38,6 +38,7 @@ struct equiv_bit_t
 {
 	int depth;
 	bool inverted;
+	RTLIL::Cell *drv;
 	RTLIL::SigBit bit;
 
 	bool operator<(const equiv_bit_t &other) const {
@@ -45,6 +46,8 @@ struct equiv_bit_t
 			return depth < other.depth;
 		if (inverted != other.inverted)
 			return inverted < other.inverted;
+		if (drv != other.drv)
+			return drv < other.drv;
 		return bit < other.bit;
 	}
 };
@@ -216,7 +219,7 @@ struct PerformReduction
 			out_inverted = std::vector<bool>(sat_out.size(), false);
 	}
 
-	void analyze(std::vector<std::vector<equiv_bit_t>> &results, std::vector<int> &bucket, int level)
+	void analyze(std::vector<std::set<int>> &results, std::map<int, int> &results_map, std::vector<int> &bucket, int level)
 	{
 		if (bucket.size() <= 1)
 			return;
@@ -233,10 +236,9 @@ struct PerformReduction
 		std::vector<int> modelVars = sat_out;
 		std::vector<bool> model;
 
-		if (verbose_level >= 2) {
-			modelVars.insert(modelVars.end(), sat_def.begin(), sat_def.end());
+		modelVars.insert(modelVars.end(), sat_def.begin(), sat_def.end());
+		if (verbose_level >= 2)
 			modelVars.insert(modelVars.end(), sat_pi.begin(), sat_pi.end());
-		}
 
 		if (ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_list), ez.expression(ezSAT::OpOr, sat_inv_list)))
 		{
@@ -248,11 +250,17 @@ struct PerformReduction
 							out_inverted.at(idx) ? "~" : "", log_signal(out_bits[idx]));
 			}
 
-			std::vector<int> buckets[2];
-			for (int idx : bucket)
-				buckets[model[idx] ? 1 : 0].push_back(idx);
-			analyze(results, buckets[0], level+1);
-			analyze(results, buckets[1], level+1);
+			std::vector<int> buckets_a;
+			std::vector<int> buckets_b;
+
+			for (int idx : bucket) {
+				if (!model[sat_out.size() + idx] || model[idx])
+					buckets_a.push_back(idx);
+				if (!model[sat_out.size() + idx] || !model[idx])
+					buckets_b.push_back(idx);
+			}
+			analyze(results, results_map, buckets_a, level+1);
+			analyze(results, results_map, buckets_b, level+1);
 		}
 		else
 		{
@@ -263,16 +271,58 @@ struct PerformReduction
 				log("\n");
 			}
 
-			std::vector<equiv_bit_t> result;
+			int result_idx = -1;
 			for (int idx : bucket) {
+				if (results_map.count(idx) == 0)
+					continue;
+				if (result_idx == -1) {
+					result_idx = results_map.at(idx);
+					continue;
+				}
+				int result_idx2 = results_map.at(idx);
+				results[result_idx].insert(results[result_idx2].begin(), results[result_idx2].end());
+				for (int idx2 : results[result_idx2])
+					results_map[idx2] = result_idx;
+				results[result_idx2].clear();
+			}
+
+			if (result_idx == -1) {
+				result_idx = results.size();
+				results.push_back(std::set<int>());
+			}
+
+			results[result_idx].insert(bucket.begin(), bucket.end());
+		}
+	}
+
+	void analyze(std::vector<std::vector<equiv_bit_t>> &results)
+	{
+		std::vector<int> bucket;
+		for (size_t i = 0; i < sat_out.size(); i++)
+			bucket.push_back(i);
+
+		std::vector<std::set<int>> results_buf;
+		std::map<int, int> results_map;
+		analyze(results_buf, results_map, bucket, 1);
+
+		for (auto &r : results_buf)
+		{
+			if (r.size() <= 1)
+				continue;
+
+			std::vector<equiv_bit_t> result;
+
+			for (int idx : r) {
 				equiv_bit_t bit;
 				bit.depth = out_depth[idx];
 				bit.inverted = out_inverted[idx];
+				bit.drv = drivers.count(out_bits[idx]) ? drivers.at(out_bits[idx]).first : NULL;
 				bit.bit = out_bits[idx];
 				result.push_back(bit);
 			}
 
 			std::sort(result.begin(), result.end());
+
 			if (result.front().inverted)
 				for (auto &bit : result)
 					bit.inverted = !bit.inverted;
@@ -287,14 +337,6 @@ struct PerformReduction
 				results.push_back(result);
 		}
 	}
-
-	void analyze(std::vector<std::vector<equiv_bit_t>> &results)
-	{
-		std::vector<int> bucket;
-		for (size_t i = 0; i < sat_out.size(); i++)
-			bucket.push_back(i);
-		analyze(results, bucket, 1);
-	}
 };
 
 struct FreduceHelper
@@ -318,6 +360,9 @@ struct FreduceHelper
 		ct.setup_stdcells();
 
 		std::vector<std::set<RTLIL::SigBit>> batches;
+		for (auto &it : module->wires)
+			if (it.second->port_input)
+				batches.push_back(sigmap(it.second).to_sigbit_set());
 		for (auto &it : module->cells) {
 			if (ct.cell_known(it.second->type)) {
 				std::set<RTLIL::SigBit> inputs, outputs;
@@ -426,7 +471,10 @@ struct FreducePass : public Pass {
 		log("\n");
 		log("This pass performs functional reduction in the circuit. I.e. if two nodes are\n");
 		log("equivialent, they are merged to one node and one of the redundant drivers is\n");
-		log("removed.\n");
+		log("unconnected. A subsequent call to 'clean' will remove the redundant drivers.\n");
+		log("\n");
+		log("This pass is undef-aware, i.e. it considers don't-care values for detecting\n");
+		log("equivialent nodes.\n");
 		log("\n");
 		log("    -v, -vv\n");
 		log("        enable verbose or very verbose output\n");

From 1f80557adeede4d6fb90bab76e9a8acc2450136c Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 2 Jan 2014 19:58:59 +0100
Subject: [PATCH 45/49] Added SAT undef model for $pmux and $safe_pmux

---
 kernel/satgen.h | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 510240f5..208ae165 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -299,6 +299,9 @@ struct SatGen
 			std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep);
 			std::vector<int> s = importDefSigSpec(cell->connections.at("\\S"), timestep);
 			std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
+
+			std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
 			std::vector<int> tmp = a;
 			for (size_t i = 0; i < s.size(); i++) {
 				std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
@@ -306,12 +309,24 @@ struct SatGen
 			}
 			if (cell->type == "$safe_pmux")
 				tmp = ez->vec_ite(ez->onehot(s, true), tmp, a);
-			ez->assume(ez->vec_eq(tmp, y));
+			ez->assume(ez->vec_eq(tmp, yy));
 
-			if (model_undef) {
-				log("FIXME: No SAT undef model cell type %s!\n", RTLIL::id2cstr(cell->type));
+			if (model_undef)
+			{
+				std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
+				std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
+				std::vector<int> undef_s = importUndefSigSpec(cell->connections.at("\\S"), timestep);
 				std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
-				ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_y)));
+
+				tmp = a;
+				for (size_t i = 0; i < s.size(); i++) {
+					std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
+					tmp = ez->vec_ite(s.at(i), part_of_undef_b, tmp);
+				}
+				tmp = ez->vec_ite(ez->onehot(s, true), tmp, cell->type == "$safe_pmux" ? a : std::vector<int>(tmp.size(), ez->TRUE));
+				tmp = ez->vec_ite(ez->expression(ezSAT::OpOr, undef_s), std::vector<int>(tmp.size(), ez->TRUE), tmp);
+				ez->assume(ez->vec_eq(tmp, undef_y));
+				undefGating(y, yy, undef_y);
 			}
 			return true;
 		}

From 456ae31a8a63d4ffa283c7fc8d62081de22058a7 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 2 Jan 2014 20:23:34 +0100
Subject: [PATCH 46/49] Added "rename -hide" command

---
 passes/cmds/rename.cc | 45 ++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 44 insertions(+), 1 deletion(-)

diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc
index a582de56..519dce45 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -69,17 +69,30 @@ struct RenamePass : public Pass {
 		log("Assign short auto-generated names to all selected wires and cells with private\n");
 		log("names.\n");
 		log("\n");
+		log("    rename -hide [selection]\n");
+		log("\n");
+		log("Assign private names (the ones with $-prefix) to all selected wires and cells\n");
+		log("with public names. This ignores all selected ports.\n");
+		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
 		bool flag_enumerate = false;
+		bool flag_hide = false;
+		bool got_mode = false;
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
 			std::string arg = args[argidx];
-			if (arg == "-enumerate") {
+			if (arg == "-enumerate" && !got_mode) {
 				flag_enumerate = true;
+				got_mode = true;
+				continue;
+			}
+			if (arg == "-hide" && !got_mode) {
+				flag_hide = true;
+				got_mode = true;
 				continue;
 			}
 			break;
@@ -117,6 +130,36 @@ struct RenamePass : public Pass {
 			}
 		}
 		else
+		if (flag_hide)
+		{
+			extra_args(args, argidx, design);
+
+			for (auto &mod : design->modules)
+			{
+				RTLIL::Module *module = mod.second;
+				if (!design->selected(module))
+					continue;
+
+				std::map<RTLIL::IdString, RTLIL::Wire*> new_wires;
+				for (auto &it : module->wires) {
+					if (design->selected(module, it.second))
+						if (it.first[0] == '\\' && it.second->port_id == 0)
+							it.second->name = NEW_ID;
+					new_wires[it.second->name] = it.second;
+				}
+				module->wires.swap(new_wires);
+
+				std::map<RTLIL::IdString, RTLIL::Cell*> new_cells;
+				for (auto &it : module->cells) {
+					if (design->selected(module, it.second))
+						if (it.first[0] == '\\')
+							it.second->name = NEW_ID;
+					new_cells[it.second->name] = it.second;
+				}
+				module->cells.swap(new_cells);
+			}
+		}
+		else
 		{
 			if (argidx+2 != args.size())
 				log_cmd_error("Invalid number of arguments!\n");

From 5a0f561d9c6dd35e42a3ee0f0d5162ded6276f2b Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 2 Jan 2014 20:35:37 +0100
Subject: [PATCH 47/49] Now */ is optional in */<mode>:<arg> selections

---
 passes/cmds/select.cc | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/passes/cmds/select.cc b/passes/cmds/select.cc
index 5712a023..ec560772 100644
--- a/passes/cmds/select.cc
+++ b/passes/cmds/select.cc
@@ -529,7 +529,10 @@ static void select_stmt(RTLIL::Design *design, std::string arg)
 	} else {
 		size_t pos = arg.find('/');
 		if (pos == std::string::npos) {
-			arg_mod = arg;
+			if (arg.find(':') == std::string::npos)
+				arg_mod = arg;
+			else
+				arg_mod = "*", arg_memb = arg;
 		} else {
 			arg_mod = arg.substr(0, pos);
 			arg_memb = arg.substr(pos+1);

From 536e20bde159db3ad8c77aeb9001a8dddde884a8 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 2 Jan 2014 23:40:20 +0100
Subject: [PATCH 48/49] Fixed more complex undef cases in freduce

---
 passes/sat/freduce.cc | 40 ++++++++++++++++++++++++++++++++++++----
 1 file changed, 36 insertions(+), 4 deletions(-)

diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 9974f935..4b868b3c 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -224,9 +224,18 @@ struct PerformReduction
 		if (bucket.size() <= 1)
 			return;
 
-		if (verbose_level >= 1)
+		if (verbose_level == 1)
 			log("%*s  Trying to shatter bucket with %d signals.\n", 2*level, "", int(bucket.size()));
 
+		if (verbose_level > 1) {
+			std::vector<RTLIL::SigBit> bucket_sigbits;
+			for (int idx : bucket)
+				bucket_sigbits.push_back(out_bits[idx]);
+			RTLIL::SigSpec bucket_sig(bucket_sigbits);
+			bucket_sig.optimize();
+			log("%*s  Trying to shatter bucket with %d signals: %s\n", 2*level, "", int(bucket.size()), log_signal(bucket_sig));
+		}
+
 		std::vector<int> sat_list, sat_inv_list;
 		for (int idx : bucket) {
 			sat_list.push_back(ez.AND(sat_out[idx], sat_def[idx]));
@@ -264,6 +273,27 @@ struct PerformReduction
 		}
 		else
 		{
+			std::vector<int> undef_slaves;
+
+			for (int idx : bucket) {
+				std::vector<int> sat_def_list;
+				for (int idx2 : bucket)
+					if (idx != idx2)
+						sat_def_list.push_back(sat_def[idx2]);
+				if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list)))
+					undef_slaves.push_back(idx);
+			}
+
+			if (undef_slaves.size() == bucket.size()) {
+				if (verbose_level >= 1)
+					log("%*s    Complex undef overlap. None of the signals covers the others.\n", 2*level, "");
+				// FIXME: We could try to further shatter a group with complex undef overlaps
+				return;
+			}
+
+			for (int idx : undef_slaves)
+				out_depth[idx] = std::numeric_limits<int>::max();
+
 			if (verbose_level >= 1) {
 				log("%*s    Found %d equivialent signals:", 2*level, "", int(bucket.size()));
 				for (int idx : bucket)
@@ -339,7 +369,7 @@ struct PerformReduction
 	}
 };
 
-struct FreduceHelper
+struct FreduceWorker
 {
 	RTLIL::Module *module;
 
@@ -347,7 +377,7 @@ struct FreduceHelper
 	drivers_t drivers;
 	std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> inv_pairs;
 
-	FreduceHelper(RTLIL::Module *module) : module(module), sigmap(module)
+	FreduceWorker(RTLIL::Module *module) : module(module), sigmap(module)
 	{
 	}
 
@@ -384,6 +414,8 @@ struct FreduceHelper
 
 		int bits_count = 0;
 		std::map<std::vector<RTLIL::SigBit>, std::vector<RTLIL::SigBit>> buckets;
+		buckets[std::vector<RTLIL::SigBit>()].push_back(RTLIL::SigBit(RTLIL::State::S0));
+		buckets[std::vector<RTLIL::SigBit>()].push_back(RTLIL::SigBit(RTLIL::State::S1));
 		for (auto &batch : batches)
 		{
 			RTLIL::SigSpec batch_sig(std::vector<RTLIL::SigBit>(batch.begin(), batch.end()));
@@ -512,7 +544,7 @@ struct FreducePass : public Pass {
 		for (auto &mod_it : design->modules) {
 			RTLIL::Module *module = mod_it.second;
 			if (design->selected(module))
-				bitcount += FreduceHelper(module).run();
+				bitcount += FreduceWorker(module).run();
 		}
 
 		log("Rewired a total of %d signal bits.\n", bitcount);

From fb2bf934dc6d2c969906b350c9a1b09a972bfdd7 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 3 Jan 2014 00:22:17 +0100
Subject: [PATCH 49/49] Added correct handling of $memwr priority

---
 frontends/ast/genrtlil.cc       |  2 ++
 kernel/rtlil.cc                 |  1 +
 manual/CHAPTER_CellLib.tex      |  3 +++
 passes/memory/memory_collect.cc | 21 +++++++++++++++++++--
 tests/simple/memory.v           | 17 +++++++++++++++++
 5 files changed, 42 insertions(+), 2 deletions(-)

diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 1b6fc1d8..e44b2d36 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -1271,6 +1271,8 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 
 			cell->parameters["\\CLK_ENABLE"] = RTLIL::Const(0);
 			cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(0);
+
+			cell->parameters["\\PRIORITY"] = RTLIL::Const(RTLIL::autoidx-1);
 		}
 		break;
 
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 4916ca72..1311f31c 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -567,6 +567,7 @@ namespace {
 				param("\\MEMID");
 				param("\\CLK_ENABLE");
 				param("\\CLK_POLARITY");
+				param("\\PRIORITY");
 				port("\\CLK", 1);
 				port("\\EN", 1);
 				port("\\ADDR", param("\\ABITS"));
diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index 61713e74..b84e1b30 100644
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -272,6 +272,9 @@ the \B{CLK} input is not used.
 \item \B{CLK\_POLARITY} \\
 Clock is active on positive edge if this parameter has the value {\tt 1'b1} and on the negative
 edge if this parameter is {\tt 1'b0}.
+
+\item \B{PRIORITY} \\
+The cell with the higher integer value in this parameter wins a write conflict.
 \end{itemize}
 
 The HDL frontend models a memory using RTLIL::Memory objects and asynchronous
diff --git a/passes/memory/memory_collect.cc b/passes/memory/memory_collect.cc
index ca1a3666..ad4df228 100644
--- a/passes/memory/memory_collect.cc
+++ b/passes/memory/memory_collect.cc
@@ -20,9 +20,19 @@
 #include "kernel/register.h"
 #include "kernel/log.h"
 #include <sstream>
+#include <algorithm>
 #include <stdlib.h>
 #include <assert.h>
 
+static bool memcells_cmp(RTLIL::Cell *a, RTLIL::Cell *b)
+{
+	if (a->type == "$memrd" && b->type == "$memrd")
+		return a->name < b->name;
+	if (a->type == "$memrd" || b->type == "$memrd")
+		return (a->type == "$memrd") < (b->type == "$memrd");
+	return a->parameters.at("\\PRIORITY").as_int() < b->parameters.at("\\PRIORITY").as_int();
+}
+
 static void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory)
 {
 	log("Collecting $memrd and $memwr for memory `%s' in module `%s':\n",
@@ -48,11 +58,18 @@ static void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory)
 	RTLIL::SigSpec sig_rd_data;
 
 	std::vector<std::string> del_cell_ids;
+	std::vector<RTLIL::Cell*> memcells;
 
-	for (auto &cell_it : module->cells)
-	{
+	for (auto &cell_it : module->cells) {
 		RTLIL::Cell *cell = cell_it.second;
+		if ((cell->type == "$memwr" || cell->type == "$memrd") && cell->parameters["\\MEMID"].decode_string() == memory->name)
+			memcells.push_back(cell);
+	}
 
+	std::sort(memcells.begin(), memcells.end(), memcells_cmp);
+
+	for (auto cell : memcells)
+	{
 		if (cell->type == "$memwr" && cell->parameters["\\MEMID"].decode_string() == memory->name)
 		{
 			wr_ports++;
diff --git a/tests/simple/memory.v b/tests/simple/memory.v
index aea014a2..eaeee01d 100644
--- a/tests/simple/memory.v
+++ b/tests/simple/memory.v
@@ -1,4 +1,21 @@
 
+module test00(clk, setA, setB, y);
+
+input clk, setA, setB;
+output y;
+reg mem [1:0];
+
+always @(posedge clk) begin
+	if (setA) mem[0] <= 0;  // this is line 9
+	if (setB) mem[0] <= 1;  // this is line 10
+end
+
+assign y = mem[0];
+
+endmodule
+
+// ----------------------------------------------------------
+
 module test01(clk, wr_en, wr_addr, wr_value, rd_addr, rd_value);
 
 input clk, wr_en;