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 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