Universality Property Pattern
Intent:
The Universality Property Pattern is used to specify portions of a design model’s verification execution that contains states or events1 that have a desired property. Also known as Henceforth and Always.
Motivation:
In the verification execution of an RTL state-based model, there are often specific conditions (i.e., events or states) that must always hold true at every clock cycle. As an example, let us consider the case of a FIFO of size N, where a FIFO controller keeps track of the next available position in the FIFO storage through a write counter (representing locations 0 through N-1). If the write counter indicates that the current FIFO depth is N-1 (that is, the FIFO is currently full), then the FIFO full status bit should be set. Similarly, if the FIFO depth is less than N-1, then the FIFO full status bit should not be set.
Applicability:
Any condition (i.e., event or state) that can be expressed as a Boolean equation and describes desirable state or behavior in a design for each clock cycle can be formulated into a Universality Property.
To view the entire Universality Property Pattern 
, please login with your Verification Academy Full Access account.
