New version page

Term-Level Verification of a Pipelined CISC Microprocessor

Upgrade to remove ads

This preview shows page 1-2-3-19-20-38-39-40 out of 40 pages.

Save
View Full Document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience

Upgrade to remove ads
Unformatted text preview:

Term-Level Verification of a Pipelined CISCMicroprocessorRandal E. BryantDecember, 2005CMU-CS-05-195School of Computer ScienceCarnegie Mellon UniversityPittsburgh, PA 15213This work was supported by the Semiconductor Research Corporation under contract 2002-TJ-1029.Keywords: Formal verification, Microprocessor verification, UCLIDAbstractBy abstracting the details of the data representations and operations in a microprocessor, term-levelverification can formally prove that a pipelined microprocessor faithfully implements its sequen-tial, instruction-set architecture specification. Previous efforts in this area have focused on reducedinstruction set computer (RISC) and very-large instruction word (VLIW) processors.This work reports on the verification of a complex instruction set computer (CISC) processor styledafter the Intel IA32 instruction set using the UCLID term-level verifier. Unlike many case studiesfor term-level verification, this processor was not designed specifically for formal verification. Inaddition, most of the control logic was given in a simplified hardware description language. Wedeveloped a methodology in which the control logic is translated into UCLID format automatically,and the pipelined processor and the sequential reference version were described with as muchmodularity as possible. The latter feature was made especially difficult by UCLID’s limited supportfor modularity.A key objective of this case study was to understand the strengths and weaknesses of UCLIDfor describing hardware designs and for supporting the formal verification process. Althoughultimately successful, we identified several ways in which UCLID could be improved.1 IntroductionThis report describes a case study in using the UCLID verifier to formally verify several versionsof the Y86 pipelined microprocessor presented in Bryant and O’Hallaron’s computer systems text-book [4]. The purpose of this exercise was 1) to make sure the designs are actually correct, and2) to evaluate the strengths and weaknesses of UCLID for modeling and verifying an actual hard-ware design. We ultimately succeeded in this effort, finding and correcting one serious bug in oneversion. We were able to prove both the safety and the liveness of our designs.1.1 BackgroundMicroprocessors have a succinct specifications of their intended behavior, given by their Instruc-tion Set Architecture (ISA) models. The ISA describes the effect of each instruction on the micro-processor’s architectural state, comprising its registers, the program counter (PC), and the mem-ory. Such a specification is based on a sequential model of processing, where instructions areexecuted in strict, sequential order.Most microprocessor implementations use forms of pipelining to enhance performance, over-lapping the execution of multiple instructions. Various forms of interlocking and data forwardingare used to ensure that the pipelined execution faithfully implements the sequential semantics ofthe ISA. The task of formal microprocessor verification is prove that this semantic relationshipindeed holds. That is, for any possible instruction sequence, the microprocessor will obtain thesame result as would a purely sequential implementation of the ISA model.Although the development of techniques for formally verification microprocessors has a historydating back over 20 years [6], the key ideas used in our verification effort are based on ideasdeveloped by Burch and Dill in 1994 [5]. The main effort in their approach is to prove thatthere is some abstraction function α mapping states of the microprocessor to architectural states,such that this mapping is maintained by each cycle of processor operation. Burch and Dill’skey contribution was to show that this abstraction function could be computed automatically bysymbolically simulating the microprocessor as it flushes instructions out of the pipeline. For asingle-issue microprocessor, the verification task becomes one of proving the equivalence of twosymbolic simulations: one in which the pipeline is flushed and then a single instruction is executedin the ISA model, and the other in which the pipeline operates for a normal cycle and then flushes.We call this approach to verification correspondence checking.Burch and Dill also demonstrated the value of term-level modeling for their style of micropro-cessor verification. With term-levelmodeling, the details of data representations and operations areabstracted away, viewing data values as symbolic terms. The precise functionality of operations ofunits such as the instruction decoders and the ALU are abstracted away as uninterpreted functions.Even such parameters as the number of program registers, the number of memory words, and thewidths of different data types are abstracted away. These abstractions allow the verifier to focus1its efforts on the complexities of the pipeline control logic. Although these abstractions had longbeen used when applying automatic theorem provers to hardware verification [6, 12], Burch andDill were the first to show their use in an automated microprocessor verification tool.Our research group followed Burch and Dill’s lead, developing microprocessor verificationtools that operated at both with bit-level [14] and term-level [15] representations. Even with term-level modeling, our tools operate by reducing the equivalence condition to a Boolean satisfiabilityproblem, and then applying either Binary Decision Diagrams [1] or a SAT solver [17] to provethe equivalence or to generate a counterexample in the case of inequivalence. These earlier toolswere restricted to the logic of Equality with Uninterpreted Functions and Memories, where theonly operations on terms were to test them for equality and to apply uninterpreted functions, andwhere memories were modeled with interpreted read and write operations. The tools were alsocustomized to the specific task of verifying microprocessors using correspondence checking.Burch-Dill verification proves the safety of a pipelined processor design—that every cycle ofprocessor operation has an effect consistent with some number of steps k of the ISA model. Thisincludes the case where k = 0, i.e., that the cycle did not cause any progress in the programexecution. This is indeed a possibility with our designs, when the pipeline stalls to deal witha hazard condition, or when some instructions are canceled due to a mispredicted branch. Thisimplies, however, that a processor that


Download Term-Level Verification of a Pipelined CISC Microprocessor
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Term-Level Verification of a Pipelined CISC Microprocessor and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Term-Level Verification of a Pipelined CISC Microprocessor 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?