RISC processor Wiki

Overview

A RISC processor is referred to in the supplied evidence as a reduced instruction set processor. The evidence uses the term in the description of the Verified Architecture MicroProcessor (VAMP), stating that VAMP is a "pipelined reduced instruction set (RISC) processor" based on out-of-order execution.[RISC-expansion-and-VAMP]

Example: VAMP

The supplied case study presents VAMP as a realistic model of a RISC processor. VAMP is described as inspired by IBM's G5 architecture and as having a formal processor model developed in Isabelle/HOL within the Verisoft project.[VAMP-realistic-model]

At the assembly level, the VAMP instruction set is called VAMPasm. The evidence states that VAMPasm includes 56 instructions, grouped as follows:[VAMPasm-instruction-set]

8 memory data-transfer instructions
2 constant data-transfer instructions
2 register data-transfer instructions
14 arithmetic and logical-operation instructions
16 test-operation instructions
6 shift-operation instructions
6 control-operation instructions
2 interrupt-handling instructions

Verification and testing context

In the cited case study, RISC-processor testing is discussed through VAMP. The authors generate tests from a formal instruction-set model and use those tests to check conformance between the gate-level implementation and the assembly-level model.[Conformance-testing]

The same work reports that the VAMP processor model was reused for model-based generation of test cases, including test sequences generated with HOL-TestGen on top of Isabelle/HOL.[Model-based-test-generation]

Position in the Verisoft architecture

The evidence places VAMP at the hardware layer of the Verisoft architecture, with VAMPasm at the assembly level and VAMP at the gate level. The broader Verisoft effort is described as aiming at pervasive formal verification of computer systems from application level down to silicon hardware design.[Verisoft-layering]

Related concepts and entities

VAMP: an evidenced instance of a pipelined reduced instruction set processor and the main RISC-processor example in the supplied material.

RISC processor