The process of verifying a new microprocessor is a major problem for the computer industry. Currently, however, architects design processors to be fast, power-efficient, and reliable, but they often pay little attention to verifiability. Thus, current processor designs may be more difficult to verify than if architects had considered verifiability. We propose designing processors with formal verifiability as a first-class design constraint. Using Cadence SMV, a hybrid 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.