Parametric reduction of sequential design
AssigneeInternational Business Machines Corporation
InventorsJason Raymond Baumgartner, Geert Janssen, Hari Mony, Viresh Paruthi
Life of this patent
Estimating the term…
Abstract
A method, system and computer program product for performing parametric reduction of sequential designs is disclosed. The method comprises receiving an initial design including one or more primary inputs, one or more targets, and one or more state elements. A cut of the initial design including one or more cut gates is identified, and a relation of one or more values producible to the one or more cut gates in terms of the one or more primary inputs and the one or more state elements is computed. The relation is synthesized to form a gate set, and an abstracted design is formed from the gate set. Verification is performed on the abstracted design to generate verification results.
Claims13
A system for reducing sequential digital designs, said system comprising:
- means for 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
- means for 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;
- means for 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;
- means for synthesizing said relation to form a gate set, wherein said gate set is behaviorally equivalent to said cut of said initial design;
- means for forming an abstracted design by replacing said cut of said initial design with said gate set;
- and
- means for performing verification on said abstracted design to generate verification results.
A computer program product for reducing sequential digital designs, said computer program product comprising:
- a computer-readable storage device;
- instructions on the computer-readable storage device and executable by a processor for 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;
- instructions on the computer-readable storage device executable by a processor for 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 mm-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;
- instructions on the computer-readable storage device executable by a processor for 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;
- instructions on the computer-readable storage device executable by a processor for means for synthesizing said relation to form a gate set, wherein said gate set is behaviorally equivalent to said cut of said initial design;
- instructions on the computer-readable storage device executable by a processor for forming an abstracted design by replacing said cut of said initial design with said gate set;
- and
- instructions on the computer-readable storage device executable by a processor for performing verification on said abstracted design to generate verification results.
Dependencies are inferred from the claim text.