Jump to content

SVA: implication vs. sequence. implication and delay.


Recommended Posts

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 

Link to post
Share on other sites

Join the conversation

You can post now and register later. If you have an account, sign in now to post with your account.
Note: Your post will require moderator approval before it will be visible.

Guest
Reply to this topic...

×   Pasted as rich text.   Paste as plain text instead

  Only 75 emoji are allowed.

×   Your link has been automatically embedded.   Display as a link instead

×   Your previous content has been restored.   Clear editor

×   You cannot paste images directly. Upload or insert images from URL.

×
×
  • Create New...