Formal Verification of Temporal Properties Expressed Using Local Variables
AssigneeSynopsys, Inc.
InventorsRoy Armoni, Dana Fisman Ofek, Naiyong Jin
Life of this patent
Estimating the term…
Abstract
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.
Claims19
A method for verifying whether a hardware design satisfies a temporal property, the method comprising a processor executing the steps of:
- accessing an HDL description of the hardware design;
- accessing the temporal property, the temporal property expressed using a local variable;
- determining whether the temporal property is a member of a practical subset of temporal properties, 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.
A method for verifying whether a hardware design satisfies a temporal property, the method comprising a processor executing the steps of:
- accessing an HDL description of the hardware design;
- accessing the temporal property, the temporal property expressed using a local variable;
- and
- for any temporal property that possesses an alternating automaton with no conflicts:
- formally verifying whether the hardware design satisfies the temporal property.
A system for verifying whether a hardware design satisfies a temporal property, the system comprising:
- means for accessing an HDL description of the hardware design;
- means for accessing the temporal property, the temporal property expressed using a local variable;
- means for determining whether the temporal property is a member of a practical subset of temporal properties, wherein every member of the practical subset possesses an alternating automaton with no conflicts;
- and
- means for (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.
Dependencies are inferred from the claim text.