general purpose registers Wiki

Overview

General purpose registers, abbreviated gprs in the cited VAMP processor model, are a register file used by processor operations. In the ISA-level configuration, the gprs component consists of 32 registers, each 32 bits wide. The registers are addressed by index from 0 to 31, and the first register is always set to 0. [C1]

Role in the VAMP configuration

The VAMP processor configuration described in the Isabelle/HOL programmer's model contains five elements: a program counter (pcp), a delayed program counter (dcp), general purpose registers (gprs), special purpose registers (sprs), and a memory model (mm). Within that configuration, gprs is the general purpose register file used in different operations. [C1]

Assembler-level representation

The assembler model abstracts the ISA-level representation. In this abstraction, register and memory contents are represented by integers, and the general purpose register file is represented as a list of integers. The HOL record for assembler configurations includes a gprs field of type registers: [C2]

type_synonym regcont = int
 type_synonym registers = regcont list

record ASMcoret = dpc :: nat
                pcp  :: nat
                gprs :: registers
                sprs :: registers
                mm   :: memt

Because the registers type is only a list and does not itself encode the number of registers, the assembler model uses a well-formedness predicate. The is_ASMcore predicate requires length (gprs st) = 32 and checks that every general purpose register entry indexed below 32 contains a valid assembler integer value. [C3]

Use by instructions

The assembler instruction semantics access gprs operands when executing operations. Examples in the evidence show arithmetic, logical, and shift instructions reading source operands through expressions such as reg (gprs st) RS1 and reg (gprs st) RS2, then passing the destination register RD to the execution helper. [C4]

Distinction from special purpose registers

The same VAMP configuration also includes special purpose registers (sprs), another 32-register file. Unlike gprs, which are addressed by index and used in different operations, sprs are described as being used for particular tasks; examples include a status register containing interrupt masks and registers used as flags or condition registers. [C5]