Added test cases for sat command

6 files changed, 126 insertions, 0 deletions

diff --git a/tests/sat/.gitignore b/tests/sat/.gitignore
new file mode 100644
index 000000000..397b4a762
--- /dev/null
+++ b/tests/sat/.gitignore
@@ -0,0 +1 @@
+*.log
diff --git a/tests/sat/asserts.v b/tests/sat/asserts.v
new file mode 100644
index 000000000..c6f8095e1
--- /dev/null
+++ b/tests/sat/asserts.v
@@ -0,0 +1,14 @@
+// http://www.reddit.com/r/yosys/comments/1vljks/new_support_for_systemveriloglike_asserts/
+module test(input clk, input rst, output y);
+reg [2:0] state;
+always @(posedge clk) begin
+    if (rst || state == 3) begin
+        state <= 0;
+    end else begin
+        assert(state < 3);
+        state <= state + 1;
+    end
+end
+assign y = state[2];
+assert property (y !== 1'b1);
+endmodule
diff --git a/tests/sat/asserts.ys b/tests/sat/asserts.ys
new file mode 100644
index 000000000..de5e7c9aa
--- /dev/null
+++ b/tests/sat/asserts.ys
@@ -0,0 +1,3 @@
+read_verilog asserts.v
+hierarchy; proc; opt
+sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts
diff --git a/tests/sat/asserts_seq.v b/tests/sat/asserts_seq.v
new file mode 100644
index 000000000..9715104f3
--- /dev/null
+++ b/tests/sat/asserts_seq.v
@@ -0,0 +1,87 @@
+module test_001(clk, a, a_old, b);
+    // test case taken from:
+    // http://www.reddit.com/r/yosys/comments/1wvpj6/trouble_with_assertions_and_sat_solver/
+
+    input wire clk;
+    input wire a;
+
+    output reg a_old = 0;
+    output reg b = 1;
+    wire assertion = (a_old != b);
+
+    always @(posedge clk) begin
+        a_old <= a;
+        b <= !a;
+
+        assert(a_old != b);
+    end
+endmodule
+
+module test_002(clk, a, a_old, b);
+    // copy from test_001 with modifications
+
+    input wire clk;
+    input wire a;
+
+    output reg a_old = 0;
+    output reg b = 0;  // <-- this will fail
+    wire assertion = (a_old != b);
+
+    always @(posedge clk) begin
+        a_old <= a;
+        b <= !a;
+        assert(a_old != b);
+    end
+endmodule
+
+module test_003(clk, a, a_old, b);
+    // copy from test_001 with modifications
+
+    input wire clk;
+    input wire a;
+
+    output reg a_old = 0;
+    output reg b;  // <-- this will fail
+    wire assertion = (a_old != b);
+
+    always @(posedge clk) begin
+        a_old <= a;
+        b <= !a;
+        assert(a_old != b);
+    end
+endmodule
+
+module test_004(clk, a, a_old, b);
+    // copy from test_001 with modifications
+
+    input wire clk;
+    input wire a;
+
+    output reg a_old = 0;
+    output reg b = 1;
+    wire assertion = (a_old != b);
+
+    always @(posedge clk) begin
+        a_old <= a;
+        b <= !a;
+        assert(a_old == b);  // <-- this will fail
+    end
+endmodule
+
+module test_005(clk, a, a_old, b);
+    // copy from test_001 with modifications
+
+    input wire clk;
+    input wire a;
+
+    output reg a_old = 1; // <-- inverted, no problem
+    output reg b = 0;
+    wire assertion = (a_old != b);
+
+    always @(posedge clk) begin
+        a_old <= a;
+        b <= !a;
+        assert(a_old != b);
+    end
+endmodule
+
diff --git a/tests/sat/asserts_seq.ys b/tests/sat/asserts_seq.ys
new file mode 100644
index 000000000..c622ef610
--- /dev/null
+++ b/tests/sat/asserts_seq.ys
@@ -0,0 +1,15 @@
+read_verilog asserts_seq.v
+hierarchy; proc; opt
+
+sat -verify  -prove-asserts -tempinduct -seq 1 test_001
+sat -falsify -prove-asserts -tempinduct -seq 1 test_002
+sat -falsify -prove-asserts -tempinduct -seq 1 test_003
+sat -falsify -prove-asserts -tempinduct -seq 1 test_004
+sat -verify  -prove-asserts -tempinduct -seq 1 test_005
+
+sat -verify  -prove-asserts -seq 2 test_001
+sat -falsify -prove-asserts -seq 2 test_002
+sat -falsify -prove-asserts -seq 2 test_003
+sat -falsify -prove-asserts -seq 2 test_004
+sat -verify  -prove-asserts -seq 2 test_005
+
diff --git a/tests/sat/run-test.sh b/tests/sat/run-test.sh
new file mode 100755
index 000000000..67e1beb23
--- /dev/null
+++ b/tests/sat/run-test.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+set -e
+for x in *.ys; do
+	echo "Running $x.."
+	../../yosys -ql ${x%.ys}.log $x
+done