| 主权项 |
1. A computer program product for verifying forwarding paths, the computer program product comprising:
one or more non-transitory computer-readable storage devices and program instructions stored on the one or more non-transitory computer-readable storage devices, the stored program instructions when executed by a computer perform steps of: 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; 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; 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 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; 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 verifying 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. |
