Loading patent…
AssigneeSynopsys, Inc.
InventorsEduard Cerny, Ashvin Mark Dsouza, Kevin Michael Harer, Pei-Hsin Ho
Estimating the term…
Relates to automatic conversion of assumption constraints, used in circuit design verification, that model an environment for testing a DUT/DUV, where the assumptions specify sequential behavior. Such assumptions are converted, with the use of logic synthesis tools, into a gate-level representation. For formal verification, a verification output is constructed from the gate-level representation and DUT/DUV assertion-monitoring circuitry. A formal verifier seeks to prove the verification output cannot indicate a design error. For simulation verification, the gate-level representation is converted into a hybrid representation comprising pipelines and combinational constraints. During simulation, the pipelines hold state information necessary for a solution, of the combinational constraints, to be in accord with the sequential assumption constraints. For certain sequential assumption constraints, the combinational constraints are insufficient to insure avoidance of deadend states. In a deadend state, an assumption is violated. A method is presented for augmenting the combinational constraints to avoid deadend states.
A method for performing formal verification of a design under test/verification (DUT/DUV), the method comprising:
A data processing system for, performing formal verification of a design under test/verification (DUT/DUV), comprising sub-systems configured to:
A computer-readable storage medium storing instructions that when executed by a computer cause the computer to perform a method for performing formal verification of a design under test/verification (DUT/DUV), the method comprising:
Dependencies are inferred from the claim text.