SVA: implication vs. sequence. implication and delay.

[ljepson74]

The below assertions check that gnt is not high for consecutive clk cycles.

 Q1: v1 vs. v2: Are there benefits or relevant differences between these styles.
 Q2: v2 vs. v3: Does the placement of delay matter?
Besides for end of simulation termination.

 The questions are mainly about whether some style is better for the simulator, or there is some non-obvious situation I should consider.
 

module top;
  bit clk, gnt;
  bit [19:0] gnt_a;

  initial begin
    gnt_a = 20'b0011001010_0000001101;
    #200 $finish;
  end

  assign gnt = gnt_a[19];

  always clk = #5 ~clk; 

  always@(posedge clk) begin
    gnt_a = gnt_a<<1;
    $display($time," gnt: %1b",gnt);
  end

  as_v1 : assert property ( @(posedge clk)
                           not strong(gnt[*2])
                          );
    
  as_v2 : assert property ( @(posedge clk)
                           gnt |-> ##1 !gnt
                          );
      
  as_v3 : assert property ( @(posedge clk)
                           gnt ##1 1'b1 |-> !gnt
                          );
endmodule

 

Code is also available here: https://edaplayground.com/x/4GXn