summaryrefslogtreecommitdiff
path: root/tests/sat
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-06 01:00:11 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-06 01:00:56 +0100
commit849fd62cfed9b6623865c7af76dd1bfbc6adf457 (patch)
tree3b745d082500ef0a54e6c4b14bc18c9f82636fb2 /tests/sat
parente915043144d52e2ff97e2b4638ed1af84426e359 (diff)
Added counters sat test case
Diffstat (limited to 'tests/sat')
-rw-r--r--tests/sat/counters.v35
-rw-r--r--tests/sat/counters.ys10
2 files changed, 45 insertions, 0 deletions
diff --git a/tests/sat/counters.v b/tests/sat/counters.v
new file mode 100644
index 00000000..09e27304
--- /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
index 00000000..330895f8
--- /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
+