Formal verification of integrated circuit hardware designs to implement integer division
US10796052B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Nov 5, 2019 |
| Grant date | Oct 6, 2020 |
| Priority date | — |
| Expiry date | Nov 5, 2039 |
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 relationshi…
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.