if expression in property

The if(expression) is used to select property expressions based on the if condition.

It is generally used in properties with implication operator-based assertions.

Syntax:

if(expression)
  <property_exp1>
else
  <property_exp2>;

if expression in property example

A request selects which acknowledgement must arrive and how long the assertion waits for it.

property prop;
  @(posedge clk) (req1 || req2) |-> 
  if(req1)
    (##1 ack1)
  else
   (##2 ack2);
endproperty

The antecedent (req1 || req2) first checks whether at least one request is high. Because |-> is overlapped, the if condition is selected on that same sampled clock.

If req1 = 1, the assertion checks ack1 one clock later.

If req1 = 0 and req2 = 1, the assertion checks ack2 two clocks later.

If both requests are 1, the req1 branch is selected because the condition is if(req1).

If both requests are 0, the antecedent is false and no acknowledgement branch is required for that attempt.

The else branch does not mean that req2 is always checked explicitly. It is selected when the antecedent matched but req1 is false; in that case, req2 must have been the request that made the antecedent true.

ended in sequence

The endpoint of sequence detection returns true if the previously started sequence (another sequence) reaches the endpoint when the current sequence is under execution at that particular point in time else it returns false.

Syntax:

<sequence>.ended

ended in sequence example

seq2 requires its timing point to align with the completion of seq1, and then checks ack one clock later.

sequence seq1;
  @(posedge clk) $rose(en) ##1 req1 ## req2;
endsequence

sequence seq2;
  @(posedge clk) reset ##2 seq1.ended ##1 ack;
endsequence

For seq1, suppose $rose(en) matches at cycle S. Then req1 must be true at S+1 and req2 must be true at S+2. Therefore, seq1.ended is true at S+2.

For seq2, suppose reset matches at cycle R. The sequence checks seq1.ended at R+2 and checks ack at R+3. For seq2 to match, the completion clock S+2 must be the same clock as R+2.

If seq1 completes earlier or later than the required R+2 clock, seq1.ended is false at that point and seq2 does not match. This makes .ended useful for synchronizing the endpoints of related sequences.

Points to Remember

An if expression selects one property branch; it does not check both branches.
The branch condition is sampled when the property reaches the if expression.
.ended is true only on the named sequence’s completion clock.
.ended observes an existing sequence attempt; it does not launch the sequence.