The simplest form of property in PSL takes the form of a combinational boolean condition that must be continuously true.
assert always CONDITION;
However, this form of property is not particularly useful, since it is vulnerable to race hazards. It is more common to introduce a sampling event or clock.
assert (always CONDITION) @(posedge clk);
It is also possible to define a default clock and thus avoid the need to repeat the explicit clock operator @ in every single assertion.
default clock = (posedge clk);
assert always CONDITION;
It is more common still for a property to take the form of an implication, with a pre-condition that must be satisfied before the main condition is checked.
assert always PRECONDITION -> CONDITION;
This asserts that whenever PRECONDITION holds, CONDITION must hold in the same cycle. The symbol -> denotes logical implication.
It is common (though not essential) for the precondition and condition within the assertion to each take the form of temporal sequences enclosed in braces.
assert always {a;b} |-> {c;d};
The sequence {a;b} holds if a holds in a cycle and b holds in the following cycle. The symbol |-> placed between the two sequences denotes suffix implication, meaning that if the first sequence holds, the second sequence must hold also, with the two sequences overlapping by a single cycle.
Finally, it is common for properties to include a terminating condition (such as a reset) which will cause the property to be abandoned mid-way through the matching of a temporal sequence.
assert (always ({a;b} |-> {c;d} abort reset))
@(posedge clk);
When the reset goes true, the obligation for the suffix implication to hold is removed, whether or not there has been a partial match between the property and the actual state of the design.
Next: Temporal Logic
©Copyright 2005-2019 Doulos. All rights reserved.
