Method and device for circuit verification
When designing digital circuits, the specification of the circuit is used to formulate properties and to check the applicability thereof using a model of the circuit. A verifier is employed and uses the model to determine whether a property is applicable by seeking a counterexample to which the property does not apply. Any counterexample appearing is evaluated to determine whether it is caused by a defective model or whether it should have been avoided by reformulating the property within the scope of the specification. Which exact part of the property led to the counterexample is determined when one appears. If a plurality of times is possible for a part of the property, the instant(s) at which specific events in the parts of the property lead to the counterexample is determined. A developer can evaluate the counterexample much more quickly using this information, so the development process can be accelerated.
1. A method of verifying a digital circuit using a model of the circuit and at least one required property of the circuit, which indicates whether, in the presence of an assumption of the property, an assertion of the property is applicable, the assumption and the assertion describing behavior of the circuit, with which applicability of the property is checked in that at least one counterexample to the at least one property is sought, the counterexample describing the behavior of the circuit and contradicting the assertion, wherein, on appearance of the counterexample, it is determined which part of the assertion contradicts the counterexample found.
2. The method according to claim 1 , wherein the applicability of the property is checked by a formal checker.
3. The method according to claim 1 , wherein the applicability of the property is checked by simulation.
4. The method according to claim 1 , wherein at least one of the assertion and the assumption of the property describes the behavior of the circuit as a function of time, changes in a state of the circuit being able to appear at different times, and, on appearance of the counterexample, instants at which changes in a state of the property contradicts the assertion are determined.
5. The method according to claim 4 , wherein the determined instants together with the assumption of the property are displayed.
6. The method according to claim 1 , wherein the determined part of the assertion that contradicts the counterexample is displayed together with the property.
7. The method according to claim 1 , wherein evaluations of state expressions are displayed directly at a corresponding point within the property at any desired syntactical hierarchical level of properties.
8. The method according to claim 1 , wherein at least one of the assumption and the assertion of the property comprises at least one macro in which descriptions of the behavior of the circuit are assembled.
9. An apparatus for verifying a digital circuit using a model of the circuit and at least one required property of the circuit which indicates whether, in the presence of an assumption of the property, an assertion of the property is applicable, the assumption and the assertion describing behavior of the circuit, the apparatus comprising one or more data processing devices which are configured such that the one or more data processing devices check applicability of the property by seeking at least one counterexample to the at least one property, the counterexample describing the behavior of the circuit and contradicting the assertion, and, on appearance of the counterexample, the one or more data processing devices determine which part of the assertion is contradicted by the counterexample found.
10. The apparatus according to claim 9 , wherein the one or more data processing devices comprise a formal checker that checks the applicability of the property.
11. The apparatus according to claim 9 , wherein the one or more data processing devices check the applicability of the property by simulation.
12. The apparatus according to claim 9 , wherein at least one of the assertion and the assumption of the property describes the behavior of the circuit as a function of time, changes in a state of the circuit being able to appear at different times, and, on appearance of the counterexample, instants at which changes in a state of the property contradicts the assertion are determined.
13. The apparatus according to claim 12 , further comprising a display that displays the determined instants together with the assumption of the property.
14. The apparatus according to claim 9 , further comprising a display that displays the determined part of the assertion that contradicts the counterexample together with the property.
15. The apparatus according to claim 9 , further comprising a display that displays evaluations of state expressions directly at a corresponding point within the property at any desired syntactical hierarchical level of properties.
16. The apparatus according to claim 9 , wherein at least one of the assumption and the assertion of the property comprises at least one macro in which descriptions of the behavior of the circuit are assembled.
17. A digital storage medium comprising control signals which can be read out electronically and are able to cooperate with a programmable computer device such that the computer device performs a method of verifying a digital circuit using a model of the circuit and at least one required property of the circuit, which indicates whether, in the presence of an assumption of the property, an assertion of the property is applicable, the assumption and the assertion describing behavior of the circuit, with which applicability of the property is checked in that at least one counterexample to the at least one property is sought, the counterexample describing the behavior of the circuit and contradicting the assertion, wherein, on appearance of the counterexample, it is determined which part of the assertion contradicts the counterexample found.
18. The digital storage medium according to claim 17 , wherein the control signals include signals that permit the computer device to perform a method in which the applicability of the property is checked by a formal checker.
19. The digital storage medium according to claim 17 , wherein the control signals include signals that permit the computer device to perform a method in which the applicability of the property is checked by simulation.
20. The digital storage medium according to claim 17 , wherein the control signals include signals that permit the computer device to perform a method in which at least one of the assertion and the assumption of the property describes the behavior of the circuit as a function of time, changes in a state of the circuit being able to appear at different times, and, on appearance of the counterexample, instants at which changes in a state of the property contradicts the assertion are determined.
21. The digital storage medium according to claim 20 , wherein the control signals include signals that permit the computer device to perform a method in which the determined instants together with the assumption of the property are displayed.
22. The digital storage medium according to claim 17 , wherein the control signals include signals that permit the computer device to perform a method in which the determined part of the assertion that contradicts the counterexample is displayed together with the property.
23. The digital storage medium according to claim 17 , wherein the control signals include signals that permit the computer device to perform a method in which evaluations of state expressions are displayed directly at a corresponding point within the property at any desired syntactical hierarchical level of properties.
24. The digital storage medium according to claim 17 , wherein the control signals include signals that permit the computer device to perform a method in which at least one of the assumption and the assertion of the property comprises at least one macro in which descriptions of the behavior of the circuit are assembled.