HOL CASE STUDY

Microprocessor Systems

Author

Jeff Joyce Dept. of Computer Science University of British Columbia Vancouver, British Columbia Canada V6T 1W5 Telephone: (604) 228-3061

Email: joyce@ca.ubc.cs

Concepts illustrated

Multi-level specification and verification, abstract description and specification of hardware, parameterization of theories, proof techniques based on symbolic execution, embedding other calculi in higher-order logic.

Prerequisites

Familiarity with HOL language syntax as given in Getting Started with HOL. Familiarity with the HOL system is not essential.

Supporting files

In the directory hol/Training/studies/microprocessor.

Abstract

The multi-level specification and verification of a very simple microprocessor is described. A relationship between specifications for its implementation, the external environment, and its intended behaviour is rigorously established by formal proof using the HOL system. This case study gives a detailed description of how the HOL language can be used to specify hardware structure and behaviour. It also outlines a strategy for using the HOL system to verify a set of correctness theorems which relate different levels of specification. The main proof technique is the use of inference rules to symbolically execute microinstructions and microcode. A form of temporal logic is embedded in the HOL logic for the special purpose of reasoning about asynchronous interactions between the microprocessor and external memory.

Contents

1 Introduction 5 1.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.3 Supporting files . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2 Programming level model 9 2.1 Basic data types and primitive operations . . . . . . . . . . . . . . . . . . 10 2.2 Externally visible state . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.3 Instruction word format . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.4 Instruction set semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.5 Hardware interrupts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

3 Memory interface 15 3.1 Fully synchronous mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2 Fully asynchronous mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.3 Extended cycle mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

4 Internal architecture 18 4.1 Register-transfer level structure . . . . . . . . . . . . . . . . . . . . . . . . 19 4.2 Overview of instruction interpretation . . . . . . . . . . . . . . . . . . . . . 19 4.3 Multiple interpretation levels . . . . . . . . . . . . . . . . . . . . . . . . . . 22

4.3.1 Microprogramming level . . . . . . . . . . . . . . . . . . . . . . . . 23 4.3.2 Phase level . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

4.4 Some bottom level assumptions . . . . . . . . . . . . . . . . . . . . . . . . 29

5 Abstract description and specification 30 5.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 5.2 Formal basis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

6 Formal specification 36 6.1 Specifying structure and behaviour . . . . . . . . . . . . . . . . . . . . . . 36 6.2 Internal architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

6.2.1 Primitive components of the datapath . . . . . . . . . . . . . . . . 37 6.2.2 Modelling system bus operation . . . . . . . . . . . . . . . . . . . . 38 6.2.3 More primitive components of the datapath . . . . . . . . . . . . . 40 6.2.4 Datapath implementation . . . . . . . . . . . . . . . . . . . . . . . 41 6.2.5 Microcode source and micro-assembler . . . . . . . . . . . . . . . . 42 6.2.6 Primitive components of the control unit . . . . . . . . . . . . . . . 47 6.2.7 Control unit implementation . . . . . . . . . . . . . . . . . . . . . . 48 6.2.8 Top level structure . . . . . . . . . . . . . . . . . . . . . . . . . . . 48

6.3 Programming level model . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 6.4 External memory specification . . . . . . . . . . . . . . . . . . . . . . . . . 53 7 Verification plan and methodology 53

7.1 Stating correctness results . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 7.2 Multi-level verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 7.3 Symbolic execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

8 Formal verification: ‘bread and butter’ method 56 8.1 Phase level . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 8.2 Microprogramming level . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 8.3 Completing the proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74

9 Synchronizing multiple levels of timing 79

10 Using temporal logic to deal with asynchrony 85 10.1 Specification using temporal logic operators . . . . . . . . . . . . . . . . . 86 10.2 Embedding temporal logic in higher-order logic . . . . . . . . . . . . . . . 87 10.3 Sender and receiver specifications . . . . . . . . . . . . . . . . . . . . . . . 89 10.4 Memory specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 10.5 Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91

10.5.1 Phase level . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 10.5.2 Implementation of the sender specification . . . . . . . . . . . . . . 92 10.5.3 Collapsing repeat-loops to single steps . . . . . . . . . . . . . . . . 92 10.5.4 Symbolic execution . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 10.5.5 Top level correctness statement . . . . . . . . . . . . . . . . . . . . 95

11 What has been proved ? 96

12 Relating this proof to other levels 98 12.1 Lower levels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 12.2 Higher levels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101

13 Summary 103

14 References 105

15 Suggested exercises 110

A Appendix: phase level correctness results 111

B Appendix: asynchronous memory specification 119

List of Figures

1 Functional View of the TAMARACK-3 Microprocessor. . . . . . . . . . . . 6 2 Fully Synchronous Operation. . . . . . . . . . . . . . . . . . . . . . . . . . 16 3 Synchronizing Data Transfer with Handshaking Signals. . . . . . . . . . . . 17 4 Fully Asynchronous Operation. . . . . . . . . . . . . . . . . . . . . . . . . 17 5 Extended Cycle Operation. . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 6 Register-Transfer Level Architecture. . . . . . . . . . . . . . . . . . . . . . 20 7 Hierarchy of Interpretation Levels. . . . . . . . . . . . . . . . . . . . . . . . 23 8 Control Unit Finite-State Machine Flow Diagram. . . . . . . . . . . . . . . 25 9 Mapping from FSM States to Datapath Actions. . . . . . . . . . . . . . . . 27 10 ADD Instruction Cycle Timing. . . . . . . . . . . . . . . . . . . . . . . . . 75 11 JMP Instruction Cycle Timing. . . . . . . . . . . . . . . . . . . . . . . . . 75 12 Control Part of an Interpreter. . . . . . . . . . . . . . . . . . . . . . . . . . 80 13 Abstract and Concrete Time Scales. . . . . . . . . . . . . . . . . . . . . . . 82 14 Four-Phase Handshaking Timing Diagram. . . . . . . . . . . . . . . . . . . 86

List of Tables

1 TAMARACK-3 Instruction Set . . . . . . . . . . . . . . . . . . . . . . . . 12

A Simple Microprocessor System

1 Introduction

This case study describes how the HOL system has been used to verify the design of a very simple microprocessor called TAMARACK-3. This microprocessor has just eight programming level instructions and a single addressing mode. The only kind of exception is a single level, non-vectored hardware interrupt. The microprocessor can be interfaced to external memory to operate in one of three possible modes: fully synchronous, fully asynchronous, and extended cycle mode. All I/0 is memory-mapped. Figure 1 shows a functional diagram for the externally available signals of TAMARACK-3 (excluding clock signals, reset signal and voltage sources). These signals would be pins or groups of pins in a microchip implementation of this design.

The original version of this example was described by Gordon [23, 25] for a predecessor of the HOL system called LCF LSM [24]. This example was re-done in HOL, implemented as a CMOS microchip (as an exercise in verification-driven design), and given the name TAMARACK-1 [31, 32, 40]. The design was then streamlined in TAMARACK-2 by eliminating some unessential control features as a first step in the development of this case study. The version described here, TAMARACK-3, is distinguished from earlier versions by the addition of a hardware interrupt mechanism and the ability to interact asynchronously with external devices using handshaking signals. Gordon’s original version of this example has also been used to illustrate several other approaches to simulating and verifying hardware. This includes work by Barrow [3], Camilleri [8, 9], Curzon [16], Davie [17], Richards [50], Shankar et al. [42], Van Tassel [54], and Weise [56].

Because TAMARACK-3 was designed as a verification example, it is not seriously intended for practical applications. ^{1} We have deliberately avoided some kinds of complexity found in ‘real designs’ such as multiple addressing modes which do not necessarily contribute interesting verification problems aside from the very important problem of managing the sheer size of such proofs. Multiple addressing modes are not provided because the problem of establishing correctness results for a particular instruction in different addressing modes is largely a matter of repeating the same proof strategy with slight variations for each case.

The relatively simple design of TAMARACK-3 is obviously an advantage when presenting this case study as an introduction to verifying microprocessor systems. But not every as-

1But with a few more ALU functions, more kinds of conditional branches, and an alternative to absolute addressing for instruction operands, it is possible to imagine the use of a TAMARACK-like microprocessor in a very simple real-time control application (see suggested exercise in Section 15)

TAMARACK-3

[figure]

          datain
            dack
            idle
            ireq

[figure] [figure]

                                                wmem
                                                dataout
                                                dreq
                                                addr
                                                iack

datain - data from memory  wmem  - read/write select
dack  - data acknowledge  dataout - data to memory
idle  - extended cycle mode  dreq  - data request
ireq  - interrupt request  addr  - address to memory
iack  - interrupt acknowledge

Figure 1: Functional View of the TAMARACK-3 Microprocessor. pect of TAMARACK-3 is completely trivial. By avoiding as much uninteresting complexity as possible, we have been left with a great deal of flexibility to consider several problems at the forefront of research into the use of formal methods to verify microprocessor systems. Some of the research problems considered in this work are:

• Strategies and techniques for structuring a formal verification into several layers.

• Trade-offs between using functions and relations for various parts of the formal specification.

• Reasoning about intrinsically complex aspects of system timing such as the interaction of a microprocessor with external devices.

Most of the basic proof techniques described in this case study are standard in HOL circles. Readers curious about how these basic techniques scale upwards to the complexity of a real design are referred to work by Cohn [12, 13, 14] on using the HOL system to verify the commercially-available VIPER microprocessor [15]. In addition to these basic techniques, some technical points of interest in this case study are:

• The use of uninterpreted data types (represented as polymorphic variables) in place of special-purpose data types for reasoning about hardware.

• The ‘parameterization’ of the formal theory^{2} by a representation variable which can be used to relate this theory to other levels of proof.

• Embedding another calculi, namely, a form of temporal logic, in the framework of higher-order logic.

The work described this case study owes much to previous work by Hunt on the FM8501 microprocessor [30, 4, 5] and by Cohn on the VIPER microprocessor [12, 13, 14]. These two examples are widely seen as the current state-of-the-art in microprocessor verification. Hunt was the first (as far as we know) to consider the problem of reasoning about the implementation of a handshaking protocol in a microprocessor system. Cohn’s work on VIPER has contributed a deep appreciation of the scope and limits of using formal methods to verify microprocessor systems.

The diversity of structure and behaviour in a typical microprocessor provides a rich source of verification problems. For this reason, it is likely that microprocessor verification will be the main-spring of many future developments in hardware verification.

1.1 Overview

This case study is less closely tied to the intricacies of the HOL system than some of the other case studies in this tutorial. This is partly due to the size of the formal specifications and proofs of correctness. We also interested in reaching a more general audience than just HOL users as a basis for comparisons between the HOL approach (the system, the logic and conventional specification style) and other approaches to verifying microprocessor systems.

2The term ‘theory’ has a technical meaning in the HOL system, but we use this term more generally throughout this case study to mean the formal specification of TAMARACK-3 and its logical consequences.

Readers with access to the HOL system who want to experiment with the HOL system by re-running parts of this proof will find essential documentation in Sections 5 and 6. A very straightforward version of the proof (the so-called “Bread and Butter” method) is outlined in Sections 7 and 8. Enhancements and extensions to this proof (which may only interest some readers) are described in Sections 9 and 10.

Because the proof of correctness is too large to describe in terms of HOL interactions, most of our discussion consists of proof sketches which outline the main steps in the proof. However, Sections 8.1 and 8.2 illustrate some details of how these proof steps are achieved by showing a sequence of intermediate results extracted from a HOL session. This may be helpful to readers who are interested in the level of interaction with the HOL system required for this kind of proof.

Other readers with a more general interest in how formal proof can be used to reason about a large hardware design will find methodology discussed throughout this document. Some of our discussion concerns the HOL system, but much of it is also relevant to verifying hardware in other verification systems besides the HOL system. One of the aims of the work described in this case study is to avoid using special-purpose infra-structure for reasoning about hardware which might make it difficult to re-produce hardware proofs in other verification systems.

We begin by describing the design and operation of TAMARACK-3 in a conventional style of informal microprocessor description. This informal description is divided into three main parts: programming level model, memory interface, and internal operation. Some aspects of this informal description are essential documentation. Other, less-essential parts of this informal description are mostly intended to provide background for proof strategies.

1.2 Notation

Machine-readable HOL syntax is used in this document except for the following substitutions where conventional symbols from logic have been used instead of standard ASCII characters. Section 10 describes a set of additional substitutions, e.g., □, ◇, used exclusively in our discussion of how temporal logic can be embedded in the HOL logic.

∀ replaces !  ¬ replaces ~

      ∃  "     ?  λ  "     \
      ∧  "     /\  ε  "     @
      ∨  "     \/

1.3 Supporting files

Formal Specification

Section 5 \{ \begin{matrix}header.ml & - representation variable type \\ rep.ml & - basic data types and operations \end{matrix} Section 6 \{ \begin{matrix}impspec.ml & - internal architecture \\ behspec.ml & - programming level model \\ synspec1.ml & - memory model and correctness conditions \\ example1.ml & - assembling microcode with proof rules \end{matrix}

Formal Verification: “Bread and Butter” Method

Section 8 \{ \begin{matrix}proof1.ml & - symbolic execution of phase level \\ example2.ml & - detailed view of phase level \\ proof2.ml & - symbolic execution of microprogramming level \\ example3.ml & - detailed view of microprogramming level \\ proof3.ml & - top level correctness result (version 1) \end{matrix}

Synchronizing Multiple Levels of Timing

Section 9 \{ \begin{matrix}tempabs.ml & - temporal abstraction \\ synspec2.ml & - memory model and correctness conditions \\ proof4.ml & - symbolic execution of microprogramming level \\ proof5.ml & - top level correctness result (version 2) \end{matrix}

Using Temporal Logic to Deal with Asynchrony

Section 10 \{ \begin{matrix}tlops.ml & - temporal logic operators and derived rules \\ handspecs.ml & - sender and receiver specifications \\ handthms1.ml & - handshaking theorems (sender conditions) \\ handthms2.ml & - handshaking theorems (data transfers) \\ asynspec.ml & - memory model and correctness conditions \\ proof6.ml & - correct implementation of sender conditions \\ example4.ml & - simple implementation of sender conditions \\ proof7.ml & - collapse ‘waitidle’ loops to single steps \\ proof8.ml & - collapse ‘waitdack’ loops to single steps \\ proof9.ml & - symbolic execution of microprogramming level \\ proof10.ml & - top level correctness result (version 3) \end{matrix}

Relating This Proof to Other Levels

Section 12 { example5.ml - linking this proof into a verified stack

2 Programming level model

The programming level model, or external architecture, of TAMARACK-3 is a description of its operation as seen by a programmer. This model hides all aspects of the internal architecture which the programmer does not need to know about when writing programs for this microprocessor.

The programming level model can be viewed as an interpreter for manipulating a set of variables which corresponds to the externally visible state of the microprocessor. It consists of four main parts:

• Basic data types and primitive operations.

• Variables manipulated by the interpreter.

• Format of instructions.

• Instructions semantics.

Our presentation of the programming level model is organized around these four main parts. Although we describe hardware interrupts separatedly from the semantics of ordinary program instructions, hardware interrupts in TAMARACK-3 can be regarded as just another kind of instruction in the programming level model. ^{3}

2.1 Basic data types and primitive operations

We begin with the basic data types and primitive operations used in the programming level model. The data type :bool is used to represent voltage values or logical conditions. The data type :num is used when some lower level form of data is interpreted as the representation of a natural number. The remaining data types correspond to machine words, groups of bits within a machine word, and memory states. A complete list of basic data types used in the programming level model is shown below.

:bool  - Boolean values {T,F}
:num  - natural numbers {0,1,2,… }
:*wordn  - full-size machine words
:*word3  - instruction opcodes
:*address - memory addresses
:*memory - memory states

A conventional description would typically be very precise about details such as the number of bits in a machine word and the size of memory. However, we avoid specifying these details by regarding :*wordn, :*word3, :*address and :*memory as uninterpreted types. The actual representation of these basic data types may be thought of as implementation dependent details. We use the prefix * to distinguish these as uninterpreted types.

Functional elements such as the ALU (Arithmetic Logic Unit) at the lowest level of architectural description perform various operations on data. It is also possible and desirable to avoid specifying any details about these operations. Instead, these operations are regarded as uninterpreted primitives. Primitive operations used to describe the design and operation of TAMARACK-3 are listed below along with an informal description of their types. Although we use the syntax of HOL to describe these types, a slightly different set of types is used in the formal theory for reasons explained later in Section 5.2.

3This is because the current instruction cycle executes to completion before an interrupt request is allowed to interrupt the normal flow of program execution. Instructions are also indivisible (with respect to external interrupt requests) in many commercially-available microprocessors such as the M68000.

  iszero   :*wordn→bool  test if zero
  inc      :*wordn→*wordn  increment
  add      :(*wordn×*wordn)→*wordn  addition
  sub      :(*wordn×*wordn)→*wordn  subtraction

wordn    :num→*wordn  representation of a number
valn     :*wordn→num  value of a full-size word

  opcode   :*wordn→*word3  extract opcode field

val3     :*word3→num  value of an opcode

  address  :*wordn→*address  extract address field
  fetch    :(*memory×*address)→*wordn  read memory
  store    :(*memory×*address×*wordn)→*memory write memory

The above list also gives a suggested interpretation for each of the uninterpreted primitives. Although we avoid specific details about the operations denoted by these uninterpreted primitives, we sometimes relax our presentation style by referring to an uninterpreted primitive in terms of its suggested interpretation.

Our use of uninterpreted types for data and uninterpreted primitives for operations on these data types is one of the key concepts presented in this case study. It reflects our approach to formal specification which aims to separate irrelevant detail from those aspects of the design have been formally considered in the formal proof of correctness. We elaborate on this idea and our approach to formal specification later in Section 5. Furthermore, by not specifying any details about basic data types or primitive operations on data, we have an informal description which is generalized over a whole range of possible word and memory sizes and possible interpretations for the primitive operations.

2.2 Externally visible state

The set of variables manipulated by the programming level model corresponds to the externally visible state of the microprocessor. In TAMARACK-3, these variables are:

mem - memory
pc  - program counter
acc - accumulator
rtn - return address register
iack - interrupt acknowledge flag

The memory stores memory states, represented by the data type :*memory. Each of the registers stores full-size memory words, represented by the data type :*wordn. The interrupt acknowledge flag is stored internally by a flipflop whose value belongs to the data type :bool.

2.3 Instruction word format

Instructions are exactly one full-size machine word. Although specific details about word size and instruction word format are not given in this description, we can assume that the

Instruction Opcode Value Effect
JZR  0  jump if zero
JMP  1  jump
ADD  2  add accumulator
SUB  3  subtract accumulator
LDA  4  load accumulator
STA  5  store accumulator
RFI  6  return from interrupt
NOP  7  no operation

Table 1: TAMARACK-3 Instruction Set

instruction word consists of a 3-bit opcode (since there are eight different instructions) with the remaining bits used as an operand address. The operand address is the absolute address of a memory word which may be used as the address of either data or an instruction.

3-bit opcode  operand address

Opcodes and operand addresses are represented by the uninterpreted types :*word3 and :*address. They are extracted from an instruction word by the uninterpreted primitives

opcode and address.

2.4 Instruction set semantics

The eight TAMARACK-3 programming level instructions are in Table 1. Their opcode values and a brief explanation of each instruction are also given in the table. The opcode is extracted from the current instruction word by opcode and its numerical value is then obtained by applying val3 to the extracted opcode.

The four data processing instructions, ADD, SUB, LDA and STA, involve both the accumulator acc and memory mem. The other four instructions, JZR, JMP, RFI and NOP, are control instructions with no effect on either the accumulator or memory. The only conditional branch, JZR, tests whether the accumulator acc contains the machine representation of zero.

The address of the current instruction is always given by the program counter pc at the beginning of each instruction cycle. Operationally, the program counter pc is full-size register but only the address field of this register is used to access the current instruction word from memory. When a jump is taken as a result of either a JMP or JZR instruction, the entire instruction word is loaded into the program counter pc but only the address field has any significance.

The eight programming level instructions are described in the below. Only changes to the current state of the external architecture are described. Unaffected components of the externally visible state are not mentioned. Some of these descriptions are simplified by using the abbreviations,

     inst = fetch (mem,(address pc))
     operand = fetch (mem,(address inst))

for the current instruction word and the operand addressed by this instruction. The informal notation,

<destination> ← <expression>

is used to denote when a value computed from the current machine state is loaded into a register, flipflop or memory to form a component of the next machine state.

JZR - jump if zero

     pc ← if iszero acc then inst else inc pc

If the result of applying iszero to the current contents of the accumulator acc is T, then the current instruction word is loaded into the program counter pc. Otherwise, the inc operation is applied to the current contents of the program counter pc to obtain its new value.

JMP - jump

     pc ← inst

The current instruction word is unconditionally loaded into the program counter pc.

ADD - add accumulator

     acc ← add (acc,operand)
     pc ← inc pc

The add operation is applied to the current contents of the accumulator acc and the memory word addressed by the operand address field of the current instruction. The result is loaded into the accumulator acc. The inc operation is applied to the current contents of the program counter pc to obtain its new value.

SUB - subtract accumulator

     acc ← sub (acc,operand)
     pc ← inc pc

The sub operation is applied to the current contents of the accumulator acc and the memory word addressed by the operand address field of the current instruction. The result is loaded into the accumulator acc. The inc operation is applied to the current contents of the program counter pc to obtain its new value.

LDA - load accumulator

     acc ← operand
     pc ← inc pc

The memory word addressed by the operand address field of the current instruction is loaded into the accumulator acc. The inc operation is applied to the current contents of the program counter pc to obtain its new value.

STA - store accumulator

     mem ← store (mem,address inst,acc)
     pc ← inc pc

The current contents of the accumulator acc are stored in external memory at the location specified by the operand address field of the current instruction. The inc operation is applied to the current contents of the program counter pc to obtain its new value.

RFI - return from interrupt

     pc ← rtn
     iack ← F

The current contents of the return address register rtn are loaded into the program counter pc and the interrupt acknowledge flag iack is reset to F. This instruction does not check whether the interrupt acknowledge flag iack is currently set.

NOP - no operation

     pc ← inc pc

The inc operation is applied to the current contents of the program counter pc to obtain its new value.

2.5 Hardware interrupts

In the normal flow of program execution, instructions are sequentially executed according their semantics described in Section 2.4. The only kind of exception is a single level, nonvectored, non-maskable hardware interrupt which is generated by setting the interrupt request pin irq to T.

An interrupt request will be detected and processed as soon as execution of the current instruction is completed. Normally, the interrupt will be detected within a few clock cycles but this may be delayed for an arbitrary number of clock cycles when the microprocessor is operating in either fully asynchronous mode or extended cycle mode. Because only a single level of interrupt is supported, the value of the interrupt request pin irq will be ignored if the interrupt acknowledge flag is already T indicating that a previous interrupt is still being serviced.

     if iack = F then
        pc ← 0
        rtn ← pc
        iack ← T

The interrupt request is processed by saving the current value of the program counter pc in the return address register rtn, setting the interrupt acknowledge flag iack to T and loading the machine representation of zero into the program counter pc. The interrupt service routine is assumed to begin at location zero in memory.

At the end of the interrupt service routine, a return-from-interrupt instruction RFI is executed causing the saved return address stored in rtn to be loaded into the program counter pc and the interrupt acknowledge flag to be reset to F.

3 Memory interface

The microprocessor can be interfaced to external memory to operate in one of three possible modes: fully synchronous, fully asynchronous, or extended cycle mode. The mode of operation is selected by the input pins dack and idle. The dack pin is used as a handshaking signal in fully asynchronous mode and extended cycle mode. In extended cycle mode, the idle pin is used in place of a handshaking signal to indicate when the external memory is idle and ready to begin another interaction.

Although a bi-directional bus would typically be used to transfer data between a microprocessor and external memory, the design of TAMARACK-3 uses two separate unidirectional busses, datain and dataout. Data is sent to external memory on the dataout bus and received from external memory on the datain bus. Memory addresses are sent to external memory on the addr bus.

The operations performed by external memory are denoted by the uninterpreted primitives fetch and store. Although the synchronization details depend on the memory mode, the result of a read request is described by the equation,

     datain = fetch (mem,addr)

and the result of a write request is described by the following update to the internal state of memory.

     mem ← store (mem,addr,dataout)

Synchronization details for each of the three memory modes are described below.

3.1 Fully synchronous mode

In fully synchronous mode, every memory interaction is completed in a single cycle. The microprocessor is made to operate in this mode by wiring both of the pins idle and dack TAMARACK-3

           datain
             dack
             idle
             ireq

        T
        T

                                   wmem
                                   dataout
                                   dreq
                                   addr
                                   iack

Memory

Figure 2: Fully Synchronous Operation.

to T. A detailed timing analysis is needed to ensure that the external memory can always satisfy memory requests within a single clock cycle.

Figure 2 shows the interconnections between external memory and TAMARACK-3 when operating in fully synchronous mode. The memory request pin dreq is not needed in this mode because every clock cycle is assumed to be either a read or write request. The type of request is indicated by the wmem pin which is normally reset to F except when writing to memory.

3.2 Fully asynchronous mode

Fully asynchronous interaction with external memory is achieved when no assumptions are made about the speed of the external memory relative to the microprocessor clock speed. This allows the microprocessor to be interfaced to a mixture of fast and slow devices in the address space of external memory. The transfer of data (and memory addresses) between the microprocessor and external memory is synchronized by handshaking signals following the four-phase bundled data convention illustrated in Figure 3. It is only assumed that wire delays between the microprocessor and external memory are approximately uniform.

Figure 4 shows the interconnections between external memory and TAMARACK-3 when operating in fully asynchronous mode. In this mode, the idle pin is permanently wired to F. The acknowledgement signal dack is generated by the external memory (or by peripheral devices in the case of memory-mapped I/0).

A memory request is signaled by setting the memory request pin dreq to T. The type of request is indicated by the wmem pin which is normally reset to F except when writing to memory. After signaling a memory request, dreq must remain T and the wmem flag, address bus addr and dataout bus dataout must remain at stable values until dack becomes T signaling that the request has been satisfied. In the case of a read request, incoming data from the external memory will be stable from when the acknowledgement signal dack becomes T until the request signal dreq returns to its original value of F. Finally, the microprocessor waits for dack to also return to F before starting another memory request.

[figure: dack; datain; dreq; wmem; dataout; addr]

Figure 3: Synchronizing Data Transfer with Handshaking Signals.

TAMARACK-3

datain
  dack
  idle
  ireq

F

                        wmem
                        dataout
                        dreq
                        addr
                        iack

Memory

Figure 4: Fully Asynchronous Operation.

TAMARACK-3

          datain
            dack
            idle
            ireq

       T

                                   wmem
                                   dataout
                                   dreq
                                   addr
                                   iack

Memory

Figure 5: Extended Cycle Operation.

The use of handshaking signals to synchronize data transfers between the microprocessor and external memory requires very little extra circuitry and no additional control states. Best case performance by the external memory will result in exactly the same number of clock cycles as fully synchronous mode.

3.3 Extended cycle mode

A small, but significant variation of fully asynchronous memory interaction is found in many commercially-available microprocessors including VIPER [49]. In TAMARACK-3, this mode is selected by permanently wiring the idle pin to T as shown in Figure 5. As before, the acknowledgement signal dack is generated by external memory.

The only difference concerns the completion of the memory cycle after the request signal dreq has been reset to F. Unlike fully asynchronous mode, the control logic does not force the microprocessor to wait until the acknowledgement signal dack also returns to F before starting another memory request. Instead, it is assumed that the external memory will always complete the current memory cycle in time for another request to begin as early as the next clock cycle. This is a significant difference from fully asynchronous mode because the speed of external memory is no longer independent of the microprocessor clock speed.

Because extended cycle mode is very similar to fully asynchronous mode, it is ignored in the rest of this description. The formal proof of correctness for TAMARACK-3 does not consider this mode of operation.

4 Internal architecture

This section begins with a structural view of the internal architecture and an overview of how programming level instructions are interpreted by the hardware. This is followed by a more detailed view of the internal architecture as a series of increasingly concrete interpretation levels. Finally, we outline some bottom level assumptions which bridge the gap between our most detailed level of description and actual hardware.

4.1 Register-transfer level structure

Figure 6 shows a structural view of the TAMARACK-3 register-transfer level architecture. It consists of two main parts: a microcoded control unit and a single-bus datapath.

The control unit is implemented by the microcode program counter mpc, a ROM (Read Only Memory) for storing microcode, a decoder which separates the ROM output into various microinstruction fields, and combinational logic for computing the address of the next microinstruction.

The datapath includes the program counter pc, accumulator acc, return address register rtn, and interrupt acknowledge flag iack which are components of the externally visible state at the programming level. In addition to these, several internal registers are needed to interpret programming level instructions. These additional, full-size word registers are:

mar - memory address register
ir - instruction word register
arg - argument register for ALU input
buf - buffer for ALU output

The datapath also includes several functional elements:

alu  - four functions: add, sub, inc and the constant (wordn 0)
interface - switching between system bus and memory data pins
opc  - implements opcode for extracting opcode field
addr  - implements address for extracting address field
zeroflag - implements iszero to test for zero
dreq  - two-input OR-gate

The storage devices and functional elements of the datapath are interconnected by a single system bus. The width of the system bus is exactly one full-size machine word. The datapath is controlled by signals from the control unit which, in turn, receives feedback from the datapath.

4.2 Overview of instruction interpretation

Each TAMARACK-3 instruction is executed by a sequence of steps which varies depending on the particular instruction, the machine state and external inputs. In general, the following actions are taken by the internal architecture to interpret each programming level instruction.

• Check for interrupt request, otherwise continue …

• Fetch instruction addressed by program counter pc.

• Decode instruction.

[figure: interface; dreq; mar; addr; pc; acc; zeroflag; ir; opc; rtn; iack; arg; alu; buf; wmem; dataout; dreq; addr; iack; system; bus; wmem; rmem; wmar; wpc; rpc; wacc; racc; wir; rir; wrtn; rrtn; warg; alu0; alu1; rbuf; rom; mpc; next; dack; idle; ireq; datain]

Figure 6: Register-Transfer Level Architecture.

• Fetch operand if needed.

• Execute instruction.

• Increment program counter pc if necessary.

Not all of these actions are performed for each instruction. In particular, the control instructions JZR, JMP, RFI and NOP do not require an operand to be fetched from memory. Similarly, the program counter does not need to be incremented for the JMP and RFI instructions or for the JZR instruction when the jump is taken. There are several opportunities for overlapping some of these steps (e.g. incrementing the program counter while executing the current instruction) but this has not been done for the current design of TAMARACK-3 (see suggested exercise in Section 15).

The interpretation of an ADD instruction illustrates with greater detail how the internal architecture of TAMARACK-3 is used to implement its instruction set. An ADD instruction is interpreted by a sequence of data transfers over the system bus, interactions with memory, and operations on data performed by the various functional elements. The informal notation,

<destination> ← <expression>

is used here to denote when a value computed from the current machine state is loaded into a register, flipflop or memory to form a component of the next machine state. But unlike its previous use to describe state changes in the programming level model between instruction cycles, this informal notation now describes state changes at the registertransfer level between clock cycles.

Exactly eight steps are required to interpret the ADD instruction but some of these steps might be repeated (i.e., they are repeat-loops) when the microprocessor is operating in fully asynchronous mode ^{4}.

mar ← pc  repeat if ¬(idle or ¬dack)

    ir ← fetch (mem,(address mar))  repeat if ¬dack

mar ← ir  repeat if ¬(idle or ¬dack)
arg ← acc  repeat if ¬(idle or ¬dack)

    buf ← add (arg,fetch (mem,(address mar))) repeat if ¬dack

    acc ← buf
    buf ← inc pc
    pc ← buf

The equation,

     clock cycles = 8+n1+n2+n3+n4+n5

4The fetch operation performed by external memory is not necessarily completed until the last iteration of the repeat-loop.

gives the total number of clock cycles needed to interpret an ADD instruction. Since every step is executed at least once, at least eight clock cycles are required. The variables n1, n2, n3, n4 and n5 denote the number of additional clock cycles spent waiting for the external memory at various steps in the instruction cycle.

In fully synchronous mode, none of the eight steps are ever repeated because the pins idle and dack are both wired to T. In this case, the variables n1, n2, n3, n4 and n5 will all be equal to zero. Hence, the instruction cycle will be completed in exactly eight clock cycles.

In fully asynchronous mode, some of the above steps may be repeated but this will have no untoward effect except to increase the number of clock cycles. In this case when the microprocessor is using handshaking signals to interact with memory, the variables n1, n2, n3, n4 and n5 will depend on the latency of external memory. For best case performance, these variables will all be zero resulting in exactly the same number of clock cycles as fully synchronous mode. More generally, it is only known that each wait loop will eventually terminate. This fact depends on the correct implementation of the handshaking protocol by both the microprocessor and external memory; establishing this fact is a major step in the TAMARACK-3 proof of correctness.

In either mode of operation, the cumulative effect of the ADD instruction interpretation sequence is described by the following updates to the accumulator acc and the program counter pc.

     acc ← add (acc,fetch (mem,(address fetch (mem,(address pc)))))
     pc ← inc pc

Simplifying these expressions with the earlier mentioned abbreviations inst and operand, yields the programming level description of the ADD instruction semantics given earlier in Section 2.4.

     acc ← add (acc,operand)
     pc ← inc pc

The interpretation of the other seven programming level instructions and the processing of a hardware interrupt can be described in a similar way by a sequence of steps. Showing by formal proof for each programming level instruction that the cumulative effect of each sequence satisfies the semantics of that particular instruction is another major part of the TAMARACK-3 proof of correctness.

4.3 Multiple interpretation levels

The programming level model of a microprocessor sits at the top of a hierarchy of interpretation levels implemented by the internal architecture. The internal operation of a microprocessor can generally be described in terms of the following language levels [2].

programming level model

microprogramming level interpreter

phase level interpreter microinstruction sequences

control signals

Figure 7: Hierarchy of Interpretation Levels.

Programming level  - sequential execution of user programs
Microprogramming level - sequential execution of microcode
Phase level  - concurrent elementary hardware operations
Instant level  - asynchronous sequencing in a clock phase
Basic logic components - circuit level behaviour

This description of TAMARACK-3 focuses on the three highest levels of interpretation (i.e., only down to the phase level). The programming level has already been described in terms of the instruction set semantics and the hardware interrupt facility. Below the programming level, increasingly concrete views of the internal operation of TAMARACK-3 are described at the microprogramming level and at the phase level.

At the microprogramming level, a programming level instruction is interpreted by executing a sequence of microinstructions. This sequence of microinstructions is generated by a FSM (Finite State Machine) implemented by the control unit. Microinstructions are executed by an operational part corresponding to the datapath.

The phase level description decomposes the interpretation of a single microinstruction into the parallel execution of a set of elementary operations. This decomposition reveals the structural organization of the internal architecture in terms of register-transfer level components.

The concept of multiple interpretation levels is used by architects to achieve a “progressive translation of functions in several stages” [2]. We will later describe how this concept also provides a very effective strategy for controlling proof complexity in the formal verification of TAMARACK-3.

4.3.1 Microprogramming level

Every programming level instruction is interpreted by a different sequence of actions even though they share many individual steps in common. This sequence partially depends on the instruction opcode which is only known part way through the sequence after the instruction word has been fetched from memory. The sequence of steps taken may also depend on the machine state, in particular, on the contents of the accumulator acc in the case of a jump-if-zero JZR instruction.

The interpretation of each instruction, that is, the sequence of actions taken for each instruction, and similarly, the actions taken to process a hardware interrupt are determined by the control unit. The control unit FSM generates datapath commands (represented by microinstructions) each clock cycle. Each command causes an action to be performed by the datapath during the current clock cycle.

The interpretation algorithm implemented by the control unit FSM is based on conditional branches, that is, a Moore machine approach in contrast to a Mealy machine approach based on conditional instructions. Inputs are used to select the next machine state but do not determine the current output of the state machine. Some of these inputs consists of feedback from the datapath, in particular, the opcode field of the instruction word register ir contents, a test-accumulator-for-zero flag zeroflag, and the current value of the interrupt acknowledge flag iack. The FSM also receives external inputs from the idle, dack and ireq pins which determine the behaviour of the FSM. The FSM for the TAMARACK-3 control unit is described by the flow graph in Figure 8.

The start of an instruction cycle occurs when the FSM is in state 0 and about to exit to either state 1 or state 2. If an interrupt is requested and the iack flag is not already set, then the FSM exits to state 1 to process the interrupt. Otherwise, the FSM exits to state 2 and causes the current instruction word to be fetched from memory. In state 3, the FSM dispatches on the opcode field to the start of the remaining interpretation sequence for the current instruction. For instance, the interpretation of an ADD instruction would cause a transition from state 3 to state 6. From this point onwards, the FSM follows a sequence of state transitions leading back to state 0. In the case of a JZR instruction, the FSM selects one of two possible exits from state 4 depending the test-accumulator-for-zero feedback from the datapath. Assuming that the FSM never loops indefinitely in a particular state, then in all cases, including the processing of interrupts, the FSM always returns to state 0 to begin the next instruction cycle.

For example, the interpretation of an ADD instruction in fully synchronous mode results in the following sequence of states.

0, 2, 3, 6, 13, 15, 11, 12, and back to 0.

In fully asynchronous mode, additional clock cycles caused by delayed handshaking signals from the external memory could result in a sequence such as:

0, 2, 2, 2, 3, 3, 6, 13, 13, 13, 15, 11, 12, and back to 0.

Each FSM state causes a specific action to be performed by the datapath. The mapping from FSM states to actions is shown in Figure 9. This mapping, combined with the flow graph in Figure 8, gives a complete description of the internal architecture of TAMARACK-3 at one level of abstraction. This level of description contains no structural details aside from the conceptual distinction between the function of the control unit and the operation

[figure: waitidle = ¬(idle or ¬dack); waitdack = ¬dack; waitidle; 0; interrupt; 1; waitdack; 2; waitidle; 3; JZR; JMP; ADD; SUB; LDA; STA; RFI; NOP; 4; 5; waitidle; 6; waitidle; 7; waitdack; 8; waitdack; 9; 10; acc is zero; waitdack; 13; waitdack; 14; 15; 11; 12]

Figure 8: Control Unit Finite-State Machine Flow Diagram. of datapath. Although the components of the internal state are visible in this view, updates to machine state are described functionally. This abstract view of the internal architecture is the basis of an intermediate step in the formal verification of TAMARACK-3.

4.3.2 Phase level

Each command generated by the FSM is a microinstruction which is interpreted by a set of register-transfer level operations. The phase level description decomposes a microprogramming level action such as,

     buf ← add (arg,fetch (mem,(address mar)))

into the parallel execution of a set of elementary operations:

     addr = address mar
     datain = fetch (mem,addr)
     bus = datain
     alu = add (arg,bus)
     buf ← alu

This decomposition reveals the structural organization of the microprocessor. Each of the elementary operations shown above corresponds to a functional element of the register-transfer architecture or, in the case of fetch, to a primitive operation performed by external memory.

The phase level description of TAMARACK-3 also refines certain abstract features of the microprogramming level description. In particular, it reveals that the FSM is implemented by:

• A microcode program counter mpc to hold the current state of the FSM.

• The microcode ROM which encodes the abstract mapping from FSM states to actions given in Figure 9.

• A decoder which separates the ROM output into various microinstruction fields.

• The next address logic which computes the next FSM state according the flow graph given in Figure 8.

The microcode program counter is a register which stores values belonging to an uninterpreted data type:

:*word4 - FSM state

Several uninterpreted primitives for this data type are needed later on to describe the computation performed by the next address logic.

word4  :num→*word4 representation of a number
val4   :*word4→num numerical value of a FSM state

[figure: 0; ⟹; 8; ⟹; mar ← pc; acc ← datain; dreq = T]
[figure: 1; ⟹; 9; ⟹; rtn ← pc; buf ← wordn 0; iack ← T; dataout = acc; wmem = T; dreq = T]
[figure: 2; ⟹; 10; ⟹; ir ← datain; dreq = T; pc ← rtn; iack ← F]
[figure: 3; ⟹; 11; ⟹; mar ← ir; buf ← inc pc]

[figure: 4; ⟹; 12; ⟹; <nothing>; pc ← buf]

[figure: 5; ⟹; 13; ⟹; pc ← ir; buf ← add (arg,datain); dreq = T]
[figure: 6; ⟹; 14; ⟹; arg ← acc; buf ← sub (arg,datain); dreq = T]
[figure: 7; ⟹; 15; ⟹; arg ← acc; acc ← buf]

in all states except where indicated otherwise: wmem = F dreq = F dataout = wordn 0 addr = address mar Figure 9: Mapping from FSM States to Datapath Actions.

Every clock cycle, the current value of the microcode program counter mpc is used to fetch the current microinstruction from the microcode ROM. The microcode is horizontal which means, in this case, that every control signal is determined by a unique bit in the microinstruction word. The format of microinstruction words is shown below.

addr1      addr2 datapath control bits  next address logic control bits  microinstruction addresses

The fifteen datapath control bits are extracted from the output of the microcode ROM and sent to the data path over a set of control lines. These control bits generate individual control signals including ‘write’ signals for storage elements, ‘read’ signals for devices which can assert values onto the system bus, and signals to control the operation of the functional elements such as the ALU.

In addition to control bits for the datapath, the microinstruction word contains several other fields which are used to encode a partial computation of the next FSM state. The four next address logic control bits determine how the next address logic computes the next FSM state. The two microinstruction address fields, addr1 and addr2 (both of the type :*word4), specify destination fields for various kinds of conditional branches in the microcode which may be selected by the next address logic as the next FSM state. The next address logic is just a block of combinational logic whose function can be derived from the flow graph in Figure 8.

The interpretation of a microinstruction at the phase level during a single clock cycle results in a sequence of events which includes:

• Fetch the current microinstruction.

• Compute the address of the next microinstruction.

• Read data onto the system bus.

• Evaluate operations performed by functional elements.

• Update storage elements such as memory, registers and flipflops.

Some of these events clearly precede other events. For instance, the current microinstruction has to be fetched from the microcode ROM before it can be interpreted. On the other hand, many of these events take place concurrently: for example, the address of the next microinstruction is computed by the next address logic while the datapath executes the actions specified by the current microinstruction. Indeed, much of the activity during a clock cycle is not necessarily synchronized by an explicit control mechanism: a change in the inputs to a functional element such as the ALU might be propagated to its outputs after a few nanoseconds depending on its implementation.

Even though some constraints on the order of events during a clock cycle could be described, this has not be done in this description of TAMARACK-3. Instead, functional elements such as the ALU are modelled without delay and the update of storage elements is described as an atomic action. A fundamental feature of this abstraction is the assumption that updates to storage elements do not propagate to their outputs until the end of the clock cycle, i.e., there is no possibility of an closed feedback path resulting in a race condition.

4.4 Some bottom level assumptions

The relatively abstract view of how a microinstruction is interpreted during a single clock cycle is the lowest level in this description of TAMARACK-3. The phase level view is also the lowest level of specification in the formal proof of correctness. The semantic gap between this abstraction and actual hardware is bridged by several informally stated assumptions.

First of all, it is assumed that the design is implemented by digital circuitry in some kind of synchronous logic design style (e.g., two-phase, non-overlapping logic). Depending on the design style, certain rules must be followed to ensure, for instance, that updates to storage elements do not propagate to their outputs until the end of the clock cycle. Assuming that these rules have been followed and certain other constraints have been satisfied, ^{5} synchronous logic gives rise to the abstract view where functional elements are modelled without delay and the update of storage elements is described as an atomic action. ^{6}

Synchronous logic only ensures that this abstraction is valid for the internal logic; some additional considerations are required to ensure that this abstraction is valid for the interface between internal logic and external devices.

Asynchronous input events, such as a transition from F to T on the hardware interrupt request pin ireq, may occur at any time. In particular, they may occur at any point during the clock cycle used to synchronize the internal logic. Asynchronous input events may or may not be detected during the clock cycle depending on when they occur with respect to the minimum set-up time of any internal storage device that samples (directly or indirectly) this input. Carefully designed interface circuitry would be required to minimize the metastability problem, that is, the possibility of unstable equilibria in cross-coupled circuits [51].

5Conventional CAD tools are commonly used to check that synchronous logic has been correctly implemented with respect to the rules of a particular design style and that other constraints are satisfied (e.g., no problems with clock skew for a given clock period).

6Although the relatively abstract view of sequential behaviour in our lowest level of specification is valid, there is a semantic gap between this particular level of formal specification and the view of sequential behaviour supported by many sophisticated CAD tools. As it happened, this contributed to design error when the formal specification of TAMARACK-2 was hand-translated into the design specification language of the GENESIL silicon compiler system by Shankar et al. [42]. Even though the design was correct with respect to the built-in rules for the two-phase, non-overlapping design style, there was a mismatch between the single-phase view of sequential behaviour in the formal specification and the two-phase view supported by the silicon compiler. Although this experiment in verification-driven design revealed a semantic gap for this particular level of bottom level specification, this is does not represent any kind of inherent limitation of formal methods.

In addition to sampling asynchronous inputs, the internal logic generates asynchronous outputs such as the interrupt acknowledge flag iack. External outputs may be sampled at any point in continuous time and every change in their value is significant. During a clock cycle, synchronous logic may generate several transient values before settling on a set of final values. For signals used internally, these transient values have no effect, but additional interface circuitry may be required to ensure that transient values do not propagate to asynchronous outputs.

These informal assumptions underlie the abstract view of how a microinstruction is interpreted during a single clock cycle. In the formal theory, asynchronous input and output events are modelled with respect to the same discrete time scale used to model internal synchronous logic. The model represents the observed behaviour of the external environment as seen by the internal logic. An asynchronous output event is described by changing the value of an output signal between adjacent points of discrete time. It is assumed that the output signal is otherwise stable with respect to continuous time.

5 Abstract description and specification

The informal description of TAMARACK-3 introduced a set of basic data types and operations involving these data types. Specific details such as the number of bits in a machine word were avoided by regarding these data types and operations as uninterpreted types and uninterpreted primitives. In this section, we briefly explain some of the motivations for using uninterpreted types and uninterpreted primitives in our approach to formal specification. A more complete explanation may be found in [41]. We also describe a formal basis for using uninterpreted types and uninterpreted primitives in the HOL formulation of higher-order logic.

5.1 Motivation

The formal verification of TAMARACK-3 focuses very specifically on the register-transfer level operation of the internal architecture. Below and above this level there are aspects of a complete design for TAMARACK-3 which are not formally considered. For instance, the formal proof does not consider whether the register-transfer components have been designed correctly. Similarly, the formal proof only shows that the design satisfies the semantics of the instruction set but it does not consider whether these instructions could be combined to write useful programs.

To clearly demarcate the boundaries between what has and what has not been formally considered in this proof, we have taken an abstract approach to both the informal description and formal specification of TAMARACK-3. ^{7} Very few details are given about the basic data types and primitive operations used to describe the design and operation of TAMARACK-3.

7This abstract approach to the specification of TAMARACK-3 was prompted by discussions with researchers at SRI International, Menlo Park. The EHDM verification system developed at SRI also supports a form of abstract specification using parameterized modules [55]. Eveking has similarly advocated ‘the separation of concerns’ as a general principle of hardware verification [21].

This is quite different than conventional microprocessor descriptions which are usually very specific about details such as word size and various operations performed on data. Nevertheless, it is possible to explain and reason about a great deal of the internal architecture without specifying these details. The ability to make use of this abstract description without knowing these details is one way in which formal verification is distinguished from conventional simulation where these details would generally need to be known.

Because we do not specify details about basic data types and operations on basic data types, computational aspects of our formal theory are somewhat transparent. This is illustrated by the add operation which appears in both the bottom and top levels of description. At the bottom level, it is used to describe one of the functions performed by the ALU. At the top level, it is used to give the semantics of the TAMARACK-3 ADD instruction. The name of this operation strongly suggests that it has something to do with arithmetic addition, but the exact nature of this operation depends on both the word size and the particular representation of numbers, e.g., addition of unsigned 16-bit words. Although the name add is used to denote this operation, no particular meaning is associated with this operation except its type: it is only known to be an operation on a pair of machine words which yields another machine word as a result. The formal proof only shows that the ADD instruction is correctly implemented in the sense that the add operation is applied to the correct operands and the result stored in the correct destination by the end of the instruction cycle.

Another motivation for our abstract approach is pragmatic. A great deal of extra infrastructure in the formal theory can be avoided by using uninterpreted data types and uninterpreted primitive operations. The specification of TAMARACK-3 differs in this respect from earlier versions of this example [25, 31, 32] as well as the verification of VIPER [12, 13] by not using the built-in HOL types and postulated axioms (inherited from the LCF LSM system) for bit-patterns and machine words. This also means that this example can be re-produced in other formalisms which lack infra-structure for reasoning about hardware.

The cost of using uninterpreted types and uninterpreted primitives is surprisely small: just two assumptions about the data types and primitive operations are needed to verify TAMARACK-3. One of these assumptions, for instance, states that the numerical value of every 3-bit word is less than eight. These two assumptions appear explicitly in the correctness theorems.

As mentioned earlier, there is one more benefit of our abstract approach. By not specifying any details about word size or the primitive operations performed on data, we have an informal description and formal specification which are generalized over a whole range of possible word sizes and possible interpretations for the primitive operations.

5.2 Formal basis

Our use of the prefix * for uninterpreted data types in the informal description of TAMARACK-3, e.g., :*word, hinted at our intention to use polymorphic types for uninterpreted types in the formal specification. We also need a formal basis for uninterpreted primitives, e.g., add, which denote operations on these basic data types.

One possibility would be to simply introduce the names of these operations as constants in the formal theory. With this approach, the operations denoted by these constants would have fixed, unknown values. Although this approach is appealingly simple, the association of operation names with fixed, unknown values would be inconvenient if we ever wanted to extend the formal theory by giving an interpretation to the heretofore uninterpreted data types and primitive operations. ^{8}

Instead of a theory with constants denoting fixed, unknown values for primitive operations, we would like to ‘parameterize’, in an intuitive sense, the theory by the data types and primitive operations mentioned in the theory. The theory could be ‘instantiated’ by giving an interpretation to the data types and primitive operations (as we show in Section 12). This would be useful when combining correctness results for register-transfer architecture of TAMARACK-3 with another theory about the implementation of various register-transfer level components.

Although it is not possible, in a literal sense, to parameterize a HOL theory, the desired effect can be achieved in the HOL logic by parameterizing definitions in the theory by an extra variable, rep, which denotes the ‘representation’ of a theory.

The representation parameter can be thought of as a package containing values for each of the primitive operations. A particular operation can be specified by applying a selector function to the representation. To avoid introducing more names than necessary, we have just re-used names from the informal description for the corresponding selector functions. Whereas these names were used in the informal description to directly refer to primitive operations, they are used in the formal specification to denote selector functions which must be applied to the representation variable. Instead of saying,

‘the operation denoted by add’

we refer to this operation as:

‘the operation selected by add’

For instance, the terms inc, add and sub denote selector functions for the three operations performed by the ALU. Applying each of these terms to the representation variable rep yields the three ALU operations specified by the representation variable rep.

Like any other term in the HOL logic, the representation variable rep is associated with a type. We have taken the straightforward approach of representing this variable in the HOL logic as an n-tuple where each element corresponds to one of the primitive operations on uninterpreted data types. Selectors for primitive operations are defined in the formal theory by composing various sequences of the two selectors FST and SND.

8There is also a technical reason why this scheme might not work very well for the HOL system, in particular, that unbound type variables are not allowed in definitions.

The ML variable rep_ty is used throughout the formal specification to denote the compound type of the representation variable. When it appears inside a HOL term preceded by a caret ^(ML anti-quotation), it is expanded to the type expression shown below. This use of ML anti-quotation is unfortunate, but proper type abbreviation cannot be introduced here because this type expression contains polymorphic variables.

  let rep_ty =
    ":(*wordn->bool)#                       % iszero %
      (*wordn->*wordn)#                     % inc %
      (*wordn#*wordn->*wordn)#              % add %
      (*wordn#*wordn->*wordn)#              % sub %
      (num->*wordn) #                       % wordn %
      (*wordn->num) #                       % valn %
      (*wordn->*word3)#                     % opcode %
      (*word3->num)#                        % val3 %
      (*wordn->*address)#                   % address %
      (*memory#*address->*wordn)#           % fetch %
      (*memory#*address#*wordn->*memory)#   % store %
      (num->*word4)#                        % word4 %
      (*word4->num)";;                      % val4 %

The particular ordering of elements in this n-tuple is completely arbitrary. While a less concrete representation could be used, any extra effort in this regard is probably not worthwhile. Details of this particular representation are isolated to a very small part of the formalization, in particular, the following definitions of the selector functions for each of the primitive operations.

let iszero = new_definition (
`iszero`,
"iszero (rep:^rep_ty) = FST rep");;
let inc = new_definition(
`inc`,
"inc (rep:^rep_ty) = FST(SND rep)");;
let add = new_definition (
`add`,
"add (rep:^rep_ty) = FST(SND(SND rep))");;
let sub = new_definition (
`sub`,
"sub (rep:^rep_ty) = FST(SND(SND(SND rep)))");;
let wordn = new_definition (
`wordn`,
"wordn (rep:^rep_ty) = FST(SND(SND(SND(SND rep))))");;
let valn = new_definition (
`valn`,
"valn (rep:^rep_ty) = FST(SND(SND(SND(SND(SND rep)))))");;

let opcode = new_definition (
`opcode`,
"opcode (rep:^rep_ty) =
  FST(SND(SND(SND(SND(SND(SND rep))))))");;
let val3 = new_definition (
`val3`,
"val3 (rep:^rep_ty) =
  FST(SND(SND(SND(SND(SND(SND(SND rep)))))))");;
let address = new_definition (
`address`,
"address (rep:^rep_ty) =
  FST(SND(SND(SND(SND(SND(SND(SND(SND rep))))))))");;
let fetch = new_definition (
`fetch`,
"fetch (rep:^rep_ty) =
  FST(SND(SND(SND(SND(SND(SND(SND(SND(SND rep)))))))))");;
let store = new_definition (
`store`,
"store (rep:^rep_ty) =
  FST(SND(SND(SND(SND(SND(SND(SND(SND(SND(SND rep))))))))))");;
let word4 = new_definition (
`word4`,
"word4 (rep:^rep_ty) =
  FST(SND(SND(SND(SND(SND(SND(SND(SND(SND(SND(SND rep)))))))))))");;
let val4 = new_definition (
`val4`,
"val4 (rep:^rep_ty) =
  SND(SND(SND(SND(SND(SND(SND(SND(SND(SND(SND(SND rep)))))))))))");;

As just mentioned, two assumptions about uninterpreted types and uninterpreted primitives are needed to verify TAMARACK-3. These assumptions are expressed by predicates Val3_CASES_ASM and Val4Word4_ASM which are both parameterized by the representation variable rep.

  let Val3_CASES_ASM = new_definition (
    `Val3_CASES_ASM`,
    "Val3_CASES_ASM (rep:^rep_ty) = ∀w. ((val3 rep) w) < 8");;
  let Val4Word4_ASM = new_definition (
    `Val4Word4_ASM`,
    "Val4Word4_ASM (rep:^rep_ty) =
     ∀n. n < 16 ==> (((val4 rep) ((word4 rep) n)) = n)");;

The predicate Val3_CASES_ASM expresses the assumption that the numerical value of every 3-bit word is less than eight. The predicate Val4Word4_ASM expresses the assumption that :val4 and :word4 are inverses for numbers less than sixteen.

6 Formal specification

The formal specification of TAMARACK-3 is based on the informal descriptions given earlier in Sections 2, 3 and 4. It consists of three main parts:

• The design of the internal architecture in terms of its structural organization and behavioural models for primitive components.

• The programming level model based on the semantics of the instruction set and the processing of hardware interrupts.

• A specification of the external environment, in particular, a behavioural model for external memory.

We begin by describing how structure and behaviour are represented in the formal specification. Following these preliminaries, we present the three main parts of the formal specification of TAMARACK-3.

6.1 Specifying structure and behaviour

The specification of TAMARACK-3 models devices at all levels of the specification hierarchy by predicates which express relations on time-dependent signals. These predicate are parameterized, in part, by variables representing physical input and output signals. They may also be parameterized by other signals representing the internal state or external conditions governing the behaviour of the device. Time-dependent signals are modelled as functions from discrete time to signal values. As shown in the following type abbreviation, discrete time is represented by the natural numbers.

  new_type_abbrev (`time`,":num");;

The behaviour of a primitive device is specified directly in terms of defined operators such as logical connectives and arithmetic functions. The uninterpreted primitives just described in Section 5.2 may also be used to directly specify the behaviour of a device. Typically, the behaviour of a primitive component is expressed by an equation for output signals in terms of input signals, internal state, and external conditions. Universal quantification over explicit time variables is used to state that the behaviour holds at all points in discrete time.

The behaviour of a non-primitive device is specified indirectly by composing behaviours for simpler devices. The interconnection of components through similarly-named ports is expressed by logical conjunction. Existential quantification is used to hide internal signals. This can be viewed as a structural specification of the device.

6.2 Internal architecture

The formal specification of the internal architecture of TAMARACK-3 begins with behaviour models for primitive components such as the ALU and the registers. Higher up the specification hierarchy, non-primitive devices such as the control unit and datapath are specified structurally as the composition of simpler devices.

As explained earlier in Section 4.4, the internal operation of TAMARACK-3 is described at a relatively abstract level where functional elements such as the ALU are modelled without delay and the update of a storage element is an atomic action. The formal specifications in this section are based on this abstract view of behaviour.

6.2.1 Primitive components of the datapath

The ALU implements four different operations: the operation performed by the ALU is determined by the two ALU control signals f0 and f1. The operation selected from the representation variable rep by the selector function inc takes a single full-size word as an argument and returns a full-size word as a result. The operations selected by add and sub take two full-size words as arguments and return a single full-size word as a result. The fourth operation implemented by the ALU takes no arguments: it yields a constant result, namely, the full-size word representation of the number zero.

  let ALU = new_definition (
    `ALU`,
    "ALU (rep:^rep_ty) (f0,f1,inp1,inp2,out) =
      ∀t:time.
        out t =
          (((f0 t,f1 t) = (T,T)) => ((inc rep) (inp2 t)) |
           ((f0 t,f1 t) = (T,F)) => ((add rep) (inp1 t,inp2 t)) |
           ((f0 t,f1 t) = (F,T)) => ((sub rep) (inp1 t,inp2 t)) |
                                    ((wordn rep) 0))");;

Definitions for OpcField and AddrField specify devices which implement the operations selected by opcode and address respectively for extracting the opcode and address fields from a full-size word. Depending on how the opcode and address fields are represented, the implementation of these two devices could be nothing more than some wiring connections to appropriate bits.

  let OpcField = new_definition (
    `OpcField`,
    "OpcField (rep:^rep_ty) (inp,out) =
      ∀t:time. out t = (opcode rep) (inp t)");;
  let AddrField = new_definition (
    `AddrField`,
    "AddrField (rep:^rep_ty) (inp,out) =
      ∀t:time. out t = (address rep) (inp t)");;

The definition of TestZero specifies a device which implements the operation selected

by testzero.
  let TestZero = new_definition (
    `TestZero`,
    "TestZero (rep:^rep_ty) (inp,out) =
      ∀t:time. out t = (iszero rep) (inp t)");;

6.2.2 Modelling system bus operation

The system bus of the TAMARACK-3 datapath is used to transfer data between various devices in the datapath. Modelling the operation of this bus presents some special problems because control over the bus signal is decentralized. A correct design will never allow more than one device at a time to read a value onto the system bus. Some very simple models of the datapath bus (e.g., modelling a bus as a many-input multiplexor) are based on the informal assumption that this aspect of the design is correct. However, we would like to establish this fact as part of our formal proof.

One possibility is to invent an extra value called ‘bottom’ or Z to denote the floating (or high-impedance) state. The tri-state word types built into the HOL system (but not used here) are an example of this approach [24, 25, 32]. The value of bus is determined by a function which combines the outputs of all the bus drivers. If more than one driver has a non-floating output, then the result returned by the combining function is either an ‘error’ value or unknown. This scheme is appealing partly because it is familiar from switch level simulation models such as MOSSIM [7]. It is also similar in concept to resolution functions in the VHDL hardware description language [1].

We have chosen to model the datapath in a different way which takes advantage of our relationship style of formal specification. In this approach, the behavioural model of a bus device is regulated by a time-dependent condition on its environment. This condition only allows the device to assert a value onto the system bus if no other device is also attempting to assert a value onto the bus. This condition may be thought of as an additional control signal to the device although it does not correspond to any physical signal.

At the register-transfer level, each bus device has a ‘read’ signal which controls when the device attempts to assert a value onto the system bus. In TAMARACK-3, these ‘read’ signals are:

     rmem, rpc, racc, rir, rrtn, and rbuf

The time-dependent condition regulating the behaviour of bus drivers in the TAMARACK-3 datapath can be defined in terms of these signals: a value can be successfully read onto the system bus if and only if at most one of these signals is equal to T. This condition is expressed by the following definition of BusOkay.

  let BusOkay = new_definition (
    `BusOkay`,
    "BusOkay (rmem,rpc,racc,rir,rrtn,rbuf,busokay) =
      ∀t:time.
        busokay t =
          ((rmem t)  => (¬(rpc t ∨ racc t ∨ rir t ∨ rrtn t ∨ rbuf t)) |
          ((rpc t)  => (¬(racc t ∨ rir t ∨ rrtn t ∨ rbuf t)) |
          ((racc t)  => (¬(rir t ∨ rrtn t ∨ rbuf t)) |
          ((rir t)  => (¬(rrtn t ∨ rbuf t)) |
          ((rrtn t)  => (¬(rbuf t)) |
                       T)))))");;

BusOkay may be thought of as a virtual device in the datapath. Although it does not correspond to a physical component of the datapath, its specification can be derived directly from a structural description of the datapath by determining which devices share the system bus as a common output port.

6.2.3 More primitive components of the datapath

The definition of Interface specifies a device which provides a two-way interface between the system bus and the memory data pins. The device attempts to read data received from memory onto the system bus when the read signal r is equal to T. In the output direction, the current value of the system bus is connected to the output pins when the write signal w is equal to T; otherwise, the machine representation of zero is assigned to the output pins as a default value.

  let Interface = new_definition (
    `Interface`,
    "Interface (rep:^rep_ty) (busokay,w,r,bus,datain,dataout) =
      ∀t:time.
        ((busokay t) ==> (r t) ==> (bus t = datain t)) ∧
        (dataout t = ((w t) => (bus t) | ((wordn rep) 0)))");;

Following our scheme for modelling the operation of the system bus, the predicate Interface is parameterized by the virtual signal busokay which is the time-dependent condition specified in the definition of BusOkay. When data is being read from memory and no other device is attempting to assert a value onto the system bus, then the memory data will be successfully read onto the bus.

The basic storage element in the datapath of TAMARACK-3 is a selectively loadable register for storing full-size words. If the ‘write’ signal is equal to T, then the current input will be loaded into the register; otherwise, the contents of the register are unchanged. The out signal serves as both an output signal and a signal representing the internal state of the register. The register can also be interfaced to the system bus: the register attempts to read its contents onto the system bus when its ‘read’ signal is equal to T. Like the definition of Interface, the definition of Register is parameterized by the virtual signal busokay which determines when the register can successfully assert its contents onto the system bus.

  let Register = new_definition (
    `Register`,
    "Register (busokay,w,r,inp,bus,out:time->*wordn) =
      ∀t:time.
        ((busokay t) ==> (r t) ==> (bus t = out t)) ∧
        (out (t+1) = ((w t) => (inp t) | (out t)))");;

A set of fifteen individual control signals runs from the control unit to the datapath. It is convenient to view these fifteen control signals collectively as a single input to the datapath. Once inside the datapath, this bundle of control signals is separated into the fifteen individual control signals.

In the formal specification, this bundle can be represented as a signal whose value at any discrete point in time is an n-tuple with fifteen elements. The following definition of DecodeCntls specifies a block of wiring which separates this bundle of control signals into fifteen individual signals by ‘assigning’ elements of n-tuple representation to corresponding control signals. This definition is expressed in terms of an equation where the left and right hand sides of the equation are n-tuples. Two n-tuples are equal if and only if they have exactly the same number of elements and matching elements of each n-tuple are equal both in type and in value. In effect, we are using properties of n-tuples to model bit manipulation operations, in particular, the extraction of individual bits from a group of bits.

  new_type_abbrev (
    `cntls_ty`,
    ":bool#bool#bool#bool#bool#bool#bool#
      bool#bool#bool#bool#bool#bool#bool#bool");;
  let DecodeCntls = new_definition (
    `DecodeCntls`,
    "DecodeCntls (
      cntls:time->cntls_ty,
      wmem,rmem,wmar,wpc,rpc,wacc,racc,
      wir,rir,wrtn,rrtn,warg,alu0,alu1,rbuf) =
      ∀t:time.
        (wmem t,rmem t,wmar t,wpc t,rpc t,wacc t,racc t,
         wir t,rir t,wrtn t,rrtn t,warg t,alu0 t,alu1 t,rbuf t) =
        (cntls t)");;

The remaining three components needed to implement the datapath are a JK flip-flop, a two-input OR gate and voltages sources, i.e, ‘power’ and ‘ground’.

  let JKFF = new_definition (
    `JKFF`,
    "JKFF (j,k,out) =
      ∀t:time. out (t+1) = (((j t) ∧ ¬(out t)) ∨ (¬(k t) ∧ (out t)))");;
  let OR = new_definition (
    `OR`,
    "OR (inp1,inp2,out) = ∀t:time. out t = ((inp1 t) ∨ (inp2 t))");;
  let PWR = new_definition (`PWR`,"PWR out = ∀t:time. out t = T");;
  let GND = new_definition (`GND`,"GND out = ∀t:time. out t = F");;

6.2.4 Datapath implementation

The register-transfer level implementation of the datapath is formally specified by the definition of Datapath in terms of the above-mentioned primitive components.

let DataPath = new_definition (
`DataPath`,
"DataPath (rep:^rep_ty)
(cntls,datain,mar,pc,acc,ir,rtn,iack,
arg,buf,dataout,wmem,dreq,addr,zeroflag,opc) =
∃bus busokay alu pwr gnd rmem wmar wpc rpc
wacc racc wir rir wrtn rrtn warg alu0 alu1 rbuf.
DecodeCntls (
  cntls,
  wmem,rmem,wmar,wpc,rpc,wacc,racc,
  wir,rir,wrtn,rrtn,warg,alu0,alu1,rbuf) ∧
BusOkay (rmem,rpc,racc,rir,rrtn,rbuf,busokay) ∧
Interface rep (busokay,wmem,rmem,bus,datain,dataout) ∧
OR (wmem,rmem,dreq) ∧
Register (busokay,wmar,gnd,bus,bus,mar) ∧
AddrField rep (mar,addr) ∧
Register (busokay,wpc,rpc,bus,bus,pc) ∧
Register (busokay,wacc,racc,bus,bus,acc) ∧
TestZero rep (acc,zeroflag) ∧
Register (busokay,wir,rir,bus,bus,ir) ∧
OpcField rep (ir,opc) ∧
Register (busokay,wrtn,rrtn,bus,bus,rtn) ∧
JKFF (wrtn,rrtn,iack) ∧
Register (busokay,warg,gnd,bus,bus,arg) ∧
ALU rep (alu0,alu1,arg,bus,alu) ∧
Register (busokay,pwr,rbuf,alu,bus,buf) ∧
PWR pwr ∧
GND gnd");;

The predicate Datapath is parameterized by a number of signals. Some of these signals,

cntls, datain, iack dataout, wmem, dreq, addr, zeroflag and opc

correspond to physical inputs and outputs of the datapath. Other signals,

mar, pc, acc, ir, rtn, arg and buf

only exists as physical signals within the datapath. Outside the datapath, they are virtual signals representing various parts of the internal state of the datapath.

6.2.5 Microcode source and micro-assembler

We use a straightforward representation for each microinstruction word as a n-tuple where each element corresponds to one of the sub-fields described earlier in Section 4.3.2. For example, the n-tuple,

     ((F,F,T,F,T,F,F,F,F,F,F,F,F,F,F),(T,F),(T,F),(addr1,addr2))

is the representation of a typical microinstruction word. The first three elements of this representation are also n-tuples; they represent sub-fields which consist of individual bits. The fourth element is a pair of microcode addresses belonging to the type :*word4.

Instead of specifying the microcode directly in terms of bit patterns, a simple microassembler allows the microcode to be specified in a more readable form. The microassembler consists of the following definitions.

let waitdack = new_definition (`waitdack`,"waitdack = (T,T)");;
let waitidle = new_definition (`waitidle`,"waitidle = (T,F)");;
let continue = new_definition (`continue`,"continue = (F,F)");;
let jump = new_definition (`jump`,"jump = (T,T)");;
let jireq = new_definition (`jireq`,"jireq = (T,F)");;
let jzero = new_definition (`jzero`,"jzero = (F,T)");;
let jopcode = new_definition (`jopcode`,"jopcode = (F,F)");;
let Cntls = new_definition (
`Cntls`,
"Cntls (tok1,tok2,tok3) =
((tok2 = `wmem`),
(tok1 = `rmem`),
(tok2 = `wmar`),
(tok2 = `wpc`),
(tok1 = `rpc`),
(tok2 = `wacc`),
(tok1 = `racc`),
(tok2 = `wir`),
(tok1 = `rir`),
(tok2 = `wrtn`),
(tok1 = `rrtn`),
(tok2 = `warg`),
((tok3 = `inc`) ∨ (tok3 = `add`)),
((tok3 = `inc`) ∨ (tok3 = `sub`)),
(tok1 = `rbuf`))");;
let rom_ty = ":cntls_ty#(bool#bool)#(bool#bool)#(*word4#*word4)";;
let CompileMicroCode = new_definition (
`CompileMicroCode`,
"CompileMicroCode (rep:^rep_ty) (cntl,wcode,jcode,(n,m)) =
((Cntls cntl,wcode,jcode,((word4 rep) n,(word4 rep) m)):^rom_ty)");;

The microcode source is specified by the definition of MicroCode. This function is a mapping from natural numbers to specifications of individual microinstructions.

  let MicroCode = new_definition (
    `MicroCode`,
    "MicroCode n =
      ((n = 0) => ((`rpc`,`wmar`,`none`), waitidle, jireq, (1,2)) |
       (n = 1) => ((`rpc`,`wrtn`,`zero`), continue, jump, (12,0)) |
       (n = 2) => ((`rmem`,`wir`,`none`), waitdack, jump, (3,0)) |
       (n = 3) => ((`rir`,`wmar`,`none`), waitidle, jopcode, (4,0)) |
       (n = 4) => ((`none`,`none`,`none`), continue, jzero, (5,11)) |
       (n = 5) => ((`rir`,`wpc`,`none`), continue, jump, (0,0)) |
       (n = 6) => ((`racc`,`warg`,`none`), waitidle, jump, (13,0)) |
       (n = 7) => ((`racc`,`warg`,`none`), waitidle, jump, (14,0)) |
       (n = 8) => ((`rmem`,`wacc`,`none`), waitdack, jump, (11,0)) |
       (n = 9) => ((`racc`,`wmem`,`none`), waitdack, jump, (11,0)) |
       (n = 10) => ((`rrtn`,`wpc`,`none`), continue, jump, (0,0)) |
       (n = 11) => ((`rpc`,`none`,`inc`), continue, jump, (12,0)) |
       (n = 12) => ((`rbuf`,`wpc`,`none`), continue, jump, (0,0)) |
       (n = 13) => ((`rmem`,`none`,`add`), waitdack, jump, (15,0)) |
       (n = 14) => ((`rmem`,`none`,`sub`), waitdack, jump, (15,0)) |
                   ((`rbuf`,`wacc`,`none`), continue, jump, (11,0)))");;

The formal specification of the microcode source is based on the informal description of the FSM given earlier in Section 4.3.1, in particular, the flow graph in Figure 8 and the mapping from FSM states to actions in Figure 9. Each line of the microcode specification consists of four parts corresponding to the four sub-fields of the microinstruction word. For example, the term,

     ((`rpc`,`wmar`,`none`),waitidle,jireq,(1,2))

specifies the microinstruction at location 0 in the microcode.

The first part specifies the action to be performed by the datapath in terms of a data transfer from a source to a destination and an ALU operation. In this case, the contents of the program counter pc are read onto the bus and written into the memory address register mar. The string `none` indicates that no specific ALU operation is required.

The second part of each microinstruction specifies one of three wait conditions,

                    waitidle - repeat if ¬(idle or ¬dack)
                    waitdack - repeat if ¬dack

continue - do not repeat

which may cause this particular microinstruction to be repeated.

The third part of the microinstruction specifies how to compute the address of the next microinstruction (when not waiting in a repeat-loop).

          jump  - use addr1
          jireq  - use addr1 if ireq is T, else use addr2

jzero  - use addr1 if acc is zero, else use addr2
jopcode - add opcode to offset in addr1

The last part of the microinstruction specifies two microinstruction addresses or, in the case of jopcode, the offset to be added to the opcode field in computing the address of the next microinstruction.

Microinstruction specifications are individually assembled by the micro-assembler function CompileMicroCode. For example, the result of applying CompileMicroCode to the microinstruction at location 0 is described by the following theorem (after unfolding with definitions for the micro-assembler functions).

|- CompileMicroCode rep(MicroCode 0) =
((F,F,T,F,T,F,F,F,F,F,F,F,F,F,F),(T,F),(T,F),word4 rep 1,word4 rep 2)

Specifying the microcode source in pure logic and using a theorem prover to unfold this specification is a very secure way (at least as secure as theorem-proving) to assemble a microcode code source into bit patterns. The result of assembling the TAMARACK-3 microcode source is shown below (where a let-expression has been introduced for prettyprinting purposes).

|- CompileMicroCode rep(MicroCode n) =
let addrs (p,q) = (word4 rep p,word4 rep q) in
((n = 0) => ((F,F,T,F,T,F,F,F,F,F,F,F,F,F,F),(T,F),(T,F),addrs(1,2)) |
(n = 1) => ((F,F,F,F,T,F,F,F,F,T,F,F,F,F,F),(F,F),(T,T),addrs(12,0)) |
(n = 2) => ((F,T,F,F,F,F,F,T,F,F,F,F,F,F,F),(T,T),(T,T),addrs(3,0)) |
(n = 3) => ((F,F,T,F,F,F,F,F,T,F,F,F,F,F,F),(T,F),(F,F),addrs(4,0)) |
(n = 4) => ((F,F,F,F,F,F,F,F,F,F,F,F,F,F,F),(F,F),(F,T),addrs(5,11)) |
(n = 5) => ((F,F,F,T,F,F,F,F,T,F,F,F,F,F,F),(F,F),(T,T),addrs(0,0)) |
(n = 6) => ((F,F,F,F,F,F,T,F,F,F,F,T,F,F,F),(T,F),(T,T),addrs(13,0)) |
(n = 7) => ((F,F,F,F,F,F,T,F,F,F,F,T,F,F,F),(T,F),(T,T),addrs(14,0)) |
(n = 8) => ((F,T,F,F,F,T,F,F,F,F,F,F,F,F,F),(T,T),(T,T),addrs(11,0)) |
(n = 9) => ((T,F,F,F,F,F,T,F,F,F,F,F,F,F,F),(T,T),(T,T),addrs(11,0)) |
(n = 10) => ((F,F,F,T,F,F,F,F,F,F,T,F,F,F,F),(F,F),(T,T),addrs(0,0)) |
(n = 11) => ((F,F,F,F,T,F,F,F,F,F,F,F,T,T,F),(F,F),(T,T),addrs(12,0)) |
(n = 12) => ((F,F,F,T,F,F,F,F,F,F,F,F,F,F,T),(F,F),(T,T),addrs(0,0)) |
(n = 13) => ((F,T,F,F,F,F,F,F,F,F,F,F,T,F,F),(T,T),(T,T),addrs(15,0)) |
(n = 14) => ((F,T,F,F,F,F,F,F,F,F,F,F,F,T,F),(T,T),(T,T),addrs(15,0)) |
            ((F,F,F,F,F,T,F,F,F,F,F,F,F,F,T),(F,F),(T,T),addrs(11,0)))

A proof procedure for assembling the TAMARACK-3 microcode is given in:

hol/Training/studies/microprocessor/proof/example1.ml

6.2.6 Primitive components of the control unit

Section 4.3.2 outlined the implementation of the control unit FSM by a microcode program counter, microcode ROM, ROM output decoder and next address logic.

The microcode program counter mpc is modelled as a register which is unconditionally updated each clock cycle with its current input.

  let MPC = new_definition (
    `MPC`,
    "MPC (inp,out:time->*word4) = ∀t:time. out (t+1) = inp t");;

The microcode ROM is specified as a combinational device which takes a FSM state as input and returns a microinstruction word as a result. The actual contents of the ROM have already been specified by the earlier definition of MicroCode.

  let ROM = new_definition (
    `ROM`,
    "ROM (rep:^rep_ty) (inp,out) =
      ∀t:time.
        out t = (CompileMicroCode rep) (MicroCode ((val4 rep) (inp t)))");;

The output of the ROM is an n-tuple with elements corresponding to microinstruction sub-fields. The definition of DecodeROM specifies a device which separates the output of the ROM into various microinstruction sub-fields. The specification of this device is similar to the earlier definition of DecodeCntls.

  let DecodeROM = new_definition (
    `DecodeROM`,
    "DecodeROM (rom:time->^rom_ty,f0,f1,f2,f3,addr1,addr2,cntls) =
      ∀t:time. (cntls t,(f0 t,f1 t),(f2 t,f3 t),(addr1 t,addr2 t)) = rom t");;

The definition of NextMPC specifies the computation of FSM states according to the flow graph in Figure 8. Although the definition of NextMPC looks rather complex for a primitive component, it is just a block of combinational logic which could be implemented by a set of logic gates, some multiplexors and an adder. The formal verification of TAMARACK-3 could be extended by proving that a particular implementation of the next address logic satisfies the behavioural specification shown below (see suggested exercise in Section 15).

let NextMPC = new_definition (
`NextMPC`,
"NextMPC (rep:^rep_ty)
(f0,f1,f2,f3,dack,idle,ireq,iack,
zeroflag,opc,addr1,addr2,mpc,next) =
∀t:time.
let waitcond =
  ((((f0 t,f1 t) = waitdack) ∧ ¬(dack t)) ∨
   (((f0 t,f1 t) = waitidle) ∧ ¬((idle t) ∨ ¬(dack t)))) in
(next t =
  (waitcond => (mpc t) |
   ((f2 t,f3 t) = jump) => (addr1 t) |
   ((f2 t,f3 t) = jireq) =>
     (((ireq t) ∧ ¬(iack t)) => (addr1 t) | (addr2 t)) |
   ((f2 t,f3 t) = jzero) =>
     ((zeroflag t) => (addr1 t) | (addr2 t)) |
     ((word4 rep)
       (((val3 rep) (opc t)) + ((val4 rep) (addr1 t))))))");;

6.2.7 Control unit implementation

The register-transfer level implementation of the control unit FSM is formally specified by the definition of CntlUnit.

let CntlUnit = new_definition (
`CntlUnit`,
"CntlUnit (rep:^rep_ty) (dack,idle,ireq,iack,zeroflag,opc,mpc,cntls) =
∃f0 f1 f2 f3 addr1 addr2 next rom.
NextMPC rep (
  f0,f1,f2,f3,dack,idle,ireq,iack,
  zeroflag,opc,addr1,addr2,mpc,next) ∧
MPC (next,mpc) ∧
ROM rep (mpc,rom) ∧
DecodeROM (rom,f0,f1,f2,f3,addr1,addr2,cntls)");;

With the sole exception of mpc, all the signal names in the parameter list of CntlUnit correspond to physical inputs and outputs of the control unit FSM. The microcode program counter mpc is a physical signal only within the implementation of the control unit. Outside the control unit, the microcode program counter mpc is a virtual signal representing the internal state of the FSM.

6.2.8 Top level structure

The control unit and datapath are combined to implement the internal architecture of TAMARACK-3. The control signals, cntl, and feedback signals, zeroflag and opc, are internal connections between the control unit and datapath.

  let TamarackImp = new_definition (
    `TamarackImp`,
    "TamarackImp (rep:^rep_ty)
      (datain,dack,idle,ireq,mpc,mar,pc,
       acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr) =
      ∃zeroflag opc cntls.
        CntlUnit rep (dack,idle,ireq,iack,zeroflag,opc,mpc,cntls) ∧
        DataPath rep (
          cntls,datain,mar,pc,acc,ir,rtn,iack,
          arg,buf,dataout,wmem,dreq,addr,zeroflag,opc)");;

The signals,

     datain, dack, idle, ireq, iack, dataout, wmem, dreq and addr

correspond to physical input and output pins of the microprocessor. The remaining signals in the parameter list of TamarackImp,

     mpc, mar, pc, acc, ir, rtn, arg and buf

only exists as physical signals within the internal architecture. They appear in the parameter list as virtual signals representing the internal state of the microprocessor.

6.3 Programming level model

The formal specification of the programming level model is based on the informal descriptions given in Section 2.4 and 2.5 of the instruction set semantics and the hardware interrupt facility.

The semantics of each instruction is given individually by the definition of a function which returns the next (externally visible) state of the microprocessor, i.e., the next values of the memory state mem, program counter pc, accumulator acc, return address register rtn and interrupt acknowledge flag iack. The following definitions specify how these values are computed from the current state of the microprocessor.

let JZR_SEM = new_definition (
`JZR_SEM`,
"JZR_SEM (rep:^rep_ty)
(mem:*memory,pc:*wordn,acc:*wordn,rtn:*wordn,iack:bool) =
let inst = (fetch rep) (mem,(address rep) pc) in
let nextpc = ((iszero rep) acc) => inst | ((inc rep) pc) in
  (mem,nextpc,acc,rtn,iack)");;
let JMP_SEM = new_definition (
`JMP_SEM`,
"JMP_SEM (rep:^rep_ty)
(mem:*memory,pc:*wordn,acc:*wordn,rtn:*wordn,iack:bool) =
let inst = (fetch rep) (mem,(address rep) pc) in
  (mem,inst,acc,rtn,iack)");;
let ADD_SEM = new_definition (
`ADD_SEM`,
"ADD_SEM (rep:^rep_ty)
(mem:*memory,pc:*wordn,acc:*wordn,rtn:*wordn,iack:bool) =
let inst = (fetch rep) (mem,(address rep) pc) in
let operand = (fetch rep) (mem,(address rep) inst) in
  (mem,(inc rep) pc,(add rep) (acc,operand),rtn,iack)");;
let SUB_SEM = new_definition (
`SUB_SEM`,
"SUB_SEM (rep:^rep_ty)
(mem:*memory,pc:*wordn,acc:*wordn,rtn:*wordn,iack:bool) =
let inst = (fetch rep) (mem,(address rep) pc) in
let operand = (fetch rep) (mem,(address rep) inst) in
  (mem,(inc rep) pc,(sub rep) (acc,operand),rtn,iack)");;
let LDA_SEM = new_definition (
`LDA_SEM`,
"LDA_SEM (rep:^rep_ty)
(mem:*memory,pc:*wordn,acc:*wordn,rtn:*wordn,iack:bool) =
let inst = (fetch rep) (mem,(address rep) pc) in
let operand = (fetch rep) (mem,(address rep) inst) in
  (mem,(inc rep) pc,operand,rtn,iack)");;
let STA_SEM = new_definition (
`STA_SEM`,
"STA_SEM (rep:^rep_ty)
(mem:*memory,pc:*wordn,acc:*wordn,rtn:*wordn,iack:bool) =
let inst = (fetch rep) (mem,(address rep) pc) in
let newmem = (store rep) (mem,(address rep) inst,acc) in
  (newmem,(inc rep) pc,acc,rtn,iack)");;

let RFI_SEM = new_definition (
  `RFI_SEM`,
  "RFI_SEM (rep:^rep_ty)
    (mem:*memory,pc:*wordn,acc:*wordn,rtn:*wordn,iack:bool) =
    (mem,rtn,acc,rtn,F)");;
let NOP_SEM = new_definition (
  `NOP_SEM`,
  "NOP_SEM (rep:^rep_ty)
    (mem:*memory,pc:*wordn,acc:*wordn,rtn:*wordn,iack:bool) =
    (mem,(inc rep) pc,acc,rtn,iack)");;

The processing of a hardware interrupt is described in a similar way by the definition of a function which computes the next state of the microprocessor from its current state.

let IRQ_SEM = new_definition (
  `IRQ_SEM`,
  "IRQ_SEM (rep:^rep_ty)
    (mem:*memory,pc:*wordn,acc:*wordn,rtn:*wordn,iack:bool) =
    (mem,((wordn rep) 0),acc,pc,T)");;

The opcode of the current instruction word determines which instruction is executed during a particular instruction cycle. The following set of definitions specify the opcode value for each instruction.

let JZR_OPC = new_definition (`JZR_OPC`,"JZR_OPC = 0");;
let JMP_OPC = new_definition (`JMP_OPC`,"JMP_OPC = 1");;
let ADD_OPC = new_definition (`ADD_OPC`,"ADD_OPC = 2");;
let SUB_OPC = new_definition (`SUB_OPC`,"SUB_OPC = 3");;
let LDA_OPC = new_definition (`LDA_OPC`,"LDA_OPC = 4");;
let STA_OPC = new_definition (`STA_OPC`,"STA_OPC = 5");;
let RFI_OPC = new_definition (`RFI_OPC`,"RFI_OPC = 6");;
let NOP_OPC = new_definition (`NOP_OPC`,"NOP_OPC = 7");;

The opcode value of the current instruction is obtained by fetching the memory word addressed by the program counter, extracting the value of its opcode field and interpreting the opcode as a number between 0 and 7. This procedure is specified in the definition of

OpcVal
let OpcVal = new_definition (
    `OpcVal`,
    "OpcVal (rep:^rep_ty) (mem,pc) =
      (val3 rep) ((opcode rep) ((fetch rep) (mem,(address rep) pc)))");;

Every instruction cycle results in the execution of an programming level instruction unless a hardware interrupt is detected and processed during this cycle. The following definition of NextState specifies the overall control mechanism for determining what happens during a particular instruction cycle.

  let NextState = new_definition (
    `NextState`,
    "NextState (rep:^rep_ty) (ireq,mem,pc,acc,rtn,iack) =
      let opcval = OpcVal rep (mem,pc) in
      ((ireq ∧ ¬iack)    => IRQ_SEM rep (mem,pc,acc,rtn,iack) |
       (opcval = JZR_OPC) => JZR_SEM rep (mem,pc,acc,rtn,iack) |
       (opcval = JMP_OPC) => JMP_SEM rep (mem,pc,acc,rtn,iack) |
       (opcval = ADD_OPC) => ADD_SEM rep (mem,pc,acc,rtn,iack) |
       (opcval = SUB_OPC) => SUB_SEM rep (mem,pc,acc,rtn,iack) |
       (opcval = LDA_OPC) => LDA_SEM rep (mem,pc,acc,rtn,iack) |
       (opcval = STA_OPC) => STA_SEM rep (mem,pc,acc,rtn,iack) |
       (opcval = RFI_OPC) => RFI_SEM rep (mem,pc,acc,rtn,iack) |
                             NOP_SEM rep (mem,pc,acc,rtn,iack))");;

Finally, we use the function NextState to define the predicate TamarackBeh which specifies the intended behaviour of the microprocessor as a relation on the time-dependent

signals mem, pc, acc, rtn and iack.

  let TamarackBeh = new_definition (
    `TamarackBeh`,
    "TamarackBeh (rep:^rep_ty) (ireq,mem,pc,acc,rtn,iack) =
      ∀u:time.
        (mem (u+1),pc (u+1),acc (u+1),rtn (u+1),iack (u+1)) =
        NextState rep (ireq u,mem u,pc u,acc u,rtn u,iack u)");;

The programming level model not only hides structural details of the internal architecture but also timing details about the number of microinstructions executed for each instruction. To be more precise, the programming level model describes the operation of the microprocessor in terms of an abstract time scale where each instruction is uniformly executed in a single unit of time. This abstract time scale is different than the time scale used to specify the behaviour of register-transfer level components where a single unit of time corresponds to a single clock cycle. To emphasize this difference, we have used the explicit time variable u instead of t in the above definition of TamarackBeh (but there is logical distinction between these two variable names). As we will see in Section 7, part of the verification task is to establish a formal relationship between these two granularities of discrete time.

6.4 External memory specification

A behavioural model for fully synchronous memory expressed by the predicate SynMemory. The definition of this predicate is shown below.

  let SynMemory = new_definition (
    `SynMemory`,
    "SynMemory (rep:^rep_ty) (w,addr,dataout,mem,datain) =
      ∀t:time.
        (¬(w t) ==> (datain t = (fetch rep) (mem t,addr t))) ∧
        (mem (t+1) =
          ((w t) => ((store rep) (mem t,addr t,dataout t)) | (mem t)))");;

External memory implements the uninterpreted operations selected by fetch and store. The write signal w controls which operations are performed by the memory each clock cycle. Data is sent to external memory on the dataout bus and received from external memory on the datain bus. Memory addresses are sent to external memory on the addr bus. The internal state of memory is represented by the virtual signal mem.

A fully asynchronous version of external memory also implements the uninterpreted operations selected by fetch and store but uses handshaking signals to synchronize its interaction with the microprocessor. A formal specification for a fully asynchronous memory device is deferred until Section 10.

7 Verification plan and methodology

This section describes the logical form used to state correctness results for TAMARACK-3, a plan to achieve these results and some of the basic proof techniques which are used to carry out this plan in the HOL system.

7.1 Stating correctness results

Although the terms ‘correctness’ and ‘verification’ may be understood in an informal context to mean different things to different people, these terms have a precise, technical meaning when formal logic is used to verify a hardware design. The formal verification (or proof of correctness) for TAMARACK-3 refers to the derivation of a theorem by formal proof in the HOL formulation of higher-order logic. This theorem relates the specification of the internal architecture, given by the predicate TamarackImp, to the specification of its intended behaviour, given by the predicate TamarackBeh.

We actually give three different versions of the top level correctness theorem but they are all the same basic form: that the constraints imposed by the implementation predicate TamarackImp satisfy the requirements expressed by the behaviour predicate TamarackBeh. The general form of this theorem is a logical implication:

     |- Implementation Specification ==> Behaviour Specification

The precise form of this theorem (in each of the three cases) depends on a formally established relationship between the two different granularities of time used to specify register-transfer level behaviour and the programming level model. The correctness theorems also include a behavioural model of external memory and a description of how memory is interfaced to the microprocessor.

For readers curious at this point in the appearance of these correctness results, the following theorem is (a slightly expanded form of) the result obtained by the procedure outlined in Section 8.

  |- ∀datain pwr dataout wmem dreq addr.
       Val3_CASES_ASM (rep:^rep_ty) ∧
       Val4Word4_ASM rep ∧
       TamarackImp rep (
         datain,pwr,pwr,ireq,mpc,mar,pc,
         acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr) ∧
       SynMemory rep (wmem,addr,dataout,mem,datain) ∧
       PWR pwr ∧
       (((val4 rep) o mpc) 0 = 0)
       ==>
       let f = TimeOfCycle rep (ireq,mem,pc,acc,rtn,iack) in
       TamarackBeh rep (ireq o f,mem o f,pc o f,acc o f,rtn o f,iack o f)

7.2 Multi-level verification

Although most of the low level tedious work of theorem-proving can be done mechanically by the HOL system, the formal verification of non-trivial hardware (and other kinds of proofs) requires a considerable amount of guidance from the user. More powerful (and more specialized) proof procedures could be programmed in ML to increase the degree of automation, ^{9} but complete automation for non-trivial designs is not a foreseeable possibility (in HOL or in any other verification system). Furthermore, we suggest that complete automation would undermine the true purpose of formal verification [40, 41].

Much of the creative work in using the HOL system centers upon the problem of discovering high-level proof strategies when routine HOL interactions like STRIP TAC, BOOL CASES TAC and ASM REWRITE TAC are not enough to complete a proof. Theoremproving experience or mathematical insight is sometimes the source of a successful proof strategy. However, an equally important source for hardware verification, and more specifically, the verification of microprocessor systems is conventional design methodology where many useful strategies for controlling the complexity of reasoning informally about computer architecture are already well-known.

In particular, we have found that the concept of multiple interpretation levels, used by architects to achieve a “progressive translation of functions in several stages” [2] is a very effective strategy for controlling the complexity of verifying the correctness of TAMARACK-3. As explained earlier in Section 4.3, TAMARACK-3 has two levels of interpretation beneath the programming level: the microprogramming level and phase level. We use this structured view of the internal operation of the microprocessor to organize the bulk of the formal proof into two main steps:

9Although guidance may be required from the user, every step in the proof is mechanically checked by the system. The design and implementation of the HOL theorem generation kernel (inherited from LCF LSM) ensures that user defined proof procedures cannot compromise proof security.

1. Prove that each microinstruction is correctly interpreted at the phase level.

2. Prove that each programming level operation is correctly interpreted at the microprogramming level.

The proof is completed in a third (and relatively short) step by establishing a formally defined relationship between the two different granularities of discrete time used to specify the internal architecture and programming level model.

3. Relate clock cycles view of behaviour to instruction cycle view of behaviour.

Verifying the phase level operation of TAMARACK-3 in Step (1) does not depend on a behavioural model for external memory. However, different versions of Steps (2) and (3) are needed for fully synchronous mode and fully asynchronous mode.

7.3 Symbolic execution

Many different kinds of computation systems are implemented by a hierarchy of interpretation levels. Showing that one level correctly implements the next higher level is equivalent to showing that the higher level is an abstract view of the lower level. Each operation at a given level in the hierarchy is typically interpreted (directly or indirectly) by one or more operations at the next lower level. To demonstrate that this level is correctly implemented by the next lower level, each operation is shown to be correctly implemented by the corresponding sequence of lower level operations. This is established by deriving the cumulative effect of each sequence and comparing it to the intended effect of the corresponding higher level operation.

It is relatively straightforward to reason about a fixed sequence (or a finite set of fixed sequences) of lower level operations. To derive the cumulative effect of a sequence of lower level operations, we use inference rules of higher-order logic to symbolically execute this sequence. The term ‘symbolic execution’ is used here in a purely descriptive sense for a proof technique which is actually nothing more than repeatedly unfolding various parts of the specification (or consequences of this specification derived at lower levels).

It is natural to use forward proof to symbolically execute a sequence of operations starting with assumptions about the initial state and applying inference rules to derive subsequent states in the computation. Similar techniques were also used to verify the VIPER microprocessor. As Cohn remarks [13], forward proofs of this kind are a rather unsophisticated use of the HOL system which may produce unforeseen results. However, the use of formal proof in this case is indicated by the nature of the problem.

Even though forward proof lies at the heart of symbolic execution, it is very convenient (in the HOL system) to carry out these forward proofs in the overall context of a backward (or goal-oriented) proof using the built-in sub-goals package. ^{10} After an initial bit of backward proof, forward inference steps are achieved by repeated use of resolution tactics with some direct manipulation of the intermediate results.

The following section illustrates the general concept of symbolic execution and the mechanics of using this proof technique in the HOL system.

8 Formal verification: ‘bread and butter’ method

In this section, we describe the formal verification of TAMARACK-3 when operating in fully synchronous mode. Verifying TAMARACK-3 in this mode is relatively simple because each programming level operation is implemented by a fixed sequence (or finite set of fixed sequences) of microinstructions. The considerably more difficult task of verifying TAMARACK-3 for fully asynchronous mode is outlined later in Section 10.

8.1 Phase level

As explained earlier in Section 4.3.2, the phase level operation of TAMARACK-3 is described in terms of elementary operations performed by register-transfer level components. The interpretation of a microinstruction at the phase level during a single clock cycle results in a sequence of events which includes:

• Fetch the current microinstruction.

• Compute the address of the next microinstruction.

• Read data onto the system bus.

• Evaluate operations performed by functional elements.

• Update storage elements such as memory, registers and flipflops.

Verifying the operation of the microprocessor at this level is a matter of deriving the cumulative effect of these elementary operations for each of the sixteen microinstructions. We show that the cumulative effect of these operations satisfies the intended effect of each microinstruction.

To illustrate this process, we outline the steps taken to establish that microinstruction 0, i.e., the microinstruction at location 0 in the microcode, is correctly interpreted at the phase level. The intended effect of microinstruction 0,

     MicroCode 0 = ((`rpc`,`wmar`,`none`), waitidle, jireq, (1,2))

10Backward proof and the sub-goal package are described in Getting Started with HOL under Goal oriented proof: tactics and tacticals.

is to transfer the contents of the program counter pc to the memory address register mar and update the microcode program counter mpc according to conditions given in the flow graph of Figure 8. Furthermore, the execution of this microinstruction must leave the internal state of the memory mem and the contents of the program counter pc, accumulator acc, return address register rtn and interrupt acknowledge flag iack unchanged. The effect of this microinstruction on the remaining components of the internal state, namely, the arg and buf registers, is unimportant and can be ignored. Finally, the memory data output bus dataout must be set to its default value and the memory control flags, wmem and dreq, must be set to F.

These requirements are formally expressed in the goal term of the following call to the ML function set_goal. This is the first step in an interactive proof to formally derive this goal^{11} as a theorem using the HOL sub-goal package.

11The term ‘goal’ has technical meaning in the HOL system (as a ML type abbreviation) but we use it more generally to mean a yet-to-be-proven theorem.

  set_goal (
    [],
    "Val3_CASES_ASM (rep:^rep_ty) ∧
     Val4Word4_ASM rep ∧
     TamarackImp rep (
       datain,dack,idle,ireq,mpc,mar,pc,
       acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
     ==>
     ∀t.
      (((val4 rep) o mpc) t = 0)
      ==>
      (((val4 rep) o mpc) (t+1) =
         ((¬((idle t) ∨ ¬(dack t))) => 0 |
          ((ireq t) ∧ ¬(iack t)) => 1 | 2)) ∧
      (mar (t+1) = pc t) ∧
      (pc (t+1) = pc t) ∧
      (acc (t+1) = acc t) ∧
      (rtn (t+1) = rtn t) ∧
      (iack (t+1) = iack t) ∧
      (dataout t = ((wordn rep) 0)) ∧
      (wmem t = F) ∧
      (dreq t = F)");;

A sequence of interactions with the sub-goal package eventually results in the generation of this goal as a theorem. To illustrate the strategy which underlies this sequence of interactions and more generally, how formal proof can be used to symbolically execute hardware, we describe a condensed view of the proof procedure given in:

     hol/Training/studies/microprocessor/proof/example2.ml

The reader may wish to examine this HOL source file for details of the actual interactions used to generate this proof since we only describe the proof procedure in terms of intermediate results generated by the HOL system in response to these interactions.

We begin by expanding the above goal with the definitions for TamarackImp, CntlUnit and DataPath. We then apply standard goal reduction techniques to strip antecedents from the goal and break them up into a number of assumptions which are put into the assumption list. The result is shown below where each assumption appears as a term between a matching pair of brackets [ and ]. Most of these assumptions correspond to primitive components of the internal architecture with internal connections (hidden in the specification by existential quantification) now exposed as free variables in the assumption list.

OK..
"(val4 rep(mpc(t + 1)) =
((¬(idle t ∨ ¬dack t)) => 0 | ((ireq t ∧ ¬iack t) => 1 | 2))) ∧
(mar(t + 1) = pc t) ∧
(pc(t + 1) = pc t) ∧
(acc(t + 1) = acc t) ∧
(rtn(t + 1) = rtn t) ∧
(iack(t + 1) = iack t) ∧
(dataout t = wordn rep 0) ∧
(wmem t = F) ∧
(dreq t = F)"
[ "Val3_CASES_ASM rep" ]
[ "Val4Word4_ASM rep" ]
[ "NextMPC
   rep
   (f0,f1,f2,f3,dack,idle,ireq,iack,zeroflag,opc,addr1,addr2,mpc,
    next)" ]
[ "MPC(next,mpc)" ]
[ "ROM rep(mpc,rom)" ]
[ "DecodeROM(rom,f0,f1,f2,f3,addr1,addr2,cntls)" ]
[ "DecodeCntls
   (cntls,wmem,rmem,wmar,wpc,rpc,wacc,racc,wir,rir,wrtn,rrtn,warg,
    alu0,alu1,rbuf)" ]
[ "BusOkay(rmem,rpc,racc,rir,rrtn,rbuf,busokay)" ]
[ "Interface rep(busokay,wmem,rmem,bus,datain,dataout)" ]
[ "OR(wmem,rmem,dreq)" ]
[ "Register(busokay,wmar,gnd,bus,bus,mar)" ]
[ "AddrField rep(mar,addr)" ]
[ "Register(busokay,wpc,rpc,bus,bus,pc)" ]
[ "Register(busokay,wacc,racc,bus,bus,acc)" ]
[ "TestZero rep(acc,zeroflag)" ]
[ "Register(busokay,wir,rir,bus,bus,ir)" ]
[ "OpcField rep(ir,opc)" ]
[ "Register(busokay,wrtn,rrtn,bus,bus,rtn)" ]
[ "JKFF(wrtn,rrtn,iack)" ]
[ "Register(busokay,warg,gnd,bus,bus,arg)" ]
[ "ALU rep(alu0,alu1,arg,bus,alu)" ]
[ "Register(busokay,pwr,rbuf,alu,bus,buf)" ]
[ "PWR pwr" ]
[ "GND gnd" ]
[ "val4 rep(mpc t) = 0" ]
() : void

After this initial bit of backward proof, forward inference steps are achieved by repeated use of resolution tactics. Theorems generated by resolution in this manner are logical consequences of the assumptions already in the assumption list. These theorems contribute various facts which incremently advance the state of the symbolic execution. As theorems are generated, they are added to the current list of assumptions and may be used by subsequent resolution steps to generate more theorems.

Since this part of the proof is only concerned with generating new theorems for the assumption list, we just show what gets added onto the end of the assumption list after each main step. We begin by using the definition of ROM to generate the following equation for the current output of the ROM.

     rom t = CompileMicroCode rep(MicroCode 0)

Instead of adding this equation directly to the assumption list, we use the microcode specification MicroCode and definitions for the micro-assembler functions given in Section 6.2.5 to transform it into an equation which gives the assembled form of microinstruction 0.

  OK..

…

      [ "rom t =
         (F,F,T,F,T,F,F,F,F,F,F,F,F,F,F),(T,F),(T,F),word4 rep 1,
         word4 rep 2" ]
  () : void

The definition of DecodeROM is then used to separate the ROM output into datapath control bits, cntls, next address logic control bits, f0, f1, f2 and f3, and microcode addresses, addr1 and addr2.

  OK..

…

      [ "cntls t = F,F,T,F,T,F,F,F,F,F,F,F,F,F,F" ]
      [ "f0 t = T" ]
      [ "f1 t = F" ]
      [ "f2 t = T" ]
      [ "f3 t = F" ]
      [ "addr1 t = word4 rep 1" ]
      [ "addr2 t = word4 rep 2" ]
  () : void

The next address logic control bits and microcode addresses extracted from the current output of the ROM are used to derive an expression for the output of the next address logic. This expression is obtained from the definition of NextState. The value of this expression depends on external inputs, idle, dack, and ireq, and the current value of the interrupt acknowledge flag iack.

  OK..

…

      [ "next t =
         ((¬(idle t ∨ ¬dack t)) =>
          mpc t |
          ((ireq t ∧ ¬iack t) => word4 rep 1 | word4 rep 2))" ]
  () : void

At the end of the clock cycle, the value computed by the next address logic is loaded into the microcode program counter mpc. The definition of MPC is used to establish this fact.

  OK..

…

      [ "mpc(t + 1) =
         ((¬(idle t ∨ ¬dack t)) =>
          mpc t |
          ((ireq t ∧ ¬iack t) => word4 rep 1 | word4 rep 2))" ]
  () : void

Meanwhile, the datapath is performing actions specified by the datapath control bits. To derive the result of these actions, we start with the definition of DecodeCntls to separate the bundle of control bits into individual control signals.

  OK..

…

      [ "wmem t = F" ]
      [ "rmem t = F" ]
      [ "wmar t = T" ]
      [ "wpc t = F" ]
      [ "rpc t = T" ]
      [ "wacc t = F" ]
      [ "racc t = F" ]
      [ "wir t = F" ]
      [ "rir t = F" ]
      [ "wrtn t = F" ]
      [ "rrtn t = F" ]
      [ "warg t = F" ]
      [ "alu0 t = F" ]
      [ "alu1 t = F" ]
      [ "rbuf t = F" ]
  () : void

The definitions of PWR and GND yield equations for the voltage sources pwr and gnd. These two signals are used to permanently enable or disable various functions in the datapath.

  OK..

…

      [ "pwr t = T" ]
      [ "gnd t = F" ]
  () : void

All of the ‘read’ signals are equal to F except for rpc satisfying the condition that only one bus device can attempt to read a value onto the system bus. The definition of BusOkay is used to establish that the virtual signal busokay is equal to T indicating that this condition is satisfied.

  OK..

…

      [ "busokay t = T" ]
  () : void

Using these values for rpc and busokay, the definition of Register yields an equation for the value of the system bus.

  OK..

…

      [ "bus t = pc t" ]
  () : void

Hence, the contents of the program counter pc are successfully read onto the bus. The data transfer is completed by writing the value of the bus into the memory address register mar. The contents of other registers in the datapath (ignoring buf) and the value of the interrupt acknowledge flag iack remain unchanged. These facts can be established from the above equations for the control signals and the definitions of Register and JKFF.

  OK..

…

      [ "mar(t + 1) = pc t" ]
      [ "pc(t + 1) = pc t" ]
      [ "acc(t + 1) = acc t" ]
      [ "ir(t + 1) = ir t" ]
      [ "rtn(t + 1) = rtn t" ]
      [ "arg(t + 1) = arg t" ]
      [ "buf(t + 1) = alu t" ]
      [ "iack(t + 1) = iack t" ]
  () : void

Finally, the control signals cause certain values to be generated as external outputs. The definitions of OR and Interface yield the following equations for dreq and dataout (an equation for wmem has already appeared in a previous step).

  OK..

…

      [ "dreq t = F" ]
      [ "dataout t = wordn rep 0" ]
  () : void

This completes the symbolic execution part of the proof: the results of symbolic execution are used to solve all the remaining goals of the backward proof. At the beginning of the symbolic execution part of the proof, the top level goal was:

"(val4 rep(mpc(t + 1)) =
 ((¬(idle t ∨ ¬dack t)) => 0 | ((ireq t ∧ ¬iack t) => 1 | 2))) ∧
(mar(t + 1) = pc t) ∧
(pc(t + 1) = pc t) ∧
(acc(t + 1) = acc t) ∧
(rtn(t + 1) = rtn t) ∧
(iack(t + 1) = iack t) ∧
(dataout t = wordn rep 0) ∧
(wmem t = F) ∧
(dreq t = F)"

But by the end of symbolic execution, most of the conjuncts in this goal have already been solved as a side-effect of various manipulations of the goal stack (e.g., uses of ASM_REWRITE_TAC). The original goal has been reduced to:

"val4
rep
((¬(idle t ∨ ¬dack t)) =>
 mpc t |
 ((ireq t ∧ ¬iack t) => word4 rep 1 | word4 rep 2)) =
((¬(idle t ∨ ¬dack t)) => 0 | ((ireq t ∧ ¬iack t) => 1 | 2))"

This reduced goal is easily solved by case analysis on Boolean terms and using the assumption expressed by Val4Word4_ASM.

  OK..
  goal proved

… additional output deleted here …

  |- Val3_CASES_ASM rep ∧
     Val4Word4_ASM rep ∧
     TamarackImp
     rep
     (datain,dack,idle,ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,dataout,
      wmem,dreq,addr) ==>
     (∀t.
       (((val4 rep) o mpc)t = 0) ==>
       (((val4 rep) o mpc)(t + 1) =
        ((¬(idle t ∨ ¬dack t)) => 0 | ((ireq t ∧ ¬iack t) => 1 | 2))) ∧
       (mar(t + 1) = pc t) ∧
       (pc(t + 1) = pc t) ∧
       (acc(t + 1) = acc t) ∧
       (rtn(t + 1) = rtn t) ∧
       (iack(t + 1) = iack t) ∧
       (dataout t = wordn rep 0) ∧
       (wmem t = F) ∧
       (dreq t = F))
  Previous subproof:
  goal proved
  () : void

A similar pattern of reasoning is used to derive correctness results for the remaining fifteen microinstructions (these results are given in Appendix A). Each of these theorems shows that the microinstruction satisfies a set of equations for the next state of the microprocessor at time t+1 in terms of its state at time t. Each theorem expresses the minimal (or close to minimal) set of results needed at higher proof levels; irrelevent details (such as the effect of microinstruction 0 on arg and buf) are ignored.

These sixteen correctness results collectively capture the informal description conveyed by the flow graph in Figure 8 and corresponding datapath actions described in Figure 9.

8.2 Microprogramming level

The second main step of the verification procedure is to examine the interpretation of programming level operations by sequences of microinstructions. Here we consider the operation of the microprocessor in fully synchronous mode where each programming level operation is implemented by a fixed sequence of microinstructions, or in the case of a JZR instruction, by one of two possible sequences. Symbolic execution of these microinstruction sequences is used to show that their cumulative effect satisfies the semantics of the instruction set formally defined in Section 6.3. Symbolic execution of microinstructions is also used to show that hardware interrupts are correctedly implemented.

A behavioural model for external memory was not needed to verify the phase level operation of the microinstruction since correctness results at that level are simply concerned with sampling and generating inputs and outputs on pins of the microchip. However, a behavioural model for external memory is needed to verify the microprogramming level. Whereas the terms fetch and store did not appear the correctness results for the phase level, they do appear in correctness results for the microprogramming level.

The predicate SynSystem is defined below to specify a system consisting of the TAMARACK-3 microchip interfaced to a fully synchronous memory device. The specification of the memory device was given earlier in Section 6.4 by the definition of SynMemory. The internal architecture is made to operate in fully synchronous mode by wiring the two pins dack and idle to T, i.e., the output of a voltage source.

  let SynSystem = new_definition (
    `SynSystem`,
    "SynSystem (rep:^rep_ty)
      (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) =
      ∃datain pwr dataout wmem dreq addr.
        TamarackImp rep (
          datain,pwr,pwr,ireq,mpc,mar,pc,
          acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr) ∧
        SynMemory rep (wmem,addr,dataout,mem,datain) ∧
        PWR pwr");;

Each programming level operation is interpreted by a non-empty, fixed sequence of microinstructions (or pair of possible sequences in the case of the JZR instruction). It is convenient to define the function MicroCycles which specifies the length of sequence about to be executed given the current state of the microprocessor (assuming that the microprocessor is operating in fully synchronous mode).

  let MicroCycles = new_definition (
    `MicroCycles`,
    "MicroCycles (rep:^rep_ty) (ireq,mem,pc,acc,rtn:*wordn,iack) =
      (ireq ∧ ¬iack) => 3 |
      let opcval = OpcVal rep (mem,pc) in
      ((opcval = 0) => (((iszero rep) acc) => 5 | 6) |
       (opcval = 1) => 4 |
       (opcval = 2) => 8 |
       (opcval = 3) => 8 |
       (opcval = 4) => 6 |
       (opcval = 5) => 6 |
       (opcval = 6) => 4 |
                       5)");;

MicroCycles provides the basis for relating behaviour models of TAMARACK-3 expressed in terms of different granularities of time. ^{12} Later in Section 9, we describe a more general way of relating different granularities of time that does not involve MicroCycles.

To reason about the implementation of particular programming level operation at the microprogramming level, we assume that the value of the microcode program counter mpc is equal to zero at time t, that is, the beginning of the instruction cycle. The results of symbolic execution are used to determine the state of the microprocessor and memory at the end of the instruction cycle denoted as time t+m where m is the value returned by MicroCycles. Correctness results are obtained by showing that the state of system at the end of the interpretation sequence is consistent with the definition of NextState. To eventually get rid of the assumption about the value of the microcode program counter mpc at the beginning of the cycle, we must also show that its value returns to zero at the end of the cycle.

These requirements could be translated directly into an individual statement of correctness for each programming level operation. But all of these correctness statements would be nearly identical except for minor (textual) distinctions such as the opcode value of the current instruction in each case. We can avoid a great deal of redundant text by defining a predicate SynCorrectness1 which is a generalized form of correctness statement. It is parameterized by the variables,

ircond  - interrupt condition
opcval  - opcode value

      iszerocond - result of testzero operation

which distinguish one programming level operation from another.

12The function MicroCycles is similar in purpose to the function NUMBER OF STEPS in the VIPER proof and the oracle function in the verification of FM8501 (except that the FM8501 oracle also takes account of handshaking delays).

  let SynCorrectness1 = new_definition (
    `SynCorrectness1`,
    "SynCorrectness1 (rep:^rep_ty) (ircond,opcval,iszerocond) =
      ∀ireq mpc mar pc acc ir rtn arg buf iack mem.
        Val3_CASES_ASM (rep:^rep_ty) ∧
        Val4Word4_ASM rep ∧
        SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)
        ==>
        ∀t:time.
          (((val4 rep) o mpc) t = 0) ∧
          ((ireq t ∧ ¬(iack t)) = ircond) ∧
          (OpcVal rep (mem t,pc t) = opcval) ∧
          ((iszero rep) (acc t) = iszerocond)
          ==>
          let m = MicroCycles rep (ireq t,mem t,pc t,acc t,rtn t,iack t) in
          ((((val4 rep) o mpc) (t+m) = 0) ∧
           ((mem (t+m),pc (t+m),acc (t+m),rtn (t+m),iack (t+m)) =
            NextState rep (ireq t,mem t,pc t,acc t,rtn t,iack t)))");;

To illustrate details of this verification step, we consider the sequence of microinstructions for an ADD instruction. As shown earlier in Section 4.3.1, the ADD instruction is interpreted in fully synchronous mode by the sequence of microinstructions stored in the microcode ROM at the following locations.

0, 2, 3, 6, 13, 15, 11 and 12

The ADD instruction case is specified by the assumption that the opcode of the current instruction is the ADD instruction opcode and that a hardware interrupt is not about to be processed in this cycle. Since the result of the testzero operation are not relevant in this case, the value for iszerocond is given by a variable b. The desired correctness result is expressed by the goal term in the following call to set_goal.

  set_goal ([],"∀b. SynCorrectness1 (rep:^rep_ty) (F,ADD_OPC,b)");;

The style of interaction with the HOL system described earlier for verifying the phase level is also used here to verify the microprogramming level. The steps shown below are based (more or less) on the proof procedure given in:

     hol/Training/studies/microprocessor/proof/example3.ml

We begin with a little backward proof to expand the correctness condition expressed by SynCorrectness1 and move the expanded result into the assumption list. Definitions for MicroCycles and NextState along with some arithmetic facts are then used to simplify the goal for the ADD instruction case.

  OK..
  "let m = 8
   in
    ((((val4 rep) o mpc)(t + m) = 0) ∧
     (mem(t + m),pc(t + m),acc(t + m),rtn(t + m),iack(t + m) =
      ADD_SEM rep(mem t,pc t,acc t,rtn t,iack t)))"
      [ "Val3_CASES_ASM rep" ]
      [ "Val4Word4_ASM rep" ]
      [ "TamarackImp
         rep
         (datain,pwr,pwr,ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,dataout,
          wmem,dreq,addr)" ]
      [ "SynMemory rep(wmem,addr,dataout,mem,datain)" ]
      [ "∀t. pwr t = T" ]
      [ "((val4 rep) o mpc)t = 0" ]
      [ "ireq t ∧ ¬iack t = F" ]
      [ "val3 rep(opcode rep(fetch rep(mem t,address rep(pc t)))) = 2" ]
      [ "iszero rep(acc t) = b" ]
  () : void

After this initial bit of backward proof, we begin the symbolic execution of the microcode for the ADD instruction. The symbolic execution begins with the value of the microcode program counter mpc equal to zero. We use correctness results for microinstruction 0 (obtained earlier from the verification of the phase level) to derive the state of the machine at time t+1.

  OK..

…

      [ "iack(t + 1) = iack t" ]
      [ "rtn(t + 1) = rtn t" ]
      [ "acc(t + 1) = acc t" ]
      [ "pc(t + 1) = pc t" ]
      [ "mar(t + 1) = pc t" ]
      [ "mem(t + 1) = mem t" ]
      [ "((val4 rep) o mpc)(t + 1) = 2" ]
  () : void

As we have assumed that the microprocessor is operating in fully synchronous mode and that an interrupt request is not about to be processed in this cycle, we can show that the value of the microcode program counter mpc becomes equal to two at time t+1. To advance the state of the symbolic execution to time t+2, we use the correctness results for microinstruction 2 and the behavioural model of external memory to obtain:

  OK..

…

      [ "iack(t + 2) = iack t" ]
      [ "rtn(t + 2) = rtn t" ]
      [ "ir(t + 2) = fetch rep(mem t,address rep(pc t))" ]
      [ "acc(t + 2) = acc t" ]
      [ "pc(t + 2) = pc t" ]
      [ "mar(t + 2) = pc t" ]
      [ "mem(t + 2) = mem t" ]
      [ "((val4 rep) o mpc)(t + 2) = 3" ]
  () : void

By time t+2, the instruction addressed by the program counter pc has been read from memory and loaded into the instruction register ir. The opcode field of the instruction register now contains the opcode for the current instruction which, in the case of ADD, has the value two. Correctness results for microinstruction 2 show that the address of the next microinstruction is obtained by adding four to the value of the opcode; hence, the address of the next microinstruction is six.

  OK..

…

      [ "iack(t + 3) = iack t" ]
      [ "rtn(t + 3) = rtn t" ]
      [ "ir(t + 3) = fetch rep(mem t,address rep(pc t))" ]
      [ "acc(t + 3) = acc t" ]
      [ "pc(t + 3) = pc t" ]
      [ "mar(t + 3) = fetch rep(mem t,address rep(pc t))" ]
      [ "mem(t + 3) = mem t" ]
      [ "((val4 rep) o mpc)(t + 3) = 6" ]
  () : void

This sequence continues with the symbolic execution of microinstruction at locations 6, 13, 15, 11 and 12. New assumptions added to the assumption list for each step are shown below.

OK..

…

[ "iack(t + 4) = iack t" ]
[ "arg(t + 4) = acc t" ]
[ "rtn(t + 4) = rtn t" ]
[ "acc(t + 4) = acc t" ]
[ "pc(t + 4) = pc t" ]
[ "mar(t + 4) = fetch rep(mem t,address rep(pc t))" ]
[ "mem(t + 4) = mem t" ]
[ "((val4 rep) o mpc)(t + 4) = 13" ]
() : void

OK..

…

[ "iack(t + 5) = iack t" ]
[ "buf(t + 5) =
   add
   rep
   (acc t,
    fetch rep(mem t,address rep(fetch rep(mem t,address rep(pc t)))))" ]
[ "arg(t + 5) = acc t" ]
[ "rtn(t + 5) = rtn t" ]
[ "acc(t + 5) = acc t" ]
[ "pc(t + 5) = pc t" ]
[ "mar(t + 5) = fetch rep(mem t,address rep(pc t))" ]
[ "mem(t + 5) = mem t" ]
[ "((val4 rep) o mpc)(t + 5) = 15" ]
() : void

OK..

…

[ "iack(t + 6) = iack t" ]
[ "rtn(t + 6) = rtn t" ]
[ "acc(t + 6) =
   add
   rep
   (acc t,
    fetch rep(mem t,address rep(fetch rep(mem t,address rep(pc t)))))" ]
[ "pc(t + 6) = pc t" ]
[ "mem(t + 6) = mem t" ]
[ "((val4 rep) o mpc)(t + 6) = 11" ]
() : void

OK..

…

[ "iack(t + 7) = iack t" ]
[ "buf(t + 7) = inc rep(pc t)" ]
[ "rtn(t + 7) = rtn t" ]
[ "acc(t + 7) =
   add
   rep
   (acc t,
    fetch rep(mem t,address rep(fetch rep(mem t,address rep(pc t)))))" ]
[ "mem(t + 7) = mem t" ]
[ "((val4 rep) o mpc)(t + 7) = 12" ]
() : void

OK..

…

[ "iack(t + 8) = iack t" ]
[ "rtn(t + 8) = rtn t" ]
[ "acc(t + 8) =
   add
   rep
   (acc t,
    fetch rep(mem t,address rep(fetch rep(mem t,address rep(pc t)))))" ]
[ "pc(t + 8) = inc rep(pc t)" ]
[ "mem(t + 8) = mem t" ]
[ "((val4 rep) o mpc)(t + 8) = 0" ]
() : void

Eventually we obtain a set of equations for the state of the system at the end of this particular execution sequence, that is, at time t+8. These equations describe the net effect of executing the microinstruction sequence which implements an ADD instruction. The backward proof is easily completed by showing that these equations are consistent with the definition of ADD_SEM.

  OK..
  goal proved

… additional output deleted here …

  |- ∀b. SynCorrectness1 rep(F,ADD_OPC,b)
  Previous subproof:
  goal proved
  () : void

There are nine further cases to consider: one case for the JZR instruction when the value of the accumulator is zero; another case for JZR instruction when the accumulator is non-zero; one case for each of the six remaining instructions; and finally, a case for the processing of a hardware interrupt. Correctness results for these nine further cases are expressed by the following theorems:

  |- ∀b. SynCorrectness1 rep(F,JZR_OPC,T)
  |- ∀b. SynCorrectness1 rep(F,JZR_OPC,F)
  |- ∀b. SynCorrectness1 rep(F,JMP_OPC,b)
  |- ∀b. SynCorrectness1 rep(F,SUB_OPC,b)
  |- ∀b. SynCorrectness1 rep(F,LDA_OPC,b)
  |- ∀b. SynCorrectness1 rep(F,STA_OPC,b)
  |- ∀b. SynCorrectness1 rep(F,RFI_OPC,b)
  |- ∀b. SynCorrectness1 rep(F,NOP_OPC,b)
  |- ∀n b. SynCorrectness1 rep(T,n,b)

The penultimate step in verifying the microprogramming level is to combine the above correctness results for individual programming level operations into a single theorem. The theorem shown below is obtained by case analysis on the three parameters of SynCorrectness1.

Since ircond and iszerocond are Boolean variables, case analysis on these variables yields a finite number of cases to consider in the analysis. The variable opcval, a natural number, also yields a finite number of cases: either it is equal to one of the eight opcode values, i.e., opcval < 8, or it is not a valid opcode value, i.e., 8 ≤ opcval, in which case the theorem is vacuously true because of the condition expressed by Val3_CASES_ASM.

  |- ∀b1 n b2. SynCorrectness1 rep(b1,n,b2)

The predicate SynCorrectness1 is useful as a parameterized correctness condition when the correctness of programming level operations are considered individually. But when these individual correctness results are combined in the above theorem, the parameterized variables of SynCorrectness1 no longer have a useful role. The final step in verifying the microprogramming level is to eliminate this overhead to obtain the following theorem.

  |- Val3_CASES_ASM rep ∧
     Val4Word4_ASM rep ∧
     SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)
     ==>
     ∀t.
       (((val4 rep) o mpc) t = 0)
       ==>
       let m = MicroCycles rep (ireq t,mem t,pc t,acc t,rtn t,iack t) in
        ((((val4 rep) o mpc) (t+m) = 0) ∧
         ((mem (t+m),pc (t+m),acc (t+m),rtn (t+m),iack (t+m)) =
          NextState rep (ireq t,mem t,pc t,acc t,rtn t,iack t)))

Although we extend our correctness proof with one more step to obtain the top level statement of correctness, the above theorem can stand alone as a substantial result about the correctness of the TAMARACK-3 design. For all possible instruction cycles, we have shown that the net effect of the instruction cycle corresponds to the state change specified by NextState and that MicroCycles correctly specifies the length of each instruction cycle.

8.3 Completing the proof

As mentioned earlier in Section 6.3, the programming level operation and internal architecture are formally specified at different granularities of time. A formal relationship needs to be established between these two granularities of discrete time in order to complete the verification of TAMARACK-3 (operating in fully synchronous mode).

The chief source of difficulty in the formal definition of this timing relationship is that a unit of discrete time at the abstract programming level time scale does not correspond to a constant number of clock cycles on the concrete microprogramming level time scale.

[figure: ADD; u; u+1; programming level:; f:; •; •; microprogramming level:; •; •; •; •; •; •; •; •; •; t; t+8; mpc:; 0; 2; 3; 6; 13; 15; 11; 12; 0]

Figure 10: ADD Instruction Cycle Timing.

[figure: JMP; u; u+1; programming level:; f:; •; •; microprogramming level:; •; •; •; •; •; t; t+4; mpc:; 0; 2; 3; 5; 0]

Figure 11: JMP Instruction Cycle Timing.

If every programming level operation was implemented by the same number of microinstructions, then the relationship between the two time scales could be expressed by a very simple arithmetic equation. However, this is not the case for our implementation of the microprocessor. For instance, the ADD instruction is implemented by a sequence of eight microinstructions as shown in Figure 10 whereas the JMP instruction is implemented by a sequence of four microinstructions as shown in Figure 11.

Instead, we define a primitive recursive function TimeOfCycle which computes the concrete time of every abstract time point using MicroCycles to determine the number of microinstructions executed between adjacent points on the abstract time scale. ^{13} To compute the concrete time of u+1, we recursively compute the concrete time of u and then add the number given by MicroCycles for the length of the next microinstruction sequence to be executed. As with the definition of TamarackBeh in Section 6.3, we emphasize the distinction between abstract and concrete time by using the variable u for abstract time and the variable t for concrete time.

13The definition of TimeOfCycle is actually just a ‘wrapper’ for the definition of CURRIED TimeOfCycle; this is a consequence of pragmatic restrictions imposed by the HOL system on the format of parameter lists in primitive recursive definitions.

  let CURRIED_TimeOfCycle = new_prim_rec_definition (
    `CURRIED_TimeOfCycle`,
    "(CURRIED_TimeOfCycle (rep:^rep_ty) ireq mem pc acc rtn iack 0 = 0) ∧
     (CURRIED_TimeOfCycle rep ireq mem pc acc rtn iack (SUC u) =
      let t = CURRIED_TimeOfCycle rep ireq mem pc acc rtn iack u in
      (t + (MicroCycles rep (ireq t,mem t,pc t,acc t,rtn t,iack t))))");;
  let TimeOfCycle = new_definition (
    `TimeOfCycle`,
    "TimeOfCycle (rep:^rep_ty) (ireq,mem,pc,acc,rtn,iack) =
      CURRIED_TimeOfCycle u rep ireq mem pc acc rtn iack u");;

The function denoted by,

     TimeOfCycle (rep:^rep_ty) (ireq,mem,pc,acc,rtn,iack)

is the desired mapping from abstract time to concrete time represented by the downward arrows in Figures 10 and 11. For instance, in the ADD microinstruction sequence where t is the concrete time of u, the next point on the abstract time scale u+1, is mapped to t+8 on the concrete time scale. In the JMP microinstruction sequence, u+1 is mapped to

t+4.

Using this specification of the relationship between abstract and concrete time scales, we can derive correctness results expressed in terms of the abstract time scale from results already obtained which are expressed in terms of the concrete time scale. In particular, we want to show that from one abstract time point to the next, the microprocessor executes a single programming level instruction.

We first need to show that every point on the abstract time scale corresponds to the start of a microinstruction sequence. It is sufficient to show that every abstract time point maps to a concrete time when the microcode program counter is zero since every microinstruction sequence begins at this location. It is necessary to assume that the microcode program counter initially has the value zero; that is, time begins when the microcode program counter is reset. The following theorem can be proved by mathematical induction on u.

  |- Val3_CASES_ASM (rep:^rep_ty) ∧
     Val4Word4_ASM rep ∧
     SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) ∧
     (((val4 rep) o mpc) 0 = 0)
     ==>
     let f = TimeOfCycle rep (ireq,mem,pc,acc,rtn,iack) in
     ∀u. ((val4 rep) o mpc) (f u) = 0");;

Once we have shown that every point on the abstract time scale corresponds to the beginning of an instruction cycle, it is a relatively simple matter to complete the last step in this version of the correctness proof for TAMARACK-3. The top-level correctness theorem is expressed by the goal term in the following call to set_goal.

  set_goal (
    [],
    "Val3_CASES_ASM (rep:^rep_ty) ∧
     Val4Word4_ASM rep ∧
     SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) ∧
     (((val4 rep) o mpc) 0 = 0)
     ==>
     let f = TimeOfCycle rep (ireq,mem,pc,acc,rtn,iack) in
     TamarackBeh rep (ireq o f,mem o f,pc o f,acc o f,rtn o f,iack o f)");;

We begin the backward proof for this theorem by just expanding the goal with the definition of TamarackBeh. We can see from the result of this step that the proof is simply a matter of combining correctness results for the microprogramming level with facts derived the definition of TimeOfCycle. In a nutshell, we must show that the externally visible state of the microprocessor at time u+1 is determined by the function NextState from its state at time u.

  OK..
  "Val3_CASES_ASM rep ∧
   Val4Word4_ASM rep ∧
   SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) ∧
   (((val4 rep) o mpc)0 = 0) ==>
   let f = TimeOfCycle rep(ireq,mem,pc,acc,rtn,iack)
   in
    (∀u.
      (mem o f)(u + 1),(pc o f)(u + 1),(acc o f)(u + 1),(rtn o f)(u + 1),
      (iack o f)(u + 1) =
      NextState
      rep
      ((ireq o f)u,(mem o f)u,(pc o f)u,(acc o f)u,(rtn o f)u,(iack o f)u))"
  () : void

Next, we use standard HOL techniques to further expand the goal and move antecedents into the assumption list. However, the use of standard goal reduction techniques alone would result in a goal with some cumbersome sub-terms. These particular sub-terms are unnecessary and it is helpful (as a technique for managing proof complexity) to replace them with simple variables, namely, t and m. These variables are introduced by means of the following two theorems (which are trivial facts of logic).

  |- ∃t. TimeOfCycle rep(ireq,mem,pc,acc,rtn,iack)u = t
  |- ∃m. MicroCycles rep(ireq t,mem t,pc t,acc t,rtn t,iack t) = m

After these simplifications, the new goal is:

  OK..
  "mem(t + m),pc(t + m),acc(t + m),rtn(t + m),iack(t + m) =
   NextState rep(ireq t,mem t,pc t,acc t,rtn t,iack t)"
      [ "Val3_CASES_ASM rep" ]
      [ "Val4Word4_ASM rep" ]
      [ "SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)" ]
      [ "((val4 rep) o mpc)0 = 0" ]
      [ "TimeOfCycle rep(ireq,mem,pc,acc,rtn,iack)u = t" ]
      [ "MicroCycles rep(ireq t,mem t,pc t,acc t,rtn t,iack t) = m" ]
  () : void

We have already shown that every point on the abstract time scale corresponds to the beginning of an instruction cycle. In particular, we know that the value of the microcode program counter mpc at time t is 0.

  OK..

…

      [ "((val4 rep) o mpc)t = 0" ]
  () : void

We have also shown (in Section 8.2) that the externally visible state of the microprocessor at the end of the instruction cycle is related to its initial state at the beginning of the instruction cycle by the function NextState. This fact is used to solve the current goal and complete the final step in this version of the correctness proof for TAMARACK-3.

  OK..

… additional output deleted here …

  goal proved
  |- Val3_CASES_ASM rep ∧
     Val4Word4_ASM rep ∧
     SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) ∧
     (((val4 rep) o mpc)0 = 0) ==>
     let f = TimeOfCycle rep(ireq,mem,pc,acc,rtn,iack)
     in
      TamarackBeh rep(ireq o f,mem o f,pc o f,acc o f,rtn o f,iack o f)
  Previous subproof:
  goal proved
  () : void

This theorem relates the design of the internal architecture given by the definition of TamarackImp to its behavioural specification given by the predicate TamarackBeh. In particular, we show that the constraints imposed by TamarackImp on the register-transfer level signals of the internal architecture satisfy the constraints imposed by TamarackBeh on the corresponding programming level signals.

9 Synchronizing multiple levels of timing

The simple approach just described in Section 8.3 for relating different granularities of time is not very general because it depends on the implementation of programming level operation by fixed microinstruction sequences whose pre-determined lengths are specified by the definition of MicroCycles. In general, programming level operations may not necessarily be implemented at lower levels by fixed sequences.

An example of when it is not possible to define a simple function like MicroCycles to compute the exact length of each instruction cycle is the operation of TAMARACK-3 in fully asynchronous mode when delayed handshaking signals may cause microinstructions to be repeated. Although there are ways to partially circumvent this problem using an oracle function to ‘guess’ the length of each instruction cycle, the result may not be completely general^{14} or correspond very well to an intuitive view of this timing relationship.

The term temporal abstraction (or temporal projection) has been used in verification circles [20, 18, 27, 28, 45, 47, 52] to denote the idea of relating different rates of computation in a formal specification. This idea naturally arises from the more general concept

14If all functions must be total, then use of an oracle function to guess the length of each instruction cycle implies that every instruction cycle is finite, in particular, that handshaking sequences always run to completion. A completely general approach would not imply that every handshaking sequence terminates, but instead, require (as we do) that this fact be established by formal proof.

interpreter control part

end of execution commands status next instruction request

instructions

status

Figure 12: Control Part of an Interpreter.

of viewing computer hardware as a hierarchy of interpretation levels where a timing relationship between two levels of interpretation is sometimes called a synchronization scheme (or synchronization mechanism). The control part of each level in the interpretation hierarchy can be viewed as a virtual machine with the generalized form shown in Figure 12. To paraphrase the description by Anceau in [2]:

A given level is only allowed to generate a new command once it has received an end-of-execution signal for the present command from the levels below. In turn, it sends a similar signal to the control part immediately above requesting the next instruction. The end-of-instruction signal received by the lowest level of synchronous logic is simply the clock signal of the machine. The next-instruction signal issued by the microprogramming level implies the fetching of the next instruction from memory.

In this section, we describe a formalization which corresponds directly to the imagery of Figure 12 where a next-instruction signal at the microprogramming level implies the fetching of the next programming level instruction from memory. At this level, the nextinstruction signal is not a physical signal, but rather, a time-dependent condition on the internal state of the machine.

In fully synchronous mode, the end of the instruction cycle occurs when the value of the microprocessor program counter returns to zero. Hence, the next-instruction signal generated by the microprogramming level is the time-dependent condition expressed by the term,

     ((val4 rep) o mpc) Eq 0

where Eq is an infix temporal operator for relating a signal to a particular value in terms of equality.

let Eq = new_infix_definition (`Eq`,"$Eq (P:time->*) c = λt. P t = c");;

If an instruction cycle begins at time t, then it terminates at time t+m if and only if t+m is the first time that the microcode program counter mpc becomes equal to zero since time t. This condition is expressed by the term,

Next (((val4 rep) o mpc) Eq 0) (t,t+m)

where the predicate Next is defined as:

let Next = new_definition (
`Next`,
"Next g (t1,t2) = t1 < t2 ∧ (∀t. t1 < t ∧ t < t2 ==> ¬(g t)) ∧ (g t2)");;

It is possible to show that this condition holds for each of the fixed microinstruction sequences that implement programming level operations in fully synchronous mode. In place of the predicate SynCorrectness1, a slightly different form of parameterized correctness condition is used to verify the implementation of each programming level operation.

let SynCorrectness2 = new_definition (
`SynCorrectness2`,
"SynCorrectness2 (rep:^rep_ty) (ircond,opcval,iszerocond) =
∀ireq mpc mar pc acc ir rtn arg buf iack mem.
Val3_CASES_ASM (rep:^rep_ty) ∧
Val4Word4_ASM rep ∧
SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)
==>
∀t:time.
(((val4 rep) o mpc) t = 0) ∧
((ireq t ∧ ¬(iack t)) = ircond) ∧
(OpcVal rep (mem t,pc t) = opcval) ∧
((iszero rep) (acc t) = iszerocond)
==>
∃m.
  Next (((val4 rep) o mpc) Eq 0) (t,t+m) ∧
  ((mem (t+m),pc (t+m),acc (t+m),rtn (t+m),iack (t+m)) =
   NextState rep (ireq t,mem t,pc t,acc t,rtn t,iack t))");;

[figure: abstract time:; •; •; •; f:; concrete time:; •; •; •; •; •; •; •; •; •; •; g:; F; F; T; F; F; F; T; F; T; F]

Figure 13: Abstract and Concrete Time Scales.

In this version of the correctness condition, the length of the instruction cycle is an existentially quantified variable instead of a value computed by MicroCycles. The proofs of correctness for each programming level operation are almost the same as before except that we must keep track of the microcode program counter mpc throughout the instruction cycle and show that it is never equal to zero before the end of the instruction cycle. Combining individual correctness results for each programming level operation and eliminating, as before, the overhead of a parameterized correctness condition yields the following theorem.

  |- Val3_CASES_ASM (rep:^rep_ty) ∧
     Val4Word4_ASM rep ∧
     SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)
     ==>
     ∀t.
       (((val4 rep) o mpc) t = 0)
       ==>
       ∃m.
         Next (((val4 rep) o mpc) Eq 0) (t,t+m) ∧
         ((mem (t+m),pc (t+m),acc (t+m),rtn (t+m),iack (t+m)) =
          NextState rep (ireq t,mem t,pc t,acc t,rtn t,iack t))

The next step is to define a general purpose function TimeOf which uses an nextinstruction signal g to construct a mapping f from an abstract time scale to a concrete time scale. The relationship between abstract and concrete time is shown in Figure 13. The following definition of TimeOf is similar to definitions given in previous work by Dhingra [18], Herbert [28] and Melham [45] (the name ‘TimeOf’ is used here for continuity with previous work). It is defined in terms of the predicates First and Next using primitive recursion and Hilbert’s ε-operator. ^{15}

15Our definition of TimeOf is simplified by avoiding the existential quantification found in corresponding definitions given by [18, 28, 45]. When the constraint that g is ‘true infinitely often’ holds, this function yields exactly the same mapping from abstract time to concrete time. When this constraint does not hold, both versions (with and without existential quantification) yield an incomplete mapping.

  let First = new_definition (
    `First`,
    "First g t = (∀p. p < t ==> ¬(g p)) ∧ (g t)");;
  let TimeOf = new_prim_rec_definition (
    `TimeOf`,
    "(TimeOf g 0 = εt. First g t) ∧
     (TimeOf g (SUC u) = εt. Next g (TimeOf g u,t))");;

The first point on the abstract time scale corresponds to the first time that the nextinstruction signal g is true with respect to the concrete time scale. Subsequent points on the abstract time scale are defined recursively. The next point after u on the abstract time scale, i.e., u+1, corresponds to the next time that the next-instruction signal g becomes true with respect to the concrete time scale.

Applying TimeOf to the next-instruction signal generated at microprogramming level of TAMARACK-3,

     TimeOf (((val4 rep) o mpc) Eq 0)

yields a mapping from points on the abstract time scale to points on the concrete time scale. This mapping is the synchronization scheme which relates behaviour at the abstract programming level time scale to behaviour at the concrete microprogramming level time scale.

As with most definitions that use Hilbert’s ε-operator, some additional proof infrastructure is needed to reason about specifications involving TimeOf. For instance, it is necessary to establish the fact that the next-instruction signal is true infinitely often [31, 45]. Fortunately, the main result of this proof infrastructure can be summed up in a compact theorem:

  |- ∀g r.
       (∃t. g t) ∧ (∀t. g t ==> ∃m. Next g (t,t+m) ∧ r (t,t+m))
       ==>
       ∀u. r (TimeOf g u,TimeOf g (u+1))

For any next-instruction signal g and next state relation r, this theorem can be used to reduce the problem of establishing,

     ∀u. r (TimeOf g u,TimeOf g (u+1))

to a pair of simpler problems:

     ∃t. g t
     ∀t. g t ==> ∃m. Next g (t,t+m) ∧ r (t,t+m)

The last step in verifying TAMARACK-3 is essentially a question about the synchronization scheme which relates behaviour at the programming level time scale to behaviour at the microprogramming level time scale. The above theorem provides a way to translate this question into a pair of simpler problems. ^{16} In particular, it is used mid-way through a backward proof of the top-level correctness statement to reduce the goal,

OK..
"∀u.
mem(TimeOf g(u + 1)),pc(TimeOf g(u + 1)),acc(TimeOf g(u + 1)),
rtn(TimeOf g(u + 1)),iack(TimeOf g(u + 1)) =
NextState
rep
(ireq(TimeOf g u),mem(TimeOf g u),pc(TimeOf g u),acc(TimeOf g u),
rtn(TimeOf g u),iack(TimeOf g u))"
[ "((val4 rep) o mpc) Eq 0 = g" ]
[ "Val3_CASES_ASM rep" ]
[ "Val4Word4_ASM rep" ]
[ "SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)" ]
[ "∃t. ((val4 rep) o mpc)t = 0" ]
() : void

to the following pair of sub-goals. ^{17}

"∃t. g t"
[ "((val4 rep) o mpc) Eq 0 = g" ]
[ "Val3_CASES_ASM rep" ]
[ "Val4Word4_ASM rep" ]
[ "SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)" ]
[ "∃t. ((val4 rep) o mpc)t = 0" ]
() : void

16This is analogous to how axioms and rules of Hoare logic can be used to translate questions about program correctness into verification conditions [26].

17A generalized form of this backward proof step could be implemented as a HOL tactic in the same way that axioms and rules of Hoare Logic can be ‘inverted’ into a tactic [26].

  "∀t.
    g t ==>
    (∃m.
      Next g(t,t+m) ∧
      (mem(t + m),pc(t + m),acc(t + m),rtn(t + m),iack(t + m) =
       NextState rep(ireq t,mem t,pc t,acc t,rtn t,iack t)))"
      [ "((val4 rep) o mpc) Eq 0 = g" ]
      [ "Val3_CASES_ASM rep" ]
      [ "Val4Word4_ASM rep" ]
      [ "SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)" ]
      [ "∃t. ((val4 rep) o mpc)t = 0" ]
  () : void

The first sub-goal is satisfied by assumptions in the assumption list combined with the definition of Eq. The second sub-goal is satisfied by previously mentioned correctness results for the microprogramming level. The satisfaction of these two sub-goals yields the following correctness theorem for TAMARACK-3.

  |- Val3_CASES_ASM (rep:^rep_ty) ∧
     Val4Word4_ASM rep ∧
     SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) ∧
     (∃t. ((val4 rep) o mpc) t = 0)
     ==>
     let f = TimeOf (((val4 rep) o mpc) Eq 0) in
     TamarackBeh rep (ireq o f,mem o f,pc o f,acc o f,rtn o f,iack o f)

This is nearly identical to the previous version of the top level correctness statement in Section 8.3 except for the sub-term which specifies the relationship between the two time scales.

10 Using temporal logic to deal with asynchrony

This section gives a very brief outline of the formal verification of TAMARACK-3 when operating in fully asynchronous mode. The main specification problem is to define a behavioural model for fully asynchronous memory which is completely general and independent from the microprocessor specification. The main verification problem is to derive an abstract view of the instruction cycle where handshaking interactions are collapsed into fixed sequences of steps.

Our solution to these problems is to embed a form of temporal logic in higher-order logic by regarding a set of temporal logic operators as abbreviations for higher-order functions. Temporal logic is especially useful for specifying and reasoning about relative order in a set of events. This approach results in succinct specifications and simplifies

               [figure: t1; t2; t3; t4; dack; dreq]

Figure 14: Four-Phase Handshaking Timing Diagram.

the verification task by hiding some low-level aspects of proof, in particular, the use of mathematical induction, in derived inference rules for temporal logic operators.

In this section, we only present details on how temporal logic operators are used to specify constraints on the handshaking signals themselves, i.e., dreq and dack. A complete model of external memory also involves a formal specification of constraints on the address and data signals which are synchronized by the handshaking signals. For completeness, this latter part of the memory specification is given in Appendix B but these details are not discussed here.

10.1 Specification using temporal logic operators

We use the temporal logic operators,

□ - “henceforth”
◇ - “eventually”
◯ - “next”
∪ - “until”

and a number of connectives (not, ⟶, and) corresponding to logical connectives in propositional logic. Later on, we give precise definitions for these operators and connectives as abbreviations for higher-order functions. For now, the intuitive meanings suggested above are enough to illustrate the use of these operators in the formal specification of a handshaking protocol.

Figure 14 shows a stylized timing diagram for a four-phase handshaking sequence. A request at time t1 by the sender is acknowledged at time t2 by the receiver. A request to end the interaction is signaled at time t3 and eventually acknowledged at time t4.

The handshaking protocol is formally specified by a number of constraints imposed on both the sender and receiver. For now, these can be understood as constraints imposed on the sender and receiver viewed together as a single system; later on, we say which constraints are imposed on which process.

A handshaking interaction is initiated whenever dreq becomes true. dreq must continue to be true until this is acknowledged. This constraint is expressed by:

     (dreq ⟶ (dreq ∪ dack))

A request must be eventually be acknowledged. Furthermore, once dack becomes true, it must remain true until dreq becomes false.

     (dreq ⟶ (◇ dack))
     (dack ⟶ (dack ∪ (not  dreq)))

Once a request has been acknowledged, dreq must eventually become false again to signal the end of the interaction. The next request cannot be signaled until dack also returns to false.

     (dack ⟶ (◇ (not  dreq)))
     ((not  dreq) ⟶ ((not  dreq) ∪ (not  dack)))

When dreq becomes false, dack must also becomes false and stay false until the next request.

     ((not  dreq) ⟶ (◇ (not  dack)))
     ((not  dack) ⟶ ((not  dack) ∪ dreq))

Upon completion of the handshaking interaction, the protocol requires another request to be initiated sometime in the future. This final constraint is usually included in the handshaking protocol specification to obtain the property that system activity never ceases.

     ((not  dack) ⟶ (◇ dreq))

The use of temporal logic operators to specify the relative order of events in a handshaking protocol has been described by others including Bochman [6], Dill and Clarke [19], and Fujita et al. [22].

10.2 Embedding temporal logic in higher-order logic

Temporal logics are often treated as primitive systems based on semantic definitions for temporal logic operators. However, our higher-order logic framework allows us to regard temporal logic operators as simply abbreviations for higher-order functions. The following definitions yield temporal logic operators for a form of temporal logic known as Linear Temporal Logic.

  let H = new_definition (`H`,"□ P = λt. ∀n. P (t+n)");;
  let E = new_definition (`E`,"◇ P = λt. ∃n. P (t+n)");;
  let N = new_definition (`N`,"◯ P = λt. ((P (t+1)):bool)");;
  let Until = new_infix_definition (
    `Until`,
    "$∪ P Q = λt. ∀n. (∀m. m < n ==> ¬(Q (t+m))) ==> P (t+n)");;
  let Not = new_definition (`Not`,"not P = λt. ¬(P t)");;
  let Imp = new_infix_definition (`Imp`,"$⟶ P Q = λt. P t ==> Q t");;
  let And = new_infix_definition (`And`,"$and P Q = λt. P t ∧ Q t");;

Each operator is defined in terms of a function which maps discrete points in time, modelled by the natural numbers, to Boolean values. These operators can can be combined with variables such as P and Q to form assertions in temporal logic. In both first-order logic and higher-order logic, every assertion, for instance,

     ∀b. b ∨ ¬b

is a Boolean expression which is either true or false. However, an assertion in temporal logic such as,

      (P ⟶ ◇ (Q ∪ R))

is only true or false relative to a particular instant of time. When stated as an assertion, this is informally understood to mean that the assertion is true at every instant of time. However, to formally represent temporal logic assertions as assertions in our higher-order logic framework, we introduce an notion of validity where a temporal logic assertion is valid if and only if it is true at all times.

  let VALID = new_definition (`VALID`,"VALID P = ∀t. P t");;

Powerful inferences rules for direct manipulation of temporal logic assertions can be derived in higher-order logic from the above definitions. Many such rules effectively ‘package up’ what would otherwise be tedious and repetitive patterns of inference. For instance, the following theorem provides a particularly useful rule; this rule achieves, in a single step, an inference which would otherwise involve a proof by mathematical induction.

  |- ∀P Q. VALID((P and (not Q)) ⟶ (◯ P)) ==> VALID(P ⟶ (P U Q))

A recent survey article [11] describes ‘traditional logic’ (which includes higher-order logic) and temporal logic as two alternative kinds of pure formalisms for reasoning about hardware. But when temporal logic operators are simply abbreviations for higher-order functions, anything which can done with the temporal logic operators can also be done without them using explicit time variables. In fact, we have taken a mixed-mode approach of using both temporal operators and explicit time variables. The right mixture of temporal operators and explicit time variables yields relatively succinct specifications and much easier proofs.

Previous work by Hale [27] demonstrated that the idea of embedding of a temporal logic in higher-order logic was of practical use. Leeser [43] has also embedded temporal logic in a theorem proving environment to reason about hardware. Both Hale and Leeser used another form of temporal logic called Interval Temporal Logic developed by Moszkowski [47, 48] to reason about digital systems in general. However, the more ordinary form of temporal logic captured in our definitions for □, ◇, ◯, etc., is adequate for the very specific purpose of reasoning about handshaking interactions between TAMARACK-3 and external memory.

10.3 Sender and receiver specifications

Earlier we gave a formal specification of the handshaking protocol in terms of constraints expressed by a set of temporal logic assertions. Seitz [51] distinguishes between functional constraints on outputs which must be satisfied by a process and domain constraints which are allowable assumptions about inputs. In the handshaking protocol, constraints imposed on dreq are functional constraints for the sender process and domain constraints for the receiver process. Constraints imposed on dack are functional constraints for the receiver process and domain constraints for the sender process.

It turns out that only some of the domain constraints are actually needed in each case. Furthermore, these domain constraints are only needed to establish specific functional constraints. For example, the domain constraint,

     (dreq ⟶ (dreq ∪ dack))

that dreq, once true, must remain true can be assumed in showing that the receiver satisfies the functional constraint,

     (dreq ⟶ (◇ dack))

that it will eventually detect and acknowledge the request.

The following definitions give the functional constraints for the sender and receiver respectively and, where required, the domain constraints which can be assumed in showing that a process satisfies a particular functional constraint.

let Sender = new_definition (
`Sender`,
"Sender (dreq,dack) =
 VALID (dreq ⟶ (dreq ∪ dack)) ∧
 VALID ((not dreq) ⟶ ((not dreq) ∪ (not dack))) ∧
 (VALID (dack ⟶ (dack ∪ (not dreq))) ==>
  VALID (dack ⟶ (◇ (not dreq)))) ∧
 (VALID ((not dack) ⟶ ((not dack) ∪ dreq)) ==>
  VALID ((not dack) ⟶ (◇ dreq)))");;
let Receiver = new_definition (
`Receiver`,
"Receiver (dreq,dack) =
 VALID (dack ⟶ (dack ∪ (not dreq))) ∧
 VALID ((not dack) ⟶ ((not dack) ∪ dreq)) ∧
 (VALID (dreq ⟶ (dreq ∪ dack)) ==>
  VALID (dreq ⟶ (◇ dack))) ∧
 (VALID ((not dreq) ⟶ ((not dreq) ∪ (not dack))) ==>
  VALID ((not dreq) ⟶ (◇ (not dack))))");;

When the sender and receiver parts of the handshaking protocol specification are both satisfied, this results in the set of constraint mentioned at the beginning of this section for the system as a whole. This is shown by the following theorem.

|- Sender(dreq,dack) ∧
Receiver(dreq,dack)
==>
VALID (dreq ⟶ (dreq ∪ dack)) ∧
VALID (dreq ⟶ (◇ dack)) ∧
VALID (dack ⟶ (dack ∪ (not dreq))) ∧
VALID (dack ⟶ (◇ (not dreq))) ∧
VALID ((not dreq) ⟶ ((not dreq) ∪ (not dack))) ∧
VALID ((not dreq) ⟶ (◇ (not dack))) ∧
VALID ((not dack) ⟶ ((not dack) ∪ dreq)) ∧
VALID ((not dack) ⟶ (◇ dreq))

10.4 Memory specification

The predicate Receiver is used to partially specify a behavioural model of fully asynchronous memory. The rest of the memory specification (given in Appendix B) specifies constraints on the address and data signals which are synchronized by the handshaking signals. These two parts of the specification are combined together in the definition of AsynMemory (also given in Appendix B).

The memory specification is a formal rendering of the description given earlier in Section 3. In particular, it is precise statement about details such as the constraint that:

After signaling a memory request, dreq must remain equal to T and the wmem, address bus addr and dataout bus dataout must remain at stable values until dack becomes equal to T signaling that the request has been satisfied.

As with the specification of fully synchronous memory, SynMemory, the operations performed by memory are selected from the representation variable by fetch and store. For example, when dack becomes equal to T at time t+n in response to a read request initiated at time t, the value of the datain bus is described by the following equation:

     datain (t+n) = (fetch rep) (mem t,(address rep) (mar t))

One of the main differences from the FM8501 specification [30] is that our relational specification style allows the memory model to have an entirely independent specification. Thus, it is possible to reason independently about the internal operation of TAMARACK-3 at the phase level without need of a memory model. It is only necessary to compose specifications for TAMARACK-3 and external memory in order to reason about their interaction at the microprogramming level. This contrasts with the functional specification style used for FM8501 where “the characterization of external devices are wrapped up in the same function which specifies the microprocessor” [30].

10.5 Verification

Verifying the operation of TAMARACK-3 in fully asynchronous mode is much more difficult than fully synchronous mode because of the unknown length of microcode repeat-loops during an instruction cycle. The overall strategy is to first show that every handshaking sequence runs to completion, then collapse repeat-loops to single steps in an abstract view of behaviour. Symbolic execution is then used to reason about the fixed sequences of operations in this abstract view of behaviour. Finally, we use the function TimeOf described earlier in Section 9 to specify a synchronization scheme for asynchronous mode.

10.5.1 Phase level

Earlier correctness results described in Section 8.1 (and given in Appendix A) for the phase level operation of TAMARACK-3 are re-used in this version of the correctness proof without change or addition. We recall that phase level correctness results do not depend on any particular model of external memory. The interaction of the microprocessor with external memory only concerns the operation of its internal architecture at the microprogramming level.

10.5.2 Implementation of the sender specification

One of the first steps in verifying the operation of TAMARACK-3 in fully asynchronous mode is to show that the microprogramming level correctly implements the sender part of the handshaking specification. The derivation of the following theorem is tedious but very routine. This proof step does not involve a behavioural model for external memory.

  |- Val3_CASES_ASM rep ∧
     Val4Word4_ASM rep ∧
     TamarackImp rep (
       datain,dack,gnd,idreq,mpc,mar,pc,
       acc,ir,rtn,arg,buf,idack,dataout,wmem,dreq,addr) ∧
     GND gnd ∧
     (((val4 rep) o mpc) 0 = 0)
      ==>
     Sender (dreq,dack)

The proof procedure used to establish this result is illustrated in the following HOL source file by proving that a very simple state machine also satisfies the sender part of the handshaking protocol specification.

     hol/Training/studies/microprocessor/proof/example4.ml

Once it has been established that the microprogramming level satisfies the constraints expressed by Sender, this result can be combined with the specification of external memory, in particular, the constraints expressed by Receiver to obtain some very useful facts for reasoning about handshaking interactions. Among other things, one of the useful facts implied by the combined constraints of Sender and Receiver is that every handshaking sequence runs to completion, that is, every repeat-loop in the microcode eventually terminates.

10.5.3 Collapsing repeat-loops to single steps

The microprocessor specification and behavioural model of external memory are combined together in the definition of AsynSystem to reason about interactions of the TAMARACK-3 microchip with fully asynchronous memory. As mentioned earlier, the memory specification AsynSystem includes the constraints expressed by Receiver.

  let AsynSystem = new_definition (
    `AsynSystem`,
    "AsynSystem (rep:^rep_ty)
      (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,dack,mem) =
      ∃datain gnd dataout wmem dreq addr.
        TamarackImp rep (
          datain,dack,gnd,ireq,mpc,mar,pc,
          acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr) ∧
        AsynMemory rep (dreq,dack,mem,wmem,addr,dataout,datain) ∧
        GND gnd");;

The fact that every repeat-loop in the microcode terminates makes it possible to derive theorems which, in effect, collapse repeat-loops to single steps in an abstract view of behaviour at the microprogramming level.

For instance, the following theorem provides a collapsed view of the repeat-loop in state 6 of the FSM flow graph. This theorem states that the repeat-loop will terminate after zero or more clock cycles with no changes to the internal state of the microprocessor.

  |- Val3_CASES_ASM rep ∧
     Val4Word4_ASM rep ∧
     AsynSystem rep (idreq,mpc,mar,pc,acc,ir,rtn,arg,buf,idack,dack,mem) ∧
     (((val4 rep) o mpc) 0 = 0)
     ==>
     ∀t.
       (((val4 rep) o mpc) t = 6)
       ==>
       ∃n.
         (dack (t+n) = F) ∧
         (∀m. m < n ==> (dack (t+m) = T)) ∧
         (((val4 rep) o mpc) (t+n) = 6) ∧
         (mem (t+n) = mem t) ∧
         (mar (t+n) = mar t) ∧
         (pc (t+n) = pc t) ∧
         (acc (t+n) = acc t) ∧
         (rtn (t+n) = rtn t) ∧
         (idack (t+n) = idack t)

Another example is the theorem shown below which provides a collapsed view of the repeat-loop in state 13. It is convenient to state this result as a transition which begins in state 6 and terminates in state 15. During this transition, a value is fetched from memory mem, added to the current contents of the accumulator acc, and the result temporarily placed in the ALU buffer buf.

  |- Val3_CASES_ASM rep ∧
     Val4Word4_ASM rep ∧
     AsynSystem rep (idreq,mpc,mar,pc,acc,ir,rtn,arg,buf,idack,dack,mem) ∧
     (((val4 rep) o mpc) 0 = 0)
     ==>
     ∀t.
       (((val4 rep) o mpc) t = 6) ∧
       (dack t = F)
       ==>
       ∃n.
         (∀m. m < n ==> ¬(((val4 rep) o mpc) (t+m) = 0)) ∧
         (((val4 rep) o mpc) (t+n) = 15) ∧
         (mem (t+n) = mem t) ∧
         (pc (t+n) = pc t) ∧
         (buf (t+n) =
           add rep (acc t,fetch rep (mem t,(address rep (mar t))))) ∧
         (rtn (t+n) = rtn t) ∧
         (idack (t+n) = idack t)

The above pair of theorems describe two successive steps in the symbolic execution of the microprogramming level. In the course of reasoning about the microinstruction sequence for an ADD instruction, the first theorem advances the state of the symbolic execution to end of the repeat-loop in state 6 and the second theorem advances the symbolic execution from this point to state 15.

10.5.4 Symbolic execution

A complete set of theorems for collapsing repeat-loops into single steps represent an abstract view of behaviour where programming level operations are implemented by fixed sequences of actions. Hence, the symbolic execution proof technique described earlier in Section 8 for fully synchronous mode can also be used here to show that programming level operations are correctly implemented by microinstruction sequences which involve handshaking interactions with external memory.

Correctness results for each programming level operation are combined by case analysis to obtain the following theorem.

  |- Val3_CASES_ASM rep ∧
     Val4Word4_ASM rep ∧
     AsynSystem rep (idreq,mpc,mar,pc,acc,ir,rtn,arg,buf,idack,dack,mem) ∧
     (((val4 rep) o mpc) 0 = 0)
     ==>
     ∀t.
       (((val4 rep) o mpc) t = 0) ∧
       (dack t = F)
       ==>
       ∃n.
         Next ((((val4 rep) o mpc) Eq 0) and (not dack)) (t,t+n) ∧
         ((mem (t+n),pc (t+n),acc (t+n),rtn (t+n),idack (t+n)) =
          NextState rep (idreq t,mem t,pc t,acc t,rtn t,idack t))

The above theorem is almost identical to the top-level correctness theorem for fully synchronous mode given in Section 9 except for the term used to denote the next-instruction signal. Instead of,

     (((val4 rep) o mpc) Eq 0)

the next-instruction signal is denoted by the term,

     (((val4 rep) o mpc) Eq 0) and (not dack)

which states that the next instruction cycle does not begin until the control unit FSM is about to leave state 0. The use of this condition for the next-instruction signal is not necessarily an obvious choice. We leave it an exercise for the reader to determine why other conditions, e.g., when the FSM first enters state 0, are not suitable.

10.5.5 Top level correctness statement

This version of the proof is completed by repeating the proof procedure outlined earlier in Section 9 for using the function TimeOf to construct a mapping from abstract time to concrete time. The top-level correctness statement for this version of the proof is shown below.

  |- Val3_CASES_ASM rep ∧
     Val4Word4_ASM rep ∧
     AsynSystem rep (idreq,mpc,mar,pc,acc,ir,rtn,arg,buf,idack,dack,mem) ∧
     (((val4 rep) o mpc) 0 = 0)
     ==>
     let f = TimeOf ((((val4 rep) o mpc) Eq 0) and (not dack)) in
     TamarackBeh rep (idreq o f,mem o f,pc o f,acc o f,rtn o f,idack o f)

11 What has been proved ?

We have described three different correctness theorems for the design of TAMARACK-3. The first two theorems state correctness results for the operation of TAMARACK-3 in fully synchronous mode. These two theorems differ only in how they define a timing relationship between different levels of specification. The third theorem states correctness results for the operation of TAMARACK-3 in fully asynchronous mode. As mentioned earlier, we have not formally considered the operation of TAMARACK-3 in extended cycle mode.

Each correctness theorem includes explicit assumptions about the external environment, in particular, a behavourial model of external memory and how it is interfaced to the microprocessor. In each case, the correctness theorem states that the predicate TamarackBeh is an abstract model of the internal architecture as specified by the predicate TamarackImp. Therefore, true statements about the behaviour of the abstract model can be related to true statements about the specification of the internal architecture.

In the course of establishing these general results, we have obtained some more specific results about particular aspects of the design including:

• That the system bus is never multiply-driven by more than one bus device at any one time.

• That the microprocessor design correctly implements the sender part of the handshaking protocol.

• A precise description of the next-instruction signal marking the end of an instruction cycle (which might not be obvious in the case of fully asynchronous mode).

Most of the proof effort concerns the fetch-decode-execute sequence for each programming level operation during an instruction cycle. But the proof goes further than this by considering the overall operation of the microprocessor, that is, how one instruction cycle is related to the next instruction cycle. For instance, it shows that an interrupt request does not interrupt the completion of a memory interaction (i.e. the repeat-loop in state 0). It also shows that an interrupt request take precedence, as one would expect, over the normal flow of program control (when a previous interrupt is not still being serviced).

It is also important to describe the limitations of this proof of correctness. As we remarked earlier, the formal verification of TAMARACK-3 focuses very specifically on the register-transfer level operation of the internal architecture. Below and above this level there are aspects of a complete design for TAMARACK-3 which are not formally considered.

Section 4.4 described some aspects of the semantic gap between the abstract view of sequential behaviour in our lowest level of formal specification and timing relationships in actual hardware. This gap is bridged by a number of informal assumptions which are not explicitedly mentioned in the correctness results. Although our formal theory could be extended with several more, increasingly detailed levels of timing, ^{18} there will always be a gap between formal proof (a mathematical concept) and actual hardware (a physical device). As Cohn [13] remarks,

18Herbert [28] describes proofs techniques in the HOL logic for relating more detailed levels of timing to synchronous level models. Leeser [43] describes similar work in a temporal logic framework.

… a material device can only be observed and measured, not verified. It can be described in an abstracted way, and the simplified description verified, but again, there is no way to assure the accuracy of the description.

There is also a gap between our behavioural models of external memory and the operation of real memory devices. But in the case of fully asynchronous memory, this gap is more an instance of over-simplification than well-conceived abstraction. The model of fully asynchronous memory completely ignores the possibility of any kind of failure in the handshaking protocol. This simplification allows us to prove, for instance, that every memory interaction runs to completion even though TAMARACK-3 does not have a time-out mechanism to handle failures in the handshaking protocol. ^{19}

It is also important to understand that our formal theory says nothing, with the exception of two assumptions which appear explicitly in the correctness theorems, about the basic data types used to represent data in the microprocessor and primitive operations involving these data types. It may surprise some readers that these details do not need to be known, but their unimportance underlines the fact that very little few aspects of the computation performed by the hardware is actually taken account of in the formal proof. The only significant forms of computation considered in the proof are:

• Computation of microinstruction addresses by the next address logic.

• Resolving decentralized control over access to the system bus in the datapath.

• Extraction of individual bits and other sub-fields from microinstruction words by decoding logic.

This lack of detail about basic types and primitive operations should not be seen as a shortcoming or unfinished step in our formal proof. We have deliberately avoided these details to clearly demarcate the boundaries between what has and what has not been considered in the formal verification of TAMARACK-3. Building more details than necessary into the computation model would have risked the false impression that these details have been considered in the formal proof. Instead, other levels of concern should be considered in separate theories. The next section suggests how a hierarchy of parameterized theories (in the non-technical, general sense) could be stacked upon one another linked together through representation variables.

19The absence of a time-out mechanism is merely a case of simplification. There is no intrinsic reason why a time-out mechanism would be difficult to reason about in the formal verification of a microprocessor design (see suggested exercise in Section 15).

12 Relating this proof to other levels

The representation variable rep which appears as an extra parameter in definitions throughout the formal specification of TAMARACK-3 is effectively a parameterization of the formal theory. It provides a means of relating this theory to both lower and higher level models of computation.

This section illustrates how our formal theory for TAMARACK-3 might be linked into a verified stack^{20} with examples drawn from the following HOL source file:

     hol/Training/studies/microprocessor/proof/example5.ml

12.1 Lower levels

By assigning an appropriate value to the representation variable rep, the formal theory about TAMARACK-3 can made to stack upon a lower level theory about the implementation of register-transfer level devices. This lowel level theory might, in turn, be parameterized by its own representation variable and stacked upon an even lower level of representation at the transistor level.

To illustrate this idea with a simple example, the constant REP16 is defined as a value for rep based on the built-in HOL data types described in [24, 32, 13]. In this case, we have created data types for a 16-bit version of TAMARACK-3. ^{21}

20The term ‘verified stack’ is due to researchers at Computational Logic Inc. who have made noteworthy progress in the development of this concept [4, 5].

21In the HOL88 system, these built-in data types are provided by eval library. However, the constants V and SEG are no longer supported and must now be defined by the user.

loadt `eval`;;
declare_word_widths [3;4;13;16];;
declare_memories [13,16];;
let ISZERO16 = new_definition (
`ISZERO16`,
"ISZERO16 w = ((VAL16 w) = 0)");;
let INC16 = new_definition (
`INC16`,
"INC16 w = WORD16 ((VAL16 w) + 1)");;
let ADD16 = new_definition (
`ADD16`,
"ADD16 (w1,w2) = WORD16 ((VAL16 w1) + (VAL16 w2))");;
let SUB16 = new_definition (
`SUB16`,
"SUB16 (w1,w2) = WORD16 ((VAL16 w1) - (VAL16 w2))");;
let OPCODE = new_definition (
`OPCODE`,
"OPCODE w = WORD3 (V (SEG (0,2) (BITS16 w)))");;
let ADDRESS = new_definition (
`ADDRESS`,
"ADDRESS w = WORD13 (V (SEG (3,15) (BITS16 w)))");;
let REP16 = new_definition (
`REP16`,
"REP16 =
  ISZERO16,                             % iszero %
  INC16,                                % inc %
  ADD16,                                % add %
  SUB16,                                % sub %
  WORD16,                               % wordn %
  VAL16,                                % valn %
  OPCODE,                               % opcode %
  VAL3,                                 % val3 %
  ADDRESS,                              % address %
  (λ(x,y). FETCH13 x y),                % fetch %
  (λ(x,y,z). STORE13 y z x),            % store %
  WORD4,                                % word4 %
  VAL4");;                              % val4 %

The current version of these built-in HOL data types (as given by the eval library in the HOL88 system) is not fully axiomatized or secure,^{22} but with a complete axiomatization it would be possible to derive the assumptions expressed by the predicates Val3_CASES_ASM and Val4Word4_ASM as proven theorems.

  |- Val3_CASES_ASM REP16
  |- Val4Word4_ASM REP16

If these assumptions were established as theorems for this particular value of the representation variable, we could then obtain the following correctness result for a 16-bit version of TAMARACK-3 (along with similar results for fully synchronous mode).

  |- AsynSystem REP16 (idreq,mpc,mar,pc,acc,ir,rtn,arg,buf,idack,dack,mem) ∧
     ((VAL4 o mpc) 0 = 0)
     ==>
     let f = TimeOf (((VAL4 o mpc) Eq 0) and (not dack)) in
     TamarackBeh REP16 (idreq o f,mem o f,pc o f,acc o f,rtn o f,idack o f)

Hence, one of the purposes of relating our formal theory to lower levels is to replace assumptions about uninterpreted data types by theorems derived from lower level representations of data.

Another purpose is to derive correctness results for implementations of register-transfer level primitives, for example, to verify that an implementation of the ALU correctly implements a set of arithmetic/logical operations.

Because the current version of the built-in HOL data types for machine words is not fully axiomatized or secure, we have used an alternate representation where bit patterns are modelled by functions which map bit positions to bit values. In addition to completeness and security, this representation offers the advantage of being able to parameterize specifications by the number of bits in a machine word instead of the fixed word widths provided by the built-in HOL data types. Functions such as Valn and Wordn are defined to establish relationships between this function-based representation and higher-algebraic levels, i.e., the natural numbers. Correctness results for implementations of registertransfer level primitives are expressed in terms of Valn and Wordn. We have used this approach to verify a complete implementation of an earlier version of TAMARACK-3 down to the transistor level [33, 34, 36, 39, 40].

22An incomplete set of postulated axioms exists in the form of evaluation rules which use mk thm to create unproven theorems. The recursive data types package developed for HOL by Melham [46] provides a foundation for building a secure set of data types for reasoning about machine words and bit patterns.

12.2 Higher levels

While lower levels of representation may yield theorems to replace assumptions about data types, stacking higher levels upon our correctness results for TAMARACK-3 may conversely require the introduction of more assumptions about the data types. As explained earlier, the use of uninterpreted data types and uninterpreted primitives for operations on these data types makes computational aspects of our programming level model somewhat transparent. To reason about the execution of programs requires the introduction of some more primitives and more assumptions to provide the programming level model with more computation details.

At the very least, it would likely be necessary to provide some details of the operation selected by inc, used to increment the program counter pc, in order to reason about the sequential execution of TAMARACK-3 instructions. For example, the predicate INC_ASM,

  let INC_ASM = new_definition (
    `INC_ASM`,
    "INC_ASM n (rep:^rep_ty) =
      ∀w. ((valn rep) ((inc rep) w)) = ((((valn rep) w) + 1) MOD (2 EXP n))");;

could be defined to provide an arithmetic interpretation for the operation selected from the representation variable by inc. ^{23} In this case, machine words (of various sizes) are modelled at this higher level by natural numbers where the finite precision of operations performed by hardware is modelled by modular arithmetic. The parameter n is the number of bits in a full-size machine word; for instance, n would be equal to sixteen for a 16-bit version of TAMARACK-3.

Similar assumptions expressed by ADD_ASM and SUB_ASM provide arithmetic interpretations for the operations selected by add and sub. ^{24} The predicate FETCH_STORE_ASM provides an interpretation for memory operations.

23The assumption expressed by INC ASM is stronger than necessary if it is only necessary to know that the address field of the full-size machine word is incremented. This assumption would be too restrictive for an implementation where the address bits are not necessarily the low-order bits of the full-size machine word stored in the program counter pc.

24Subtraction in the natural numbers as axiomatized in HOL does not correspond exactly to subtraction in two’s complement arithmetic. The definition of two’s complement subtraction given in [36] provides a more accurate model of how this ALU operation would likely be implemented in hardware.

let ISZERO_ASM = new_definition (
`ISZERO_ASM`,
  "ISZERO_ASM (rep:^rep_ty) =
    ∀w. ((iszero rep) w) = (((valn rep) w) = 0)");;
let ADD_ASM = new_definition (
  `ADD_ASM`,
  "ADD_ASM n (rep:^rep_ty) =
    ∀w1 w2.
      ((valn rep) ((add rep) (w1,w2))) =
        ((((valn rep) w1) + ((valn rep) w2)) MOD (2 EXP n))");;
let SUB_ASM = new_definition (
  `SUB_ASM`,
  "SUB_ASM n (rep:^rep_ty) =
    ∀w1 w2.
      ((valn rep) ((sub rep) (w1,w2))) =
        ((((valn rep) w1) - ((valn rep) w2)) MOD (2 EXP n))");;
let FETCH_STORE_ASM = new_definition (
  `FETCH_STORE_ASM`,
  "FETCH_STORE_ASM (rep:^rep_ty) =
    ∀m a1 a2 w.
      ((a1 = a2) =>
        ((fetch rep) (((store rep) (m,a1,w)),a2) = w) |
        ((fetch rep) (((store rep) (m,a1,w)),a2) = (fetch rep) (m,a2)))");;

Like the assumptions expressed by Val3_CASES_ASM and Val4Word4_ASM, these additional assumptions could be proven as theorems from a lower level representation of data. For instance, a complete axiomatization of built-in HOL data types for machine words would yield the theorems,

|- INC_ASM 16 REP16
|- ISZERO_ASM REP16
|- ADD_ASM 16 REP16
|- SUB_ASM 16 REP16
|- FETCH_STORE_ASM REP16

as properties of the constant REP16. In the case of INC_ASM, ADD_ASM and SUB_ASM, the axiomatization would need to include the following property. A similar theorem has been derived for the function-based representation described in [34, 36].

  |- ∀m. VAL16 (WORD16 m) = (m MOD (2 EXP 16))

Together with some additional assumptions about operations for extracting the opcode and operand address bits from a full-size machine word, the above assumptions would introduce enough substance to the programming level model of TAMARACK-3 to reason about the execution of programs. In particular, it would provide enough computational power to support the compiler verification study reported in [37, 38].

13 Summary

The expressive power of higher-order logic has been an advantage in several ways for the work described in this case study. One of the most important uses of higher-order functions and relations has been to parameterize definitions by a representation variable providing a formal basis for our approach to abstract specification.

We have also found several instances where the ability to use a relation in place of a function was very desirable. Our model of the datapath bus experiments with relations as an alternative to using combining functions. In Section 10 we described some advantages of a relational style of specification which allows independent specifications to be given for the microprocessor and external memory. Most of the time, functions are more natural and simpler to use, but occasionally, the well-conceived use of a relation in place of a function gives a superior result.

It was extremely useful (in fact, much more useful than we initially expected) to embed some operators from temporal logic in our higher-order framework especially when we compare this approach with our previous attempts to reason about asynchrony [35]. It is likely that work on embedding other calculi in higher-order logic will be a particularly interesting area of future development in the HOL user community. In addition to Hale’s work on Interval Temporal Logic [27], some other examples include work by Gordon on program logics [26], by Loewenstein on a theory for deterministic and non-deterministic state machines [44], and by Camilleri on CSP trace theory [10].

A number of errors in the design and specification of TAMARACK-3 were discovered in the course of verifying its correctness. A few of these errors were not simple mistakes and not the kind of error easily revealed by simulation (they concerned subtle aspects of the handshaking protocol specification). However, many simple mistakes were also found by verification but they could have been discovered earlier without incurring the high cost of verification if the specifications had been executable. Camilleri [9] points out the advantage of executing formal specifications as a means of supporting a verification methodology. In this respect, the Boyer-Moore approach [30, 4, 5] offers the advantage of directly executable specifications. The increased expressiveness of higher-order logic results in terms which do not always have an obvious interpretation as an executable specification. However, the implementation of an executable subset of higher-order logic is a foreseeable addition to the HOL system. ^{25}

25Camilleri’s thesis [8] describes simulation tools for an executable subset of higher-order logic oriented

There is a very steep learning curve for the HOL system and many new users must wonder if they can afford to invest enough effort to receive any return on their investment. We can offer some encouragement by observing that simply getting a large design specification to be successfully type-checked by the HOL system is a significant accomplishment. Fully automated type-checking often reveals errors which would go unnoticed without the scrutinizing eye of the type-checker. A typical example would be the interconnection of two ports with mismatched types (e.g. a 16-bit bus connected to a 13-bit bus). While type-checking problems require an understanding of higher-order logic, it does not require any familiarity with theorem-proving. Of course, there are conventional CAD tools (as well as ordinary, strongly-typed programming languages) which can be used to check the consistency of a design. However, using the HOL system to type-check a design represents an intermediate goal for new users along the path towards full-scale verification.

Acknowledgements. The work described in this case study owes a great deal to many people. A complete set of acknowledgements are given in [41], however, I would particularly like to mention past and present developers of the HOL system (and its software parent, the LCF system); this work would not have been possible without the elegant tool they have created. Furthermore, the remarkably painless transition from an earlier version of HOL to the HOL88 system is a tribute to the skill of Mike Gordon and Tom Melham.

to hardware simulation.

14 References

[1] James R. Armstrong, Chip-Level Modelling with VHDL, Prentice-Hall, Englewood Cliffs, N.J., 1989.

[2] F. Anceau, The Architecture of Microprocessors, Addison-Wesley Publishing Company, Wokingham, 1986.

[3] H. Barrow, VERIFY: A Program for Proving Correctness of Digital Hardware Designs, Artificial Intelligence, Vol. 24, No. 1-3, December 1984, pp. 437-491.

[4] William R. Bevier, Warren A. Hunt, Jr., and William D. Young, in: Towards Verified Execution Environments, in: Procs. of the 1987 IEEE Symposium on Security and Privacy, 27-29 April 1987, Oakland, California Computer Society Press, Washington, D.C., 1987 pp. 106-115. Also Report No. 5, Computational Logic, Inc., Austin, Texas, February 1987.

[5] W. Bevier, W. Hunt, J Moore, and W. Young, An Approach to Systems Verification, Journal of Automated Reasoning, Vol. 5, No. 4, November 1989.

[6] G. Bochman, Hardware Specification with Temporal Logic, IEEE Transactions on Computers, Vol. C-31, No. 3, March 1982, pp. 223-231.

[7] Randy Everitt Bryant, A Switch-Level Simulation Model for Integrated Logic Circuits, Ph.D. Thesis, Dept. of Electrical Engineering and Computer Science, Report No. MIT/LCS/TR-259, Laboratory for Computer Science, Massachusetts Institute of Technology, March 1981.

[8] Albert John Camilleri, Executing Behavioural Definitions in Higher Order Logic, Ph.D. Thesis, Report No. 140, Computer Laboratory, Cambridge University, February 1988.

[9] Albert John Camilleri, Simulation as an Aid to Verification Using the HOL Theorem Prover, in: D. Edwards, ed., Procs. of the IFIP TC10 Working Conf. on Design Methodology in VLSI and Computer Architecture, Pisa, Italy, 19-21 September 1988, North-Holland, Amsterdam, 1989, pp. 147-168. Also Report No. 150, Computer Laboratory, Cambridge University, October 1988.

[10] Albert John Camilleri, Mechanizing CSP Trace Theory in Higher Order Logic, (in preparation), Hewlett-Packard Laboratories, Bristol, England, 1989.

[11] Paolo Camurati and Paolo Prinetto, Formal Verification of Hardware Correctness, IEEE Computer, Vol. 21, No. 7, July 1988, pp. 8-19.

[12] Avra Cohn, A Proof of Correctness of the Viper Microprocessor: The First Level, in: G. Birtwistle and P. Subrahmanyam, eds., VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, Boston, 1988, pp. 27-71. Also Report No. 104, Computer Laboratory, Cambridge University, January 1987.

[13] Avra Cohn, Correctness Properties of the Viper Block Model: The Second Level, in: G. Birtwistle and P. Subrahmanyam, eds., Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, New York, 1989, pp. 1-91. Also Report No. 134, Computer Laboratory, Cambridge University, May 1988.

[14] Avra Cohn, The Notion of Proof in Hardware Verification, Journal of Automated Reasoning, Vol. 5, May 1989, pp. 127-139.

[15] W.J. Cullyer, High Integrity Computing, in: M. Joseph, ed., Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science, No. 331, Springer-Verlag, Berlin, 1988. pp. 1-35.

[16] Paul Curzon, Ph.D. Thesis, (in preparation), Computer Laboratory, Cambridge University, 1989.

[17] Bruce S. Davie, A Formal, Hierarchical Design and Validation Methodology for VLSI, Ph.D. Thesis, Report CST-55-88, Dept. of Computer Science, University of Edinburgh, October 1988.

[18] Inderpreet S. Dhingra, Formalising an Integrated Circuit Design Style in Higher-Order Logic, Ph.D. Thesis, Report No. 151, Computer Laboratory, Cambridge University, 1989.

[19] D. Dill and E. Clarke, Automatic Verification of Asynchronous Circuits using Temporal Logic, IEE Procs., Vol. 133, Pt. E, No. 5, September 1986, pp. 276-282.

[20] H. Eveking, Formal Verification of Synchronous Systems, in: G. Milne and P. Subrahmanyam, eds., Formal Aspects of VLSI Design, Procs. of the 1985 Edinburgh Conference on VLSI, North-Holland, Amsterdam, 1986, pp. 137-152.

[21] H. Eveking, How to Design Correct Hardware and Know It. G. Milne, ed., The Fusion of Hardware Design and Verification, Procs. of the IFIP WG 10.2 Intl. Working Conf., Glasgow, Scotland, 3-6 July 1988, North-Holland, Amsterdam, 1988, pp. 250-262.

[22] M. Fujita, H. Tanaka and T. Moto-oka., Temporal Logic Based Hardware Description and Its Verification with Prolog, New Generation Computing, No. 1, 1983, pp. 195-203.

[23] M. Gordon, A Model of Register Transfer Systems with Applications to Microcode and VLSI Correctness, Internal Report CSR-82-81, Department of Computer Science, University of Edinburgh, 1981.

[24] M. Gordon, LCF LSM, Report No. 41, Computer Laboratory, Cambridge University, 1983.

[25] M. Gordon, Proving a Computer Correct using the LCF LSM Hardware Verification System, Report No. 42, Computer Laboratory, Cambridge University, 1983.

[26] Michael J. C. Gordon, Mechanizing Programming Logics in Higher Order Logic, in: G. Birtwistle and P. Subrahmanyam, eds., Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, New York, 1989, pp. 387-439. Also Report No. 145, Computer Laboratory, Cambridge University, September 1988.

[27] Roger W. S. Hale, Programming in Temporal Logic, Ph.D. Thesis, Report No. 173, Computer Laboratory, Cambridge University, July 1989.

[28] John M. J. Herbert, Application of Formal Methods to Digital System Design, Ph.D. Thesis, Computer Laboratory, Cambridge University, 1986.

[29] John Herbert, Temporal Abstraction of Digital Designs, G. Milne, ed., The Fusion of Hardware Design and Verification, Procs. of the IFIP WG 10.2 Intl. Working Conf., Glasgow, Scotland, 3-6 July 1988, North-Holland, Amsterdam, 1988, pp. 1-25.

[30] Warren A. Hunt, FM8501, A Verified Microprocessor, Ph.D. Thesis, Report No. 47, Institute for Computing Science, University of Texas, Austin, December 1985.

[31] Joyce, J., G. Birtwistle and M. Gordon, Proving a Computer Correct in Higher Order Logic, Report No. 100, Computer Laboratory, Cambridge University, 1986.

[32] Jeffrey J. Joyce, Formal Verification and Implementation of a Microprocessor, in: G. Birtwistle and P. Subrahmanyam, eds., VLSI Specification, Verification and Synthesis, Procs. of a Workshop, 12-16 January 1987, Kluwer Academic Publishers, Boston, 1988, pp. 129-157.

[33] Jeffrey J. Joyce, Multi-Level Verification of a Simple Microprocessor, First Year Ph.D. Progress Report and Research Proposal, Computer Laboratory, Cambridge University, December 1987.

[34] Jeffrey J. Joyce, Generic Structures in the Formal Specification and Verification of Digital Circuits, in: G. Milne, ed., The Fusion of Hardware Design and Verification, Procs. of the IFIP WG 10.2 Intl. Working Conf., Glasgow, Scotland, 3-6 July 1988, North-Holland, Amsterdam, 1988, pp. 50-74.

[35] Jeffery J. Joyce, Formal Specification and Verification of Asynchronous Processes in Higher-Order Logic, in: C. Rattray, ed., BCS-FACS Workshop on Specification and Verification of Concurrent Processes, Stirling, Scotland, 6-8 July 1988, (to be published by Springer Verlag). Also Report No. 136, Computer Laboratory, Cambridge University, June 1988.

[36] Jeffery J. Joyce, Using Higher-Order Logic to Specify Computer Hardware and Architecture, in: D. Edwards, ed., Design Methodologies for VLSI and Computer Architecture, Procs. of the IFIP TC10 Working Conf. on Design Methodology in VLSI and Computer Architecture, Pisa, Italy, 19-21 September 1988, North-Holland, Amsterdam, 1989, pp. 129-146.

[37] Jeffrey J. Joyce, A Verified Compiler for a Verified Microprocessor, Report No. 167, Computer Laboratory, Cambridge University, March 1989.

[38] Jeffrey J. Joyce, Totally Verified Systems: Linking Verified Software to Verified Hardware, in: M. Leeser and G. Brown, eds., Specification, Verification and Synthesis: Mathematical Aspects, Procs. of a Workshop, 5-7 July 1989, Ithaca, N.Y., Springer-Verlag, 1989. Also Report No. 178, Computer Laboratory, Cambridge University, September 1989.

[39] Jeffrey J. Joyce, Formal Specification and Verification of Synthesized MOS Structures, in: G. Musgrave and U. Lauther, eds., VLSI 89, Procs. of the IFIP TC10/WG 10.5 Intl. Conf. on Very Large Scale Integration, Munich, Germany, 16-18 August 1989, (to be published by Elsevier Science Publishers).

[40] Jeffrey J. Joyce, Formal Specification and Verification of Microprocessor Systems, Integration, the VLSI journal, Vol. 7, September 1989, pp. 247-266.

[41] Jeffrey J. Joyce, Ph.D. Thesis, (in preparation), Computer Laboratory, Cambridge University, 1989.

[42] J. Joyce, E. Liu, J. Rushby, N. Shankar, R. Suaya, F. von Henke: From Hardware Verification to Silicon Compilation, (in preparation) SRI International, Menlo Park, 1990.

[43] Miriam E. Leeser. Reasoning about the Function and Timing of Integrated Circuits with Prolog and Temporal Logic, Ph.D. Thesis, Computer Laboratory, Report No. 132, Computer Laboratory, Cambridge University, April 1988.

[44] Paul Loewenstein, Reasoning about State Machines in Higher-Order Logic, in: M. Leeser and G. Brown, eds., Specification, Verification and Synthesis: Mathematical Aspects, Procs. of a Workshop, 5-7 July 1989, Ithaca, N.Y., Springer-Verlag, 1989.

[45] Thomas F. Melham, Abstraction Mechanisms for Hardware Verification, in: G. Birtwistle and P. Subrahmanyam, eds., VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, Boston, 1988, pp. 267-291. Also Report No. 103, Computer Laboratory, Cambridge University, January 1987.

[46] Thomas F. Melham, Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic, Ph.D. Thesis, Computer Laboratory, Cambridge University, 1989.

[47] Benjamin C. Moszkowski, Reasoning about Digital Circuits, Ph.D. Thesis, Report CS-83-970, Dept. of Computer Science, Stanford University, 1983.

[48] Benjamin Moszkowski, A Temporal Logic for Multilevel Reasoning about Hardware, IEEE Computer Vol. 18, No. 2, February 1985, pp. 10-19.

[49] C. Pygott, Electrical, Environmental and Timing Specification of the Viper Microprocessor, Memorandum No. 3753, RSRE, British Ministry of Defense, December 1984.

[50] Martin Richards, BSPL: A Language for Describing the Behaviour of Synchronous Hardware, Report No. 84, Computer Laboratory, Cambridge University, July 1986.

[51] C. Seitz, Chapter 7: System Timing, in: C. Mead and L. Conway, Introduction to VLSI Systems, Addison-Wesley, Reading, Massachusetts, 1980, pp. 218-262.

[52] P. A. Subrahmanyam, Toward a Framework for Dealing with System Timing in Very High Level Silicon Compilers, in: G. Birtwistle and P. Subrahmanyam, eds., VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, Boston, 1988, pp. 159-215.

[53] P. A. Subrahmanyam, What’s in a Timing Discipline ?: Considerations in the Specification and Synthesis of Systems with Interacting Asynchronous and Synchronous Components, in: M. Leeser and G. Brown, eds., Specification, Verification and Synthesis: Mathematical Aspects, Procs. of a Workshop, 5-7 July 1989, Ithaca, N.Y., Springer-Verlag, 1989.

[54] John P. Van Tassel, The Semantics of VHDL with VAL and HOL: Towards Practical Verification Tools, M.Sc. Thesis, Dept. of Computer Science and Engineering, Wright State University, 1989.

[55] F. W. von Henke, J. S. Crow, R. Lee, J. M. Rushby and R. A. Whitehurst, The EHDM Verification Environment: An Overview, Proceedings of the 11th National Computer Security Conference, Baltimore, October 1988, pp. 147-155.

[56] Daniel Weise, Formal Multilevel Hierarchical Verification of Synchronous MOS VLSI Circuits, Ph.D Thesis, Report No. 978, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, 1987.

15 Suggested exercises

1. Design an implementation of the next address logic using devices such as logic gates, multiplexors and an adder. Verify this design by showing that it satisfies the behavioural specification expressed by NextMPC.

2. Replace the next address logic and microcode ROM by a single PLA structure. Verify that this new design is functionally equivalent to the original design of the control unit. This may require a more concrete representation for microinstruction addresses.

3. Experiment with trade-offs between defining NextState as a function (as done in the current version) and defining it as a relation. In particular, re-define the semantics of the return-from-interrupt RFI instruction so that the value of the return address register rtn after executing the RFI instruction is either:

(a) Some fixed but unknown value.

(b) Some unpredictable value which “may vary from moment to moment, implementation to implementation, instruction to instruction within an implementation” ^{26}.

4. Re-design the internal architecture of TAMARACK-3 so that the program counter is incremented in parallel with data operations on the accumulator and external memory. Verify that the new design is correct with respect to the programming level model.

5. Enlarge the TAMARACK-3 instruction set to provide more ALU operations, more forms of conditional branches (e.g., branch on overflow), and an alternative to absolute addressing for instruction operands.

6. Generalize some of the proof procedures used to verify TAMARACK-3 to provide greater automation for verifying TAMARACK-like architectures. For instance, generalize the proof procedure for symbolic execution of the microprogramming level by having the proof procedure use intermediate results for the mpc to determine the microinstruction sequence instead of supplying this sequence beforehand.

7. Modify the design of TAMARACK-3 to include a time-out mechanism to handle failures in handshaking interactions while operating in fully asynchronous mode. Weaken the behavioural model of fully asynchronous memory to allow for the possibility of such failures. Verify the modified design (with appropriate modifications to the programming level model) using the more realistic model of external memory.

26Timothy E. Leonard, ed., VAX Architectural Reference Manual, Digital Equipment Corp., 1987.

A Appendix: phase level correctness results

Correctness results for each of the sixteen microinstructions are shown below. These results are used to verify the microprogramming level operation of TAMARACK-3 for both fully synchronous and fully asynchronous mode.

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 0)
==>
(((val4 rep) o mpc) (t+1) =
   ((~((idle t) ∨ ~(dack t))) => 0 |
    ((ireq t) ∧ ~(iack t)) => 1 | 2)) ∧
(mar (t+1) = pc t) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = rtn t) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 1)
==>
(((val4 rep) o mpc) (t+1) = 12) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = pc t) ∧
(buf (t+1) = ((wordn rep) 0)) ∧
(iack (t+1) = T) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 2)
==>
(((val4 rep) o mpc) (t+1) = ((dack t) => 3 | 2)) ∧
(mar (t+1) = mar t) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = acc t) ∧
(ir (t+1) = datain t) ∧
(rtn (t+1) = rtn t) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = T) ∧
(addr t = (address rep) (mar t))

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 3)
==>
(((val4 rep) o mpc) (t+1) =
   ((~((idle t) ∨ ~(dack t))) => 3 |
     (((val3 rep) ((opcode rep) (ir t))) + 4))) ∧
(mar (t+1) = ir t) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = acc t) ∧
(ir (t+1) = ir t) ∧
(rtn (t+1) = rtn t) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 4)
==>
(((val4 rep) o mpc) (t+1) = (((iszero rep) (acc t)) => 5 | 11)) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = acc t) ∧
(ir (t+1) = ir t) ∧
(rtn (t+1) = rtn t) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 5)
==>
(((val4 rep) o mpc) (t+1) = 0) ∧
(pc (t+1) = ir t) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = rtn t) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 6)
==>
(((val4 rep) o mpc) (t+1) =
  ((~((idle t) ∨ ~(dack t))) => 6 | 13)) ∧
(mar (t+1) = mar t) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = rtn t) ∧
(arg (t+1) = acc t) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 7)
==>
(((val4 rep) o mpc) (t+1) =
  ((~((idle t) ∨ ~(dack t))) => 7 | 14)) ∧
(mar (t+1) = mar t) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = rtn t) ∧
(arg (t+1) = acc t) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 8)
==>
(((val4 rep) o mpc) (t+1) = ((dack t) => 11 | 8)) ∧
(mar (t+1) = mar t) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = datain t) ∧
(rtn (t+1) = rtn t) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = T) ∧
(addr t = (address rep) (mar t))

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 9)
==>
(((val4 rep) o mpc) (t+1) = ((dack t) => 11 | 9)) ∧
(mar (t+1) = mar t) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = rtn t) ∧
(iack (t+1) = iack t) ∧
(dataout t = acc t) ∧
(wmem t = T) ∧
(dreq t = T) ∧
(addr t = (address rep) (mar t))

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 10)
==>
(((val4 rep) o mpc) (t+1) = 0) ∧
(pc (t+1) = rtn t) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = rtn t) ∧
(iack (t+1) = F) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 11)
==>
(((val4 rep) o mpc) (t+1) = 12) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = rtn t) ∧
(buf (t+1) = ((inc rep) (pc t))) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 12)
==>
(((val4 rep) o mpc) (t+1) = 0) ∧
(pc (t+1) = buf t) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = rtn t) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 13)
==>
(((val4 rep) o mpc) (t+1) = ((dack t) => 15 | 13)) ∧
(mar (t+1) = mar t) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = rtn t) ∧
(arg (t+1) = arg t) ∧
(buf (t+1) = ((add rep) ((arg t),(datain t)))) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = T) ∧
(addr t = (address rep) (mar t))

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 14)
==>
(((val4 rep) o mpc) (t+1) = ((dack t) => 15 | 14)) ∧
(mar (t+1) = mar t) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = acc t) ∧
(rtn (t+1) = rtn t) ∧
(arg (t+1) = arg t) ∧
(buf (t+1) = ((sub rep) ((arg t),(datain t)))) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = T) ∧
(addr t = (address rep) (mar t))

|- Val3_CASES_ASM rep ∧
Val4Word4_ASM rep ∧
TamarackImp rep (
 datain,dack,idle,ireq,mpc,mar,pc,
 acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
==>
∀t.
(((val4 rep) o mpc) t = 15)
==>
(((val4 rep) o mpc) (t+1) = 11) ∧
(pc (t+1) = pc t) ∧
(acc (t+1) = buf t) ∧
(rtn (t+1) = rtn t) ∧
(iack (t+1) = iack t) ∧
(dataout t = ((wordn rep) 0)) ∧
(wmem t = F) ∧
(dreq t = F)

B Appendix: asynchronous memory specification

The predicate ReceiverData is a generalized specification for the receiving part of the handshaking interaction. The asynchronous memory model is an instance of this generalized specification.

let When = new_infix_definition (`When`,"$when P Q = ((Q ⟶ P) ∪ Q)");;
let ReceiverData = new_definition (
`ReceiverData`,
"ReceiverData (f1:(*#**)->***,f2) (req,ack,mem,datain,dataout) =
  (∀x. VALID (((not req) and (mem Eq x)) ⟶ (◯ (mem Eq x)))) ∧
  (∀x y.
    VALID (
      ((not req) and (◯ req)) ⟶
      (◯ (mem Eq x)) ⟶
      (◯ ((datain Eq y) ⟶ ((datain Eq y) ∪ ack))) ⟶
      (◯ ((((dataout Eq (f1 (x,y))) and (mem Eq (f2 (x,y)))) ∪ (not req))
        when ack))))");;
let ReadFunc = new_definition (
`ReadFunc`,
"ReadFunc (rep:^rep_ty) (memval,(wmemval,addrval,datainval)) =
  (wmemval => datainval | ((fetch rep) (memval,addrval)))");;
let WriteFunc = new_definition (
`WriteFunc`,
"WriteFunc (rep:^rep_ty) (memval,(wmemval,addrval,datainval)) =
  (wmemval => ((store rep) (memval,addrval,datainval)) | memval)");;
let AsynMemory = new_definition (
`AsynMemory`,
"AsynMemory (rep:^rep_ty) (
  req,ack,mem,wmem,addr,datain,dataout) =
  Receiver (req,ack) ∧
  ReceiverData (ReadFunc rep,WriteFunc rep)
    (req,ack,mem,(λt:time.(wmem t,addr t,datain t)),dataout)");;