Formal verification of a logic design

摘要

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.

主权项

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 instruction pipeline stages for executing a plurality of instructions, the method comprising:
creating a design under test by using at least a first instance 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 using the second instance of the design under test with random initial values in its instruction 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 outputs of the instruction pipeline executing the instruction for each instance; and in case the instruction is verifiable by formal model checking, approving correctness of the logic design if the comparison result is true, or in case the instruction is not verifiable by formal model checking, approving correctness of a sequenced computation in the instruction pipeline, if the comparison result is true.