Assertion Passes even when it is supposed to fail

SystemVerilog
,
1

Hi,

I have a very simple example. Please see the EDA playground link below.

property p1;
@(posedge clk)
$rose(a) |=> not(b) ##1 (c);
endproperty

Even though ‘c’ is never true, the assertion passes the first time it sees not(b) to be true. It does not check for (c) to be true after ##1 clock delay. ???

Thanks for any clarification you offer. I tried this both on VCS and Questa.

2

In reply to a72:

Am very surprised that this compiled;

 
$rose(a) |=> not(b) ##1 (c);
// the not is a property operator 
// the ## is a sequence operator 
// it is illegal to have a property ##1 sequence 
// the following is legal 

$rose(a) |=> !b ##1 (c);
3

In reply to ben@SystemVerilog.us:

Cool. Thanks very much. This is very obscure and hard to remember semantic. Yep, it compiles and runs.

4

In reply to a72:

$rose(a) |=> not(b) ##1 (c);

gets interpreted as

$rose(a) |=> not ( b ##1 c );

So if in the cycle after a rises b is not true, the assertion passes.

It also passes if in the cycle after a rises b is true, in the next cycle c is not true.

5

In reply to dave_59:

Thanks Dave, I missed the interpretation as I usually put parentheses around the “not” operator.

6

In reply to ben@SystemVerilog.us:

Revisiting this issue, 1800 says:

 
property_expr ::= 
  not  property_expr 
// with 
not(b) ##1 (c)
// it is not really clear that because of the () 
// around the b, the "not" applies to only "b" or the sequence b ##q c
// one could argue that because the syntax of the "not" does not require () 
// It becomes 
not ( b ##1 c )

As a good style, always surround the not full expression with ()
and avoid superfluous ()