Patent ID: 9459878
Filing Date: 2016-10-04
CPC Classification: G06F

Claim Text:
1. A method for verifying forwarding paths, the method comprising: a computer system creating a first and a second logic design copy of an instruction pipeline, wherein the first logic design copy is driven in such a way that the first logic design copy executes a selected sequence of a first instruction and a second instruction without forwarding enabled, and the second logic design copy, is driven in such a way that the second logic design copy executes the selected sequence of the first instruction and the second instruction with forwarding enabled; the computer system retrieving the first instruction and the second instruction, wherein the first instruction and the second instruction have been previously proven to compute a mathematically correct result when executed separately; the computer system abstracting data flow of the first and second logic design copies of the instruction pipeline, wherein abstracting the data flow of the first and second logic design copies includes creating a construct of a plurality of un-interpreted functions that represent every possible value that is present in the data flow, and replacing data flow logic of the first and second logic design copies of the instruction pipeline with the construct, wherein replacing includes overriding the data flow logic pertaining data logic, reducing aspects of the data flow to be analyzed to aspects related to forwarding control logic, and enabling verification of correctness of the aspects related to the forwarding control logic; the computer system adjusting for latency differences between issuing of the second instruction in the first logic design copy and issuing of the second instruction in the second logic design copy of the instruction pipeline, wherein adjusting for the latency differences between the issuing of the second instruction in the first logic design and issuing of the second instruction in the second logic design copies of the instruction pipeline, comprises at least one of: driving the issuance of the first instruction, to the first logic design copy, without forwarding enabled, a number of clock cycles earlier, wherein the number of clock cycles earlier is equal to the number of clock cycles gained by implementing forwarding, in the second logic design copy, with forwarding enabled; staging the result of the second instruction in the second logic design copy, with forwarding enabled, in a buffer for a fixed number of cycles, wherein the number of cycles is equal to the number of cycles required by the first logic design copy, without forwarding enabled, to write the result of the second instruction to a register; and driving the issuance of the second instruction to the first and second logic design copies in such a way that the result of the second instructions in the first logic design copy, and the result of the second instruction in the second logic design copy, are available in the register in the same cycle; and the computer system verifying correctness of a result of the second instruction in the first logic design copy to a result of the second instruction in the second logic design copy of the instruction pipeline.