summaryrefslogtreecommitdiff
path: root/tests/sat
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-04 13:43:34 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-04 13:43:34 +0100
commit7a66b38c3e7e05e712144d63691f517ecca18d1d (patch)
treeb15747a95b464ab78101d0c46caed2daaff57a00 /tests/sat
parent6891fd79a32d8b528978893e88dcb8b25bf66ef0 (diff)
Added test cases for sat command
Diffstat (limited to 'tests/sat')
-rw-r--r--tests/sat/.gitignore1
-rw-r--r--tests/sat/asserts.v14
-rw-r--r--tests/sat/asserts.ys3
-rw-r--r--tests/sat/asserts_seq.v87
-rw-r--r--tests/sat/asserts_seq.ys15
-rwxr-xr-xtests/sat/run-test.sh6
6 files changed, 126 insertions, 0 deletions
diff --git a/tests/sat/.gitignore b/tests/sat/.gitignore
new file mode 100644
index 00000000..397b4a76
--- /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 00000000..c6f8095e
--- /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 00000000..de5e7c9a
--- /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 00000000..9715104f
--- /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 00000000..c622ef61
--- /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 00000000..67e1beb2
--- /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