Overview
ASMcoret is an Isabelle record representing an assembler-level processor configuration. It is defined after the register-file type, where register contents are integers and a register file is a list of those integer register contents. [C1]
type_synonym regcont = int
text ‹contents of register›
type_synonym registers = regcont list
text ‹register file›
record ASMcoret = dpc :: nat
pcp :: nat
gprs :: registers
sprs :: registers
mm :: memt
Fields
The record stores: [C1]
dpc :: nat— delayed program counter.pcp :: nat— program-counter-related natural-number field.gprs :: registers— general-purpose register file.sprs :: registers— special-purpose register file.mm :: memt— memory component.
Because registers is only a list type, the type itself does not encode the number of registers. The cited model therefore uses a separate well-formedness predicate, is_ASMcore, to restrict valid ASMcoret configurations. [C2]
Well-formedness via is_ASMcore
The is_ASMcore predicate defines well-formed assembler configurations. It requires dpc and pcp to satisfy asmnat, requires both gprs and sprs to have length 32, checks the first 32 general and special registers with asm_int, and requires every data-memory cell read from mm to satisfy asm_int. [C2]
definition is_ASMcore :: ASMcoret ⇒ bool where
is_ASMcore st ≡ asmnat (dpc st) ∧
asmnat (pcp st) ∧
length (gprs st) = 32 ∧
length (sprs st) = 32 ∧
(∀ ind < 32. asm_int (reg (gprs st) ind)) ∧
(∀ ind < 32. asm_int (sreg (sprs st) ind)) ∧
(∀ ad. asm_int (data_mem_read (mm st) ad))
Role in instruction semantics
The assembler instruction set is defined as an Isabelle datatype instr, with constructors for categories including memory data transfer, constant data transfer, register data transfer, arithmetic/logical operations, test operations, shift operations, control operations, and interrupts. [C3]
Instruction semantics are given by exec_instr, which maps an ASMcoret configuration and an instr to the resulting ASMcoret configuration. Examples in the evidence include arithmetic, logical, and shift instructions that call helper functions such as arith_exec. [C4]
fun exec_instr :: [ASMcoret, instr] ⇒ ASMcoret
Transition function
The transition function Step takes an ASMcoret configuration and returns its successor. It is defined by executing the current instruction selected from the delayed program counter context via current_instr st. [C5]
definition Step :: ASMcoret ⇒ ASMcoret
where Step st ≡ exec_instr st (current_instr st)
The cited study uses these transition relations as the basis for test specifications. The assembler model is described as more abstract than the processor model, making details such as interrupt handling, virtual memory and caching, pipelining, and instruction reordering transparent. [C6]