A methodology for hardware verification using compositional model checking

DOI10.1016/S0167-6423(99)00030-1MaRDI QIDQ1566919zbMATH OpenOpenAlexFDO

Authors K. L. McMillan

Publication date 4 June 2000

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0167-6423(99)00030-1

zbMATH Keywords

compositional model checkinghardware verification

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07)

Recommendations

• Compositional Reasoning for Hardware/Software Co-verification
• Model checking: a hardware design perspective
• scientific article; zbMATH DE number 1796150
• Hardware/Software Co-Verification: Models and Methods
• Model checking: from hardware to software.
• Progress in certifying hardware model checking results
• Compositional Verification for Component-Based Systems and Application
• A methodology for hardware verification based on logic simulation
• A compositional approach to the verification of hybrid systems

Cited in

(21)

• Verifying Reference Counting Implementations
• Partial order reduction for deep bug finding in synchronous hardware
• scientific article; zbMATH DE number 2112983 (Why is no real title available?)
• Computer Aided Verification
• Functional Verification of Power Gated Designs by Compositional Reasoning
• Compositional Reasoning for Hardware/Software Co-verification
• scientific article; zbMATH DE number 2060812 (Why is no real title available?)
• Model checking: a hardware design perspective
• scientific article; zbMATH DE number 1796150 (Why is no real title available?)
• Exploring structural symmetry automatically in symbolic trajectory evaluation
• Dominant controllability check using QBF-solver and netlist optimizer
• A mechanism of function calls in MSVL
• A compositional behavioral modeling framework for embedded system design and conformance checking
• Formal Methods for Hardware Verification
• Functional verification of power gated designs by compositional reasoning
• Word level bitwidth reduction for unbounded hardware model checking
• Temporal prophecy for proving temporal properties of infinite-state systems
• A methodology to take credit for high-level verification during RTL verification
• Automatic assume-guarantee reasoning for safety and liveness using passive learning
• Mind the Shapes: Abstraction Refinement Via Topology Invariants
• Verification of AMBA using a combination of model checking and theorem proving

Describes a project that uses

Uses Software

• MOCHA

This page was built for publication: A methodology for hardware verification using compositional model checking

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