PSL Assertion, General Structure

The general structure of a PSL assertion has the following parts:

• A name or label that can be used for diagnostic output.
• A verification directive, such as assert.
• When to check, such as always or eventually!.
• The property to be checked: a state expression or a temporal logic expression.
• A qualifying guard, such as a clock edge or enable signal at which time we expect the assertion to hold.

• always a; // Predicate a holds all the time.
• never a; // The same as always not(a);
• eventually! a; // Predicate a will hold at some point in the future
• next a ; // Predicate a will hold in the next clock cycle (or other interval as qualified by the guard).