Device, system and method for formal verification
View Patent ↗Device, system and method of efficient automata-based implementation of liveness properties for formal verification. A system according to embodiments of the invention includes a property transformation module to receive an assume verification directive on a liveness property in a property specification language, and to translate the property a fairness statement that uses a deterministic automaton. The deterministic automaton is exponential in the size of the input property. The assume verification directive may be transformed into a strong suffix implication in the property specification language.
1. A method for verification of a design, comprising:
receiving a specification that the design is expected to satisfy subject to a group of one or more properties that are assumed to apply in the verification, the group comprising a liveness property, stating that a certain event will eventually occur in a state space of the design;
adding to the design a deterministic automaton having a set of states and representing an occurrence of the event over the states;
replacing the liveness property in the group of the properties that are assumed to apply in the verification with a fairness constraint, requiring that the states in the set must be traversed infinitely often as the design traverses the state space; and
applying a computerized model checker to verify the design, including the added deterministic automaton, subject to the fairness constraint.
2. The method according to claim 1 , wherein adding the deterministic automaton comprises constructing the deterministic automaton corresponding to a suffix implication in which a prefix comprising a first sequence of the states is followed by a suffix comprising a second sequence of the states.
3. The method according to claim 2 , wherein the suffix implication is a strong implication, such that when the prefix occurs, the suffix is then required to eventually occur.
4. The method according to claim 2 , wherein constructing the deterministic automaton comprises constructing nondeterministic automata representing the first and second sequences of the states, and converting the nondeterministic automata into the deterministic automaton.
5. The method according to claim 1 , wherein the one or more properties are received in a property specification language.
6. A system for verification of a design, comprising:
a memory, which is configured to store program code; and
one or more processors, which are configured to receive a specification that the design is expected to satisfy subject to a group of one or more properties that are assumed to apply in the verification, the set comprising a liveness property, stating that a certain event will eventually occur in a state space of the design, to add to the design a deterministic automaton having a set of states and representing an occurrence of the event over the states, to replace the liveness property in the group of the properties that are assumed to apply in the verification with a fairness constraint, requiring that the states in the set must be traversed infinitely often as the design traverses the state space, and to apply a model checking engine to verify the design, including the added deterministic automaton, subject to the fairness constraint.
7. The system according to claim 6 , wherein the deterministic automaton corresponds to a suffix implication in which a prefix comprising a first sequence of the states is followed by a suffix comprising a second sequence of the states.
8. The system according to claim 7 , wherein the suffix implication is a strong implication, such that when the prefix occurs, the suffix is then required to eventually occur.
9. The system according to claim 7 , wherein the deterministic automaton is produced by constructing nondeterministic automata representing the first and second sequences of the states, and converting the nondeterministic automata into the deterministic automaton.
10. The system according to claim 6 , wherein the one or more properties are received in a property specification language.
11. A computer program product comprising a computer-readable storage medium including a computer-readable program, wherein the computer-readable program when executed on a computer causes the computer to receive a specification that the design is expected to satisfy subject to a group of one or more properties that are assumed to apply in the verification, the set comprising a liveness property, stating that a certain event will eventually occur in a state space of the design, to add to the design a deterministic automaton having a set of states and representing an occurrence of the event over the states, to replace the liveness property in the group of the properties that are assumed to apply in the verification with a fairness constraint, requiring that the states in the set must be traversed infinitely often as the design traverses the state space, and to apply a model checking engine, which when executed, causes the computer to verify the design, including the added deterministic automaton, subject to the fairness constraint.
12. The product according to claim 11 , wherein the deterministic automaton corresponds to a suffix implication in which a prefix comprising a first sequence of the states is followed by a suffix comprising a second sequence of the states.
13. The product according to claim 12 , wherein the suffix implication is a strong implication, such that when the prefix occurs, the suffix is then required to eventually occur.
14. The product according to claim 12 , wherein the deterministic automaton is produced by constructing nondeterministic automata representing the first and second sequences of the states, and converting the nondeterministic automata into the deterministic automaton.
15. The system according to claim 11 , wherein the one or more properties are received in a property specification language.