Verisoft project

Organization

The Verisoft project was a German research project aimed at pervasive formal verification of computer systems from application software down to silicon-level hardware design. It provided the context for the development and verification of the VAMP processor and the VAMOS micro-kernel, and its Isabelle/HOL models were later reused for model-based processor test generation.

First seen 5/25/2026

Last seen 5/26/2026

Evidence 3 chunks

Wiki v2

WIKI

Overview

The Verisoft project was a German research project whose goal was the pervasive formal verification of computer systems from the application level down to silicon-level hardware design. Together with VerisoftXT, it provided the context in which the Verified Architecture Microprocessor (VAMP) and the VAMOS micro-kernel were developed and verified. [C1]

A later case study describes Verisoft as having produced Isabelle/HOL formal models for both the VAMP processor and a small operating system. Those models were reused for model-based generation of processor test programs intended to check whether hardware conforms to the VAMP model. [C2]

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

2 connections

VAMP (Verified Architecture Microprocessor) ← part of 100% 1e

VAMP was developed as part of the Verisoft project.

VAMOS microkernel ← part of 100% 1e

VAMOS was developed and verified in the Verisoft project.

CITATIONS

12 sources

12 citations — click to expand

[1] Verisoft was a German research project aimed at pervasive formal verification from application level to silicon, and VAMP and VAMOS were developed and verified in the context of Verisoft and VerisoftXT. Test Program Generation for a Microprocessor: A Case Study

[2] Verisoft developed Isabelle/HOL formal models for both the VAMP processor and a small operating system, and later work reused the processor model for conformance-oriented test generation. Test Program Generation for a Microprocessor: A Case Study

[3] The Verisoft architecture comprised four main layers, each structured into sub-layers. Test Program Generation for a Microprocessor: A Case Study

[4] The application, system-software, tools, and hardware layers covered user-process verification on VAMOS, VAMOS infrastructure, compiler correctness, and hardware functional correctness respectively. Test Program Generation for a Microprocessor: A Case Study

[5] VAMPasm is the assembly-level instruction set of VAMP, and VAMP is a pipelined RISC processor based on an out-of-order execution principle. Test Program Generation for a Microprocessor: A Case Study

[6] The VAMPasm model contains 56 instructions across memory transfer, constant transfer, register transfer, arithmetic/logical, test, shift, control, and interrupt-handling categories. Test Program Generation for a Microprocessor: A Case Study

[7] The Verisoft VAMP programmer's model was specified in Isabelle/HOL as transitions over ISA configurations containing a program counter, delayed program counter, general-purpose registers, special-purpose registers, and memory model. Test Program Generation for a Microprocessor: A Case Study

[8] The ISA-level VAMP configuration includes 30-bit program-counter fields, 32 general-purpose 32-bit registers, 32 special-purpose 32-bit registers, and a byte-addressable memory model. Test Program Generation for a Microprocessor: A Case Study

[9] VAMP implements the full DLX instruction set from Hennessy and Patterson, including load/store, shift, jump-and-link, arithmetic, and logical operations. Test Program Generation for a Microprocessor: A Case Study

[10] An assembly-language abstraction of the VAMP ISA represents addresses as natural numbers and register and memory contents as integers. Test Program Generation for a Microprocessor: A Case Study

[11] The assembler model abstracts additional ISA features: readable abstract instruction datatypes, no visible address translation, linear virtual memory, no visible interrupts, and a record-based configuration using natural-number counters, integer-list registers, and a natural-to-integer memory mapping. Test Program Generation for a Microprocessor: A Case Study

[12] HOL-TestGen was used to generate test sequences from the VAMP model, and its Isabelle/HOL basis enabled reuse of existing HOL verification models. Test Program Generation for a Microprocessor: A Case Study