Miroslav N. Velev. Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer. In 2002 Design, Automation and Test in Europe Conference and Exposition (DATE 2002), 4-8 March 2002, Paris, France. pages 28-35, IEEE Computer Society, 2002. [doi]
Abstract is missing.