Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution

No abstract is available for this paper.

• Publication year

  1998

• Venue

  Formal Methods in Computer-Aided Design

• Publication date

  1998-11-04

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/3-540-49519-3_2
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking

  1998cited by this paper
• Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification

  1998cited by this paper
• You Assume, We Guarantee: Methodology and Case Studies

  1998cited by this paper
• Processor Verification with Precise Exeptions and Speculative Execution

  1998influential reference
• Formal Verification of Out-of-Order Execution Using Incremental Flushing

  1998cited by this paper
• Decomposing the Proof of Correctness of pipelined Microprocessors

  1998cited by this paper
• Verifying out-of-order executions

  1997cited by this paper
• Trace Table Based Approach for Pipeline Microprocessor Verification

  1997influential reference
• Techniques for verifying superscalar microprocessors

  1996cited by this paper
• Mechanically Checking a Lemma Used in an Automatic Verification Tool

  1996cited by this paper
• Efficient validity checking for processor verification

  1995cited by this paper
• Automatic verification of Pipelined Microprocessor Control

  1994cited by this paper
• Computer Architecture: A Quantitative Approach

  1969cited by this paper

• Separation of concerning things: a simpler basis for defining and programming with the C/C++ memory model (extended version)

  2022cites this paper
• Parallelized Sequential Composition and Hardware Weak Memory Models

  2021cites this paper
• ABSTRACTIONS ANDREDUCTIONS INMODEL CHECKING

  2015cites this paper
• Dynamic abstraction model checking

  2013cites this paper
• Formal Verification of Instruction Dependencies in Microprocessors

  2011cites this paper
• A Refinement-Based Compositional Reasoning Framework for Pipelined Machine Verification

  2008cites this paper
• Automatic verification of safety and liveness for pipelined machines using WEB refinement

  2008cites this paper
• Top-level Re nement in Processor Veri cationSava

  2007cites this paper
• Decomposing the Veri cation of PipelinedMicroprocessors with Invariant

  2007cites this paper
• Efficient Verification of Bit-Level Pipelined Machines Using Refinement

  2007cites this paper
• A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification

  2006cites this paper
• Structuring instruction-sets with higher-order functions

  2005cites this paper
• A complete compositional reasoning framework for the efficient verification of pipelined machines

  2005cites this paper
• A general decomposition strategy for verifying register renaming

  2004cites this paper
• Safe and Precise WCET Determination by Abstract Interpretation of Pipeline Models

  2004cites this paper
• Verification of an Advanced mips-Type Out-of-Order Execution Algorithm

  2004cites this paper
• Counterexample-guided abstraction refinement for symbolic model checking

  2003cites this paper
• Formal Verification of a Complex Pipelined Processor

  2003cites this paper
• Algebraic models of correctness for abstract pipelines

  2003cites this paper
• A framework for superscalar microprocessor correctness statements

  2003cites this paper
• A Hazards-Based Correctness Statement for Pipelined Circuits

  2003cites this paper
• Correct Hardware Design and Verification Methods

  2003cites this paper
• Relating Multi-step and Single-Step Microprocessor Correctness Statements

  2002cites this paper
• Abstractions and Reductions in Model Checking

  2002cites this paper
• Formal Verification of Out-of-Order Execution with Incremental Flushing

  2002cites this paper
• Verifying a Simple Pipelined Microprocessor Using Maude

  2001cites this paper
• Formal Sequential Equivalence Checking of Digital Systems by Symbolic Simulation

  2001cites this paper
• Formal sequential equivalence checking of digital systems by symbolic simulation

  2001cites this paper
• A Methodology for Deductive Verification of Out-of-Order Execution Systems Based on Predicted Values,

  2001cites this paper
• A Framework for Microprocessor Correctness Statements

  2001cites this paper
• Formal verification of superscalar microprocessors with multicycle functional units, exceptions, and branch prediction

  2000cites this paper
• Frontiers of Combining Systems

  2000cites this paper
• Algebraic Models of Correctness for Microprocessors

  2000cites this paper
• Combinations of Model Checking and Theorem Proving

  2000cites this paper
• Automatic abstraction in model checking

  2000cites this paper
• Correctness and Verification of Hardware Systems Using

  2000cites this paper
• Verifying Advanced Microarchitectures that Support Speculation and Exceptions

  2000cites this paper
• Correctness and Verification of Hardware Systems Using Maude

  2000cites this paper
• Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach

  1999cites this paper
• Formal Verification of Designs with Complex Control by Symbolic Simulation

  1999cites this paper
• A systematic incrementalization technique and its application to hardware design

  1999cites this paper
• Top-level Reenement in Processor Veriication

  1998cites this paper