DIGITAL CIRCUIT VERIFICATION WITH AUTOMATED SPECIFICATION ENUMERATION

A method for automatically generating a set of specifications against which a model of the digital circuit can be verified. In one embodiment, the method includes an initial step in which a specification class that corresponds to a type of behavior of the digital circuit is defined. A set of specification formulae that satisfies the defined specification class is then enumerated. Each formula in the set of formulae is then applied to the model of the digital circuit to determine whether the digital circuit satisfies the corresponding formula. The definition of the specification class preferably includes a set of input conditions, a set of output or response conditions, and a temporal component. Preferably, the enumeration of the specification formulae includes all specification formulae that satisfy the specification class. The application of the set of formulae to the model of the digital circuit is preferably achieved with a verification engine such as a model checker. Preferably, the specification formulae are expressed in temporal logic such as computational tree logic (CTL). In one embodiment the specification formulae are quantified such that the digital circuit satisfies a formula only if the formula always holds true. In another embodiment, the specification formulae are quantified such that the digital circuit satisfies the formula if the formula ever holds true. The preferred embodiment of the invention preferably includes displaying the results achieved by applying the specification formulae to the digital circuit models.