Patent ID: 7421669
Filing Date: 2008-09-02
Classification: G06F

Abstract:
1. A method for generating a constraint for use in the verification of an integrated circuit design, comprising: identifying a target in a netlist representation (N) of the integrated circuit design, wherein the netlist representation N includes sequential gates, random gates, or combinational logic; wherein said target is a vector including multiple target gates; Initializing a constraint node and appending the constraint node to N, creating an over-approximate abstraction (N′) of the netlist representation N by modifying the netlist representation N through replacement of a sequential gate in N with a random gate; computing a space state S′ of N′ including enumerating the states of N′ from which it is possible to assert the identified target, wherein said enumerating includes: enumeration a first set of states that can hit the target in 0 time steps by building a binary decision diagram (BDD) for a function of the target and quantifying out random gates; enumerating a second set of states that can hit the target in “i” time steps by substituting a next state function for a corresponding register in a BDD of the function of the target in an “i-1” time step and then quantifying out the random gates; deriving a constraint space C′ from the state space S′, wherein C′ is the complement of S′; and synthesizing a constraint from constraint space C′ and applying said constraint to said integrated circuit design.