Skip to content
STIMSMITH

is_ASMcore predicate

CodeArtifact WIKI v1 · 5/25/2026

The is_ASMcore predicate is an Isabelle well-formedness predicate for ASMcoret assembler configurations. It validates program-counter fields, requires both general-purpose and special-purpose register files to contain exactly 32 registers, and checks that register and memory cell contents are valid assembler integers.

is_ASMcore predicate

is_ASMcore is a well-formedness predicate for assembler configurations represented by the ASMcoret record. In the referenced Isabelle model, register contents are integers and a register file is modeled as a list of such integers. The ASMcoret record contains delayed and current program-counter fields (dpc, pcp), general-purpose registers (gprs), special-purpose registers (sprs), and memory (mm). [C1]

The predicate exists because the assembler-level representation of addresses and values is less restrictive than the bit-vector representation, and because the registers type itself does not encode the required number of registers. is_ASMcore therefore restricts configurations to meaningful assembler states. [C2]

Definition

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))

Validation conditions

For a state st : ASMcoret, is_ASMcore st requires: [C3]

  • dpc st is accepted by asmnat.
  • pcp st is accepted by asmnat.
  • gprs st has length 32.
  • sprs st has length 32.
  • Every general-purpose register index below 32 contains a value accepted by asm_int.
  • Every special-purpose register index below 32 contains a value accepted by asm_int.
  • Every data-memory read value is accepted by asm_int.

Role in the assembler model

The predicate validates ASMcoret configurations at the assembler level. The same model defines assembler instructions as an Isabelle datatype and defines execution over ASMcoret configurations with exec_instr; the Step transition function maps a configuration to its successor by executing the current instruction. [C4]

LINKED ENTITIES

1 links
ASMcoret record VALIDATES

CITATIONS

4 sources
4 citations
[1] The model defines register contents as integers, register files as lists of integers, and ASMcoret with fields dpc, pcp, gprs, sprs, and mm. Test Program Generation for a Microprocessor: A Case Study
[2] is_ASMcore is the well-formedness predicate for assembler configurations and was introduced because the assembler representation and register-file type are less restrictive than the intended meaningful configuration domain. Test Program Generation for a Microprocessor: A Case Study
[3] The formal definition of is_ASMcore checks asmnat for dpc and pcp, requires gprs and sprs to have length 32, checks all register values below index 32 with asm_int, and checks all data-memory read values with asm_int. Test Program Generation for a Microprocessor: A Case Study
[4] The assembler model defines instructions as an Isabelle datatype, defines exec_instr over ASMcoret configurations and instructions, and defines Step as executing the current instruction to produce the successor configuration. Test Program Generation for a Microprocessor: A Case Study