Formal Verification of Out-of-Order Processor

Out-of-order execution is a fundamental technique to achieve instruction-level parallelization in processor designs. The verification of out-of-order processor is a main challenge in processor design. This paper presents a formal method to model and check the correctness of out-of-order design at instruction level. This method is based on model checking, a widely used formal verification technique. The rules to generate properties an out-of-order design should satisfy are also provided. The abstracted model can be verified with NuSMV, a popular model checking tool. If the properties cannot be satisfied, a counterexample is created to help correct the design.