A Methodology for Formal Hardware Verification, with Application to Microprocessors.
CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
Pagination or Media Count:
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 IO behavior once, in the methodology, allows the focus when verifying a circuit to be on the localized effects of single state transitions
- Computer Hardware