1 module test_001(clk, a, a_old, b);
2 // test case taken from:
3 // http://www.reddit.com/r/yosys/comments/1wvpj6/trouble_with_assertions_and_sat_solver/
10 wire assertion = (a_old != b);
12 always @(posedge clk) begin
20 module test_002(clk, a, a_old, b);
21 // copy from test_001 with modifications
27 output reg b = 0; // <-- this will fail
28 wire assertion = (a_old != b);
30 always @(posedge clk) begin
37 module test_003(clk, a, a_old, b);
38 // copy from test_001 with modifications
44 output reg b; // <-- this will fail
45 wire assertion = (a_old != b);
47 always @(posedge clk) begin
54 module test_004(clk, a, a_old, b);
55 // copy from test_001 with modifications
62 wire assertion = (a_old != b);
64 always @(posedge clk) begin
67 assert(a_old == b); // <-- this will fail
71 module test_005(clk, a, a_old, b);
72 // copy from test_001 with modifications
77 output reg a_old = 1; // <-- inverted, no problem
79 wire assertion = (a_old != b);
81 always @(posedge clk) begin