Reimplement opt_share to work on $alu and $pmux

20 files changed, 295 insertions, 17 deletions

diff --git a/tests/opt/opt_share_add_sub.v b/tests/opt/opt_share_add_sub.v
new file mode 100644
index 000000000..30e093a39
--- /dev/null
+++ b/tests/opt/opt_share_add_sub.v
@@ -0,0 +1,10 @@
+module opt_share_test(
+               input [15:0]  a,
+               input [15:0]  b,
+               input 				 sel,
+               output [15:0] res,
+               );
+
+  assign res = {sel ? a + b : a - b};
+
+endmodule
diff --git a/tests/opt/opt_share_add_sub.ys b/tests/opt/opt_share_add_sub.ys
new file mode 100644
index 000000000..4a5406791
--- /dev/null
+++ b/tests/opt/opt_share_add_sub.ys
@@ -0,0 +1,13 @@
+read_verilog opt_share_add_sub.v
+proc;;
+copy opt_share_test merged
+
+alumacc merged
+opt merged
+opt_share merged
+opt_clean merged
+
+miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter
+sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
+
+select -assert-count 1 -module merged t:$alu
diff --git a/tests/opt/opt_share_cat.v b/tests/opt/opt_share_cat.v
index c32073360..605dcfe59 100644
--- a/tests/opt/opt_share_cat.v
+++ b/tests/opt/opt_share_cat.v
@@ -1,4 +1,4 @@
-module add_sub(
+module opt_share_test(
                input [15:0]  a,
                input [15:0]  b,
                input [15:0]  c,
diff --git a/tests/opt/opt_share_cat.ys b/tests/opt/opt_share_cat.ys
index c3f2f5a2f..7de69bfde 100644
--- a/tests/opt/opt_share_cat.ys
+++ b/tests/opt/opt_share_cat.ys
@@ -1,9 +1,13 @@
 read_verilog opt_share_cat.v
-prep -flatten
-opt
-pmuxtree
-opt_share
-opt_clean
+proc;;
+copy opt_share_test merged
 
-select -assert-count 2 t:$sub
-select -assert-count 0 t:$add
+alumacc merged
+opt merged
+opt_share merged
+opt_clean merged
+
+miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter
+sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
+
+select -assert-count 2 -module merged t:$alu
diff --git a/tests/opt/opt_share_cat_multiuser.v b/tests/opt/opt_share_cat_multiuser.v
new file mode 100644
index 000000000..9ac0ceec8
--- /dev/null
+++ b/tests/opt/opt_share_cat_multiuser.v
@@ -0,0 +1,22 @@
+module opt_share_test(
+               input [15:0] 		 a,
+               input [15:0] 		 b,
+               input [15:0] 		 c,
+               input [15:0] 		 d,
+               input 						 sel,
+               output reg [47:0] res,
+               );
+
+  wire [15:0] 									 add_res = a+b;
+  wire [15:0] 									 sub_res = a-b;
+  wire [31: 0] 									 cat1 = {add_res, c+d};
+  wire [31: 0] 									 cat2 = {sub_res, c-d};
+
+  always @* begin
+    case(sel)
+      0: res = {cat1, add_res};
+      1: res = {cat2, add_res};
+    endcase
+  end
+
+endmodule
diff --git a/tests/opt/opt_share_cat_multiuser.ys b/tests/opt/opt_share_cat_multiuser.ys
new file mode 100644
index 000000000..6a82fbd79
--- /dev/null
+++ b/tests/opt/opt_share_cat_multiuser.ys
@@ -0,0 +1,13 @@
+read_verilog opt_share_cat_multiuser.v
+proc;;
+copy opt_share_test merged
+
+alumacc merged
+opt merged
+opt_share merged
+opt_clean merged
+
+miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter
+sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
+
+select -assert-count 3 -module merged t:$alu
diff --git a/tests/opt/opt_share_diff_port_widths.v b/tests/opt/opt_share_diff_port_widths.v
new file mode 100644
index 000000000..5e2971e30
--- /dev/null
+++ b/tests/opt/opt_share_diff_port_widths.v
@@ -0,0 +1,21 @@
+module opt_share_test(
+               input [15:0] 		 a,
+               input [15:0] 		 b,
+							 input [15:0] 		 c,
+							 input [1:0] 			 sel,
+							 output reg [15:0] res
+               );
+
+  wire [15:0] 							 add0_res = a+b;
+  wire [15:0] 							 add1_res = a+c;
+
+  always @* begin
+    case(sel)
+      0: res = add0_res[10:0];
+      1: res = add1_res[10:0];
+      2: res = a - b;
+      default: res = 32'bx;
+    endcase
+  end
+
+endmodule
diff --git a/tests/opt/opt_share_diff_port_widths.ys b/tests/opt/opt_share_diff_port_widths.ys
new file mode 100644
index 000000000..ec5e9f7b0
--- /dev/null
+++ b/tests/opt/opt_share_diff_port_widths.ys
@@ -0,0 +1,13 @@
+read_verilog opt_share_diff_port_widths.v
+proc;;
+copy opt_share_test merged
+
+alumacc merged
+opt merged
+opt_share merged
+opt_clean merged
+
+miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter
+sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
+
+select -assert-count 2 -module merged t:$alu
diff --git a/tests/opt/opt_share_extend.v b/tests/opt/opt_share_extend.v
new file mode 100644
index 000000000..5ed6bde6f
--- /dev/null
+++ b/tests/opt/opt_share_extend.v
@@ -0,0 +1,19 @@
+module opt_share_test(
+											input signed [7:0] 			 a,
+											input signed [10:0] 		 b,
+											input signed [15:0] 		 c,
+											input [1:0] 						 sel,
+											output reg signed [15:0] res
+											);
+
+
+  always @* begin
+    case(sel)
+      0: res = a + b;
+      1: res = a - b;
+      2: res = a + c;
+      default: res = 16'bx;
+    endcase
+  end
+
+endmodule
diff --git a/tests/opt/opt_share_extend.ys b/tests/opt/opt_share_extend.ys
new file mode 100644
index 000000000..c553ee0fb
--- /dev/null
+++ b/tests/opt/opt_share_extend.ys
@@ -0,0 +1,13 @@
+read_verilog opt_share_extend.v
+proc;;
+copy opt_share_test merged
+
+alumacc merged
+opt merged
+opt_share merged
+opt_clean merged
+
+miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter
+sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
+
+select -assert-count 1 -module merged t:$alu
diff --git a/tests/opt/opt_share_large_pmux_cat.v b/tests/opt/opt_share_large_pmux_cat.v
new file mode 100644
index 000000000..6208c796b
--- /dev/null
+++ b/tests/opt/opt_share_large_pmux_cat.v
@@ -0,0 +1,22 @@
+module opt_share_test(
+											input [15:0] 			a,
+											input [15:0] 			b,
+											input [15:0] 			c,
+											input [2:0] 			sel,
+											output reg [31:0] res
+											);
+
+
+  always @* begin
+    case(sel)
+      0: res = {a + b, a};
+      1: res = {a - b, b};
+      2: res = {a + c, c};
+      3: res = {a - c, a};
+      4: res = {b, b};
+      5: res = {c, c};
+      default: res = 32'bx;
+    endcase
+  end
+
+endmodule
diff --git a/tests/opt/opt_share_large_pmux_cat.ys b/tests/opt/opt_share_large_pmux_cat.ys
new file mode 100644
index 000000000..4186ca52e
--- /dev/null
+++ b/tests/opt/opt_share_large_pmux_cat.ys
@@ -0,0 +1,13 @@
+read_verilog opt_share_large_pmux_cat.v
+proc;;
+copy opt_share_test merged
+
+alumacc merged
+opt merged
+opt_share merged
+opt_clean merged
+
+miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter
+sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
+
+select -assert-count 1 -module merged t:$alu
diff --git a/tests/opt/opt_share_large_pmux_cat_multipart.v b/tests/opt/opt_share_large_pmux_cat_multipart.v
new file mode 100644
index 000000000..f97971bf6
--- /dev/null
+++ b/tests/opt/opt_share_large_pmux_cat_multipart.v
@@ -0,0 +1,25 @@
+module opt_share_test(
+											input [15:0] 			a,
+											input [15:0] 			b,
+											input [15:0] 			c,
+											input [15:0] 			d,
+											input [2:0] 			sel,
+											output reg [31:0] res
+											);
+
+  wire [15:0] 													add0_res = a+d;
+
+  always @* begin
+    case(sel)
+      0: res = {add0_res, a};
+      1: res = {a - b, add0_res[7], 15'b0};
+      2: res = {b-a, b};
+      3: res = {d, b - c};
+      4: res = {d, b - a};
+      5: res = {c, d};
+      6: res = {a - c, b-d};
+      default: res = 32'bx;
+    endcase
+  end
+
+endmodule
diff --git a/tests/opt/opt_share_large_pmux_cat_multipart.ys b/tests/opt/opt_share_large_pmux_cat_multipart.ys
new file mode 100644
index 000000000..54d200dc7
--- /dev/null
+++ b/tests/opt/opt_share_large_pmux_cat_multipart.ys
@@ -0,0 +1,15 @@
+read_verilog opt_share_large_pmux_cat_multipart.v
+proc;;
+copy opt_share_test merged
+
+alumacc merged
+opt merged
+
+opt_share merged
+opt_clean merged
+opt -full
+
+miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter
+sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
+
+select -assert-count 4 -module merged t:$alu
diff --git a/tests/opt/opt_share_large_pmux_multipart.v b/tests/opt/opt_share_large_pmux_multipart.v
new file mode 100644
index 000000000..e7ba318ef
--- /dev/null
+++ b/tests/opt/opt_share_large_pmux_multipart.v
@@ -0,0 +1,24 @@
+module opt_share_test(
+											input [15:0] 			a,
+											input [15:0] 			b,
+											input [15:0] 			c,
+											input [15:0] 			d,
+											input [2:0] 			sel,
+											output reg [15:0] res
+											);
+
+
+  always @* begin
+    case(sel)
+      0: res = a + d;
+      1: res = a - b;
+      2: res = b;
+      3: res = b - c;
+      4: res = b - a;
+      5: res = c;
+      6: res = a - c;
+      default: res = 16'bx;
+    endcase
+  end
+
+endmodule
diff --git a/tests/opt/opt_share_large_pmux_multipart.ys b/tests/opt/opt_share_large_pmux_multipart.ys
new file mode 100644
index 000000000..11182df1a
--- /dev/null
+++ b/tests/opt/opt_share_large_pmux_multipart.ys
@@ -0,0 +1,13 @@
+read_verilog opt_share_large_pmux_multipart.v
+proc;;
+copy opt_share_test merged
+
+alumacc merged
+opt merged
+opt_share merged
+opt_clean merged
+
+miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter
+sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
+
+select -assert-count 2 -module merged t:$alu
diff --git a/tests/opt/opt_share_large_pmux_part.v b/tests/opt/opt_share_large_pmux_part.v
new file mode 100644
index 000000000..138be0cd6
--- /dev/null
+++ b/tests/opt/opt_share_large_pmux_part.v
@@ -0,0 +1,22 @@
+module opt_share_test(
+											input [15:0] 			a,
+											input [15:0] 			b,
+											input [15:0] 			c,
+											input [2:0] 			sel,
+											output reg [15:0] res
+											);
+
+
+  always @* begin
+    case(sel)
+      0: res = a + b;
+      1: res = a - b;
+      2: res = a + c;
+      3: res = a - c;
+      4: res = b;
+      5: res = c;
+      default: res = 16'bx;
+    endcase
+  end
+
+endmodule
diff --git a/tests/opt/opt_share_large_pmux_part.ys b/tests/opt/opt_share_large_pmux_part.ys
new file mode 100644
index 000000000..6b594a3d6
--- /dev/null
+++ b/tests/opt/opt_share_large_pmux_part.ys
@@ -0,0 +1,13 @@
+read_verilog opt_share_large_pmux_part.v
+proc;;
+copy opt_share_test merged
+
+alumacc merged
+opt merged
+opt_share merged
+opt_clean merged
+
+miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter
+sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
+
+select -assert-count 1 -module merged t:$alu
diff --git a/tests/opt/opt_share_mux_tree.v b/tests/opt/opt_share_mux_tree.v
index 807ed2978..c90826204 100644
--- a/tests/opt/opt_share_mux_tree.v
+++ b/tests/opt/opt_share_mux_tree.v
@@ -1,4 +1,4 @@
-module add_sub(
+module opt_share_test(
                input [15:0] 		 a,
                input [15:0] 		 b,
                input [15:0] 		 c,
diff --git a/tests/opt/opt_share_mux_tree.ys b/tests/opt/opt_share_mux_tree.ys
index 94d6aa7d2..58473039f 100644
--- a/tests/opt/opt_share_mux_tree.ys
+++ b/tests/opt/opt_share_mux_tree.ys
@@ -1,10 +1,13 @@
 read_verilog opt_share_mux_tree.v
-prep -flatten
-opt
-pmuxtree
-opt_share;
-opt_share;
-opt_clean
+proc;;
+copy opt_share_test merged
 
-select -assert-count 1 t:$add
-select -assert-count 0 t:$sub
+alumacc merged
+opt merged
+opt_share merged
+opt_clean merged
+
+miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter
+sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter
+
+select -assert-count 1 -module merged t:$alu