PhD Thesis: Formal Construction of Instruction Set Architectures

Abstract

The Instruction Set Architecture (ISA) is that part of a computing machine visible for programming, including its native data types, instructions, registers, memory architecture, exception handling and external interfaces. The ISA also includes the specification of the machine’s native language: that is its instructions and their actions. This thesis proposes the use of the Event-B formal notation to construct a sequence of formal specifications applicable to a range of ISAs, by abstractly capturing their shared properties. Initial, very abstract, descriptions are refined by the incremental addition of greater detail, each increment providing a template for development of the next. The use of Event-B allows correctness, i.e. the preservation of the properties of the previous step, to be verified over successive refinements. This is achieved by the creation and proving of logical hypotheses, or proof obligations. The process enables development of ISAs with predictable behaviour when executing both correct and erroneous programs, by identification of the precise preconditions required for successful execution of instructions, their resulting actions, and all possible error conditions. Application of property proving techniques allows for the formal verification of desirable properties. A methodology is proposed for the incremental construction of the common elements of an ISA, and its features are discussed. The methodology is initially used to construct a generic description, which is then demonstrated by refinement to two representative ISAs capable of executing compiled C binary executables. The complete refinement process is demonstrated by the creation and testing of Virtual Machines automatically generated via novel translation tools. Prior art has relied on the provision of single-layered descriptions of specific ISAs to enable formal verification of implementations, placing a burden of correctness on these specifications. This work contributes by the provision of a common context for correct derivation of these previously independant descriptions. The work introduces novel levels of abstraction to allow re-use on any sequential computing machine, provides a framework for the comparison of different ISAs relative to a single datum, and enables analysis of design options during the creation and extension of ISAs. Further contributions are the construction of multiple ISAs from a single abstract description, and the introduction of automatic source-code generation techniques to the Event-B method, which include features to assist in the development and test of useable ISAs.