UBC Theses and Dissertations
Formal verification of a 32-bit pipelined RISC processor Darwish, Mohammad Mostafa
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 Citations and Data