Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-Of-Order Microprocessors with a Reorder Buffer

Rewriting rules and Positive Equality [4] are combined in an automatic way in order to formally verify out-of-order processors that have a Reorder Buffer, and can issue/retire multiple instructions per clock cycle. Only register-register instructions are implemented, and can be executed out-of-order, as soon as their data operands can be either read from the Register File, or forwarded as results of instructions ahead in program order in the Reorder Buffer. The verification is based on the Burch and Dill correctness criterion [6]. Rewriting rules are used to prove the correct execution of instructions that are initially in the Reorder Buffer, and to remove them from the correctness formula. Positive Equality is then employed to prove the correct execution of newly fetched instructions. The rewriting rules resulted in up to 5 orders of magnitude speedup, compared to using Positive Equality alone. That made it possible to formally verify processors with up to 1,500 instructions in the Reorder Buffer, and issue/retire widths of up to 128 instructions per clock cycle