# US 10,503,852 B2 · Formal verification of integrated circuit hardware designs to implement integer division

> Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt

- Number: US 10,503,852 B2
- Document ID: US10503852B2
- Status: Granted
- Kind: B2
- Application number: 15/875,176
- Filed: 2018-01-19
- Published: 2018-07-19
- Granted: 2019-12-10
- Earliest claimed: 2017-01-19
- Assignees: Imagination Technologies Limited
- Applicants: Imagination Technologies Limited
- Inventors: Emiliano Morini; Sam Elliott
- Web page: https://patentgrep.com/patent/US10503852B2

## CPC

- G06F 30/3323: using formal methods, e.g. equivalence checking or property checking
- G06F 30/30: Circuit design
- G06F 2111/20: Configuration CAD, e.g. designing by assembling or positioning modules selected from libraries of predesigned modules
- G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N)

## 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 relationships.

## Claims

### Claim 1

A computer-implemented method of verifying an integrated circuit hardware design to implement an integer divider, the integer divider configured to receive a numerator N and a denominator D and output a quotient q and a remainder r, the method comprising, in one or more processors:
verifying a base property of the integrated circuit hardware design, wherein verifying the base property verifies 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;
formally verifying, by a formal verification tool, one or more range reduction properties of the integrated circuit hardware design, wherein verifying the one or more range reduction properties verifies 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 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 relationships; and
outputting one or more signals indicating whether the properties have been successfully verified.

### Claim 2 (depends on 1)

The method of claim 1, further comprising, in response to the one or more signals indicating that at least one property was not successfully verified, modifying the integrated circuit hardware design.

### Claim 3 (depends on 1)

The method of claim 1, further comprising, in response to the one or more signals indicating that the properties were successfully verified, manufacturing, at an integrated circuit manufacturing system, an integrated circuit according to the integrated circuit hardware design.

### Claim 4 (depends on 1)

The method of claim 1, wherein the one or more predetermined relationships between N and N′ comprises N′=N+D.

### Claim 5 (depends on 1)

The method of claim 1, wherein the one or more predetermined relationships between N and N′ comprises N′=N+1.

### Claim 6 (depends on 1)

The method of claim 1, wherein the one or more predetermined relationships between N and N′ comprises N′=2zN, 2zN+1, 2zN+2, . . . 2zN+(2z−1), wherein z is an integer.

### Claim 7 (depends on 6)

The method of claim 6, wherein z is equal to one.

### Claim 8 (depends on 7)

The method of claim 7, wherein the one or more range reduction properties comprises:
if N′=2N and 2r<D then r′=2r and q′=2q;
if N′=2N and 2r≥D then r′=2r−D and q′=2q+1;
if N′=2N+1 and 2r<D then r′=2r+1 and q′=2q; and
if N′=2N+1 and 2r≥D then r′=2r+1−D and q′=2q+1.

### Claim 9 (depends on 1)

The method of claim 1, wherein the one or more predetermined relationships between N and N′ comprises N′=αN, αN+1, αN+2, . . . αN+(α−1), wherein α is an integer.

### Claim 10 (depends on 6)

The method of claim 6, wherein the subset of non-negative input pairs comprises non-negative input pairs N, D where N=0.

### Claim 11 (depends on 10)

The method of claim 10, wherein the base property is that in response to any input pair in the subset of non-negative input pairs each output pair q, r satisfies q=0 and r=0.

### Claim 12 (depends on 1)

The method of claim 1, wherein the subset of non-negative input pairs comprises non-negative input pairs N, D where N<D.

### Claim 13 (depends on 12)

The method of claim 12, wherein the base property is that in response to any input pair in the subset of non-negative input pairs each output pair q, r satisfies q=0 and r=N.

### Claim 14 (depends on 1)

The method of claim 1, further comprising verifying one or more sign relation properties of the integrated circuit hardware design, wherein verifying the one or more sign relation properties verifies that if an instantiation of the integrated circuit hardware design produces an output pair q, r in response to a non-negative input pair N, D that an instantiation of the integrated circuit hardware design will produce an output pair q′, r′ that has a predetermined relationship with q, r in response to another input pair N′, D′ where N′=−N and/or D′=−D.

### Claim 15 (depends on 14)

The method of claim 14, wherein the one or more sign relation properties comprises:
if N′=N and D′=−D, then q′=−q and r′=r;
if N′=−N and D′=D, then q′=−q and r′=−r; and
if N′=−N and D′=−D, then q′=q and r′=−r.

### Claim 16 (depends on 14)

The method of claim 14, wherein the numerator N is represented in two's-complement format, and the method further comprises verifying one or more largest negative numerator properties of the integrated circuit hardware design, wherein verifying the one or more largest negative numerator properties verifies that in response to any input pair N, D wherein N is the largest negative numerator representable in the two-complement format an instantiation of the integrated circuit hardware design will generate a correct output pair q, r.

### Claim 17 (depends on 14)

The method of claim 14, wherein the denominator D is represented in two's-complement format, and the method further comprises verifying one or more largest negative denominator properties of the integrated circuit hardware design, wherein verifying the one or more largest negative denominator properties verifies that in response to any input pair N, D wherein D is the largest negative denominator representable in the two-complement format an instantiation of the integrated circuit hardware design to implement the integer divider will generate a correct output pair q, r.

### Claim 18 (depends on 1)

The method of claim 1, wherein processing the integrated circuit hardware design at an integrated circuit manufacturing system causes the integrated circuit manufacturing system to manufacture an integrated circuit that implements an integer divider.

### Claim 19

A system to verify an integrated circuit hardware design to implement an integer divider, the integer divider configured to receive a numerator N and a denominator D and output a quotient q and a remainder r, the system comprising:
one or more processors; and
memory, comprising:
a formal verification tool;
computer-readable instructions that when executed by the one or more processors cause the one or more processors to:
verify a base property of the integrated circuit hardware design, wherein verifying the base property verifies 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;
formally verify, by the formal verification tool, one or more range reduction properties of the integrated circuit hardware design, wherein verifying the one or more range reduction properties verifies 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 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 relationships; and
output one or more signals indicating whether the properties have been successfully verified.

### Claim 20

A non-transitory computer readable storage medium having stored thereon computer readable instructions that, when executed at a computer system, cause the computer system to:
verify a base property of an integrated circuit hardware design to implement an integer divider, the integer divider configured to receive a numerator N and a denominator D and output a quotient q and a remainder r, wherein verifying the base property verifies 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;
formally verify, by a formal verification tool, one or more range reduction properties of the integrated circuit hardware design, wherein verifying the one or more range reduction properties verifies 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 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 relationships; and
output one or more signals indicating whether the properties have been successfully verified.