SystemVerilog Assertion
Part 4: Property Layer
Prev: Property Types |
Next: Recursive Property
Implication Operators
As we mentioned earlier, an implication refers to a situation in which
in order for a behavior to occur, a preceding sequence must have occured.
This preceding sequence in this case is known as antecedent.
The suceeding behavior is known as consequent. Thus, in other
words, an antecedent sequence implies a consequent property
expression. This is shown by the following notation:
antecedent |-> consequent;
The property top_prop is an example that demonstrates this.
In this example, seq0 is a sequence that as an antecedent
implies the consequent property expression prop0. The sequence
seq0 matches when signal sig_a appears two clocks before
sig_b. The property prop0 consists of another sequence
seq1 that matches when signal sig_d follows sig_d
after 5 clock ticks.
property top_prop;
seq0 |-> prop0;
endproperty
property prop0;
seq1;
endproperty
sequence seq0;
sig_a ##2 sig_b;
endsequence
sequence seq1;
sig_c ##5 sig_d;
endsequence
Equivalently, top_prop can also be written as:
property top_prop;
(sig_a ##2 sig_b) |-> (sig_c ##5 sig_d);
endproperty
without any change in the property definition.
A closer look into an implication type property definition reveals
several of its characteristics.
- An antecedent sequence (such as seq0 in the above example) in
general may match zero, one or more than one time.
- If there is no match for the antecedent sequence, that is, if seq0
never occurs, even then the property top_prop evaluates to be true.
This is known as Vacuous Success.
- The end point of matching an antecedent sequence is the start point
of evaluation of the consequent property expression.
- An antecedent may match even when the consequent is being evaluated
for a previous match. Each match of the antecedent will result in
separate thread of evaluation for the consequent. As an example, let us
assume that seq0 has a match. This results in a match of prop0.
Let us further assume that sig_c is asserted and the only other
requirement for a match of prop0 (or of seq1) is an
assertion of sig_d after 5 clock ticks. When two of these five clock
ticks are over, seq0 has another match. In this case, a separate
thread for evaluation of top_prop will be created for this second
match of seq0. The whole property evaluates to be true if and only
if all such threads return a true value between a given start and end point
pair.
The Implication Operator '|=>'
For the implication operator |=> the consequent property expression is
evaluated one clock tick after the antecedent sequence ends. This means
a property expression
antecedent |=> consequent;
can also be written as
antecedent ##1 `true |-> consequent;
More Examples of Implication
Here are some more examples of implication operators for various types
of property expressions.
Clocking Event
An antecedent sequence and a consequent property expression both may
have a clocking event associated with them.
property clk_implication_example;
@(posedge src_clk) seq0 |=> @(posedge dst_clk) prop0;
endproperty
Other Types of Property Expressions
An implication can be used along with any other type of property
expression. For instance, an 'if...else' type property expression
can nest implication.
property top_prop;
if (sig_back2back)
seq0 |-> prop0;
else
seq0 |=> prop0;
endproperty
Prev: Property Types |
Next: Recursive Property
|