Special purpose registers

Special purpose registers (SPRs, represented as sprs) are a register-file component in the VAMP processor model. The VAMP ISA configuration includes program-counter state, general purpose registers, special purpose registers, and memory; within that configuration, sprs is described as a register file of 32 registers of 32 bits each used for particular tasks. The first special purpose register is the status register, which contains interrupt masks, and some special purpose registers are used as flags registers or condition registers. Each special purpose register is addressed directly by its name. [Definition and role in VAMP]

Representation in the assembler abstraction

The assembler model abstracts the VAMP ISA by representing addresses as natural numbers and register and memory contents as integers. In that abstraction, the assembler configuration contains fields for the program counter, delayed program counter, general purpose register file, special purpose register file, and memory model. The sprs field is a list of integers representing the special purpose register file. [Assembler configuration representation]

The register-file type is defined as a list of integer register contents:

type_synonym regcont = int
  -- contents of register
type_synonym registers = regcont list
  -- register file

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

[Register-file type]

Well-formedness constraints

Because the generic registers type is only a list and does not itself encode a fixed number of registers, the assembler model defines a well-formedness predicate for configurations. The predicate requires both the general purpose register file and the special purpose register file to contain exactly 32 registers, and it checks that all special-register cells contain valid assembler integer values. [Well-formedness of sprs]

Relationship to other processor state

Special purpose registers differ from general purpose registers in the cited VAMP model. General purpose registers are described as 32 32-bit registers used in different operations and addressed by index from 0 to 31, while special purpose registers are 32 32-bit registers used for particular tasks and addressed directly by name. [GPR and SPR addressing contrast]