Patent ID: 7290229

Claim:
A method for verifying a design through symbolic simulation, said method comprising: creating one or more binary decision diagram variables for one or more inputs of a next state of a design containing one or more state variables; building a binary decision diagram for a first node of one or more nodes in said design; generating a binary decision diagram for an initial state function of one or more state variables of said design; synthesizing one or more binary decision diagrams for one or more constraints; accumulating a set of constraint values over time by combining said binary decision diagrams for said one or more constraints with a set of previously generated binary decision diagrams for a set of constraints previously used in one or more previous time-steps; constructing a binary decision diagram for said next state function of said one or more state variables in said design; updating said one or more state variables in said design by propagating said binary decision diagram for said next state function to said one or more state variables; calculating a set of binary decision diagrams for said one or more targets in the presence of said one or more constraints; constraining said set of binary decision diagrams for one or more targets; and verifying said design by determining whether said one or more targets were hit.