diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/sat/.gitignore | 1 | ||||
-rw-r--r-- | tests/sat/asserts.v | 14 | ||||
-rw-r--r-- | tests/sat/asserts.ys | 3 | ||||
-rw-r--r-- | tests/sat/asserts_seq.v | 87 | ||||
-rw-r--r-- | tests/sat/asserts_seq.ys | 15 | ||||
-rwxr-xr-x | tests/sat/run-test.sh | 6 |
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 |