Assertion failure using strong property

[LFT]

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 a2 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

[rswarbrick]

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?

[LFT]

Across 3 EDA tools ( 2025 version ) I do observe the fail action block executing.

On 1 tool I see no output ( which possibly could be a tool limitation )

[rswarbrick]

Hmm, that sounds like it might belong in a bug report I can’t see any obvious wiggle room for the tool vendor allowing the tool to do something unusual here.

[LFT]

Ben has shared his perspective on this topic :: linkedin.com/posts/ben-cohen

Thus, if $finish is executed in the Active region, it's a KILL switch as far as
simulation is concerned and all other regions are not executed.
However, the 𝘀𝗶𝗺𝘂𝗹𝗮𝘁𝗶𝗼𝗻 𝗶𝘀 𝘀𝘁𝗶𝗹𝗹 𝗿𝗲𝘀𝗽𝗼𝗻𝘀𝗶𝗯𝗹𝗲 𝘁𝗼 𝗽𝗿𝗼𝘃𝗶𝗱𝗲 𝗶𝗻𝗳𝗼𝗿𝗺𝗮𝘁𝗶𝗼𝗻 𝗮𝗯𝗼𝘂𝘁 𝗮𝗻𝘆 𝗳𝗮𝗶𝗹𝘂𝗿𝗲 𝗼𝗳 𝗮
𝘀𝘁𝗿𝗼𝗻𝗴 𝗽𝗿𝗼𝗽𝗲𝗿𝘁𝘆 𝘁𝗵𝗮𝘁 𝗱𝗼𝗲𝘀 𝗻𝗼𝘁 𝗰𝗼𝗺𝗽𝗹𝗲𝘁𝗲 The action block need not be executed 
(tool option, IMHO).

As per LRM Pass / Fail action block executes in reactive region

LRM 9.2.3 Final procedures mentions

A final procedure executes when simulation ends due to an explicit or implicit call to $finish.
All final procedures shall execute in an arbitrary order.
No remaining scheduled events shall execute after all final procedures have executed.

This above quote tells me that once $finish() executes in active region,

the remaining regions in the same time step don’t execute.

Execution of Fail action block ( as observed across 3 EDA tools ) means that reactive region does execute ( or maybe incomplete strong properties have an exception to the rule of remaining regions not executing once $finish executes )

Having referred LRM Sections 16.12.2 Sequence property and

16.12.15 Weak and strong operators,

I believe that the LRM doesn’t explicitly mention whether the fail action block executes ( in reactive region of the same time step that $finish() is called ) when strong(boolean_expression[->1]) doesn’t match till end of simulation

i.e if the strong( sequence ) “𝗰𝗮𝗻𝗻𝗼𝘁 𝗯𝗲 𝗶𝗱𝗲𝗻𝘁𝗶𝗳𝗶𝗲𝗱 𝗮𝘁 𝗮 𝗳𝗶𝗻𝗶𝘁𝗲 𝘁𝗶𝗺𝗲”

Also thank you @rswarbrick for your a3 / a4 examples .

It never occurred to me to try 0[–>1] as sequence_expression

Was surprised at first that it’s not treated as No Match.

On writing it’s equivalent expression it’s clear that it’s perfectly legal !!

[dave_59]

The LRM is not clear in this context. It only defines the semantics of strong properties in terms of static formal tools, not dynamic simulation. And the description of $finish was written for Verilog before SystemVerilog add event regions.

I get different behaviors with this testcase with all simulators.

`define FINISH
module top;
  bit clk, a,b,d;
  initial repeat(20) #5 clk =!clk;
 
  assert property (@(posedge clk) $rose(a) |-> strong( b[->1]))
    $info("you passed"); else $error("you failed");
    
    initial begin 
      @(posedge clk) a<=1;
      @(posedge clk) a<=0;
      @(posedge clk) b<=1;
      @(posedge clk) b<=0;
      @(posedge clk) a<=1;
      @(posedge clk) 
      `ifdef FINISH
      $finish
      `endif
      ;
    end
    final $display("it's final");
endmodule

My expectation is that you should always be notified of a failure. However, whether the action block executes and in which region it occurs is debatable.

[LFT]

Hi Dave,

I was referring to your response in an older thread

@dave_59

`define FINISH
module tb;
  
  bit clk, a,b,d;
  initial repeat(20) #5 clk =!clk;
 
  assert property (@(posedge clk) $rose(a) |-> strong( b[->1]))
    $info("T:%0t you passed",$time); else $error("T:%0t you failed",$time);

initial begin 
 @(posedge clk) a<=1; // T:05 :: 1st attempt results in vacuous pass
 @(posedge clk) a<=0; // T:15 :: $rose(a) is true for 2nd attempt
 @(posedge clk) b<=1; // T:25 :: 3rd attempt results in vacuous pass
 @(posedge clk) b<=0; // T:35 :: b[->1] matches. 2nd attempt passes at T:35
 @(posedge clk) a<=1; // T:45 :: 5th attempt results in vacuous pass
 @(posedge clk)       // T:55 :: Although $rose(a) is true
 `ifdef FINISH        // Since this is true by default,
   $finish()          // the antecedent wouldn't be evaluated at T:55
 `endif
      ;
 end

My expectation is that you should always be notified of a failure.

I believe the strong operator isn’t in effect for the attempt at T: 55.

Hence I wouldn’t expect a failure at end of simulation at T: 55 ( on 3 eda tools I observe output as T:35 you passed )

Once $finish() executes in active region the observed region wouldn’t execute i.e antecedent wouldn’t match and as a result consequent would start evaluation ( hence strong operator wouldn’t be active )

If I remove the `define FINISH at the top I observe the fail action block executing at T: 100 units ( across 3 EDA tools )

# run -all
# ** Info: T:35 you passed
#    Time: 35 ns Started: 15 ns  Scope: tb File: testbench.sv Line: 10
# exit
# ** Error: T:100 you failed