The Community for Technology Leaders
16th International Conference on Parallel Architecture and Compilation Techniques (PACT 2007) (2007)
Brasov, Romania
Sept. 15, 2007 to Sept. 19, 2007
ISSN: 1089-795X
ISBN: 0-7695-2944-5
pp: 83-93
Anita Lungu , Duke University
Daniel J. Sorin , Duke University
ABSTRACT
The process of verifying a new microprocessor is a major problem for the computer industry. Currently, architects design processors to be fast, power-efficient, and reliable. However, architects do not quantify the impact of these design decisions on the effort required to verify them, potentially increasing the time to market. We propose designing processors with formal verifiability as a first-class design constraint. Using Cadence SMV, a composite formal verification tool that combines model checking and theorem proving, we explore several aspects of processor design, including caches, TLBs, pipeline depth, ALUs, and bypass logic. We show that subtle differences in design decisions can lead to large differences in required verification effort.
INDEX TERMS
null
CITATION

A. Lungu and D. J. Sorin, "Verification-Aware Microprocessor Design," 16th International Conference on Parallel Architecture and Compilation Techniques (PACT 2007)(PACT), Brasov, Romania, 2007, pp. 83-93.
doi:10.1109/PACT.2007.79
81 ms
(Ver 3.3 (11022016))