Patent ID: 7367002
Filing Date: 2008-04-29
Classification: G06F

Abstract:
1. A method for reducing sequential digital designs, said method comprising: receiving an initial design including one or more primary inputs, one or more targets that correlate to one or more properties of said initial design that require verification, and one or more state elements; identifying a cut of said initial design including one or more cut gates by labeling each invariant target, constraint gate, next-state, and initial-value gate as a sink, every RANDOM gate as a source, and utilizing min-cut analysis between said labeled sources and sinks to find a minimal set of nodes at a cutpoint, and wherein said cut has minimal size with respect to a number of gates sourcing crossing edges of said cut; computing a relation of one or more values producible to said one or more cut gates in terms of said one or more primary inputs and said one or more state elements; synthesizing said relation to form a gate set, wherein said gate set is behaviorally equivalent to said cut of said initial design; forming an abstracted design by replacing said cut of said initial design with said gate set; and performing verification on said abstracted design to generate verification results.