Method and apparatus for performing formal verification of polynomial datapath
US8527924B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Apr 6, 2012 |
| Grant date | Sep 3, 2013 |
| Priority date | — |
| Expiry date | Apr 6, 2032 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F2119/18
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method and apparatus are provided for use in synthesis of RTL integrated circuit design to determine the functional equivalence of designs. For example, the receiver receives a plurality of designs for synthesis in RTL and a data flow graph is derived for each design. Internal bit widths in the data flow graph representations are restricted (52) to provide a first modified version of each of the designs. These first modified versions are compared each with the design from which it was derived in a comparison unit (54). The input bit widths of the data flow graph representation are then restricted to be no wider than the output bit widths (56) to derive second modified versions of the designs (58). These second modified versions are compared with each other (60) to determine which are equivalent. Equivalent designs can be passed to an RTL synthesis unit 62, or otherwise further evaluated.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.