Formal verification of VLIW microprocessors with speculative execution

DOI10.1007/10722167_24MaRDI QIDQ2754092zbMATH OpenFDO

Authors Miroslav N. Velev

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_24

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• Formal verification of a complex pipelined processor
• Automatic abstraction of memories in the formal verification of superscalar microprocessors
• Formal modeling and verification of microprocessors
• Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability
• Microarchitecture verification by compositional model checking

Cited in

(12)

• Algebraic models of correctness for abstract pipelines.
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Formal verification of a complex pipelined processor
• Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability
• Model checking speculation-dependent security properties: abstracting and reducing processor models for sound and complete verification
• Verifying advanced microarchitectures that support speculation and exceptions
• Automatic abstraction of memories in the formal verification of superscalar microprocessors
• Formal verification of translation validators
• Efficient Information-Flow Verification Under Speculative Execution
• Using abstract specifications to verify \(\text{PowerPC}^{\text{TM}}\) custom memories by symbolic trajectory evaluation
• FM 2005: Formal Methods
• A parallelization scheme based on work stealing for a class of SAT solvers

Describes a project that uses

Uses Software

• Velev SAT Benchmarks

This page was built for publication: Formal verification of VLIW microprocessors with speculative execution

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