A Methodology for Formal Hardware Verification, with Application to Microprocessors.
Abstract
Microprocessors are now ubiquitous, but their design is not without difficulties. Numerous microprocessors have been introduced only to find- sometimes years later-that they contain mistakes. The need for better ways of checking designs is clear. This research develops a methodology for formally verifying data-intensive circuits against abstracts state machines defined by assertions, and applies it to show that a microprocessor circuit implements its intended instruction set. 'Implementation' is a formal relation between input- output sequences: of an abstract state machine, and of a circuit. This simple abstract model of behavior is reconciled with concepts from digital-systems design including dynamic logic, pipelining, multi-phase clocks, and a separate memory system. The methodology structures proof of implementation using a series of decompositions. It exposes internal system state. It dissects sequences into their component transitions (using a new formalism called marked strings to reason about overlapped operation). For processor verification it also abstracts away most of the memory state. Making these simplification from global I/O behavior once, in the methodology, allows the focus when verifying a circuit to be on the localized effects of single state transitions
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 29, 1993
- Accession Number
- ADA270550
Entities
People
- Allan L. Fisher
- Carl-johan H. Seger
- Derek L. Beatty
- Edmund M. Clarke Jr.
- Randal Bryant
Organizations
- Carnegie Mellon University