Formal Design of a Class of Computers

— its high stage: abstract microprogramming^{3}

Li-Guo Wang^{1}

Department of Computer Science, University of Edinburgh, JCMB, The King’s Buildings, Room 1414, Edinburgh EH9 3JZ, Scotland, U.K. E-mail: lgw@dcs.ed.ac.uk

Michael Mendler^{2}

Department of Computer Science, Technical University of Denmark, Building 344, DK-2800 Lyngby, Denmark E-mail: mvm@id.dtu.dk

Abstract

We present a novel construction model of hardware and demonstrate how to use it in the entire process of formally designing a class of computers involving their specification, construction, and verification. In this report we focus on the high stages of the design: the refinement from the behaviour specification at machine instruction level to the abstract microprogram at the term transition level. The concept of term transition introduced in this work establishes a new generic high-level design stage which is common for computer architecture and design. Our approach is based on formal syntax and formal proof and constitutes a framework for the rigorous specification and verification of hardware synthesis systems.

1 Introduction

As formal methods are striving to be understood and accepted by industry the formalization of the design process itself — as opposed to mere post-design verification — receives more and more attention [1, 5, 15, 16, 31, 37]. In this report we discuss the formal design of a class of computers. By formal design we mean an approach based on theorem-proving and by a class of computers we mean the specification scheme of an abstract computer characterizing each computer in the class. We present a construction model of hardware which applies all the way from an abstract behaviour specification to an unknown structural implementation. It constitutes a new foundation for formal design where the traditional verification-oriented hardware model does not meet the goal. It admits finergrained design descriptions in which aspects of hardware and software may coexist, and it abstracts from the concrete mode of operation. The choice, for example, of a synchronous, asynchronous, or pipelined realization may be postponed until later design stages. Using the construction model the framework comprises a suite of specification, construction, and proof schemes to cover the complete formal design for a class of computers from the behaviour specification at machine instruction level to the structural specification at register transfer level. In this paper we discuss the first part of the design process: from the behaviour specification to the high-level abstract microprogram at term transition level. Through exact formal construction we can identify the term transition level as a new and rather natural design stage for computer design. Using term transitions we can capture the abstract and high-level structure of the computer above register-transfer level.

1The author is supported by a scholarship from Siemens AG Munich and scholarship from SERC GR/F 35890 U.K.

2The author is supported by a Human Capital and Mobility fellowship in the EuroForm network.

3This report is a slight extension of a paper presented at CHARME’95, Correct Hardware Design and Verification Methods, Frankfurt, October 2-4, 1995.

2 Construction Model of Hardware Design

In the field of formal hardware verification a variety of different ways of modelling behaviour have been introduced. The two salient variants are the functional and the relational paradigm. The former is well known from the work of W. Hunt [24] and usually adopted in verification research based on the Boyer-Moore theorem prover. The latter, on the other hand, probably is the most widely accepted and successfully used hardware model in the HOL community [20, 18, 19, 15, 26]. Though one method of specifying hardware often can be encoded in terms of the other, the relational paradigm is usually considered to be the more general one, covering the functional variant as a special case. For instance, in terms of relations we can directly capture phenomena which are not elementary in a purely functional setting such as bidirectionality, partiality, and nondeterminism. This work presents an extension of the components-as-relations, or to be more precise, the components-as-predicates paradigm. This paradigm, which we simply call the (first-order) verification model, can be characterized by three features:

1. Components are represented by predicates with the free variables as their ports.

2. Internal port connection is realized by

existential quantification.

3. Composition of components is achieved by logical conjunction.

For example, the delay and inverter circuits would be defined as

Del (i, z) ≡ ∀t. z (t + 1) = i t
Inv (z, o) ≡ ∀t. o (t + 1) = ¬(z t)

and the structure of the delay-inverter

i Del z Inv o

be described as ∃z. Del (i, z) ∧ Inv (z, o). The verification model originates from the obvious static-topological understanding of physical hardware focusing on the port connection structure of hardware and spatial structural abstraction. This is expressed for instance in [30] (p. 269):

“The type of abstraction most fundamental to hardware verification is structural abstraction – the suppression of information about a device’s internal structure.” Despite its generality a weakness of the verification model is that it is not flexible enough to support a process of formal synthesis and construction. It exhibits the spatial structure of hardware but fails to capture important other structure arising in a topdown construction of hardware. Examples of such non-spatial structure are the interface between software and hardware, microprograms, or behavioural constraints. Therefore the traditional verification model, which flattens away this extra conceptual structure, is intrinsically limited to post-hoc verification and transformation of complete hardware components [12, 13, 9, 24, 27, 17, 28, 30]. To capture the top-down construction of incomplete hardware, in particular for the construction of microprogrammed computers, more sophisticated structure is needed. One purpose of this paper is to introduce such a new and more general hardware model, the construction model. From our point of view the main aspect in the formal design process, taking a fine-grained sequence of refinement steps from an abstract behaviour specification to an eventual structural implementation, is logic rather than spatial refinement. In order to support this logical decomposition our construction model allows for extra logical communication of a component with its environment. With the model the inverter is written as

Inv (z, o) [E_{i}, E_{o}] ≡ ∀x. ∃y. E_{i} x ⇒ o y = ¬(z x) ∧ E_{o} y.

This formulation states that whenever a certain condition E_{i} is true at the start time point x then the inversion of the input will be effected by some time y, and after the execution the predicate E_{o} will be true. The predicates E_{i} and E_{o} are the logical interface to the environment by which the entry and exit of the component is controlled. We call E_{i} the entry and E_{o} the leaving predicate of the model. The difference to the verification model is the fact that it focuses on what makes up the behaviour of an inverter, viz. the equation o y = ¬(z x), rather than how this is achieved. The original absolute reference to a fixed propagation delay has been abstracted away and replaced by a generic time interval ⟨x, y⟩ demarcated only by the conditions E_{i} x and E_{o} y but otherwise undetermined. Here the predicates E_{i}, E_{o} are considered parameters, i.e. free variables, of the specification rather than concrete predicates. This results in a generic description, which can be instantiated in many ways to obtain a variety of different realizations of an inverter. For instance, we get back to the original formulation by taking E_{i} x ≡ x = t and E_{o} y ≡ y = t + 1, where t is a free variable referring to a global notion of time.

The substitution gives

∀x. ∃y. x = t ⇒ o y = ¬(z x) ∧ y = t + 1,

which is logically equivalent to the old Inv (z, o), but it makes explicit the essential mode of control implicit in the original formulation, viz. unconstrained operation with a fixed propagation delay relative to a global and absolute concept of time. Other modes of operation can be obtained by other choices of E_{i}, E_{o}. For instance, viewing the inverter function as part of a microprogram might lead us to choose E_{i} x ≡ addr x = 3 and E_{o} y ≡ addr y = 4, where addr refers to the microprogram address counter and x, y to the sequence number of the executed microinstruction. Another possibility is given by viewing the inverter as part of a synchronous circuit: we instantiate E_{i} x ≡ stab(z, x, Δ)∧clk(x, n) and E_{o} y ≡ clk(y, n) such that stab(z, x, Δ) means input z has been stable for at least a period of length Δ prior to time x, and clk(x, n) means x corresponds to the n-th clock tick. We leave it to the reader to add other instantiations, say to capture input constraints, multiple phase synchronous realizations, or asynchronous handshake. The semantics of the entry and leaving predicates is non-trivial in the sense that not all possible instantiations are permitted. In particular, it is not permitted to let the entry predicate be inconsistent, say E_{i} x ≡ 0 = 1. In this case the construction model would trivialize to the full relation which does not constrain the implementation at all. Our framework avoids these fallacies by keeping a rigid dicipline in the use of the entry and leaving predicates. Technically, the point is that in our constructive setting Inv (z, o) [E_{i}, E_{o}] does not have the same meaning as ∃E_{i}. Inv (z, o) [E_{i}, E_{o}]. To sum up, the construction model allows us to capture a wide range of possible modes of control and interaction, and — this is the crucial point — to keep the decomposition at an abstract level as long as convenient and defer instantiating to a particular realization until much later in the design process.

Let us consider a very simple example. Suppose in the process of construction we encounter the construction model

∀x. ∃y. E_{i} x ⇒ rec y =
ADD (send_{1} x, send_{2} x) ∧ E_{o} y (1)

as a sub-specification. It says that in the time interval ⟨x, y⟩, and under the start condition E_{i}, we are to implement an add function so that upon completion the condition E_{o} holds. We must achieve this for arbitrary x but are free to choose the exit time point y. To construct (1) we might naturally (e.g. by syntactic decomposition) introduce two new entry predicates E_{a} and E_{b} and three new ports i_{1}, i_{2}, and o as follows:

(∀x. ∃y. E_{i} x ⇒ i_{1} y = send_{1} x
∧ i_{2} y = send_{2} x ∧ E_{a} y)  (2)
∧ (∀x. ∃y. E_{a} x ⇒ o y =
ADD (i_{1} x, i_{2} x) ∧ E_{b} y)  (3)
∧ (∀x. ∃y. E_{b} x ⇒ rec y =
o x ∧ E_{o} y).  (4)

This way we have decomposed the original construction model (1) into a composition of three abstract subcomponents (2)–(4). These subcomponents communicate spatially via ordinary signals such as i_{1} or o but also logically via entry and leaving predicates such as E_{a}. By this extra dimension of interaction we have not only explicit a data-path but also abstract control reflected in the entry and leaving predicates. More concretely, if we condense every equation into a unique control signal to activate a hardware component effecting this equation within one unit of time, then we arrive directly at the following description of an abstract microprogram:

\begin{aligned}(∀t. E_{i} t & ⇒ & c_{s1} t ∧ c_{s2} t ∧ & E_{a} (t + 1)) \\ ∧ (∀t. E_{a} t & ⇒ & c_{a} t ∧ & E_{b} (t + 1)) \\ ∧ (∀t. E_{b} t & ⇒ & c_{r} t ∧ & E_{o} (t + 1)). \end{aligned}

From here we might further instantiate the entry predicates as statements about the state of a program counter to obtain a concrete microprogram:

(∀t. address t = 12 ⇒ c_{s1} t ∧ c_{s2} t
∧ address (t + 1) = 13) ∧
(∀t. address t = 13 ⇒ c_{a} t
∧ address (t + 1) = 14) ∧
(∀t. address t = 14 ⇒ c_{r} t
∧ address (t + 1) = 15).

The data-path, which implements the equations within (2)–(4),

Reg (c_{s1}, send_{1}, i_{1}) ∧ Reg (c_{s2}, send_{2}, i_{2}) ∧ Reg (c_{r}, o, rec) ∧ ALU (c_{a}, i_{1}, i_{2}, o),

consists of three registers and one ALU, which might be specified by

Reg (c, i, o) ≡
∀t. o (t + 1) = (c t ⇒ i t | o t)
ALU (c, i_{1}, i_{2}, o) ≡ ∀t. o (t + 1) =
(c t ⇒ ADD (i_{1} t, i_{2} t) ↓ i_{1} t),

where a ⇒ b ↓ c abbreviates the term “if a then b else c” [19]. All in all we get an implementation as seen the figure below.

microprogram

c_{s1} c_{s2}  c_{a}  c_{r}

Reg

send_{1} i_{1}

Reg

send_{2} i_{2}

ALU o

Reg

rec

The point we wish to make is that in the traditional verification model in which components may communicate only spatially via signals the refinement to the final implementation in terms of data-path and control must be done in one step. The intermediate design stage as given by (2)–(4) in which the decomposition into subcomponents has been performed already, but the particular mode of control has neither as yet been fixed nor localized in a separate hardware component, cannot be represented naturally and directly. In other words, the construction model of hardware has the potential for a finer-grained design, i.e. for breaking the refinement process into smaller pieces. Note again that in the description (2)–(4) different instantiations of the entry and leaving predicates would give rise to different realizations of control such as by synchronous clock or asynchronous handshake. Also, a pipelined operation is possible. If, in the abstract microprogram above, we specialize E_{i} such that ∀t. E_{i}(t) we get a pipelined implementation in which the registers and the ALU process three different values of data at every point in time; we obtain the behaviour ∀t. rec (t + 3) = ADD(i_{1} (t), i_{2} (t)). The concrete microprogram chosen above, in contrast, realizes only a single thread of control: the microinstruction address address (t) is unique and cannot be 12, 13, and 14 at the same time. This variability of instantiating the entry and leaving predicates is very useful in practice. For instance, to simulate the functional behaviour one can take a short-cut via a direct instantiation to a synchronous sequential program. In parallel, one may proceed with the actual design path towards a more sophisticated asynchronous pipelined hardware realization, along a number of further refinement steps. From this viewpoint the entry and leaving predicates are a very flexible means to change or adapt the semantics of a design to a particular mode of operation, and thus go beyond the capabilities of traditional Hoarestyle pre/post conditions or Lamport-style assumption/commitment forms. In fact, we conjecture that both can be incorporated in terms of entry and leaving predicates. However, this analysis is outside the scope of the paper. To finish off this section let us sum up our definitions formally. Extending what has been introduced above, the refinements will use a construction model in which the leaving predicate is generalized to a leaving predicate structure. This allows us to express non-linear control structure in terms of entry and leaving predicates. With this extension the abstract syntax is as given in Fig. 1. In the following we will call any instance of the scheme in Fig. 1 a construction model or simply a model. The abstract syntax is schematic in the sense that the syntactic classes mp, E, P are not further specified. They are not of interest at this stage and will only be filled up later with more structure when this is necessary to support a particular refinement step. Also, to keep matters simple, we will focus on the formal, read: syntactic, aspects of our constructions and leave aside semantical issues and correctness arguments. It deserves mention, however, that all refinements and transformations presented are based on sound logical arguments. As far as ‘meaning’ is concerned we content ourselves with a translation into an ambient (higher-order) predicate logic, which is assumed, at an intuitive level at least, to be understood throughout. In this vein, the semantics of the construction model is ‘defined’ by the following inductive translation:

(mp [E, lps])^{∗} = ∀x.∃y. E x ⇒ mp ∧ lps^{∗}
(P (lps_{1}, lps_{2}))^{∗} = P ⇒ lps_{1}^{∗} ↓ lps_{2}^{∗}
E^{∗} = E y.

Construction Model Syntactic Class:

cm ::= mp [E, lps] cm : construction model lps ::= E lps : leaving predicate structure

| P (lps, lps) mp : model predicate E : (entry or leaving) predicate P : Boolean term

Figure 1: Abstract Syntax of the Construction Model

To give an example we may write (pc y = pc x) [E_{2}, b_{1} x (E_{3}, b_{2} x (E_{4}, E_{5}))] to stand for ∀x.∃y. E_{2} x ⇒ pc y = pc x ∧ (b_{1} x ⇒ E_{3} y ↓ (b_{2} x ⇒ E_{4} y ↓ E_{5} y)). Note, this syntactic translation hardwires the special rôle of the time variables x, y as the generic start and end time points of a construction model: formally speaking, the operator [E, E] is a binding operator for x and y which are assumed to be distinguished throughout this paper. For this to work, of course, we must make sure x and y are used consistently according to this convention. This is but one of a number of other additional well-formedness conditions on our specifications which are not contained in the abstract grammar schemes. In the following all specification schemes are to be understood modulo some tacit well-formedness conditions, which for simplicity will not be mentioned, however.

The construction model mp [E_{i}, lps] being introduced the refinement process may be viewed as a repeated process of protruding particular structure for the body mp of the model which then is broken down along this structure into smaller pieces mp_{1}[E_{1i}, lps_{1o}] ∧ ⋯ ∧ mp_{n}[E_{ni}, lps_{no}] until the mp_{i} can be considered implementable. The main means of decomposition — as explored in this paper — is to break up terms syntactically into sub-terms and to introduce new entry predicates and new ports. For convenience we adopt the following assumption: Assumption [existential variables]

All new entry predicates and new signals (ports) introduced in the construction process are existential variables. With this assumption we may drop the existential quantifier ∃z. hiding an internal signal in a composite circuit and simply turn z into an existential variable. The same is done with internal entry and leaving predicates. Existential variables are supported in some theorem provers, like Lambda [14] (‘flexible’ variables) or Isabelle [33] (‘meta’ variables) and have been shown to be of great advantage in practice. In particular the work based on Lambda (e.g. [14]) makes heavy use of existential variables to support formal hardware synthesis.

3 Machine Instruction Level

In this section a generic form of behaviour specification for a class of computers at machine instruction level is defined. At this level the semantics of machine instructions is given in terms of a global state transition. To capture a class of computers we use abstract syntax for the general structure of this state transition. This abstract grammar is given in Fig. 2. The syntax is abstract because its terminal symbols are uninterpreted, albeit the relationship of the symbols is clearly defined. The syntax is a scheme for a class of computers because all concrete computers whose specifications are obtained as instantiations are treated uniformly along with the construction and refinement of the scheme. In other words, we are aiming at a higherorder refinement: we are not interested in the refinement of a particular instance of a scheme but in the refinement of the scheme itself. In the outermost layer the behaviour specification scheme of Fig. 2 describes a computer as a global state transition that is to be maintained for all points in time:

(os = iss) [E, E]. Here os is the global output state at time point y and iss the input state structure expressing the result of executing a machine cycle in the flexible time interval ⟨x, y⟩. Typically, the entry and leaving predicates will be identical, which closes the global loop of instruction execution. The output state is assumed to be composed from a fixed number of state signals sg_{1}, …, sg_{n}, viz.

os = (sg_{1} y, …, sg_{n} y). The input state structure iss is a term over a number of input states

is = (sis_{1}, …, sis_{n}), each of which is assumed to have the same number of sub-input states sis_{i} as os has components. These input states represent individual machine instructions where sis_{i} is the function that computes the i-th output state. A sub-input state sis is a term tm built from constants c, variables v, the values of signals sg at time point x, and by applying functions to terms. The input states is (or machine instructions) are organized to form the input state structure iss by applying the let in “let A in iss” and the conditional “P ⇒ iss ↓ iss”. This models the control part of the machine cycle in which the right machine instruction is selected and set up for execution. In “let A in iss” the binding A ::= v = tm declares a simple variable v to replace a term tm used in the input states of iss. The condition structure “P ⇒ iss_{1} ↓ iss_{2}” chooses for iss_{1} if P is true and for iss_{2} if it is false.

As can be seen the specification scheme is a refinement of our general construction model mp [E, E] which protrudes intricate structure for the model predicate mp, and also specializes the leaving predicate structure. Note, that the primitive components Inv, Del, Reg, ALU mentioned before are special if not trivial instances of the specification scheme 1. They are what we will call term transitions consisting of a single equation of the form sos = sis. The goal of our constructions in the next section essentially is to break down an arbitrary instance of scheme 1 into a set of (parallel and sequential) term transitions. But before we get into the details let us make things definite by way of an example.

Example [Gordon’s computer]

Gordon’s computer is a simple generalpurpose computer introduced as a nontrivial exercise in the formal specification and verification of hardware [17, 28]. The top-level specification of the computer at machine instruction level is what an assembler language programmer would need to write a program. At the top level Gordon’s computer has a memory and two registers, viz. the program counter PC and the accumulator ACC. The specification includes two parts: the front panel operation and the machine instructions.

The front panel of the computer has a stop button, a four-position knob, and data switches. When the computer is running pushing the button interrupts the execution of the program and the computer idles. The effect of pushing the button when the computer is idling is determined by the position of the knob according to the following table:

Specification Scheme 1: Syntactic Class: spsc_{1} ::= os = iss [E, E] spsc_{1} : specification scheme1 os ::= (sos, ⋯, sos) os : output state sos ::= sg y sos : sub-output state iss ::= is iss : input state structure

| let A in iss

| P ⇒ iss ↓ iss

is ::= (sis, ⋯, sis) is : input state sis ::= tm sis : sub-input state A ::= v = tm A : binding P ::= p (tm, ⋯, tm) P : Boolean term

| ¬P

| P ∘ P

tm ::= c tm : term | v v : variable | sg x sg : state signal

| f (tm, ⋯, tm)  f  : function
∘  ::= ∧  ∘  : binary relation

| ∨ | ⇒ | ⇔

E : (entry or leaving) predicate x, y : distinguished time variables p : predicate c : constant

Figure 2: Specification Scheme 1: Machine Instruction Level

Knob position Button action
0  Load PC
1  Load ACC
2  Store ACC at PC
3  Start execution at PC

The computer has eight machine instructions HALT, JMP, JZR, ADD, SUB, LOAD, STORE and SKIP, with opcode 0-7, respectively:

Code Instruction Effect
0 HALT  Stop execution
1 JMP L  Jump to addr. L
2 JZR L  Jump to addr. L

if ACC = 0

3 ADD L  Add contents of

addr. L to ACC

4 SUB L  Subtract contents of

addr. L from ACC

5 LD L  Load contents of

addr. L into ACC

6 ST L  Store contents of

ACC in addr. L

7 SKIP  Skip to next instr.

This description for Gordon’s computer may be rendered formal by the specification given in Fig. 3, following [28] closely. The meaning of the functions Val_{2}, Cut_{16 13}, Store_{13}, Opcode, Fetch_{13} is exactly as in [28]. T and F are the Boolean constants for true and false. The specification easily is seen to be an instance of our generic scheme 1.

4 Formal Construction

A step of formal construction is a transformation from one specification to another and the main aspect of this transformation is the decomposition of an abstract specification into less abstract sub-specifications. The process is repeated until concrete and minimal pieces of specification are met that are considered executable or directly implementable. This (well-known) idea can be lifted to specification schemes, so that the formal construction specifies and verifies the design process itself rather than a particular piece of hardware. In this section we discuss the high stages of the formal construction, the refinement from the machine instruction level to the term transition level. This involves a number of smaller refinement steps via intermediate levels of description, in which a number of different design decisions are introduced and higher-level structures are realized in terms of lower-level structures. Instead of going through all of these steps we will focus on only one intermediate level, which is sufficient to illustrate the basic idea. The complete treatment can be found in [40]. Starting from the specification scheme 1 (Fig. 2), among other less central ones, the following four main refinement steps are to be taken:

(1) Setting State Transition: The global state transition os = iss is distributed into local state transitions, which would correspond to single machine instructions.

Computer(button, knob, switches, memory,

pc, acc, idle) ≡

((memory y, pc y, acc y, idle y) = (idle x ⇒ Idle ↓ Busy)) [E, E]

Idle ˆ=

button x ⇒
((Val_{2} (knob x) = 0) ⇒

(memory x, Cut_{16 13} (switches x), acc x, T) ↓

(Val_{2} (knob x) = 1) ⇒

(memory x, pc x, switches x, T) ↓

(Val_{2} (knob x) = 2) ⇒

(Store_{13} (pc x) (acc x) (memory x),

pc x, acc x, T) ↓ (memory x, pc x, acc x, F)) ↓ (memory x, pc x, acc x, T)

Busy ˆ=

button x ⇒

(memory x, pc x, acc x, T) ↓

let op =

Val_{3} (Opcode (Fetch_{13} (memory x) (pc x)))

in let addr =

Cut_{16 13} (Fetch_{13} (memory x) (pc x)) in

( (op = 0) ⇒

(memory x, pc x, acc x, T) ↓

(op = 1) ⇒

(memory x, addr, acc x, F) ↓

(op = 2) ⇒
((Val_{16} (acc x) = 0) ⇒

(memory x, addr, acc x, F) ↓

(memory x, Inc_{13} (pc x), acc x, F)) ↓

(op = 3) ⇒

(memory x, Inc_{13} (pc x),

Add_{16} (acc x) (Fetch_{13} (memory x) addr), F) ↓

(op = 4) ⇒

(memory x, Inc_{13} (pc x),

Sub_{16} (acc x) (Fetch_{13} (memory x) addr), F) ↓

(op = 5) ⇒

(memory x, Inc_{13} (pc x),

Fetch_{13} (memory x) addr, F) ↓

(op = 6) ⇒

(Store_{13} addr (acc x) (memory x),

Inc_{13} (pc x), acc x, F) ↓

(memory x, Inc_{13} (pc x), acc x, F))

Figure 3: Specification of Gordon’s Computer at Machine Instruction Level Formally, the global equation os = iss is pushed into the input state structure iss to get local equations os = is, and then distributed to individual state components to get a conjunction of sub-state transitions sos = sis. The conjunction we call a substate transition set. For example, in Gordon’s computer the global state equation

(memory y, pc y, acc y, idle y) = idle x ⇒ ( button x ⇒ ( ⋯ ⇒ ⋯ (memory x, pc x, switches x, T)

↓ ⋯) ↓ ⋯) ↓ Busy

is translated into

idle x ⇒ ( button x ⇒ ( ⋯ ⇒ ⋯ (memory y = memory x ∧ pc y = pc x ∧ acc y = switches x ∧ idle y = T)

↓ ⋯) ↓ ⋯) ↓ Busy

where the resulting conjunction

memory y = memory x ∧ ⋯ ∧ idle y = T

is a sub-state transition set.

(2) Rearranging let in structure: The let in binding is our means to break up terms into pieces, i.e. undo syntactic substitution. In our later refinements the binding “A = (v = tm_{1})” in “let A in sos = tm_{2}” is going to be realized by a separate process which sequentially precedes the one generated for “sos = tm_{2}”, while the functionally equivalent “sos = tm_{2}[tm_{1}/v]” results in a single process. Thus, by rearranging the let ins we can factor out separate sub-computations and control the granularity of primitive computation steps. For example, in Gordon’s computer we may introduce a new let in such as

let v = Fetch_{13} (memory x) (pc x) in to replace the two let in constructs

let op = Val_{3} (Opcode (Fetch_{13} ⋯)) in

let addr = Cut_{16 13} (Fetch_{13} ⋯) in and substitute Val_{3} (Opcode v) to replace op and Cut_{16 13} v to replace addr. This is sensible because we consider Val_{3}, Opcode, and Cut_{16 13} as directly implementable, whence no separate computation step is necessary.

(3) Identifying Common Blocks: After setting the state transitions we identify subsets of sub-state transitions which are common to more than one sub-state transition set. These common blocks can be factored out and realized by separate processes. This step is the equivalent of rearranging let in structures at the level of sub-state transitions. To give an example, in Gordon’s computer the sub-state transition sst_{5} = (pc y = Inc_{13} (pc x) ∧ idle y = F) is shared by a number of machine instructions such as the code for op = 3, 4, 5, 7, and thus only needs to be implemented once.

(4) Selection for Parallel and Sequential Execution: In general, the term/subterm relationship does not prejudice the actual execution ordering. In a nested conditional P_{1} ⇒ (P_{2} ⇒ iss_{1} ↓ iss_{2}) ↓ iss_{3} for instance, the evaluation of P_{1} and P_{2} can be either sequential or parallel. In one case both P_{1} and P_{2} are executed within the same (flexible) time interval, in the other in consecutive intervals. There are many possible ways of distinguishing these cases syntactically. We have chosen to introduce curly brackets { and } for delimiting the borders of parallel execution. Then, the parallel version of the conditional would become {P_{1} ⇒ (P_{2} ⇒ {iss_{1}} ↓ {iss_{2}}) ↓ {iss_{3}}}. Similarly we use brackets to select the parallel or sequential execution of nested let in constructs. In let A_{1} in let A_{2} in iss the two bindings A_{1} and A_{2} can be executed in parallel whenever they do not depend on each other. In such a case we would write {let A_{1} in let A_{2} in {iss}}

Computer(button, knob, switches, memory,

pc, acc, idle) ≡

(idle x ⇒ {Idle} ↓ {Busy}) [E, E]

Idle ˆ= button x ⇒ { (Val_{2} (knob x) = 0) ⇒ {st_{0}} ↓

(Val_{2} (knob x) = 1) ⇒ {st_{1}} ↓ (Val_{2} (knob x) = 2) ⇒ {st_{2}} ↓ {st_{3}}} ↓

{st_{4}}

Busy ˆ= button x ⇒ {st_{4}} ↓ {let v = Fetch_{13} (memory x) (pc x) in { (Val_{3} (Opcode v) = 0) ⇒ {st_{4}} ↓

(Val_{3} (Opcode v) = 1) ⇒ {st_{5}} ↓ (Val_{3} (Opcode v) = 2) ⇒ {(Val_{16} (acc x) = 0) ⇒ {st_{5}} ↓

{sst_{0} ∧ [sst_{5}]}}

(Val_{3} (Opcode v) = 3) ⇒ {sst_{1} ∧ [sst_{5}]} ↓ (Val_{3} (Opcode v) = 4) ⇒ {sst_{2} ∧ [sst_{5}]} ↓ (Val_{3} (Opcode v) = 5) ⇒ {sst_{3} ∧ [sst_{5}]} ↓ (Val_{3} (Opcode v) = 6) ⇒ {sst_{4} ∧ [sst_{5}]} ↓ {sst_{0} ∧ [sst_{5}]}}}

Figure 4: Gordon’s Computer at the Intermediate Level

while the strictly sequential reading is written {let A_{1} in {let A_{2} in {iss}}}. A similar selection is introduced into the specification at the level of sub-state transition sets, with the help of square brackets: while ssts_{1} ∧ ssts_{2} means that the sub-state transition sets ssts_{1} and ssts_{2} are to executed in parallel, ssts_{1} ∧ [ssts_{2}] separates them to be executed sequentially (in left-to-right order). The state transitions within each ssts_{i} are executed in parallel, however. For example, in Gordon’s computer the condition predicates Val_{2} (knob x) = i for i = 0, …, 3 may be selected for parallel execution because they are mutually disjoint and easily implemented by a simple branch structure. The same is true for the predicates Val_{3} (Opcode (⋯)) = i where i = 0, …, 7. A complete specification of Gordon’s computer at the intermediate level is given in Fig. 4. It is the result of applying the refinements (1)–(4) to the specification in Fig. 3. The sub-state transition sets arising in Fig. 4 are abbreviated as follows:

st_{0} ˆ= ( memory y = memory x ∧

pc y = Cut_{16 13} (switches x) ∧ acc y = acc x ∧ idle y = T)

st_{1} ˆ= ( memory y = memory x ∧

pc y = pc x ∧ acc y = switches x ∧ idle y = T)

st_{2} ˆ= ( memory y = Store_{13} (pc x) (acc x) (memory x) ∧ pc y = pc x ∧ acc y = acc x ∧ idle y = T)

st_{3} ˆ= ( memory y = memory x ∧

pc y = pc x ∧ acc y = acc x ∧ idle y = F)

st_{4} ˆ= ( memory y = memory x ∧

pc y = pc x ∧ acc y = acc x ∧ idle y = T)

st_{5} ˆ= ( memory y = memory x ∧

pc y = Cut_{16 13} (v x) ∧ acc y = acc x ∧ idle y = F)

sst_{0} ˆ= ( memory y = memory x ∧

acc y = acc x)

sst_{1} ˆ= ( memory y = memory x ∧

acc y = Add_{16} (acc x)

(Fetch_{13} (memory x)

(Cut_{16 13} v)))

sst_{2} ˆ= ( memory y = memory x ∧

acc y = Sub_{16} (acc x)

(Fetch_{13} (memory x)

(Cut_{16 13} v)))

sst_{3} ˆ= ( memory y = memory x ∧

acc y = Fetch_{13} (memory x)

(Cut_{16 13} v))

sst_{4} ˆ= ( memory y = Store_{13} (Cut_{16 13} v) (acc x)

(memory x) ∧

acc y = acc x)

sst_{5} ˆ= ( pc y = Inc_{13} (pc x) ∧ idle y = F).

In [40] the refinement steps (1)-(4) discussed above have been formalized rigorously in Specification Scheme 2: Syntactic Class:

spsc2 ::= sts [E, E] spsc2 : specification scheme2 sts ::= st sts : state transition structure

| let A in ls | P ⇒ cs ↓ cs

ls ::= let A in ls ls : let in structure

| {sts}

cs ::= P ⇒ cs ↓ cs cs : condition structure

| {sts}

st ::= st ∧ [ssts] st : state transition | ssts | [ssts]

ssts ::= sst ssts: sub-state transition set

| sst ∧ ssts

sst ::= sos = sis sst : sub-state transition

Figure 5: Specification Scheme 2: Intermediate Level

terms of transformations on specification schemes and their correctness has been verified. Obviously, these refinements are nondeterministic, in general, and need a good deal of user-guidance for the appropriate selections and transformations. To account for this the constructions defined in [40] provide a maximum-degree design-freedom operational framework in which dedicated algorithms and heuristics can be accommodated as special execution strategies. As mentioned before, the detailed treatment of these construction steps is outside the scope of this paper. Here we only give the abstract syntax of the resulting intermediate specification scheme, see Fig. 5, and focus on the last refinement, from this intermediate level to the term transition level, in the next section.

5 Term Transition Level

At the term transition level a design spsc_{3} is broken up into a conjunction of construction models ttm_{1} ∧ ⋯ ∧ ttm_{n}, in which the ttm_{i} are very simple cases of construction models:

ttm_{i} = (s_{i1} y = tm_{i1} ∧ ⋯

∧ s_{ik_{i}} y = tm_{ik_{i}}) [E_{ii}, lps_{io}]

The corresponding abstract syntax scheme 3 is given in Fig. 6. The significance of specification scheme 3 is that it embodies a novel high-level design stage, the term transition level, which is obtained by exact formal construction. This, so we believe, establishes a rather natural and generic level of abstraction between the machine instruction level above (in other words: specification scheme 1) and the function unit and connection level (in other words: register transfer level) below. The term transition level can be viewed as a generalization of the computational model of Unity [8] or Synchronized Transitions [34]. A term transition model ttm (cf. Fig. 6) in our case corresponds to a basic transition, i.e. a multi-assignment, in Unity or Synchronized Transitions. A set ttms of term transition models, then, corresponds to a basic Unity or Synchronized Transitions program. However, whereas in these languages all control is flattened away and effected implicitly through state changes, in our model a rather generic form of control structure is still explicit through the entry and leaving predicates.

We are now going to formalize the construction process that leads from the intermediate level to the term transition level as a transformation Ψ of Prolog style [11] from specification scheme 2 to specification scheme 3. The construction, a simplified variant of the one from [40], is shown in Fig. 7. A few explanations will be helpful to understand Ψ. A spsc2 is always of the form sts [E_{i}, E_{o}] where the state transition structure sts is one of three possibilities, dealt with by Ψ in the equations 4.1, 4.2 and 4.3: if sts is a state transition st it is passed on to the construction function Ψ_{s} in 4.1; if it is a let in structure then 4.2 composes the result as the conjunction of two parts determined by the sub-constructions Ψ_{l1} and Ψ_{l2}, respectively; if it is a condition structure then equation 4.3 builds on the two subconstructions Ψ_{p1} and Ψ_{p2}. In this way the construction proceeds further by induction on the structure of spcs2. The construction is deterministic except for the generation of variables and the choice of their names. In 4.6 and 4.8 new (existential) signal variables s_{v}, and in 4.2, 4.4, 4.11, 4.13 new (existential) entry and leaving predicate variables are introduced. The choice of the predicate variable E_{m} in 4.2, 4.4 is arbitrary except that it must be fresh, i.e. not occur already anywhere else in the term (Since they are existential they always can be identified later if necessary). The same holds for variable s_{v} in 4.6 and 4.8. The choice of s_{v}, however, must be functional, i.e. be uniquely determined by variable v. Similarly, the choice of E_{sts} in 4.11 and 4.13 must be functional, i.e. (in some way) uniquely depend on the subterm sts.

Another remark concerns 4.9: The righthand side sts L denotes the (meta-level) application of the substitution L to term sts. The substitution L is initiated as the empty list in 4.2 and built up inductively in rule 4.8. The superscripts of ssts^{i}, st^{o}, sts^{i} (4.4, 4.7) are meta-level operations which compute statements about the protection of input and output signals:

Definition [Input and output signal protection] For a syntactic construct S the input protection is S^{i} ˆ= (r_{1} y = r_{1} x) ∧ ⋯ ∧ (r_{n} y = r_{n} x), where r_{i} (1 ≤ i ≤ n) are all the input signals in S. Similarly, S^{o} ˆ= (s_{1} y = s_{1} x) ∧ ⋯ ∧ (s_{m} y = s_{m} x), where s_{i} (1 ≤ i ≤ m) are all the output signals, is the output protection for S. In the special case where S does not contain any input or output signals we take the boolean constant T. □

The specification of Gordon’s computer at the term transition level is shown in Fig. 8. It is an instance of specification scheme 3 and formally derived by the refinements discussed. It can be obtained by applying Ψ to the specification in Fig. 4 at intermediate level (we also unify appropriate entry and leaving predicates and remove duplicate conjuncts).

From the derived specification of Gordon’s computer at term transition level we get a clear picture about how the term transition specification describes a high-level abstract computer architecture. At this level one or a group of term transitions, such as st_{2}, is taken as a ‘primitive’ component whose internal structure is left to further construction. Scheme 3 reveals the logical dependency between the term transitions, which may in fact be viewed as an abstract microprogram. A primitive component corresponds to a linear microprogram and what Specification Scheme 3: Syntactic Class: spsc_{3} ::= ttms spsc_{3} : specification scheme 3 ttms ::= ttm ttms : term transition model set

| ttm ∧ ttms

ttm ::= tts [E_{i}, lps] ttm : term transition model tts ::= tt tts : term transition set

| tt ∧ tts

tt ::= s y = tm tt : term transition tm : term s : signal lps : leaving predicate structure

Figure 6: Specification Scheme 3: Term Transition Level

Construction: 4.1 Ψ (st [E_{i}, E_{o}]) ˆ= Ψ_{s} (((T) ∧ st) [E_{i}, E_{o}]) 4.2 Ψ ((let A in ls) [E_{i}, E_{o}]) ˆ=

(Ψ_{l1} (let A in ls)) [E_{i}, E_{m}] ∧ Ψ ((Ψ_{l2} (let A in ls, [ ])) [E_{m}, E_{o}])

4.3 Ψ ((P ⇒ cs_{1} ↓ cs_{2}) [E_{i}, E_{o}]) ˆ= tts [E_{i}, Ψ_{p1} (P ⇒ cs_{1} ↓ cs_{2}, tts)] ∧ Ψ_{p2} (P ⇒ cs_{1} ↓ cs_{2}, E_{o})

4.4 Ψ_{s} (((K) ∧ st ∧ [ssts]) [E_{i}, E_{o}]) ˆ=

Ψ_{s} (((ssts^{i} ∧ K) ∧ st) [E_{i}, E_{m}]) ∧ (st^{o} ∧ K ∧ ssts) [E_{m}, E_{o}]

4.5 Ψ_{s} (((K) ∧ γ) [E_{i}, E_{o}]) ˆ= (K ∧ γ′) [E_{i}, E_{o}] where γ′ = ssts if γ = [ssts] and γ′ = γ otherwise

4.6 Ψ_{l1} (let v = tm in ls) ˆ= s_{v} y = tm ∧ Ψ_{l1}(ls) 4.7 Ψ_{l1} ({sts}) ˆ= sts^{i} 4.8 Ψ_{l2} (let v = tm in ls, L) ˆ= Ψ_{l2} (ls, [s_{v} x/v] :: L) 4.9 Ψ_{l2} ({sts}, L) ˆ= sts L

4.10 Ψ_{p1} (P ⇒ cs_{1} ↓ cs_{2}, tts_{1} ∧ tts_{2}) ˆ= P (Ψ_{p1} (cs_{1,} tts_{1}), Ψ_{p1} (cs_{2}, tts_{2})) 4.11 Ψ_{p1} ({sts}, sts^{i}) ˆ= E_{sts} 4.12 Ψ_{p2} (P ⇒ cs_{1} ↓ cs_{2}, E_{o}) ˆ= Ψ_{p2} (cs_{1}, E_{o}) ∧ Ψ_{p2} (cs_{2}, E_{o}) 4.13 Ψ_{p2} ({sts}, E_{o}) ˆ= Ψ (sts [E_{sts}, E_{o}])

Figure 7: Formal Construction of the Refinement

the scheme 3 describes is the connection relation of these linear microprograms. The abstract flowchart for Gordon’s computer is seen in Fig. 9, where for conciseness we omit the obvious signal protections. Note that since every ‘primitive’ term transition set tts is again an instance of scheme 1 the whole refinement process from scheme 1 to scheme 3 can be reiterated locally for tts if this appears appropriate. This means we can break

Computer(button, knob, switches, memory,

pc, acc, idle) ≡

kss_{0} [E, (idle x) (E_{1}, E_{2})] ∧ kss_{1} [E_{1}, (button x) (E_{3}, E_{4})] ∧ kss_{2} [E_{2}, (button x) (E_{4}, E_{5})] ∧ kss_{3} [E_{3}, (Val_{2} (knob x) = 0)

(E_{6}, (Val_{2} (knob x) = 1)

(E_{7}, (Val_{2} (knob x) = 2)

(E_{8}, E_{9})))] ∧

(s_{v} y = Fetch_{13} (memory x) (pc x) ∧

kss_{4}) [E_{5}, E_{10}] ∧ kss_{5} [E_{10}, (Val_{3} (Opcode (s_{v} x)) = 0) (E_{4}, (Val_{3} (Opcode (s_{v} x)) = 1) (E_{11}, (Val_{3} (Opcode (s_{v} x)) = 2) (E_{12}, (Val_{3} (Opcode (s_{v} x)) = 3) (E_{13}, (Val_{3} (Opcode (s_{v} x)) = 4) (E_{14}, (Val_{3} (Opcode (s_{v} x)) = 5) (E_{15}, (Val_{3} (Opcode (s_{v} x)) = 6) (E_{16}, E_{17})))))))] ∧

kss_{5} [E_{12}, (Val_{16} (acc x) = 0) (E_{11}, E_{18})] ∧ st_{0} [E_{6}, E] ∧ st_{1} [E_{7}, E] ∧ st_{2} [E_{8}, E] ∧ st_{3} [E_{9}, E] ∧ st_{4} [E_{4}, E] ∧ st_{5} [E_{11}, E] ∧ (sst_{1} ∧ kss_{6}) [E_{13}, E_{19}] ∧ (sst_{2} ∧ kss_{6}) [E_{14}, E_{19}] ∧ (sst_{3} ∧ kss_{6}) [E_{15}, E_{19}] ∧ (sst_{4} ∧ kss_{6}) [E_{16}, E_{19}] ∧ (sst_{0} ∧ kss_{6}) [E_{17}, E_{19}] ∧ (sst_{0} ∧ kss_{6}) [E_{18}, E_{19}] ∧ (sst_{5} ∧ kss_{7}) [E_{19}, E]

kss_{0} ˆ= button y = button x ∧ kss_{1} kss_{1} ˆ= knob y = knob x ∧ kss_{3} kss_{2} ˆ= kss_{4} kss_{3} ˆ= switches y = switches x ∧ kss_{4} kss_{4} ˆ= kss_{6} ∧ kss_{7} kss_{5} ˆ= s_{v} y = s_{v} x ∧ kss_{4} kss_{6} ˆ= pc y = pc x kss_{7} ˆ= memory y = memory x ∧

acc y = acc x

Figure 8: Gordon’s Computer Refined to Term Transition Level

up the terms by introducing and rearranging let ins, identify common blocks, and select for parallel and sequential execution of subterms. It is worthwhile to recall that although we have refined the computer to a microprogram level it is abstract in that it still has a large degree of design freedom. Depending on how we decide to interpret (or instantiate) the entry and leaving predicates we can get implementations quite different from a microprogrammed computer such as an abstract synchronous or asynchronous circuit (cf. Sec. 2).

In [40] a complete sequence of refinement steps has been worked out along similar lines, which from the microinstruction level leads all the way down to a concrete implementation at register-transfer level involving 10 major levels of specification schemes together with 9 construction steps. We have presented only one of these steps in this paper. All of these construction steps are rigorously defined and formally verified. If Ψ_{n} is a (nondeterministic) construction from a scheme S_{n} to a scheme S_{n+1}, then it is verified that for every instance S_{n} of scheme S_{n} the construction (guided by external choices) will produce a well-formed instance S_{n+1} of scheme S_{n+1} (= syntactic correctness and completeness), and further it is verified that ⊢ S_{n+1} ⇒ S_{n} (= semantical correctness). The framework has been applied to construct several different versions of Gordon’s computer.

6 Conclusion

We have presented a framework for the formal design of a class of microprogrammed computers based on the formal refinement of abstract specification schemes. We used Gordon’s computer to illustrate our ideas. We believe that this approach offers a feasible path towards the rigorous specification and verification of hardware synthesis systems, which still remains a major challenge [2, 3, 6, 7, 23, 21, 22, 25, 37, 38, 41]. Two technical contributions are made: (1) We introduce a novel construction model

[figure: idle?; button?; button?; knob?; Fetch; st_{0}; st_{1}; st_{2}; st_{3}; opcode?; st_{4}; st_{5}; accu?; sst_{1}; sst_{2}; sst_{3}; sst_{4}; sst_{0}; sst_{0}; sst_{5}; 0; 1; 3; +; −; +; −; +; −; 0; 1; 2; 3; 4; 5; 6; 7; = 0; ≠ 0; E; E_{1}; E_{2}; E_{3}; E_{5}; E_{6}; E_{7}; E_{8}; E_{9}; E_{10}; E_{4}; E_{11}; E_{12}; E_{13}; E_{14}; E_{15}; E_{16}; E_{17}; E_{18}; E_{19}]

Figure 9: Flowchart of Gordon’s Computer at Term Transition Level

of hardware by which the synthesis process can be split into smaller refinement steps compared to the traditional components-as-predicates verification model. (2) With the term transition level our formal construction establishes a new and natural abstraction level of computer architecture, conveniently between microinstruction and registertransfer level.

Our basic methodology stresses the importance of abstract syntax to describe the generic structure of a class of computers. At a more general level the difference between construction (qua abstract syntax schemes) and verification (qua logic formulas) [41] is less important. What matters is to reveal the fundamental structure of our research objects and their essential relationships.

Further work will be in two directions. We are developing a semi-automatic computer design system which can design a registertransfer level microprocessor from a specification at machine instruction level. The user interaction consists in the selections for highlevel allocation and scheduling. Other work aims at the theoretical foundations of our framework, in particular concerning the algebraic and logical properties of the construction model.

Acknowledgements Li-Guo Wang is indebted to Mike Fourman for his encouragement and stimulating supervision of the author’s Ph.D. research on which this work is built. We would like to thank Kees Goossens for his comments on a draft of this paper. Thanks are also due to Rocco De Nicola for inviting Michael Mendler to the University of Rome, La Sapienza, where a part of this work was carried out.

References

[1] Simon Bainbridge, Albert Camilleri and Roger Fleming, Theorem Proving as an Industrial Tool for System Level Design. In [36], pp. 253-276.

[2] David A. Basin, Geoffrey M. Brown, and Miriam E. Leeser, Formally verified synthesis of combinational CMOS circuits. In L. J. M. Claesen, editor, Formal VLSI Specification and Synthesis, page 197-206, North-Holland, 1990.

[3] D. A. Basin, Extracting Circuits from Constructive Proofs. In 1991 International Workshop on Formal Verification in VLSI Design. ACM IFIP WG 10.2, Jan. 1991.

[4] G. Birtwistle and P. Subrahmanyam, eds., VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, Boston, 1988.

[5] J. Bormann, H. Nusser-Wehlan, and G. Venzl, Formal Design in an Industrial Research Laboratory: Lessons and Perspectives. In J. Staunstrup and R. Sharp, eds., Second Workshop on Designing Correct Circuits, Lynbgy, Denmark, Jan. 1992 WG10.2, WG 10.5.

[6] D. Borrione, H. Collavizza and C. Le Faou, μSPEED: A Framework for Specifying and Verifying Microprocessors. In Int. Workshop on Formal Methods in VLSI Design, 9-11 Jan. 1991, Miami, Springer-Verlag.

[7] B. Bose and S. D. Johnson, DDD-FM9001: Derivation of a Verified Microprocessor. In [32].

[8] K. M. Chandy and J. Mishra, Parallel Program Design. A Foundation. Addison Wesley, 1988.

[9] J. Chazarain and H. Collavizza, Combining Symbolic Evaluation and Object Oriented Approach for Verifying Processor-like Architectures at the RT-level. In [32], pp. 109 - 121.

[10] L. Claesen, editor, IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 1+2, Elsevier Science Publishers, B.V. North-Holland, Amsterdam, 1989.

[11] W. F. Clocksin and C. S. Mellish, Programming in Prolog, third, revised and extended edition, Springer-Verlag, 1987.

[12] Avra Cohn, A Proof of Correctness of the Viper Microprocessor: First Level. In [4], pp. 27-71.

[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, 1989, pp.1-91.

[14] M. P. Fourman, R. L. Harris, Lambda-Logic and Mathematics Behind Design Automation, 26th ACD/IEEE Design Automation Conference, 1988.

[15] M. P. Fourman, Formal System Design. In [35], pp 191-236.

[16] Gopalakrishnan, Genesh and Fujimoto, Richard, Design and Verification of the Rollback Chip Using HOP: a Case Study of Formal Methods Applied to Hardware Design. ACM Transactions on Computer Systems, Vo. 11 No. 2 pp. 109–145, May 1993.

[17] M. J. C. Gordon, Proving a Computer Correct with the LCF LSM Hardware Verification System. Technical Report No. 42, Computer Laboratory, University of Cambridge, 1983.

[18] M. J. C. Gordon, Why higher-order logic is a good formalism for specifying and verifying hardware. in: G. Milne and P. Subrahmanyam, eds., Formal Aspects of VLSI Design, Proceedings of the 1985 Edinburgh Conference on VLSI, North-Holland, 1986, pp. 153-177.

[19] M. J. C. Gordon, HOL: A Proof Generating System for Higher-Order Logic. University of Cambridge, Computer Laboratory, Tech Report No. 103, 1987.

[20] F.K. Hanna and N.Daeche, Specification and Verification of Digital Systems using Higher-Order Predicate Logic. IEE Proceedings, Vol. 133, Part E, No. 5, September 1986, pp. 242-254.

[21] F.K. Hanna, M. Longley, and N. Daeche, Formal synthesis of digital systems. In [10], pages 532-548.

[22] F.K. Hanna and N.Daeche. Strongly-Typed Theory of Structure and Behaviors. In [32], pp. 39-54.

[23] N.A. Harman and J. V. Tucker, Algebraic Models and the Correctness of Microprocessors. In [32], pp. 92-108.

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

[25] P.B. Jackson, Nuprl and its Use in Circuit Design. In [36], pp. 311-336.

[26] G. Jones and M. Sheeran, Circuit Design in Ruby. In [35].

[27] M. Langevin and E. Cerny, Verification of Processor-like Circuits. In Proc. of the Advanced Work on Correct Hardware Design Methodology, Turin, 12-14 June 1991.

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

[29] Mahmood, M. and Mavaddat, F. and Elmasry, M.I. and Cheng, M.H.M, A Formal Language Model of Logic Microcode Synthesis. In [10], pp. 21–39.

[30] Thomas F. Melham, Abstraction mechanism for hardware verification. In G. Birtwistle and P.A. Subrahmanyam, eds., VLSI Specification, Verification, and Synthesis, pages 267-291. Kluwer Academic Publishers, 1988.

[31] G. J. Milne, Design for Verifiability. In Proc. Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects, Cornell University, USA, July 1989.

[32] G. J. Milne and L. Pierre, eds., Correct Hardware Design and Verification Methods, LNCS 683, Springer-Verlag, May 1993.

[33] Lawrence C. Paulson. Isabelle Tutorial and User’s Manual, 1990.

[34] J. Staunstrup, A Formal Approach to Hardware Design. Kluwer Academic Publishers, 1994.

[35] J. Staunstrup, editor, IFIP WG 10.5 Formal Methods for VLSI Design, North-Holland, 1990.

[36] V. Stavridou, T.F. Melham, and R.T. Boute, eds., Theorem Provers in Circuit Design: Theory, Practice and Experience. IFIP TC10/WG 10.2, North Holland, June 1992.

[37] V. Stavridou, J. A. Goguen, A. Stevens, S. M. Eker, S. N. Alonefits, and K. M. Hobley, FUNNEL and 2OBJ: Towards and Integrated Hardware Design Environment. In [36].

[38] Dany Suk, Hardware Synthesis in Constructive Type Theory. In G. Jones and M. Sheeran, eds., Designing Correct Circuits, pp 29-49, Oxford, Springer-Verlag, 1990.

[39] Li-Guo Wang, Deriving a Correct Computer. In L. J. M. Claesen and M. J. C. Gordon, eds., IFIP Transactions, Higher Order Logic Theorem Proving and its Application, pages 449-458, Elsevier Science Publisher B.V. North-Holland, Amsterdam 1993.

[40] Li-Guo Wang, Formal Derivation of A Class of Computers. PhD Thesis, LFCS, Department of Computer Science, University of Edinburgh, Oct. 1994.

[41] P. J. Windley, A Hierarchical Methodology for the Verification of Microprogrammed Microprocessors. In Proceedings of the IEEE Symposium on Security and Privacy, May 1990.