Using Event-B to construct Instruction Set Architectures

Steve Wright, Kerstin Eder

Research output: Contribution to journalArticle (Academic Journal)peer-review

3 Citations (Scopus)


The instruction set architecture (ISA) of a computing machine is the definition of the binary instructions, registers, and memory space visible to an executable binary image. ISAs are typically implemented in hardware as microprocessors, but also in software running on a host processor, i.e. virtual machines (VMs). Despite there being many ISAs in existence, all share a set of core properties which have been tailored to their particular applications. An abstract model may capture these generic properties and be subsequently refined to a particular machine, providing a reusable template for development of robust ISAs by the formal construction of all normal and exception conditions for each instruction. This is a task to which the Event-B formal notation is well suited. This paper describes a project to use the Rodin tool-set to perform such a process, ultimately producing two variants of the MIDAS (Microprocessor Instruction and Data Abstraction System) ISA as VMs. The abstract model is incrementally refined to variant models capable of automatic translation to C source code, which this is compiled to create useable VMs. These are capable of running binary executables compiled from high-level languages such as C, and compilers targeted to each variant allow demonstration programs to be executed on them.
Translated title of the contributionUsing Event-B to construct Instruction Set Architectures
Original languageEnglish
Pages (from-to)73-89
JournalFormal Aspects of Computing
Issue number1
Publication statusPublished - Jan 2010

Bibliographical note

Other identifier: 2001146


Dive into the research topics of 'Using Event-B to construct Instruction Set Architectures'. Together they form a unique fingerprint.

Cite this