assembler model

Concept

The assembler model is an Isabelle/HOL abstraction of the VAMP processor instruction-set architecture used as the basis for test specifications and conformance testing. It represents addresses as natural numbers, register and memory values as integers, hides lower-level ISA and implementation details such as address translation and interrupts, and defines instruction semantics through an executable transition function.

First seen 5/26/2026

Last seen 5/26/2026

Evidence 3 chunks

Wiki v1

WIKI

Definition

The assembler model is an Isabelle/HOL theory that abstracts the instruction-set architecture used for the VAMP processor case study. It was introduced to avoid the complexity of bit-vector representations of data and instructions: addresses are represented as natural numbers, while register contents and memory contents are represented as integers. Test specifications and experiments in the case study are based on this instruction-set, or assembler, model. [C1]

Abstraction level

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

1 connections

VAMP ISA part of → 100% 2e

The assembler model is an abstraction of the VAMP ISA.

LINKED ENTITIES

2 links

Instruction Set Architecture abstracts The evidence explicitly says that the Isabelle theory of the assembler model is an abstraction of the instruction set architecture.

HOL-TestGen used_for_test_generation_from The evidence states that HOL-TestGen produces tests from the assembler-model-based test specification.

CITATIONS

9 sources

9 citations — click to expand

[1] C1: The assembler model is an Isabelle/HOL abstraction used in the VAMP case study to avoid bit-vector representations, representing addresses as naturals and register and memory contents as integers. Test Program Generation for a Microprocessor: A Case Study

[2] C2: The assembler model hides ISA and processor details including address translation, interrupts, virtual memory and caching, pipelining, and instruction reordering. Test Program Generation for a Microprocessor: A Case Study

[3] C3: The assembler configuration is the ASMcoret record with program-counter, delayed-program-counter, general-register, special-register, and memory-model fields. Test Program Generation for a Microprocessor: A Case Study

[4] C4: The assembler model uses integer lists for register files, and is_ASMcore enforces 32-register files and validity of register and memory cell values. Test Program Generation for a Microprocessor: A Case Study

[5] C5: The assembler instruction set is an Isabelle abstract datatype whose constructors correspond to operation mnemonics and cover categories such as data transfer, arithmetic/logical, test, shift, control, and interrupt instructions. Test Program Generation for a Microprocessor: A Case Study

[6] C6: exec_instr defines instruction semantics by returning the resulting configuration, and Step defines the successor transition by executing the current instruction. Test Program Generation for a Microprocessor: A Case Study

[7] C7: The assembler-model transition relations are used as the basis of test specifications, and testing checks that the processor behaves as described in the assembler model independently of implementation details. Test Program Generation for a Microprocessor: A Case Study

[8] C8: Unit instruction testing compares the SUT with exec_instr under a conformance relation =k, and HOL-TestGen produces tests from the specification. Test Program Generation for a Microprocessor: A Case Study

[9] C9: The case study uses unit testing and sequence testing, studying memory load/store, arithmetic, logic, and control-flow instruction categories. Test Program Generation for a Microprocessor: A Case Study