Method and system for optimized handling of constraints during symbolic simulation
First Claim
1. 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.
6 Assignments
0 Petitions
Accused Products
Abstract
A method for verifying a design through symbolic simulation is disclosed. The method comprises creating one or more binary decision diagram variables for one or more inputs in a design containing one or more state variables and building a binary decision diagram for a first node of one or more nodes of the design. A binary decision diagram for the initial state function of one or more state variables of the design is generated and the design is subsequently initialized. Binary decisions diagrams for one or more constraints are synthesized. A set of constraint values is accumulated over time by combining the binary decision diagrams for the 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. A binary decision diagram for the next state function of the one or more state variables in the design is constructed in the presence of the constraints. The one or more state variables in the design are updated by propagating the binary decision diagram for the next state function to the one or more state variables and a set of binary decision diagrams for the one or more targets in the presence of the one or more constraints is calculated. The set of binary decision diagrams for one or more targets is constrained and the design is verified by determining whether the one or more targets were hit.
18 Citations
20 Claims
-
1. 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. - View Dependent Claims (2, 3, 4, 5, 6, 7)
-
-
8. A system for verifying a design through symbolic simulation, said system comprising:
-
means for building a binary decision diagram for a first node of one or more nodes in a design containing one or more state variables; means for creating one or more binary decision diagram variables for one or more inputs of a next state of said design; means for generating a binary decision diagram for an initial state function of one or more state variables of said design; means for constructing a binary decision diagram for said next state function of said one or more state variables in said design; means for 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; means for synthesizing one or more binary decision diagrams for one or more constraints; means for 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; means for calculating a set of binary decision diagrams for said one or more targets in the presence of said one or more constraints; means for constraining said set of binary decision diagrams for one or more targets; and means for verifying said design by determining whether said one or more targets were hit. - View Dependent Claims (9, 10, 11, 12, 13, 14)
-
-
15. A computer program product in a computer-readable medium for verifying a design through symbolic simulation, said computer program product comprising:
-
a computer-readable medium; instructions on the computer-readable medium for building a binary decision diagram for a first node of one or more nodes in a design containing one or more state variables; instructions on the computer-readable medium for creating one or more binary decision diagram variables for one or more inputs of a next state of said design; instructions on the computer-readable medium for generating a binary decision diagram for an initial state function of one or more state variables of said design; instructions on the computer-readable medium for constructing a binary decision diagram for said next state function of said one or more state variables in said design; instructions on the computer-readable medium for 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; instructions on the computer-readable medium for synthesizing one or more binary decision diagrams for one or more constraints; instructions on the computer-readable medium for 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; instructions on the computer-readable medium for calculating a set of binary decision diagrams for said one or more targets in the presence of said one or more constraints; instructions on the computer-readable medium for constraining said set of binary decision diagrams for one or more targets; and instructions on the computer-readable medium for verifying said design by determining whether said one or more targets were hit. - View Dependent Claims (16, 17, 18, 19, 20)
-
Specification