aboutsummaryrefslogtreecommitdiffstats
path: root/tests/opt
diff options
context:
space:
mode:
Diffstat (limited to 'tests/opt')
-rw-r--r--tests/opt/opt_share_add_sub.v10
-rw-r--r--tests/opt/opt_share_add_sub.ys13
-rw-r--r--tests/opt/opt_share_cat.v2
-rw-r--r--tests/opt/opt_share_cat.ys18
-rw-r--r--tests/opt/opt_share_cat_multiuser.v22
-rw-r--r--tests/opt/opt_share_cat_multiuser.ys13
-rw-r--r--tests/opt/opt_share_diff_port_widths.v21
-rw-r--r--tests/opt/opt_share_diff_port_widths.ys13
-rw-r--r--tests/opt/opt_share_extend.v19
-rw-r--r--tests/opt/opt_share_extend.ys13
-rw-r--r--tests/opt/opt_share_large_pmux_cat.v22
-rw-r--r--tests/opt/opt_share_large_pmux_cat.ys13
-rw-r--r--tests/opt/opt_share_large_pmux_cat_multipart.v25
-rw-r--r--tests/opt/opt_share_large_pmux_cat_multipart.ys15
-rw-r--r--tests/opt/opt_share_large_pmux_multipart.v24
-rw-r--r--tests/opt/opt_share_large_pmux_multipart.ys13
-rw-r--r--tests/opt/opt_share_large_pmux_part.v22
-rw-r--r--tests/opt/opt_share_large_pmux_part.ys13
-rw-r--r--tests/opt/opt_share_mux_tree.v2
-rw-r--r--tests/opt/opt_share_mux_tree.ys19
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