tests/sat/asserts_seq.v

   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/
   4
   5     input wire clk;
   6     input wire a;
   7
   8     output reg a_old = 0;
   9     output reg b = 1;
  10     wire assertion = (a_old != b);
  11
  12     always @(posedge clk) begin
  13         a_old <= a;
  14         b <= !a;
  15
  16         assert(a_old != b);
  17     end
  18 endmodule
  19
  20 module test_002(clk, a, a_old, b);
  21     // copy from test_001 with modifications
  22
  23     input wire clk;
  24     input wire a;
  25
  26     output reg a_old = 0;
  27     output reg b = 0;  // <-- this will fail
  28     wire assertion = (a_old != b);
  29
  30     always @(posedge clk) begin
  31         a_old <= a;
  32         b <= !a;
  33         assert(a_old != b);
  34     end
  35 endmodule
  36
  37 module test_003(clk, a, a_old, b);
  38     // copy from test_001 with modifications
  39
  40     input wire clk;
  41     input wire a;
  42
  43     output reg a_old = 0;
  44     output reg b;  // <-- this will fail
  45     wire assertion = (a_old != b);
  46
  47     always @(posedge clk) begin
  48         a_old <= a;
  49         b <= !a;
  50         assert(a_old != b);
  51     end
  52 endmodule
  53
  54 module test_004(clk, a, a_old, b);
  55     // copy from test_001 with modifications
  56
  57     input wire clk;
  58     input wire a;
  59
  60     output reg a_old = 0;
  61     output reg b = 1;
  62     wire assertion = (a_old != b);
  63
  64     always @(posedge clk) begin
  65         a_old <= a;
  66         b <= !a;
  67         assert(a_old == b);  // <-- this will fail
  68     end
  69 endmodule
  70
  71 module test_005(clk, a, a_old, b);
  72     // copy from test_001 with modifications
  73
  74     input wire clk;
  75     input wire a;
  76
  77     output reg a_old = 1; // <-- inverted, no problem
  78     output reg b = 0;
  79     wire assertion = (a_old != b);
  80
  81     always @(posedge clk) begin
  82         a_old <= a;
  83         b <= !a;
  84         assert(a_old != b);
  85     end
  86 endmodule
  87