Added test cases for sat command

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

tests/sat/.gitignore

@@ -0,0 +1 @@
+*.log

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

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

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
+

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
+

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