Question

The formal semantics in Annex H defines whether a given property holds on a given behavior. How the outcome of this evaluation relates to the design depends on the behavior that was analyzed. In dynamic verification, only behaviors that are finite in length are considered. In such a case, SystemVerilog defines four levels of satisfaction of a property:

Holds strongly:

• no bad states have been seen
• all future obligations have been met
• the property will hold on any extension of the path

Holds (but does not hold strongly):

• no bad states have been seen
• all future obligations have been met
• the property may or may not hold on a given extension of the path

Pending:

• no bad states have been seen
• future obligations have not been met
• the property may or may not hold on a given extension of the path

Fails:

• a bad state has been seen
• future obligations may or may not have been met
• the property will not hold on any extension of the path