Microarchitecture verification by compositional model checking
From MaRDI portal
Recommendations
- Deductive verification of advanced out-of-order microprocessors.
- Verification of out-of-order processor designs using model Checking and a light-weight completion function
- Compositional specification and model checking in GSTE
- Verifying advanced microarchitectures that support speculation and exceptions
- A methodology for hardware verification using compositional model checking
Cited in
(15)- Local proofs for global safety properties
- Algebraic models of correctness for abstract pipelines.
- A methodology for hardware verification using compositional model checking
- Verification of out-of-order processor designs using model Checking and a light-weight completion function
- Model checking speculation-dependent security properties: abstracting and reducing processor models for sound and complete verification
- Formal verification of VLIW microprocessors with speculative execution
- Verifying advanced microarchitectures that support speculation and exceptions
- Efficient Information-Flow Verification Under Speculative Execution
- Modeling and verification of out-of-order microprocessors in UCLID
- Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics
- Proof of correctness of a processor with reorder buffer using the completion functions approach
- Verifying safety properties of a PowerPC\(^{TM}\) microprocessor using symbolic model checking without BDDs
- Computer Aided Verification
- Deductive verification of advanced out-of-order microprocessors.
- Silicon debug of a powerPC microprocessor using model checking
This page was built for publication: Microarchitecture verification by compositional model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4551174)
