However for the 2 cases +define+M1 N without any +define the O/P differs .
I have a doubt related to the O/P using ’ s_until_with ’ operator ,
I observe a Failure at TIME : 86 ( unlike the O/P using ’ throughout ’ )
Since the Consequent hasn’t started evaluation ( it would start at Next Clock tick at TIME : 95 ) , my expectation is that failure for T : 86 shouldn’t be reported ( although the consequent is strong )
My expectation is that the O/P should be similar too since they are equivalent .
However for the solution via ’ s_until_with ’ operator I observe a Failure at
End of Simulation at TIME : 86 which isn’t present in the solution via ’ throughout ’
Any suggestions ?
My expectation is that the Failure at TIME : 86 shouldn’t occur in both cases since the consequent starts evaluation at the Next Clock tick .
I am still not clear on the working of ’ strong ’ Operator in the Consequent .
LRM 16.2.7 Implication Operator ::
For nonoverlapped implication, the evaluation of the consequent is described by two cases, depending on whether the implication is triggered by a nonempty match or by an empty match:
— If triggered by a nonempty match, the start point of the evaluation of the consequent property_expr is the clock tick after the end point of the match.
For the following example ( similar to the ’ strong ’ example above ) :: EDA_LINK2
Wouldn’t the consequent begin evaluation at the Next Clock tick after there is Non - Empty Match on the Antecedent ?
i.e Consequent would begin evaluation at TIME : 15 .
So if Simulation ends ( after TIME : 15 ) before the Consequent is True , the assertion would Fail due to ’ strong ’ Operator .
However if Simulation ends before Next Clock tick i.e before TIME : 15 ,
the Consequent hasn’t started evaluation yet and hence the ’ strong ’ Operator wouldn’t come into picture .
If you have
seq |=> strong (…) similarly for |->, #=#, #-#
the strength applies to the consequent only. Hence if the simulator has not entered the consequent there is no failure at the end of sim.
if the antecedent is in progress at end of Sim the assertion does not fail even if the property is strong.
A ##1 1 |-> strong(B ##1 c) ;
If end of Sim is at A then no failure
If end of Sim at the ##1 |->
Then B is evaluated. Regardless of B, assertion fails because of the strong.
(1) Simulation Ends after 1st Clock tick ( +define+M1 )
(2) Simulation Ends at exactly the 1st Clock tick ( +define+M2 )
(3) Simulation Ends after 2nd Clock tick ( +define+M3 )
(4) Simulation Ends at exactly the 2nd Clock tick ( +define+M4 )
**Antecedent isn’t in progress for all these 4 cases i.e
Evaluation of Antecedent is complete and it has Non - Empty match for ALL 4 cases** ,
Ideally should I observe a Failure for ALL 4 cases ?
**Also does the LRM touch upon this ? I tried looking in the LRM Section 16.12.2 Sequence property , however I couldn’t find anything related to this .
**
In reply to ben@SystemVerilog.us:
Could you please elaborate on “If end of Sim at the ##1 1 |->” Does it mean at exactly the ##1 OR between A being true and the next clock tick ?
@(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.
If A is sampled at time t2 at next @(posedge clk) and end-of-sim occurs at time t+ but before the next @(posedge clk), you execute the ##1 |-> strong(B)
but the consequent is not finished, of course. If end-of-sim occurs before and until the next @(posedge clk), the assertion should fail.
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.
@(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.
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 ?
In reply to hisingh:
You spent a lot of time on this $finish and failure.
I know that you want to understand it, and I provided a lot of explanations.
Typically though, I would think that the verification environment provided enough clocks for all the tests. I typically do not spend that much time on the strong qualification of properties, but that is me.
Ben