Infinite delay assertion

SystemVerilog
1 
module assertion_test;
  logic clk;
  logic z, a, b;
  
  initial begin
    clk = 0; 
    	z = 0; a = 0; b = 0;
    #5  z = 1; a = 0; b = 0;
    #10 z = 0; a = 0; b = 0;
    #10 z = 0; a = 0; b = 1;
    #80
    $finish;
  end
  
  initial begin
    forever #5 clk = ~clk;
  end
  
  property pr1;
    @(posedge clk)
    $rose(z) |-> ##[1:$] a ##0 b;
  endproperty
    
  assert property (pr1) $display("assertion pass"); else $display("assertion faield");
    
endmodule

I am reading a book. it says: if b arrives but a doesn’t arrive, the assertion fails. but when I run the code and set the z, a, b. the assertion doesn’t fail. can anyone explain this?

thanks in advance.

2

The book doesn’t provide a complete story. The assertion is incomplete (does not pass or fail) and is considered weak.

The delay ##0 indicates that the beginning of the second sequence is at the same clock tick as the end of the first sequence. Since ##[1:$] a is unbounded and by default sequences are weak, if you get to the end of simulation without completing the sequence, there is no assertion failure.

If there’s a requirement that after z rises, a must be 1, you want the assertion to fail if a never reaches that value. Write the property as:

 $rose(z) |-> strong( ##[1:$] a ##0 b);
2 Likes
3

Hi Dave,
Would $rose(z) |-> strong( a[->1] ##0 b); be a more simulation efficient way of expressing the infinite range ?
i.e Instead of ##[1:$] boolean_expr should one prefer to use boolean_expr[->1] ?

4

They are equivalent.

5

Hi Dave,

I see many similar cases, like we need to check when z is high, then a becomes high and keeps high until b becomes high.

if we write $rose(z) |-> ##1 $rose(a) ##0 a[*1:$] ##0 $rose(b) if a keeps high after b, the assertion is still pass. or $rose(z) |-> ##1 $rose(a) ##0 a[*1:$] ##0 $rose(b) ##1 $fell(a) it won’t pass or fail. we have to write $rose(z) |-> strong (##1 $rose(a) ##0 a[*1:$] ##0 $rose(b) ##1 $fell(a))

6

The assertion doesn’t check for ‘a’ after ‘b’ is high, hence it passes
Your intention “when z is high, then a becomes high and keeps high until b becomes high.” doesn’t mention it as well

Check this_link
Try using

property pr1;
 @(posedge clk)
 $rose(z) |-> ##1 $rose(a) ##0 a[->1] ##0 $rose(b) ##1 $fell(a);
endproperty
1 Like
7

property pr1;
@(posedge clk)
$rose(z) |-> ##1 $rose(a) ##0 a[->1] ##0 $rose(b) ##1 $fell(a);
endproperty

we cannot use a[->1] to replace a[*1:$]. a only happens once for a[->1]; a can happen from 1 to infinite times for a[*1:$]
8

That’s correct. My apologies I missed out on that part
Try any of these

property pr1;
    @(posedge clk)
    $rose(z) |-> ##1 $rose(a) ##0 first_match( a[*1:$] ##0 $rose(b) ) ##1 $fell(a) ;
endproperty

property pr2;
   @(posedge clk)
   $rose(z) |-> ##1 $rose(a) ##0 ( a throughout $rose(b)[->1] ) ##1 $fell(a);
endproperty

Note that this occurs when ‘a’ remains high throughout simulation (post $rose(a))

initial begin
      clk = 0; 
    	z = 0; a = 0; b = 0;
    #04 z = 1; a = 0; b = 0;
    #10 z = 0; a = 1; b = 0;
    #70 z = 0; a = 1; b = 1; 
    #12 $finish();
end
 
always #5 clk = ~clk;