tests/sva/sva_not.sv

   1 module top (
   2         input clk,
   3         input reset,
   4         input ping,
   5         input [1:0] cfg,
   6         output reg pong
   7 );
   8         reg [2:0] cnt;
   9         localparam integer maxdelay = 8;
  10
  11         always @(posedge clk) begin
  12                 if (reset) begin
  13                         cnt <= 0;
  14                         pong <= 0;
  15                 end else begin
  16                         cnt <= cnt - |cnt;
  17                         pong <= cnt == 1;
  18                         if (ping) cnt <= 4 + cfg;
  19                 end
  20         end
  21
  22         assert property (
  23                 @(posedge clk)
  24                 disable iff (reset)
  25                 not (ping ##1 !pong [*maxdelay])
  26         );
  27
  28 `ifndef FAIL
  29         assume property (
  30                 @(posedge clk)
  31                 not (cnt && ping)
  32         );
  33 `endif
  34 endmodule