From 7a66b38c3e7e05e712144d63691f517ecca18d1d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 4 Feb 2014 13:43:34 +0100
Subject: [PATCH] Added test cases for sat command

---
 Makefile                 |  1 +
 tests/sat/.gitignore     |  1 +
 tests/sat/asserts.v      | 14 +++++++
 tests/sat/asserts.ys     |  3 ++
 tests/sat/asserts_seq.v  | 87 ++++++++++++++++++++++++++++++++++++++++
 tests/sat/asserts_seq.ys | 15 +++++++
 tests/sat/run-test.sh    |  6 +++
 7 files changed, 127 insertions(+)
 create mode 100644 tests/sat/.gitignore
 create mode 100644 tests/sat/asserts.v
 create mode 100644 tests/sat/asserts.ys
 create mode 100644 tests/sat/asserts_seq.v
 create mode 100644 tests/sat/asserts_seq.ys
 create mode 100755 tests/sat/run-test.sh

diff --git a/Makefile b/Makefile
index 031724777..023c62def 100644
--- 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
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