diff options
author | Clifford Wolf <clifford@clifford.at> | 2014-02-04 13:43:34 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2014-02-04 13:43:34 +0100 |
commit | 7a66b38c3e7e05e712144d63691f517ecca18d1d (patch) | |
tree | b15747a95b464ab78101d0c46caed2daaff57a00 /tests/sat/asserts_seq.v | |
parent | 6891fd79a32d8b528978893e88dcb8b25bf66ef0 (diff) |
Added test cases for sat command
Diffstat (limited to 'tests/sat/asserts_seq.v')
-rw-r--r-- | tests/sat/asserts_seq.v | 87 |
1 files changed, 87 insertions, 0 deletions
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 + |