Assertion failure using strong property

SystemVerilog
, , ,
1

Hi Forum,

Consider the following concurrent assertions

`define FAIL(x) `"T:%0t x Fails`"

a1:assert property( @(posedge clk) seq_expr1 |=> seq_expr2 ) 
                                   else $display(`FAIL(a1),$time);

//  Assume  seq_expr3  is  boolean_expr[->1]
a2:assert property( @(posedge clk) seq_expr1 |=> strong( seq_expr3 ) ) 
                                   else $display(`FAIL(a2),$time);

Note that both concurrent assertions have the same antecedent.

Assume posedge of clock occurs at T0,T1,T2,…Tn and antecedent matches at T4

For a1 if the seq_expr2 doesn’t match ( assuming that there are sufficient clock ticks )

then we observe $display(“a1 Fails“)

i.e the user-defined message in fail action block associated with a1

If the consequent boolean_expr[->1] doesn’t match till end of simulation then ap2 fails

Does the user-defined message in fail action block $display(“a2 Fails“) execute in this case

or is a default $error ( possibly tool dependent ) thrown ?

I referred LRM section 16.12.2 Sequence property for this but I don’t see an explicit explanation for this case

Thanks

2

I’m making sure I understand the question properly. Here, we’ve got something that’s expected to fail with a goto repetition. Boiling it down to something stupid, I think we could probably have:

a3: assert property (@(posedge clk) 1 |=> strong (0 [->1])) else $display("Boo");

Since 0 is never true, I think I’m convinced that the property isn’t true, but I’m not an expert on liveness properties in simulation.

Thinking about it, we can boil things down even further to

a4: assert property (@(posedge clk) strong (0 [->1])) else $display("Boo");

(the implication doesn’t really do anything).

Looking at the text of 16.12.2, I think the point is that the property won’t evaluate to true because there is no match for it before the end of the simulation.

But

If I understand the question, this isn’t really a question about properties, but is rather a question about what happens when one fails at the end of a simulation?

Is the behaviour you see the same across EDA tools? With which one do you see it?