Property

Form the conjunction of two properties. Equivalent to arg0 and arg1 and ... and argN in SVA.

Specify a clock relative to which all cycle delays within prop are specified. Equivalent to @(posedge clock) prop in SVA.

Indicate that a property will eventually hold at a future point in time. This is a strong eventually, so the property has to hold within a finite number of cycles. The property does not trivially hold by waiting an infinite number of cycles.

Equivalent to s_eventually prop in SVA.

Precondition the checking of a property (the consequent) on a sequence (the antecedent). Equivalent to the overlapping implication seq |-> prop in SVA.

Non-overlapping variant of Property.implication. Equivalent to seq ##1 true |-> prop and seq |=> prop in SVA.

Form the conjunction of two properties, where the start and end times of both sequences must be identical. Equivalent to arg0 intersect arg1 intersect ... intersect argN in SVA.

Negate a property. Equivalent to not prop in SVA.

Form the disjunction of two properties. Equivalent to arg0 or arg1 or ... or argN in SVA.

Check that a property holds untile another property holds. This operator is weak: the property will hold even if input always holds and condition never holds.