Formal verification of temporal properties expressed using local variables

摘要

A certain subset of temporal properties defined using local variables can be formally verified with complexity of PSPACE or less. A subset with this characteristic, referred to as a practical subset, is therefore feasible to formally verify. For example, it can be shown that temporal properties that possess an alternating automaton with no conflicts fall within a practical subset. Temporal properties are analyzed to determine whether they are a member of the practical subset. Members of the practical subset can then be feasibly formally verified.

主权项

1. A method for verifying whether a hardware design satisfies a temporal property, the method comprising a processor executing the steps of:
accessing a hardware description language (HDL) description of the hardware design; accessing the temporal property, the temporal property expressed using a local variable; creating a parse tree for the temporal property; determining whether the temporal property is a member of a practical subset of temporal properties based on analyzing the parse tree, wherein every member of the practical subset possesses an alternating automaton with no conflicts; and (a) formally verifying whether the hardware design satisfies the temporal property for all such temporal properties that are determined to be members of the practical subset; or (b) not formally verifying whether the hardware design satisfies the temporal property for all such temporal properties that are determined not to be members of the practical subset.