Infinite delay assertion

[Have_A_Doubt]

@flyant

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

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

@flyant

$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))

Check this_link
Try using

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