Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability

DOI10.1023/A:1014122630277zbMath1014.68097OpenAlexW1490835877MaRDI QIDQ1604726

Publication date: 8 July 2002

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1014122630277

zbMATH Keywords

formal verification ACL2 theorem prover

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

ACL2

This page was built for publication: Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability