Added test cases for sat command

diff --git a/Makefile b/Makefile
index 031724777c63cc20f37b8eba409fcef36608989c..023c62def6b81d9c2e08b1a2169391d558c54d02 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -135,6 +135,7 @@ test: yosys
        cd tests/simple && bash run-test.sh
        cd tests/hana && bash run-test.sh
        cd tests/asicworld && bash run-test.sh
+       cd tests/sat && bash run-test.sh
 
 install: $(TARGETS) $(EXTRA_TARGETS)
        $(INSTALL_SUDO) mkdir -p $(DESTDIR)/bin

diff --git a/tests/sat/.gitignore b/tests/sat/.gitignore
new file mode 100644 (file)
index 0000000..397b4a7
--- /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 (file)
index 0000000..c6f8095
--- /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 (file)
index 0000000..de5e7c9
--- /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 (file)
index 0000000..9715104
--- /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 (file)
index 0000000..c622ef6
--- /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 (executable)
index 0000000..67e1beb
--- /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