Added counters sat test case

diff --git a/tests/sat/counters.v b/tests/sat/counters.v
new file mode 100644 (file)
index 0000000..09e2730
--- /dev/null
+++ b/tests/sat/counters.v
@@ -0,0 +1,35 @@
+
+module counter1(clk, rst, ping);
+       input clk, rst;
+       output ping;
+       reg [31:0] count;
+
+       always @(posedge clk) begin
+               if (rst)
+                       count <= 0;
+               else
+                       count <= count + 1;
+       end
+
+       assign ping = &count;
+endmodule
+
+module counter2(clk, rst, ping);
+       input clk, rst;
+       output ping;
+       reg [31:0] count;
+
+       integer i;
+       reg carry;
+
+       always @(posedge clk) begin
+               carry = 1;
+               for (i = 0; i < 32; i = i+1) begin
+                       count[i] <= !rst & (count[i] ^ carry);
+                       carry = count[i] & carry;
+               end
+       end
+
+       assign ping = &count;
+endmodule
+

diff --git a/tests/sat/counters.ys b/tests/sat/counters.ys
new file mode 100644 (file)
index 0000000..330895f
--- /dev/null
+++ b/tests/sat/counters.ys
@@ -0,0 +1,10 @@
+
+read_verilog counters.v
+proc; opt
+
+expose -shared counter1 counter2
+miter -equiv -make_assert -make_outputs counter1 counter2 miter
+
+cd miter; flatten; opt
+sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs
+