Decomposing the Proof of Correctness of pipelined Microprocessors

No abstract is available for this paper.

• Publication year

  1998

• Venue

  International Conference on Computer Aided Verification

• Publication date

  1998-06-28

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1007/BFb0028739
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Trace Table Based Approach for Pipeline Microprocessor Verification

  1997cited by this paper
• A scalable formal verification methodology for pipelined microprocessors

  1996cited by this paper
• Inverting the Abstraction Mapping: A Methodology for Hardware Verification

  1996cited by this paper
• Validity Checking for Combinations of Theories with Equality

  1996cited by this paper
• Formal Methods in Computer-Aided Design

  1996cited by this paper
• Techniques for verifying superscalar microprocessors

  1996cited by this paper
• Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods

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

  1995cited by this paper
• Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS

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

  1994cited by this paper
• Effective Theorem Proving for Hardware Verification

  1994cited by this paper
• Microprocessor Verification in PVS - A Methodology and Simple Example

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

  1969cited by this paper

• PipeGen: Automated Transformation of a Single-Core Pipeline Into a Multicore Pipeline for a Given Memory Consistency Model

  2024cites this paper
• Modelling and verification of parameterized architectures: A functional approach

  2021cites this paper
• An Adaptive Overlap-Pipelined Multitasking Superscalar Processor

  2020cites this paper
• An Adaptive Multitasking Superscalar Processor

  2019cites this paper
• Model Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification

  2019cites this paper
• An Integrated Environment for Efficient Formal Design and Verification

  2013cites this paper
• Automatic Datapath Abstraction Of Pipelined Circuits

  2011cites this paper
• Desynchronization: Design for verification

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

  2011cites this paper
• Modelling and Verification of Pipelined Micro-Architectures: Functional Approach

  2010cites this paper
• Verification of desynchronized circuits

  2009cites this paper
• A Rewriting Logic Approach to Type Inference

  2009cites this paper
• Automatic Formal Verification of Control Logic in Hardware Designs

  2009cites this paper
• A Rewriting Logic Approach to Defining Type Systems

  2008cites this paper
• A Rewriting Logic Approach to Type Inference: Technical Report

  2008cites this paper
• A Scalable Proof Methodology for RISC Processor Designs: A Functional Approach

  2008cites this paper
• Modelling and verification of superscalar Micro-architectures functional approach

  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 Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures

  2006cites this paper
• TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories

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

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

  2003cites this paper
• Formal verification of an Intel XScale processor model with scoreboarding, specialized execution pipelines, and impress data-memory exceptions

  2003cites this paper
• Integrating formal verification into an advanced computer architecture course

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

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

  2003influential citation
• Correct Hardware Design and Verification Methods

  2003cites this paper
• CSE548: Optimality of Tomasulo's Algorithm

  2002cites this paper
• Formal verification of a pipelined processor with new memory hierarchy using a commercial model checker

  2002cites this paper
• Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function

  2002cites this paper
• Asynchronous queue machines with explicit forwarding

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

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

  2002cites this paper
• Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability

  2002cites this paper
• - 1-Optimality of Tomasulo ’ s Algorithm

  2002cites this paper
• Model checking and theorem proving: a unified framework

  2002cites this paper
• A Mechanized Theory for Microprocessor Correctness Statements

  2002cites 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
• An algebraic framework for modelling and verifying microprocessors using HOL

  2001cites this paper
• A Framework for Microprocessor Correctness Statements

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

  2001cites this paper
• Theorem proving in technology transfer: the user’s point of view

  2000cites this paper
• Correctness of Pipelined Machines

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

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

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

  2000cites this paper
• Formal Verification of VLIW Microprocessors with Speculative Execution

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

  2000cites this paper
• Formal Verification of Explicitly Parallel Microprocessors

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

  1999cites this paper
• Algorithms and methodology for scalable model checking

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

  1999cites this paper
• Formal design verification for correctness of pipelined microprocessors with out-of-order instruction execution

  1999cites this paper
• A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer

  1999cites this paper
• Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study

  1999cites this paper
• Combining Model Checking and Theorem Proving in Hardware Verification

  1999cites this paper
• Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification

  1998cites this paper
• Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution

  1998cites this paper
• Formal Verification of Out-of-Order Execution Using Incremental Flushing

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

  1998cites this paper
• Incremental Specification and Design of a Pipelined Protocol Converter

  year unknowncites this paper
• Formal Verification of Superscalar Micro-architectures : Functional approach

  year unknowncites this paper