Assertion failure using strong property

[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