Formal verification of a complex pipelined processor

DOI10.1023/A:1024716316140MaRDI QIDQ1426941zbMATH OpenOpenAlexFDO

Authors Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam Srivas

Publication date 15 March 2004

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1024716316140

zbMATH Keywords

formal verificationPVScompletion functionsprocessor verification

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• scientific article; zbMATH DE number 1903361
• scientific article; zbMATH DE number 1670784
• scientific article; zbMATH DE number 2102694
• Formal modeling and verification of microprocessors
• Formal verification of out-of-order execution with incremental flushing

Cited in

(29)

• scientific article; zbMATH DE number 1670784 (Why is no real title available?)
• Mothers of pipelines
• scientific article; zbMATH DE number 1903361 (Why is no real title available?)
• scientific article; zbMATH DE number 2102697 (Why is no real title available?)
• A hazards-based correctness statement for pipelined circuits
• scientific article; zbMATH DE number 2079670 (Why is no real title available?)
• Computer Aided Verification
• A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
• scientific article; zbMATH DE number 1979547 (Why is no real title available?)
• Algebraic models of behaviour and correctness of SMT and CMT processors
• scientific article; zbMATH DE number 1629969 (Why is no real title available?)
• A simple, verified validator for software pipelining
• scientific article; zbMATH DE number 2102694 (Why is no real title available?)
• Advanced automation in formal verification of processors.
• Formal Methods for Hardware Verification
• Correct Hardware Design and Verification Methods
• Verification of out-of-order processor designs using model Checking and a light-weight completion function
• Computer Aided Verification
• scientific article; zbMATH DE number 1507239 (Why is no real title available?)
• Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability
• Formal Methods in Computer-Aided Design
• Formal Methods in Computer-Aided Design
• Correct Hardware Design and Verification Methods
• A pipelined multi-core MIPS machine. Hardware implementation and correctness proof
• FM 2005: Formal Methods
• Computer Aided Verification
• scientific article; zbMATH DE number 1670799 (Why is no real title available?)
• scientific article; zbMATH DE number 1701763 (Why is no real title available?)
• Computer Aided Verification

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Formal verification of a complex pipelined processor

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