Simple Properties

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

Great training!! Excellent Instructor, Excellent facility ...Met all my expectations.
Lockheed Martin

View more references