# US 2014/0195785 A1 · Formal verification of a logic design

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

- Number: US 2014/0195785 A1
- Document ID: US20140195785A1
- Status: Published application
- Kind: A1
- Application number: 14/072,990
- Filed: 2013-11-06
- Published: 2014-07-10
- Earliest claimed: 2012-11-27
- Assignees: International Business Machines Corporation
- Applicants: International Business Machines Corporation
- Inventors: Maarten Jakob BOERSMA; Udo KRAUTZ; Ulrike SCHMIDT
- Web page: https://patentgrep.com/patent/US20140195785A1

## CPC

- G06F 11/2273: {Test methods}
- G06F 30/3323: using formal methods, e.g. equivalence checking or property checking
- G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N)

## Abstract

A method is provided for verification of a logic design for a processor execution unit which includes an instruction pipeline with one or more pipeline stages. The method includes: creating a design under test using at least a first and a second instance of the logic design; initializing the instruction pipeline using the first instance of the design under test with the same value in each instruction pipeline stage and the second instance with random values in its pipeline stages; selecting an instruction of the processor execution unit out of a plurality of instructions and simultaneously issuing the instruction to each instance of the design under test; providing a comparison between the outputs of the instruction pipeline executing the instruction for each instance; and if the instruction is verifiable by formal model checking, approving the correctness of the logic design if the comparison result is true.

## Claims

### Claim 1

A method for formal verification of a logic design for a processor execution unit, the processor execution unit comprising an instruction pipeline with one or more pipeline stages for executing a plurality of instructions, the method comprising:
creating a design under test by using at least a first and a second instance of the logic design;
initializing the instruction pipeline using the first instance of the design under test with a defined initial value in each instruction pipeline stage and the second instance with random initial values in its pipeline stages;
selecting an instruction of the processor execution unit out of the plurality of instructions and simultaneously issuing the instruction to each instance of the design under test;
providing a comparison result between the outputs of the instruction pipeline executing the instruction for each instance; and
in case the instruction is verifiable by formal model checking, approving the correctness of the logic design if the comparison result is true, or in case the instruction is not verifiable by formal model checking, approving the correctness of the sequenced computation in the instruction pipeline, if the comparison result is true.

### Claim 2 (depends on 1)

The method according to claim 1, wherein the comparison result is provided by a residual state of an output of the instruction pipeline executing the selected instruction for the first instance of the design under test and a residual state of an output of the instruction pipeline executing the instruction for the at least second instance of the design under test.

### Claim 3 (depends on 2)

The method according to claim 2, wherein an output of the instruction pipeline executing the selected instruction for the first and the second instance of the design under test is verified by using a structural similarity between a reference and the design under test.

### Claim 4 (depends on 2)

The method according to claim 2, wherein the method facilitates formal verification of a floating-point data flow and control design.

### Claim 5

A computer system for formal verification of a logic design for a processor execution unit, the processor execution unit comprising an instruction pipeline with one or more pipeline stages for executing a plurality of instructions, the computer system comprising:
a memory; and
a processor in communications with the memory, wherein the computer system is configured to perform a method, the method comprising:
creating a design under test by using at least a first and a second instance of the logic design;
initializing the instruction pipeline using the first instance of the design under test with a defined initial value in each instruction pipeline stage and the second instance with random initial values in its pipeline stages;
selecting an instruction of the processor execution unit out of the plurality of instructions and simultaneously issuing the instruction to each instance of the design under test;
providing a comparison result between the outputs of the instruction pipeline executing the instruction for each instance; and
in case the instruction is verifiable by formal model checking, approving the correctness of the logic design if the comparison result is true, or in case the instruction is not verifiable by formal model checking, approving the correctness of the sequenced computation in the instruction pipeline, if the comparison result is true.

### Claim 6

A computer program product comprising:
a computer readable storage medium readable by a processing circuit and storing instructions for execution by the processing circuit for performing a method comprising:
creating a design under test by using at least a first and a second instance of the logic design;
initializing the instruction pipeline using the first instance of the design under test with a defined initial value in each instruction pipeline stage and the second instance with random initial values in its pipeline stages;
selecting an instruction of the processor execution unit out of the plurality of instructions and simultaneously issuing the instruction to each instance of the design under test;
providing a comparison result between the outputs of the instruction pipeline executing the instruction for each instance; and
in case the instruction is verifiable by formal model checking, approving the correctness of the logic design, if the comparison result is true, or in case the instruction is not verifiable by formal model checking, approving the correctness of the sequenced computation in the instruction pipeline, if the comparison result is true.