Formal verification of integrated circuit hardware designs to implement integer division
US10503852B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jan 19, 2018 |
| Grant date | Dec 10, 2019 |
| Priority date | — |
| Expiry date | Jun 4, 2038 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F2111/20
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Computer-implemented methods of verifying an integrated circuit hardware design to implement an integer divider wherein the integer divider is configured to receive a numerator N and a denominator D and output a quotient q and a remainder r. The method includes (a) verifying a base property is true for the integrated circuit hardware design and (b) formally verifying that one or more range reduction properties are true for the integrated circuit hardware design. The base property is configured to verify that an instantiation of the integrated circuit hardware design will generate a correct output pair q, r in response to any input pair N, D in a subset of non-negative input pairs. The one or more range reduction properties are configured to verify that if an instantiation of the integrated circuit hardware design will generate an output pair q, r in response to a non-negative input pair N, D then an instantiation of the integrated circuit hardware design to implement the integer divider will generate an output pair q′, r′ that has a predetermined relationship with q and r in response to another non-negative input pair N′, D where N and N′ have one of one or more predetermined relat…
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.