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]
Verisoft architecture
The Verisoft architecture was organized into four main layers: application software, system software, tools, and hardware. Each layer was itself structured into sub-layers. [C3]
At the application-software layer, the project included foundational proofs supporting verification of system-level concurrent programs running as user processes on VAMOS. At the system-software layer, VAMOS provided infrastructure for memory virtualization, hardware-device communication, processes represented as assembly-instruction sequences, and inter-process communication by synchronous message passing. At the tools layer, compiler correctness was to be verified. At the hardware layer, the functional correctness of the hardware design was formally verified. [C4]
VAMP and VAMPasm
Verisoft's hardware layer included VAMPasm, the assembly-level instruction set of the Verified Architecture Microprocessor. VAMP is described as a pipelined reduced-instruction-set-computer processor based on an out-of-order execution principle. [C5]
The VAMPasm model used in the cited case study contains 56 instructions: 8 memory-data-transfer instructions, 2 constant-data-transfer instructions, 2 register-data-transfer instructions, 14 arithmetic and logical instructions, 16 test instructions, 6 shift instructions, 6 control instructions, and 2 interrupt-handling instructions. [C6]
Isabelle/HOL processor model
In the context of Verisoft, an Isabelle/HOL programmer's-model specification of the VAMP processor was introduced. The model defines the processor as transitions over instruction-set-architecture configurations. Each ISA configuration contains five elements: a program counter, a delayed program counter, general-purpose registers, special-purpose registers, and a memory model. [C7]
The ISA-level VAMP model includes 30-bit program-counter and delayed-program-counter registers, 32 general-purpose 32-bit registers, 32 special-purpose 32-bit registers, and a byte-addressable memory model. The first general-purpose register is always set to zero, and special-purpose registers include, for example, a status register containing interrupt masks. [C8]
VAMP implements the full DLX instruction set from Hennessy and Patterson, including load and store operations for double words, words, half words, and bytes; shift operations; jump-and-link operations; and arithmetic and logical operations. [C9]
Assembly-level abstraction
To avoid complex bit-vector representations of data and instructions, an assembly-language abstraction of the VAMP ISA was introduced. In that abstraction, addresses are represented by natural numbers, while register and memory contents are represented by integers. [C10]
The Isabelle theory for the assembler model abstracts additional ISA features: instructions are represented as an abstract datatype with readable names, address translation is not visible, assembler computations operate in a linear virtual memory space, and interrupts are not visible at this level. The assembler configuration is represented as a record containing natural-number program-counter fields, integer-list register files, and a memory mapping from natural numbers to integers. [C11]
Role in test generation
The cited test-generation case study reused Verisoft's VAMP model to generate test cases for checking whether hardware conforms to the VAMP processor model. The authors note that HOL-TestGen is built on Isabelle/HOL and that its integration with Isabelle/HOL allowed direct reuse of existing higher-order-logic verification models. [C12]