Method and apparatus for solving sequential constraints
US7076753B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Dec 18, 2003 |
| Grant date | Jul 11, 2006 |
| Priority date | — |
| Expiry date | Dec 20, 2024 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.