A methodology for formal hardware verification, with application to microprocessors
Derek L. Beatty · Defense Technical Information Center (DTIC) · 1993
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