Contents

Presented at the 20th Workshop on Microprogramming, December 1-4, 1987, Colorado Springs, CO. To appear in ACM SIGMICRO Newsletter, 1988.

1 Introduction

Recent research has demonstrated the possibilities of producing hardware designs that have been verified as opposed to tested. Examples of this approach include the proof of correctness of a simple microcoded processor [1] and the verification of the design of various low-level hardware modules [2]. The tools that have been used in this work are LCF_LSM [3], VERITAS [4] and HOL [5].

Most people would agree that it is desirable for a manufacturer’s products to meet some form of specification. This requirement becomes vital when the product is used in a life-critical situation - users must know what the behaviour of the product will be. This has resulted in the emergence of a disciplined approach to design in many engineering professions. An architect checks that a new building will not fall down, an aircraft designer does detailed calculations to ensure that the wings produce enough lift. At each step of the construction process checks are made to ensure that the components used meet their specifications in the design.

Now that computers are being used in life-critical applications, such as fly-by-wire aircraft or complex life support systems, it is vital for the underlying hardware to be correct. It is impossible to exhaustively test components as simple as a 32-bit multiplier - never mind an entire processor - so different techniques must be used to verify designs. As E.W. Dijkstra has remarked [6]

Starting from an agreed formal specification a correct design can be produced if the implementation is produced by a sequence of provably correct steps. This will bring the standard of computer design to the levels expected in other branches of engineering [7]. Use of verified design methods can produce savings in time and expenditure. The need to redesign part of a VLSI device may cause a 2 or 3 month delay in its launch and several such iterations can make a device obsolete before it comes to market.

This technical note details how a verified design approach was used on sections of the IMS T800 floating-point unit microcode. The formal semantics of the occam language [8, 9] and the use of program transformations are described. Then a simple example is used to show haw a high-level specification can be developed into microcode using formal design methods that guarantee the correctness of the final design.

2 Occam

The occam language [8] allows a system to be hierarchically decomposed into a collection of concurrent processes communicating via channels. This allows it to be used to represent the behaviour of a VLSI device in a very natural way - the various top-level modules can be mapped on to individual processes with their interfacing handled by channel communication. In more traditional languages the inherent parallelism of a VLSI device has to handled by explicit programming. occam has a very efficient implementation permitting fast execution of such a behavioural description to allow for simulation. Most importantly, for the purposes of this paper, occam has rich formal semantics [9] which facilitate program transformation and proof.

2.1 Occam transformations

The algebraic semantics of occam given in [9] consists of a set of laws which define the language constructs. The algebraic semantics have been shown to be consistent with the denotational semantics establishing the validity of these laws. These transformation laws enable a normal form for finite occam programs to be defined.

A transformation law can be used to transform one program into another whose observable behaviour is equivalent. Many transformation laws are ’obviously true’ and are regularly used by programmers - for example sequential composition of processes is associative:

This is the law SEQ binassoc. Others are more complex and include preconditions for validity but, with a bit of effort, can be seen to be true.

If a sequence of transformations can be found to transform one program into another then the two programs are known to be equivalent. If, in addition, one of these programs is known to be a correct implementation of a specification then the correctness of the other can be inferred.

Using these techniques it is possible to demonstrate the correctness of implementations by transformation - doing this by experimental testing takes far too long for problems like floating-point arithmetic.

An example transformation

As an example consider the following program fragment:

These two assignment statements can be merged into one multiple assignment statement.
First the law AS id is used to add an identity assignment to each statement:

giving the program:

Next the law AS perm is applied to the second statement:

giving:

Finally these two statements are merged by the law SEQ comb:

giving:

2.2 The occam transformation system

To aid the process of transforming programs a simple interactive transformation system has been implemented in the language ML [10]. A program can be parsed into this system and then manipulated by the user. All the basic laws in [9] are implemented inside the system along with some extra ones - the system is extensible and new laws (that have been proven correct) can be coded and added if required. Regularly executed sequences of transformations can be coded as ML functions giving higher-level transformations. The example transformation shown above has been coded up as the transformation law combos which itself is used in more powerful transformations. The basic transformations often have only a small localised effect but when suitably combined they can perform significant transformations which being constructed from correct component transformations are known to be correct.

The transformation system user can select which transformation laws to apply and examine the effects of these transformations. The fact that the transformation system is being used provides the verification of the equivalence between the initial program and the transformed end result - but if necessary it would be feasible to produce the list of transformations which constitute the proof.

3 Instruction development

The instruction development process consists of specifying the operation of the instruction in the Z specification language [11]. Since Z is a mathematically based language it allows precise unambiguous statements about operations to be made concisely and - if used in a sympathetic manner - clearly.

Along with the specifications of the instructions there will be a set of specifications of system constants, system state and other global features of the design. In the case of the IMS T800 floating-point unit this consists of a formal specification of the IEEE floating-point standard - such as in [12], a specification of the internal representation of floating-point numbers in registers, a specification of the floating-point unit state - i.e. the registers and flags, and definitions of various constants that are used. This corresponds to formally describing the overall architecture.

Each instruction specification is refined into a high-level occam implementation. This can involve going via a guarded command language using pre- and post-conditions as in [13]. This high-level implementation is often the sort of implementation that a competent programmer would produce from the specification but the formal derivation ensures that no mistakes are made.

The occam program is then transformed inside the transformation system into a form equivalent to the microcode assembler source. The steps in this process are motivated by the functions available in the microcode machine. This involves:

1. refining /F conditions into the conditions available on the microcode machine
2. refining the expressions so that they use the alu and bus operations available on the microcode machine
3. refining the sequential control of the program into a form that simulates the microinstruction control in the microcode machine

The various stages of simple development used as an example are shown in the next section.

4 An example instruction development

The following example demonstrates the methods that have been found to be useful in the IMS T800 design. This example takes a high-level specification in the Z specification language [11] and refines it in a sequence of steps into a microcoded implementation that will run on a microcode machine similar to the IMS T800 floating point unit. For brevity certain simplifications have been made - notably that infinities, Not-a-Numbers and denormalised numbers are ignored.

4.1 Preliminary definitions

Before any instructions are specified and implemented it is necessary to make a few preliminary definitions. There is a need to specify the format of registers, various constants and methods for interpreting data. This is a formalisation of the top level of architectural description of the device. Only the subset of definitions relevant to this example will be given.

The definition of the real format will contain the specification of the number of bits in the fractional part of a floating-point number and the exponent bias:

Now the floating-point register format can be specified:

This states that a Floating_Point_Registers has three fields. Two of which, frac and exp, are positive integers and the third, sign, is either -1 or +1. The predicate states that both the exponent and fraction are 0 or that frac is between 2^{bitsinfrac−1} and 2^bitsinfrac – this ensures that the fraction is normalised.

The valuation function on a floating-point register fv establishes the link between a Floating_Point_Register and the value it ’holds’:

Two constants are used to represent the largest and smallest integers in the integer format. As the IMS T800 uses 32-bit 2s complement integers these are specified by:

4.2 The instruction specification

The instruction under consideration here is a component of the real to integer conversion instruction sequence. It checks that the value of Areg lies within integer range - if it doesn’t then the error flag must be set to indicate a conversion error.

The Z specification of this instruction is very simple:

The first predicate is a precondition to this operation. If 1vAreg is not an integer then the effect of this operation will be undefined. In this way the precise conditions for the correct execution of an operation are stated. This instruction is intended for use in a particular sequence of instructions and the previous instruction will have established this precondition.

It is easy to see that this specification satisfies the requirements for the instruction. Once this has been agreed to be ’correct’ the development process will ensure that the final implementation will also satisfy the requirements.

4.3 Refining to procedural form

A refinement of a specification can consist of either refining a data type or decomposing the procedural form. As the major data type - reals - has already been refined into its machine representation, by using Floating_Point_Register and the abstraction function Iv, the specification can be decomposed into procedural form. The specification can be easily implemented by:

Using the pre/post-condition laws in [13] this can be shown to implement the Z specification.

4.4 Refining to occam

This has produced a procedural implementation but the conditionals used in the if .. fi construct are not available in occam so they need to be refined into equivalent occam expressions.

To do this the lemmas about integer range shown below will be useful.

From lemmas 1 and 2 obtain:

The fact that MSBit ≤ x.frac is part of the invariant of Floating_Point_Register is used to eliminate the disjunct where x.exp = LargestINTExp.

Now using lemma 3 and adding an extra condition obtain:

From these obtain:

4.5 High-level occam implementation

The previous section allows the high-level occam implementation below to be derived.

Using two laws IF pri and IF or-disc:

this can be simplified to the program:

which is probably the implementation of the specification that a competent programmer would produce but the ’special’ case of MinInt is frequently omitted.

4.6 Transformations towards microcode

The previous sections have developed an occam program that correctly implements the specification. This can now be transformed into an equivalent form that corresponds to microcode assembler source. Full details of this process will not be given here.

Each step consists of transforming one aspect of the program towards the form used in the microcode machine. Ideally this occam program would be transformed into the final program. As the transformation system is still under development most of the laws that it contains are those that are ’general’ - i.e. are correct in all environments. This does not allow the required transformation to be performed in a forwards manner. Instead at each step a proposed implementation was constructed and this was then verified by transforming it back into the current ’correct’ implementation.

Refining the conditionals

The occam program given contains a three-way IF statement with the conditionals:

The structure of the program must be transformed to take account of the conditional signals available on the microcode machine - i.e. that conditionals are available to signal that the result of an ALU operation is less than 0 or that the result of an ALU subtraction is 0 etc.

This program for implementation with refined conditionals is shown below. The various laws for IF constructs in [9] enable this to be verified:

Refining the expressions

The previous section has produced conditionals that are available in the microcode machine. The next step is to take account of how the expressions producing these conditionals are evaluated. This stage involves introducing variables to represent the various buses and conditional flags. The conditional flags appear as the IF conditionals and are evaluated in terms of the results of the ALU operations before the IF statement.

This program for implementation with refined expressions is shown below: The laws for SEQ, VAR and assignment in [9] verify this step:

Introducing sequencing

The program now contains expressions and conditionals that can be formed in the microcode machine. However, the program does not define microwords. The final step is to mimic the microsequencing in the microcode machine by use of a variable as a microprogram counter and a WHILE loop containing an IF microinstruction selector. Each branch of the IF statement contains the ’code’ for one microinstruction - i.e. it can have one fractional ALU operation, one exponential ALU operation and defines the next microinstruction to execute - possibly with one or two conditionals.

The laws for WHILE and IF allow this program to be ’unwound’ back into its previous form.

4.7 Translation to microcode

The final program for low level occam implemenation from the previous transformations is:

This corresponds in an almost one-to-one manner with the source format for the microcode assembler. A pattern-matching program is used to translate the stylised occam of the above program into the source for the microcode assembler. The microcode assembler then produces the definition of the microcode ROM from this source.

4.8 Microcode assembler source

Finally the microcode can be derived:

This process has ensured that the ’program’ in the microcode ROM correctly implements the initial specification. It might seem possible to do this informally in this simple case which only produces four microwords. Other instructions contain up to ninety microwords where informal development can easily introduce subtle bugs. The ability to verify an implementation using program transformations has proved invaluable.

5 Current and future work

Work on the IMS T800 has shown how correct microcode can be derived from a high-level specification. However, this has assumed that the hardware implementing the microcode machine is correct. To produce a verified processor design it will be necessary to apply the same degree of rigour to the design of the microcode machine. This necessitates refining the specifications of microfunctions into hardware description language (HDL) implementations. The INMOS CAD system already ensures that silicon layout is equivalent to its HDL specification.

This correctness of design can be achieved by defining axioms for the behaviour of low-level modules in the HDL module library if necessary down to transistor level. Larger modules and circuits can then be specified in terms of compositions of these ’axiomatic’ modules. Then a logic tool, such as HOL [5], can be used to derive the behaviour of the design. Checking this against an original specification enables the correctness - or otherwise - of the design to be established.

6 Conclusions

Work at INMOS using the transformation system and a formal design strategy has been seen to be of benefit. The correctness of the microcode for the IMS T800 floating-point unit was established in far less time than would be needed by an ’adequate’ amount of testing. In addition, any amount of non-exhaustive testing leaves the possibility that certain erroneous operations have not been exercised. This has enabled INMOS to produce the IMS T800 well ahead of schedule with a high degree of confidence in the correctness of the microcode - this would not have been possible by other design methods.

Work is now in progress to incorporate this formal design strategy into the other levels of the design process to maintain the correctness of a complete design. It seems clear that the CAD system will need to incorporate a theorem prover and work is progressing at INMOS to ensure that this is the case.

References