Added test cases for expose -evert-dff

2 files changed, 48 insertions, 0 deletions

diff --git a/tests/sat/expose_dff.v b/tests/sat/expose_dff.v
new file mode 100644
index 00000000..708e2da3
--- /dev/null
+++ b/tests/sat/expose_dff.v
@@ -0,0 +1,33 @@
+
+module test1(input clk, input [3:0] a, output reg [3:0] y);
+always @(posedge clk)
+	y <= a;
+endmodule
+
+module test2(input clk, input [3:0] a, output reg [3:0] y);
+wire clk_n = !clk;
+always @(negedge clk_n)
+	y[1:0] <= a[1:0];
+always @(negedge clk_n)
+	y[3:2] <= a[3:2];
+endmodule
+
+// -----------------------------------------------------------
+
+module test3(input clk, rst, input [3:0] a, output reg [3:0] y);
+always @(posedge clk, posedge rst)
+	if (rst)
+		y <= 12;
+	else
+		y <= |a;
+endmodule
+
+module test4(input clk, rst, input [3:0] a, output reg [3:0] y);
+wire rst_n = !rst;
+always @(posedge clk, negedge rst_n)
+	if (!rst_n)
+		y <= 12;
+	else
+		y <= a != 0;
+endmodule
+
diff --git a/tests/sat/expose_dff.ys b/tests/sat/expose_dff.ys
new file mode 100644
index 00000000..95556840
--- /dev/null
+++ b/tests/sat/expose_dff.ys
@@ -0,0 +1,15 @@
+
+read_verilog expose_dff.v
+hierarchy; proc;;
+
+expose -shared -evert-dff test1 test2
+miter -equiv test1 test2 miter12
+flatten miter12; opt miter12
+
+expose -shared -evert-dff test3 test4
+miter -equiv test3 test4 miter34
+flatten miter34; opt miter34
+
+sat -verify -prove trigger 0 miter12
+sat -verify -prove trigger 0 miter34
+