Motorola Corporation

Microelectronics and Computer Technology Corporation

Carl P Pixley

Hyunwoo Cho

Andrew Kenneth Martin

Jesse R Wilson

Ralph C McGarity

Richard S Raimi

Stephen Kurt Shultz

Bernard F Plessier

Jun Yuan

Jaehong Park

Matthew J Kaufmann

Hillel Miller

A method for verifying an integrated circuit design using constraint information to develop a weighted data structure. In one embodiment, a binary decision diagram (BDD) includes a plurality of nodes (,and,) representing signals and states in the circuit, and each node has a branching probability based on user-defined weights. The BDD represents the intersection of the input space and state space which satisfies the constraints. Current state information resulting from simulation is used to dynamically adjust the branching probabilities of the BDD on the fly. In one embodiment, the constraint information is applicable for formal verification of a portion of the circuit. In another embodiment, a simulation controller (,) receives design and constraint information and generates the program to control simulator (,).

Method and apparatus for integrated circuit design verification

A method is presented for performing model checking of an integrated circuit design that avoids the need for construction of an environment model by the use of constraints (44). The method supports an assume/guarantee style of reasoning to ensure that the constraints (44) are a true abstraction of the actual environment in which the integrated circuit is designed to operate. The constraints (44) may be used to provide primary inputs for a design under analysis (DUA) (16). Also, the constraints (44) may refer to internal states and to outputs of the DUA (16). In addition, monitors (42) may be used to monitor the inputs to the DUA (16). The constraints (44) can then be used with the monitors (42) to specify complex sequential environment properties.

Method for performing model checking in integrated circuit design

The present invention determines whether two design files have identical functionality by attempting to create a binary decision diagram (BDD) for corresponding verification output pairs(302). When the BDD creations are not successful for all evaluated output pairs a set of cutpoint pair candidates are identified(303). An automatic test program generator (ATPG) is used to determine whether or not the cutpoint pair candidates are invalid cutpoints(304). The invalid cutpoints are removed from the set of cutpoint pair candidates(305). A cutpoint pair candidate having known support is selected(306). An exclusive-or of the outputs of the selected candidate is formed (307). A BDD for the resulting XOR function is attempted (308). If a BDD having a zero or one value is built then the selected candidate is valid indicating equivalence (310). If the BDD is neither the zero function nor the one function, the cutpoint pair is invalid if all of its inputs are verification inputs (311). If one or more of the inputs are cutpoint variable inputs, the function for a cutpoint variable input is substituted (309), and the flow continues to build a new BDD for the evaluation XOR having the substituted function.

Method for determining functional equivalence between design models

Measurement of the test coverage of digital simulation of electronic circuitry is obtained (54). A Composite Circuit Model (60) has two parts: a Target Circuit Model (64) and an Environment Circuit Model (62). The Environment Circuit Model (62) models the behavior of inputs to the Target Circuit (64). The Composite Circuit Model (60) is translated into implicit FSM representations utilizing BDDs. A State Bin Transition Relation is formed which represents allowable transitions among user-specified sets of states or State Bins, and a representation of the reachable State Bins is built (94). A comparison is made (102) between data accumulated over one or more simulations (40) of the Target Circuit (64) and the data contained in the State Bin Transition Relation and the representation of the reachable State Bins. Output (52) is then generated showing which sets of circuit states were and weren't visited and which transitions allowed by the State Bin Transition Relation were and weren't taken during the simulations.

Measurement of digital circuit simulation test coverage utilizing BDDs

A method and circuit for determining correspondences between storage elements of a first circuit model and storage elements of a second circuit model. A first circuit model is received (102) and a second circuit model is received (104). Next, input correspondences (106) and output correspondences (108) between the circuit models are received. Each of the circuit models include a plurality of inputs, a plurality of outputs, a plurality of storage elements, and a plurality of logic functions. Signatures of each uncorresponded storage elements in the first circuit model (110) and the second circuit model (112) are determined. The signatures of the storage elements are compared (114). When a signature of a storage element of the first circuit model compares favorably to a signature of a storage element of the second circuit model, a correspondence is determined between the respective storage elements (116). Compatible cluster analysis may also be used in the method.

Apparatus and method for deriving correspondence between storage

A method (FIGS. 12-16) and a data processing system (FIG. 4) are used to verify the correct operation of one or more tri-state multiplexers (FIG. 3) located in a circuit model (37). The tri-state multiplexer checker (38) accesses the circuit model (37) and identifies the tri-state multiplexer(s). Once identified these tri-state multiplexers are checked to ensure that: (1) no two or more select/control lines to a tri-state MUX are enabled at a critical point in time wherein tri-state MUX output line contention can occur (i.e. both a logic zero and a logic one are being driven to the MUX output); and (2) that at least one select/control line is enabled during all critical periods of time so that a high impedance (high-Z) state is not propagated incorrectly through the MUX. This checking/verification is performed in a cut-set manner which is iterative and very time efficient when compared to prior methods.

Method and data processing system for verifying the correct operation of

A method for determining sequential hardware equivalence between two designs and whether one design can replace another design is disclosed whereby the designs are compared utilizing OBDD representations of the designs. The set of states in each of the designs that are equivalent to each other, equivalent-state-pairs, is first determined and it is then determined whether there exists a sequence of inputs that can take all states pairs to the equivalent-state-pair set. This results in a declaration of equivalence in the two designs. An essential reset sequence is then determined, which is then represented by the sequence of inputs to move the designs to a reset state. This, therefore, gives an essential reset sequence for the design and also gives the essential reset states for the design. The essential reset states of the design can then be compared to all states of the designs and, if they are equal, the design is replaceable.

Growing community of inventors

Austin, TX, United States of America

Carl P Pixley