KnowHow
Free Technical Resources

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 wheneverPRECONDITION 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 ifaholds in a cycle and bholds in the following cycle. The symbol|-> placed between the two sequences denotessuffix 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