Verifying advanced microarchitectures that support speculation and exceptions

DOI10.1007/10722167_39MaRDI QIDQ2754112zbMATH OpenFDO

Authors Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam Srivas

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10722167_39

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability
• Formal verification of a complex pipelined processor
• Microarchitecture verification by compositional model checking
• Deductive verification of advanced out-of-order microprocessors.
• Formal verification of VLIW microprocessors with speculative execution

Cited in

(9)

• Algebraic models of correctness for abstract pipelines.
• Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability
• Automatic verification of fault-tolerant register emulations
• Mothers of pipelines
• Efficient Information-Flow Verification Under Speculative Execution
• Microarchitecture verification by compositional model checking
• Using abstract specifications to verify \(\text{PowerPC}^{\text{TM}}\) custom memories by symbolic trajectory evaluation
• Proof of correctness of a processor with reorder buffer using the completion functions approach
• Verification of an advanced Mips-type out-of-order execution algorithm

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Verifying advanced microarchitectures that support speculation and exceptions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2754112)