Method and system of latch mapping for combinational equivalence checking
US6247163A · kind A · utility
Assignee
Inventors
Key dates
| Filing date | Oct 13, 1998 |
| Grant date | Jun 12, 2001 |
| Priority date | — |
| Expiry date | Oct 13, 2018 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method and system of latch mapping for performing combinational equivalence checking on a specification and an implementation of a circuit that does not depend on signal names or circuit structure to determine the latch mapping. First, every latch is mapped to every other latch. Then, the resulting mapping is refined until it is semi-inductive. The refinement is performed by randomly producing a state that satisfies the mapping and applying a random input vector to the circuits. The resulting mappings are iteratively compared and new input vectors are applied to the circuits until the greatest fixed point of the refinement is found. Then, it is determined whether the greatest fixed point of refinement forces output equality. If the greatest fixed point does not force output equality, then a bug in a combinational block of the implementation is localized through an interactive procedure. If the greatest fixed point does force output equality, then it is determined whether it also satisfies a reset condition. If implementation latches are not mapped together, then conformance with the reset condition is guaranteed. Otherwise, conformance can be guaranteed only if the implementation…
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.