tests/sva/counter.sv

   1 module top (input clk, reset, up, down, output reg [7:0] cnt);
   2         always @(posedge clk) begin
   3                 if (reset)
   4                         cnt <= 0;
   5                 else if (up)
   6                         cnt <= cnt + 1;
   7                 else if (down)
   8                         cnt <= cnt - 1;
   9         end
  10
  11         default clocking @(posedge clk); endclocking
  12         default disable iff (reset);
  13
  14         assert property (up |=> cnt == $past(cnt) + 8'd 1);
  15         assert property (up [*2] |=> cnt == $past(cnt, 2) + 8'd 2);
  16         assert property (up ##1 up |=> cnt == $past(cnt, 2) + 8'd 2);
  17
  18 `ifndef FAIL
  19         assume property (down |-> !up);
  20 `endif
  21         assert property (up ##1 down |=> cnt == $past(cnt, 2));
  22         assert property (down |=> cnt == $past(cnt) - 8'd 1);
  23
  24         property down_n(n);
  25                 down [*n] |=> cnt == $past(cnt, n) - n;
  26         endproperty
  27
  28         assert property (down_n(8'd 3));
  29         assert property (down_n(8'd 5));
  30 endmodule