Assertion does not fail!

SystemVerilog
,
1

Hi All,

I have a very simple assertion.

property p1;
@(posedge clk)
rose(tagError) |-> ##[1:] ($rose(tErrorBit)) ##0 $rose(mCheck);
endproperty

I want to see a failure if $rose(tErrorBit) is true -but- $rose(mCheck) is not true at the same clock. The assertion does not fail. It simply waits for both tErrorBit and mCheck go $rose at the same clock. Then it passes. How can I make it fail when tErrorBit and mCheck do not go $rose at the same clock?

Here’s the EDA Playground link.

EDA Playground Link

Thanks very much.

2

In reply to a72:

I think you want

property p1;
    @(posedge clk)
    tagError && $rose(tErrorBit) |->  $rose(mCheck);
endproperty

Looking at this some more, you might want

property p1;
    @(posedge clk)
    tagError && ($rose(tErrorBit) | $rose(mCheck)) |->  $rose(mCheck) && $rose(mCheck);
endproperty
3

In reply to dave_59:

Thanks much, Dave. Your first solution actually does exactly what I want. The only difference is that my spec expected the entire sequence to start with $rose(tagError). But checking for level sensitive tagError will work. I should have thought of moving part of the expression as an antecedent.

Your second solution has a typo (mCheck is repeated twice). Should be,

property p1;
@(posedge clk)
tagError && ($rose(tErrorBit) | $rose(mCheck)) |-> $rose(mCheck) && $rose(tErrorBit);
endproperty

Thanks again.

4

In reply to a72:

 // an assertion of the form

a |-> ##[1:$] b ##0 c; // will never fail 
// because there are other thread's to check. 
// the fixes:
a |-> b[->1] ##0 c; // preferred
a |-> first_match(##[1:$] b) ##0 c; // option

Ben systemverilog.us

5

In reply to ben@SystemVerilog.us:

Ben, Thanks, but could you please elaborate on “because there are other threads to check”. I don’t fully understand what that means.

6

In reply to a72:

 

##[1:$] b ##0 c // is same as 
(##1 b ##0 c) or
(##2 b ##0 c) or
(##3 b ##0 c) or
...... 
(##$ b ##0 c); // $ is infinity 
// if one thread fails, maybe another will pass