| 摘要 |
The result of a property based formal verification analysis of a circuit design may include at least one counterexample for each property that is violated, which a user can use to debug the circuit design. To assist the user in this debugging process, a debugging tool displays the counterexample trace annotated in such a way to illustrate where the property violation occurs and what parts of this trace contributes to the property violation. The debugging tool thus facilitates understanding of what parts of the counterexample trace are responsible for the property failure. The user can then select any of those contributing points as a starting point for further debugging. |
