- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Formal verification of a 32-bit pipelined RISC processor
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
Formal verification of a 32-bit pipelined RISC processor Darwish, Mohammad Mostafa
Abstract
Designing a microprocessor is a significant undertaking. Modern RISC processors are no exception. Although RISC architectures originally were intended to be simpler than CISC processors, modern RISC processors are often very complex, partially due to the prominent use of pipelining. As a result, verifying the correctness of a RISC design is an extremely difficult task. Thus, it has become of great importance to find more efficient design verification techniques than traditional simulation. The objective of this thesis is to show that symbolic trajectory evaluation is such a technique. For demonstration purposes, we designed and implemented a 32-bit pipelined RISC processor, called Oryx. It is a fairly generic first-generation RISC processor with a fivestage pipeline and is similar to the MIPS-X and DLX processors. The Oryx processor is designed down to a detailed gate-level and is described in VHDL. Altogether, the processor consists of approximately 30,000 gates. We also developed an abstract, non-pipelined, specification of the processor. This specification is precise and is intended for a programmer. We made a special effort not to over-specify the processor, so that a family of processors, ranging in complexity and speed, could theoretically be implemented all satisfying the same specification. We finally demonstrated how to use an implementation mapping and the Voss veri fication system to verify important properties of the processor. For example, we verified that in every sequence of valid instructions, the ALU instructions are implemented cor rectly. This included both the actual operation performed as well as the control for fetching the operands and storing the result back into the register file. Carrying out this verification task required less than 30 minutes on an IBM RS6000 based workstation.
Item Metadata
Title |
Formal verification of a 32-bit pipelined RISC processor
|
Creator | |
Publisher |
University of British Columbia
|
Date Issued |
1994
|
Description |
Designing a microprocessor is a significant undertaking. Modern RISC processors are
no exception. Although RISC architectures originally were intended to be simpler than
CISC processors, modern RISC processors are often very complex, partially due to the
prominent use of pipelining. As a result, verifying the correctness of a RISC design is an
extremely difficult task. Thus, it has become of great importance to find more efficient
design verification techniques than traditional simulation. The objective of this thesis is
to show that symbolic trajectory evaluation is such a technique.
For demonstration purposes, we designed and implemented a 32-bit pipelined RISC
processor, called Oryx. It is a fairly generic first-generation RISC processor with a fivestage
pipeline and is similar to the MIPS-X and DLX processors. The Oryx processor
is designed down to a detailed gate-level and is described in VHDL. Altogether, the
processor consists of approximately 30,000 gates.
We also developed an abstract, non-pipelined, specification of the processor. This
specification is precise and is intended for a programmer. We made a special effort not
to over-specify the processor, so that a family of processors, ranging in complexity and
speed, could theoretically be implemented all satisfying the same specification.
We finally demonstrated how to use an implementation mapping and the Voss veri
fication system to verify important properties of the processor. For example, we verified
that in every sequence of valid instructions, the ALU instructions are implemented cor
rectly. This included both the actual operation performed as well as the control for
fetching the operands and storing the result back into the register file. Carrying out this
verification task required less than 30 minutes on an IBM RS6000 based workstation.
|
Extent |
1550522 bytes
|
Genre | |
Type | |
File Format |
application/pdf
|
Language |
eng
|
Date Available |
2009-02-27
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.
|
DOI |
10.14288/1.0064844
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Graduation Date |
1994-11
|
Campus | |
Scholarly Level |
Graduate
|
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.