Contradictory antecedent debugging in bounded model checking

In the context of formal verification Bounded Model Checking (BMC) has shown to be very powerful for large industrial designs. BMC is used to check whether a circuit satisfies a temporal property or not. Typically, such a property is formulated as an implication. In the antecedent of the property the verification engineer specifies the assumptions about the design environment and joins the respective expressions by logical AND. However, the overall conjunction may have no solution, i.e. the antecedent is contradictory. Since in this case a property trivially holds this situation has to be avoided. Furthermore, the root cause of a contradictory antecedent has to be identified which is a manual and very time-consuming process. In this paper we propose a fully automatic approach for presenting all reasons of a contradictory antecedent to the verification engineer, i.e. the approach pinpoints to the subexpressions in the antecedent that form a contradiction. Hence, our approach redu...

• Type: Conference
• Year: 2009
• Where: GLVLSI
• Authors: Daniel Große, Robert Wille, Ulrich Kühne, Rolf Drechsler
• Keywords: Contradictory Antecedent, Formal Verification, GLVLSI 2009, Model Checking, VLSI