Throughout V/S s_until_with

In reply to ben@SystemVerilog.us:

@(posedge clk) A ##1 1 |-> strong(B ##1 c) ;
Assertion are sampled at @(posedge clk).

  • If A is sampled at time t, and end-of-sim occurs at time t+ but before the next @(posedge clk) the consequent is not executed SInce the clocking event has not occurred.

So for the code :: EDA_LINK2

For +define+M1 and +define+M2 as Simulation ends before consequent is evaluated at TIME : 15 ,the assertion is Incomplete . Hence there is No O/P

  • Now if the $finish occurs in the active region, and since the assertions are executed in the Observed Region, the assertions to be executed at that time tick are not processed; The $finish is executed in a region before the processing of the assertions.

For +define+M4 as $finish() occurs in Active region whereas assertions are executed in Observed Region ,
the assertions are not processed and hence we Observe No O/P

Am I correct with my understanding of the O/P associated with the 3 scenarios ?