| 摘要 |
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.
|
