Formal Verification of Microprocessors at AMD

Abstract: Formal Verification HistoryWe have emphasized automated theorem proving.1995--96: Division and square root algorithmsfor AMD-K5 microcode[3, 5]1997--present: Proofs of floating-point algorithmsand actual RTL that use ACL2 on theAMD Athlonprocessor and its derivatives [6,7, 8]\Gamma We have a translator from our proprietary RTL toACL2 [7] that enables RTL proofs.2001: Completed some protocol-level proofs5A natural target for theorem provers [10, 4]Concise formal...