Implication Operator
An implication operator makes a property conditional. The consequent is required only when the antecedent sequence matches, which makes implication useful for rules such as: when a request occurs, an acknowledgement must follow.
An SVA implication divides a property into a trigger and a required response. The expression on the left is the antecedent, and the expression on the right is the consequent.
Syntax:
sequence_exp |-> property_exp
sequence_exp |=> property_expThe LHS operand sequence_exp is called an antecedent. It describes the event or sequence that activates the check.
The RHS operand property_exp is called a consequent. It describes what must be true after the antecedent matches.
The two operators differ only in the starting point of the consequent. |-> starts it on the antecedent’s completion clock, whereas |=> starts it on the next sampled clock.
How an Implication Is Evaluated
At each sampling clock, the assertion checks whether a new antecedent attempt can match.
If the antecedent matches, the consequent becomes an obligation that must be satisfied.
If the required consequent does not match, that assertion attempt fails.
If the antecedent does not match, the consequent is not required for that attempt; this is called a vacuous success.
An assertion can have several attempts active at the same time. For example, if the antecedent begins on several consecutive clocks, each successful antecedent match creates its own consequent obligation.
Type of Implication
SystemVerilog provides overlapped and non-overlapped implication. The correct operator depends on whether the response is allowed on the antecedent’s completion edge or must begin one edge later.
- Overlapped implication
- Non-overlapped implication
Overlapped implication
The overlapped implication operator is denoted by the |-> symbol.
The evaluation of the consequent starts immediately on the same clock cycle if the antecedent holds true.
The consequent is not evaluated if the antecedent is not true.
Example:
property prop;
@(posedge clk) valid |-> (a ##3 b);
endproperty
The property is sampled on every positive edge of clk. Here, the antecedent is the single-cycle expression valid, so it completes on the same edge on which valid is sampled as true.
Because the operator is |->, the consequent (a ##3 b) begins immediately on that completion edge. Therefore, a must be true on the same positive edge as valid. The sequence then counts three more positive edges and requires b on the third edge.
For one attempt, think of the edge where valid = 1 as relative cycle 0. Both valid and a are required at cycle 0, and b is required at relative cycle 3. If valid = 0, this attempt does not require either a or b.
Non-overlapped implication
The non-overlapped implication operator is denoted by the |=> symbol.
The evaluation of the consequent starts in the next clock cycle if the antecedent holds true.
The consequent is not evaluated if the antecedent is not true.
Example:
property prop;
@(posedge clk) valid |=> (a ##3 b);
endproperty
The antecedent valid still completes on the edge where it is sampled as true. However, |=> begins (a ##3 b) on the next positive edge, not on the valid edge.
Using the valid edge as relative cycle 0, a is required at cycle 1. The ##3 delay is counted from the edge where a is checked, so b is required at relative cycle 4.
The non-overlapped operator is appropriate when the specification says after, on the next cycle, or beginning one cycle later. If valid = 0, no consequent obligation is created for that attempt.
Overlapped and Non-overlapped Timing
Property form | Timing meaning when the antecedent completes at cycle 0 |
A |-> B | B starts at cycle 0, on the same edge that completes A |
A |=> B | B starts at cycle 1, one sampled edge after A completes |
A |-> ##1 B | B starts at cycle 1; for a common single-clock case, this expresses the same one-cycle shift as A |=> B |
The word overlapped refers to the shared boundary clock: the last clock of the antecedent is also the first clock of the consequent. Non-overlapped implication inserts one clock between those two starting points.
Simple Request and Acknowledgement Example
The following properties show how a one-character difference changes the requirement.
property p_ack_same_cycle;
@(posedge clk) req |-> ack;
endproperty
property p_ack_next_cycle;
@(posedge clk) req |=> ack;
endpropertyIn p_ack_same_cycle, a sampled req = 1 requires ack = 1 on that same positive edge. In p_ack_next_cycle, a sampled req = 1 requires ack = 1 on the next positive edge.
Neither property requires anything from ack on an edge where req = 0. If the design must also restrict early or unexpected acknowledgements, that is a separate requirement and should be checked with another property.
Implication with a Multi-cycle Antecedent
The timing boundary is based on the end of the complete antecedent, not necessarily the clock where the antecedent started.
property p_ack_same_cycle;
@(posedge clk) req |-> ack;
endproperty
property p_ack_next_cycle;
@(posedge clk) req |=> ack;
endpropertySuppose req matches at relative cycle 0 and grant matches at cycle 1. The antecedent (req ##1 grant) completes at cycle 1. Because |-> is overlapped, ready must also be true at cycle 1.
If the operator is changed to |=>, ready is checked at cycle 2. Always locate the antecedent’s completion edge first; then apply the implication operator to find the consequent’s starting edge.
Common Mistakes
- Treating |-> as next-cycle implication. Its consequent starts on the antecedent’s completion edge.
- Treating |=> as same-cycle implication. It begins the consequent one sampled edge later.
- Counting from the start of a multi-cycle antecedent instead of from the edge where that antecedent completes.
- Assuming an assertion pass proves the response was checked, even though the antecedent may never have matched.
- Using implication when the consequent must be checked unconditionally on every sampling edge.
- Combining several unrelated requirements into one long property, which makes timing failures difficult to diagnose.
SystemVerilog Assertions