Abstraction of Hardware Construction

August 21, 1995

Li-Guo Wang^{1} Room 1414, Department of Computer Science, University of Edinburgh, JCMB, The King’s Buildings, 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 concentrate on the foundation of formal hardware construction and present a new hardware-centered concept and methodology. It is a development from, and also contract to, the traditional logic-centered approach. It introduces a higher-order variable construction model of hardware and the notion of generic construction schemes. We demonstrate how the model and the schemes formalize the construction (and verification as well) for a class of computers, as an example to illustrate our concepts and method.

1 Introduction

1.1 From Application to Theory

The formal method for hardware design presented in this paper was stimulated primarily by application, concretely by the formal derivation of a class of microcomputers [39]. The search for a formal approach that is adequate at a non-academic scale on realistic computers, naturally lead us to reconsider and depart from the rather low level of formalization currently used in the area. While often “formal method” is reduced to the application of a specific calculus of formal logic or specific theorem prover, in our work is it taken in its straight meaning: as the formal manipulation of a class of objects (here computers at different levels of abstraction,) where ‘formal’ refers to the fact that these objects are represented by abstract syntax; the objects themselves, or rather their behaviours, are given by a well-defined semantics outside of the formal calculus. In this paper we will summarize the central aspects of this work.

1.2 Synthesis versus Verification

The classical application of formal methods to the design of microcomputers is concerned with formal verification, i.e. the process of proving the consistency between a given implementation and a given specification. The most well-known examples are the verification of the FM8501 by Hunt [21], of the VIPER by Cohn [9, 10], and of the TAMARACK-3 by Joyce [24]. A number of verification examples followed these pioneering works, such as the SECD [3], Mini Cayuga [31], DLX [36], just to mention a few. The approaches mainly differ in the number of abstraction levels they consider, and what logic or theorem prover they use. However, they all share the essential feature of post-hoc formal verification: specification, implementation and all intermediate level descriptions are given a priori, while the nontrivial task consists in finding a proof of correctness for each step.

1This research is supported by a scholarship from Siemens AG Munich and under SERC GR/F 35890 U.K.

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

When initially the research focused on the correctness of specific well-defined hardware designs, the importance of genericity was soon realized, and the inherent potential of the formal approach to verify whole classes of related hardware was stressed [37, 25, 20]. This trend towards proof genericity is natural not least because of the great efforts required for and the resource-demanding nature of formal verification. A side-effect of the strive for generality is to identify and formalize common hardware structure and abstraction levels along which the verification task can be organized and systematized. Examples of such work for the context of microcomputers is the notion of generic interpreter [41, 42] or the algebraic models of [19].

There are many ways to make formal proofs more generic. However, the ultimate level of genericity is not obtained by formal verification but by formal synthesis. In contrast to verification, formal synthesis subjects the very description of a computer to the process of construction not only the correctness proof. This, of course, offers maximal genericity. It also pays pragmatic tribute to the fact that in real life a specification is never completely determined. One usually starts off merely with a first approximation, which is later refined and modified as more details of the implementation become known. The idea of applying formal methods to the design process itself has been introduced rather early, for instance with the theorem provers Lambda [11, 12] or Veritas [17]. Though quite some work has been done on the formal synthesis of actual hardware, e.g. [35, 1, 2, 6], the formal synthesis of realistic (or at least nearly realistic) computers remains an open challenge. A first attempt in this direction is the formal derivation of the DDD-FM9001 [5].

As we see it, the current way of realizing formal synthesis must be seen essentially as a refinement of the tradition of formal verification. Thus, it suffers from being limited into the corset of a particular logic or theorem prover. For instance, [35] is based on Martin-Löf type theory implemented in Isabelle [30], [1, 2] is based on Martin-Löf type theory implemented in Nuprl, [6] is based on higher-order logic implemented in the Lambda prover, and finally [5] uses (a fragment of) first-order logic plus induction implemented the Boyer-Moore theorem prover. We believe that in order for formal synthesis to get off the ground this is the wrong level of formalization. After all, the main concern of synthesis should be the construction of correct computers, not in fact the construction of proofs in some logic on some theorem prover. A large stock of practical experience in formal verification has shown that for a good-structured design, once this structure has been identified, the actual verification may be quite a trivial task. We believe that synthesis in first instance should deal with the formal construction and refinement of hardware structure, and only in second instance with the construction of proofs.

1.3 Hardware-Centered versus Logic-Centered

The previous substantial efforts in applying formal methods to the hardware design process are logic centered, typically so are those based on Hol [15], Lambda [11] and Veritas [17]. These tools are all more or less directly motivated by their application to hardware, and yet they are full-fledged general-purpose theorem provers. For example, regarding Hol we have had several international conferences which showed various interesting applications of Hol in very different areas. A similar statement is true for Lambda. The first author successfully used Lambda to the mechanical synthesis of nondeterministic logic programs [38]. Thus, the traditional applications of formal methods to hardware are mainly centered around very powerful logic systems whose expressiveness is beyond the relatively narrow needs of typical hardware designs. Therefore, we may call these approaches logic-centered.

However, it appears that the strength of the logic-centered approach is at the same time its main weakness: it is far too general to deal with realistically complex hardware designs in an efficient way. This problem is hinted at in [18]:

“[...] it is still, in the authors’ opinion, a very open question as to whether these theoretical gains can be translated into practical ones. Thus far, our own computational trials have been limited to very simple circuits and it is not clear how both the computational load and the amount of human guidance required will scale with increasing size of circuit.”

Concretely, the weakness of the encode-it-in-a-general-purpose-theorem-prover approach lies in the low level of syntactic description and the expensive granularity of elementary design steps. Synthesizing a computer in terms of logical connectives and modus ponens is similar to programming an operating system in an assembler language. More subtly, the generic structure of computers is too rich to be handled by simple formula schemes. For instance, consider a specification of the machine instruction cycle in terms of a global next-state function, such as

state (t + 1) = opcode t = c_{1} → instruction_{1} (state t) ↓
opcode t = c_{2} → instruction_{2} (state t) ↓
⋯
opcode t = c_{n} → instruction_{n} (state t),

where P → Q ↓ R stands for “if P then Q else R.” A simple refinement of this specification might consist in pushing the top-level equation inwards, say in order to separate control and data:

opcode t = c_{1} → state (t + 1) = instruction_{1} (state t) ↓
opcode t = c_{2} → state (t + 1) = instruction_{2} (state t) ↓
⋯
opcode t = c_{n} → state (t + 1) = instruction_{n} (state t).

Now suppose we wanted to implement this step on a theorem prover, as a refinement that is generic in the number n of machine instructions. The most direct solution, namely to exploit the elementary genericity of syntactic substitution, does not work. The syntax of standard logic is not discriminative enough to define the class of all well-formed specifications as the substitution instances of a formula scheme (and the refinement as instances of a rule scheme). In principle, there are two opposite directions we can take to achieve genericity. The solution usually adopted is to implement the refinement as a tactic. This, however, pushes the formalization to the meta-level at the price of a significant “correctness leak”: who verifies the tactic? Although we can be sure that tactics are correct relative to the low level of formulas, there is no guarantee that they are actually sensible as refinements of hardware. A tactic must neither be too timid, so that it succeeds in all interesting cases, nor must it be too general, so that it does not mess up the proof state. Perhaps the most well-known instance of this problem is the so-called false antecedent problem: the synthesis tactics may introduce short-circuits or other inconsistencies. To specify and verify a tactic is a nontrivial problem which is rarely, if ever, attempted. The second possibility to achieve genericity is by encoding the generic structure in terms of inductive data-types, say natural numbers or lists, and recursive functions and induction rules. Such an approach is suggested for example in [20, 18]. This way of going about avoids the correctness leak of tactics. However, by pushing the important structure into the object level it introduces a “formalization leak”: Explicit structure becomes implicit and the manipulation of this structure (e.g. by recursion equations) must be implemented within rather than by the calculus. In this way the formalization becomes clumsy and in the extreme case may get close to a Gödel numbering of hardware.

When it comes to applying formal methods to hardware design then choosing the right level of formalization is a rather crucial part of the exercise. We believe that to deal with real world designs the current logic-centered approach is too low level and that, therefore, a more refined approach is needed. This new approach should be hardware-centered and restricted to the hardware construction area of interest, rather than being general purpose. The purpose of this paper is to present such an approach.

1.4 The New Concepts

The main concepts advanced in this paper are the notions of specification scheme, construction scheme, and construction model. They form the basis for a formal construction framework that has a status very similar to a formal logic, but with a higher level of description, larger degree of genericity, and focus on a particular class of hardware. Specification schemes are abstract syntax schemes to cover the generic structure of a class of concrete computers, at different levels of abstraction. They are the objects of our constructions just as formulas are the objects manipulated by a theorem prover. The semantics of a specification scheme is induced by a syntactic translation into higher-order logic. A construction scheme is a generic translation of one specification scheme to another. It might formalize a refinement from one level of description to another one, or a semantics-preserving transformation. The application of construction schemes drives the formal synthesis just as rules drive the derivation of formulas in a theorem-prover. Finally, the construction model, in our framework, is the most generic form of a specification scheme. It is meant to capture the behaviour of a hardware component as a combination of a functional aspect and a control aspect. This model applies to the whole construction process of a class of computers as shown in [39, 40]. In contrast to the traditional verification-oriented hardware model, it admits finer-grained 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.

1.5 The Higher-Order Aspect

The hardware-centered concept and methodology presented in this paper can be implemented in several logic systems such as Hol [15], Lambda [11], or Isabelle [30]. As its purpose is to handle generic structure, a minimum of higher-order features is required for an adequate implementation of (inductive) specification and construction schemes. Also, we use higher-order variables for the logic (entry predicates) and space (signal/port) parameters in the construction model.

2 Specification Schemes

Construction is inherently formal and generic. It is formal in the sense that it manipulates syntactic structure. The track of the construction process is a series of syntactic descriptions, called specifications, in our case of hardware, from a behavioural to a structural level. The construction is generic in two dimensions. The specification is a scheme that captures the common structure of a class of objects rather than that of a particular instance. This we call the horizontal genericity of construction. Moreover, a specification scheme captures the structure only at a particular level of description. It is built up from “primitive” components that are uninterpreted and whose structure is irrelevant at the given level. They may be filled in by later refinements. This we call the vertical genericity.

Propositional logic, viewed as a fragment of first-order logic, is a familiar example of a formal and generic calculus. This sub-calculus is sensitive to the structure of logical formulas only in terms of propositional connectives like conjunction and implication. The horizontal genericity lies in the inductive structure of propositional formulas as a subset of all formulas. The propositional formulas are generated from propositional variables as their primitive components. As far as the sub-calculus is concerned the structure of these primitive components is irrelevant. A propositional variable may stand for arbitrary logical sentences, which may be freely substituted for it. This is the vertical genericity of propositional logic (within first-order logic.)

To express specification schemes we use a formal language approach. A specification scheme is a context-free formal grammar presented in Backus-Naur form (BNF). Although BNF does not give us maximal control over syntactic structure, it does extend the possibilities of usual logic formulas considerably. Making use of the technology of abstract syntax BNF works well to keep all constructions and specification schemes generic and exact. To get an instance specification from the scheme we instantiate the uninterpreted primitive components (vertical instantiation) and the generic structure of the scheme (horizontal instantiation). So, the specification scheme is our main interface between formal construction and the real world. It should be generic enough to reflect the real world and exact enough, both in the sense of rigorous and informative, such that the formal construction can work on it.

Let us take a class of computers as an example. Taking a bird’s eye view a computer is nothing but a big state transition function working on a number of state signals. We can fix this structure by the following simple specification scheme:

comp ::= os = iss  comp : computer
os ::= (sg y, …, sg y) os : output state
| sg y  iss : input-state structure
sg : signal
y  : distinguished time variable.

The scheme is exact. It says that the output state os of an instruction cycle is computed according to an input-state structure iss. The output state is formed by applying a number of state signals sg_{1}, …, sg_{n} to a distinguished time variable y, which represents the completion time of the cycle. Thus, os = (sg_{1} y, …, sg_{n} y). The scheme is generic. It does not restrict how many state signals a computer has and what information is maintained in them. It does not say what the next-state structure is except that it can be evaluated to give a possible state of the computer at a particular point in time.

We may refine the specification scheme by protruding specific structure for iss. Let us adopt a programmer’s model according to which a computer is a set of machine instructions. These instructions are executed under different conditions, e.g. depending on the value of the operation code (cf. Windley’s notion of generic interpreters [42].) Let us suppose further that instructions may have sub-instructions in common. For such a class of computers, we may set up the following refinement:

iss ::= is  is  : input state
| let A in iss  A  : sharing
| P ⇒ iss ↓ iss  P  : predicate
A ::= v = comm  comm : common part
v  : variable.

Though we have supplied more detail we are still generic: We do not restrict how many instructions a computer has, and in which language they are formulated; we have not said how the instructions are selected, i.e. what kind of predicates can be used. These are generic components of the scheme, left to be filled in in different ways by different instances from the real world. Different refinements and design methods may require different kind of structure for instructions and predicates. However, what is described exactly by the scheme is the the relation between these generic components. It is an inductive and recursive structure. Its base case is an instruction and the step case tells us that through let-in and condition structure we can get any computer, no matter how complex it is.

Although this is still quite an abstract scheme, certain construction steps may find enough structure to work on, already at this level of description, without the need to supply further details. Some constructions may push inwards the global equation os = iss to localize the state transitions and separate control structure from data-structure (called setting state transitions in [39, 40].) Other constructions may rearrange, massage, or normalize the let-in and condition structure in iss. Yet another type of constructions can try break up the atomic calculation of iss into a collection of sequential and parallel computations.

At some point in the synthesis it will be important to protrude the details of the input state is, predicates P, and common part comm. There are many possibilities, depending on how powerful a language we wish to have and on what primitives we wish to build. For our purpose a simple first-order language of terms suffices:

is  ::= tm  is  : input state
| (tm, …, tm)  tm : term
P ::= tm P : predicate
comm ::= tm  comm : common part
tm  ::= c  c  : constant
| v  v  : variable
| sg x  sg  : signal
x  : distinguished time variable
| f(tm, …, tm)  f  : function.

According to this scheme an input state is a tuple of terms, and predicate and common parts are terms. A term is built up from constants, variables, the value of signals at a distinguished point in time (x stands for the start time of the instruction cycle,) and functions applied to terms.

Every construction works on a characteristic syntactic structure, which in an implementation might be established automatically by unification. However, the crucial point is that the specification schemes allow us to specify the effect and purpose of a particular construction in a rigorous way. It allows us to control genericity, which in traditional systems either goes astray in the meta-level of tactics or is obscured in the internals of a clumsy object-level encoding of the structure. The constructions considered in this paper require the structure that is made explicit by the above schemes for comp, iss, and is. We will call this level of description the machine instruction level (MIL).

A final remark is in order. Not all constraints we might wish to impose are (naturally) context-free. This is a limitation which sometimes forces us to add extra side-conditions to capture the wellformed specification instances completely. For example, we might want to constrain the variable v of a sharing ‘let v = tm in iss’ to occur at least twice in iss (otherwise the v is unnecessary,) and further require that no two sharings must use the same variable. Further, we might restrict v not to appear in any comm. Though this might be too restrictive in other circumstances, for a computer’s specification it is useful to eliminate nested or recursive sharing. Another side-condition requires that the output state os and all input states is have the same number of components. Such restrictions, which will often exist for a syntax scheme, could be handled formally too, are ignored in this paper to keep matters simple.

In order to be able to define (and verify) the correctness of construction steps we need some form of semantics. We adopt the simplest possibility: the meaning of a scheme is induced by a translation into an ambient higher-order predicate logic. This logic will not be formally introduced as it can be assumed, at an intuitive level at least, to be understood throughout. The translation is almost immediate in the sense that instances of our schemes can be viewed directly as formulas in higherorder logic containing some syntactic sugar. This would not be strictly necessary, but it stresses our point that the construction framework has the status of a formal logic.

The primitive elements of the specification scheme above, e.g. signals sg, the time variables x, y, and terms tm, are assumed to be part of the higher-order logic. Also, the meaning of composite structures like tuples and equations are taken directly from the logic. The let in and conditional structures are translated as follows:

(let v = A in iss)^{∗} = ∃v. v = A ∧ iss^{∗}
(P ⇒ iss_{1} ↓ iss_{2})^{∗} = (P^{∗} ∧ iss_{1}^{∗}) ∨ (¬P^{∗} ∧ iss_{2}^{∗}).

In this way the semantics of a computer comp is a predicate comp^{∗} over a number of free signal variables sg_{1}, …, sg_{n} and the two distinguished time variables x, y. Let us assume that time is represented by natural numbers N, and that N → α_{i}, for i = 1, …, n, is the type of sg_{i}. Then comp^{∗} is a relation over Σ × N × N where Σ = (N → α_{1}) × ⋯ × (N → α_{n}) is the set of possible state trajectories of the computer. Given s ∈ Σ and t_{1}, t_{2} ∈ N, (s, t_{1}, t_{2}) ∈ comp^{∗} intuitively means that t_{1} is the start time and t_{2} the termination time of a machine cycle in trajectory s.

3 The Construction Model

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 [21] 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 [16, 14, 12], and the basis for formal hardware design methodologies such as [23]. 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: (i) Components are represented by predicates with the free variables as their ports, (ii) Internal port connection is realized by existential quantification, and (iii) 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 [28]:

“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 top-down 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 [9, 10, 27, 13, 26, 28]. To capture the top-down construction of incomplete hardware, in particular for the construction of microprogrammed computers, more sophisticated structure is needed. We have introduced such a new and more general hardware model, the construction model [40]. From our point of view the main aspect in the formal design process 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 constructive framework avoids these fallacies by keeping a rigid discipline 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}, E_{o}. 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. 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 Hoare-style 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 this paper.

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 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.

As mentioned in Sec. refsec:sc, as far as ‘meaning’ is concerned, we adopt the simplest possible approach, viz. a translation into an ambient (higher-order) predicate logic. 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,

where mp^{∗} is the translation of mp. 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.

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. In our case the model predicates will be instances of the scheme comp and conjunctions thereof. 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 [11] (‘flexible’ variables) or Isabelle [30] (‘meta’ variables) and have been shown to be of great advantage in practice. In particular the work based on Lambda (e.g. [11]) makes heavy use of existential variables to support formal hardware synthesis.

4 Construction Schemes

Our objects, to be formally manipulated, are not just arbitrary formulas but computers. Just as a theorem prover usually does not derive ground formulas but formula schemes, our framework constructs specification schemes describing classes of computers (at different levels of description), rather than concrete instances.

The specification scheme is the high-level analogon to a formula scheme, the notion of a construction scheme discussed in this section is the high-level analogon to a derivation rule. An ordinary rule like

∀x. ϕ ∧ ∀x. ψ ⊢ ∀x. (ϕ ∧ ψ)

in predicate logic is not derived as an entailment relation between two concrete formulas but between formula schemes. The premise might be the schematic description of an implementation, and the conclusion that of a specification:

Impl ⊢ Spec.  (1)

Then, the rule can be seen as a construction scheme, which allows us to construct from every concrete specification S a concrete implementation I, such that I ⊢ S. Given S, the construction consists in computing a suitable substitution θ such that S = Spec[θ], from which the implementation can be obtained as I = Impl[θ]. The computation of θ is usually done by some form of unification.

Our plan is to lift the same idea to the case where Impl and Spec are specification schemes, such as those considered in the previous sections. A rule, then, becomes a high-level construction. In this way we do not only raise the level of description. In addition to the vertical genericity of syntactic substitution, we get the horizontal genericity of the BNF syntax schemes. Of course, we cannot any longer represent a construction as a finite rule, though in trivial cases such as

∀x_{1}. ϕ_{1} ∧ ⋯ ∧ ∀x_{n}. ϕ_{n} ⊢ ∀x_{1}. · · · ∀x_{n}. (ϕ_{1} ∧ ⋯ ∧ ϕ_{n})

a pseudo-formal representation using indices and ellipses is possible. We need a different, more general, way of looking at a rule (1) where Impl and Spec are specification schemes. The most general interpretation is to view it as a function Ψ which translates (or: refines) any instance S of scheme Spec into an instance Ψ(S) of scheme Impl such that Ψ(S) ⊢ S is provable. In other words, we use (1) as an abbreviation for the condition:

Ψ : Spec → Impl  ∀S ∈ Spec. Ψ(S) ⊢ S.

If Ψ satisfies these condition, then we write

Ψ : Impl ⊢ Spec.

Notice, the correctness involves two aspects: Ψ must be a total function from well-formed instances of Spec to well-formed instances of Impl, and it must be sound, i.e. the result of applying Ψ must be a provable refinement. Such a construction Ψ may be defined by recursion over the structure of Spec and its correctness verified by structural induction.

It is useful to be a bit more general and consider also non-deterministic constructions Ψ, which for a given input specification determine a set of refinements. In this case the correctness conditions have to be modified accordingly:

∀S ∈ Spec. ∅ ≠ Ψ(S) ⊆ Impl  ∀S ∈ Spec. ∀I ∈ Ψ(S). I ⊢ S.

Nondeterministic constructions arise in an ordinary logic calculus naturally as a set of rules with overlapping conclusions, or by rules producing more than one matching for the conclusion. An example of the latter kind is the equality rule x = e ∧ ψ ⊢ ψ{e/x}. In our framework the nondeterminism is essential, and modelling the potential external selections to steer the synthesis in one direction or other. This can be either by user interaction or by external heuristic algorithms, say for scheduling or allocation.

In this paper we concentrate on the syntactic structure decomposition aspects of construction. Mainly, we will discuss how to construct the logic, space, and time relation of hardware. However, generally speaking, the construction of hardware includes not only syntactic but also semantical aspects. The main purpose of semantic construction steps, apart from optimization, is to make each function in the specification implementable w.r.t. a given implementation level. A syntactic step decomposes the specification to the implementation level. For an example of a semantical step consider a non-implementable 13 bit counter Inc_{13} as in the model

(s y = Inc_{13} (r x)) [E_{i}, E_{o}].

It needs to be transformed semantically to the composition of three implementable functions Cut_{16 13}, Inc_{16}, and Pad_{13 16}:

(s y = Cut_{16 13} (Inc_{16} (Pad_{13 16} (r x)))) [E_{i}, E_{o}].

The syntactic aspect of a construction is to divide the specification into sub-specifications by introducing new entry predicates in logic, new signals (port) in space, and new points in time. For example, decomposing the instruction cycle

(s y = execute(fetch(pc x, mem x), mem x)) [E, E]

into a separate fetch and execution phase

(r y = fetch(pc x, mem x) ∧ mem y = mem x) [E, E_{a}] ∧ (s y = execute(r x, mem x)) [E_{a}, E]

is an example of a syntactic decomposition step. An atomic computation is made non-atomic by breaking it into two pieces. For this to be correct we need to add a signal protection constraint: the condition mem y = mem x makes sure that the fetch and the execute phase work on an identical mem state.

Definition [Input and output signal protection] For a given syntactic construct S the input signal protection S^{i} for S is (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. □

Let us now look at a number of construction schemes that perform relevant syntactic decompositions, taking the specification scheme of the microinstruction level (see Sec. 2) as our starting point:

spec ::= comp [E, E].

It presents a computer as a dynamic process comp [E, E] = (os = iss) [E, E] that executes a global state transition os = iss in a single loop [E, E]. A natural refinement goal is to implement the global transition in terms of a set of elementary local state transitions, which are executed partly in sequence and partly in parallel. To synchronize them the single loop will have to be broken up into richer control structure. In other words, we want a refinement

Ψ : simple control + complex data → complex control + simple data.

where the domain coincides with the scheme spec. But what is the structure of our target specification scheme, capturing the idea of complex control and simple data? The simplest (nontrivial) form of a computer are the instances of the scheme tt ::= sg y = tm, i.e. those with a single output state signal and the input state structure consisting of a single term. We call the sub-class tt of comp the term transitions. With the term transitions our target scheme now can be specified by

impl ::= (tt^{+} [E, lps])^{+},

where for a given scheme S, we use the notation S^{+} to stand for the finite, nonempty conjunctions of (instances of) S. Thus, an implementation is a conjunction of models

(s_{11} y = tm_{11} ∧ ⋯ ∧ s_{1k_{1}} y = tm_{1k_{1}}) [E_{1i}, lps_{1o}]
∧ ⋯ ∧
(s_{n1} y = tm_{n1} ∧ ⋯ ∧ s_{nk_{n}} y = tm_{nk_{n}}) [E_{ni}, lps_{no}].

Intuitively, each model i consist of a set of term transitions s_{i1} y = tm_{i1} ∧ ⋯ ∧ s_{ik_{1}} y = tm_{ik_{1}} executed in parallel in one control step. These sets are synchronized by the [E_{ii}, lps_{io}], which determine how the control steps are linked together. Recall that lps is the leaving predicate structure (see Sec. 2.)

The level of description expressed by the scheme impl has been called term transition level [39, 40]. It establishes, so we believe, a rather natural and generic level of abstraction between the machine instruction level above and the register transfer level below. The term transition level can be viewed as a generalization of the computational model of Unity [7] or Synchronized Transitions [33]. A term transition model tt^{+} [E, lps] here corresponds to a basic transition, i.e. a multi-assignment, there. A conjunction (tt^{+} [E, lps])^{+} 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.

To get back to our main theme, we are looking for a (nondeterministic) construction scheme Ψ that satisfies the specification impl ⊢ spec, or more explicitly,

(tt^{+} [E, lps])^{+} ⊢ comp [E, E].

As explained above, the correctness of Ψ amounts to the two conditions

∀S ∈ comp [E, E]. ∅ ≠ Ψ(S) ⊆ (tt^{+} [E, lps])^{+}  ∀S ∈ comp [E, E]. ∀I ∈ Ψ(S). I ⊢ S.

Usually a construction such as Ψ will not be defined in one step. It will be composed of a number of smaller constructions, which realize certain more or less independent aspects of the refinement. The composition is by way of certain combinators, which allow us to obtain new constructions from constructions already defined previously. In the following let us see how this would look like.

A first construction step might consist in transforming some of the data into explicit control structure. Formally, this is done by pushing the global equation inwards into iss. This way we can break up the input state structure iss into smaller pieces while at the same time producing a richer control structure, i.e. more equations. Let this construction be called Ψ^{a}. It can be defined as follows:

4.a.1 Ψ^{a}(comp) ˆ= comp | Ψ_{1}^{a}(comp)
4.a.2 Ψ_{1}^{a}(os = is) ˆ= os = is
4.a.3 Ψ_{1}^{a}(os = let A in iss) ˆ= let A in Ψ^{a}(os = iss)
4.a.4 ψ_{1}^{a}(os = (P ⇒ iss_{1} ↓ iss_{2})) ˆ= P ⇒ Ψ^{a}(os = iss_{1}) ↓ Ψ^{a}(os = iss_{2}).

Ψ^{a} is a nondeterministic construction scheme defined by induction on the structure of comp. It serves to push the outermost equation across an arbitrary number of let-ins and conditionals. In the first clause, 4.a.1, the vertical bar denotes the choice either to stop the construction or to break out one more control structure (either let-in or conditional) with the sub-construction Ψ_{1}^{a}. The new specification scheme describing the result of this construction is as follows:

comps ::= comp  comps : computer structure
| let A in comps  comp : computer
| P ⇒ comps ↓ comps A : sharing
P  : predicate.

Theorem 1 The construction Ψ^{a} satisfies the specification comps ⊢ comp, i.e. for all S ∈ comp, ∅ ≠ Ψ^{a}(S) ⊆ comps and for all I ∈ Ψ^{a}(S), I ⊢ S.

We can apply Ψ^{a} directly, or under an entry and leaving predicate structure [E, lps]. In general, if a construction Θ satisfies S ⊢ T , then the construction Θ′ = Θ [E, lps], defined as Θ′(T [E, lps]) = (Θ(T)) [E, lps], satisfies S [E, lps] ⊢ T [E, lps]. For instance,

Ψ^{a} [E, lps] : comps [E, lps] ⊢ comp [E, lps].

The operation Θ ↦ Θ [E, lps] is a first example of a combinator on constructions.

Once we have singled out some control structure with Ψ^{a}, or Ψ^{a} [E, lps], we might want to decompose the computer so that the control becomes a separate computation. Before we get to the general case let us first discuss two special cases, viz. the decomposition of a condition and the decomposition of a let-in structure.

Case 1. [decomposing condition structure]: A condition structure is formed as

(P ⇒ R ↓ S) [E_{i}, E_{o}],

where P is a predicate with time variable x and R and S are predicates with time variables x and y. We can implement the conditional model in three stages:

(b y = P ∧ R^{i} ∧ S^{i}) [E_{i}, E_{a}] ∧  (2)
(R^{i} ∧ S^{i}) [E_{a}, b x (E_{b}, E_{c})] ∧  (3)
R [E_{b}, E_{o}] ∧ S [E_{c}, E_{o}].  (4)

The first component (2) realizes the computation of the predicate P and supplies its value on a new signal b. The second component (3), then, performs the branching in the leaving predicate structure. The third stage (4) is the computation of R or S, depending on whether control is passed to entry predicate E_{b} or E_{c}. Notice, this decomposition separates the computation of the condition from from its actual execution; the computation is in done in the data, the decision is part of control. The construction introduces predicate variables E_{a}, E_{b} and E_{c} together with their implicit time variables, and port variable b. As mentioned before these variables are existential variables. The decomposition may be illustrated in a flow-graph as follows:

[figure: E_{i}; P ⇒ R ↓ S; Eo; ⇐; E_{i}; R^{i} ∧ S^{i}, b y = P; Ea; R^{i} ∧ S^{i}, b x?; T; E_{b}; R; F; Ec; S; Eo]

Case 2. [decomposing let-in structure]: A let-in structure is formed as

(let v = tm in S) [E_{i}, E_{o}],

where tm is a term (see Sec. 2) with time point variable x; v is a variable; S is a predicate with time point variables x and y. By decomposition we get

(s_{v} y = tm ∧ S^{i}) [E_{i}, E_{a}] ∧  (5)
S {s_{v} x/v} [E_{a}, E_{o}],  (6)

where s_{v} is a fresh signal variable and S {s_{v} x/v} denotes the syntactic substitution of s_{v} x for v in S. Component (5) first computes the value of tm, which is supplied on signal s_{v}. In the next control step, S picks up this value from s_{v} by (6). Notice again that the newly introduced predicate E_{a} and newly introduced signal s_{v} appear two times, which preserves the consistency in logic and in space.

One can generalize the constructions to decompose a nested sequence of let-ins and conditionals such as

(let v_{1} = tm_{1} in let v_{2} = tm_{2} in P_{1} ⇒ P_{2} ⇒ (cp_{1} ↓ cp_{2}) ↓ cp_{3}) [E_{i}, E_{o}]

into the models

(s_{v_{1}} y = tm_{1} ∧ s_{v_{2}} y = tm_{2} ∧ P_{1}^{i} ∧ P_{2}^{i} ∧ cp_{1}^{i} ∧ cp_{2}^{i} ∧ cp_{3}^{i}) [E_{i}, E_{a}] ∧
(s_{P_{1}} y = P′_{1} ∧ s_{P_{2}} y = P′_{2} ∧ cp′_{1}^{i} ∧ cp′_{2}^{i} ∧ cp′_{3}^{i}) [E_{a}, E_{b}] ∧
(cp′_{1}^{i} ∧ cp′_{2}^{i} ∧ cp′_{3}^{i}) [E_{b}, (s_{P_{1}} x)((s_{P_{2}} x)(E_{c}, E_{d}), E_{e})] ∧
cp′_{1} [E_{c}, E_{o}] ∧ cp′_{2} [E_{d}, E_{o}] ∧ cp′_{3} [E_{e}, E_{o}],

where P′_{1} abbreviates the substitution P_{1}{s_{v_{1}}/v_{1}, s_{v_{2}}/v_{2}}, and similarly for P′_{2}, cp′_{1}, cp′_{2}, cp′_{3}. The decomposition can be illustrated as seen in the picture below, where for simplicity all signal protections have been omitted:

s_{v1} y = tm_{1} ∧ s_{v2} y = tm_{2}
s_{P1} y = P′_{1} ∧ s_{P1} y = P′_{2}

F s_{P2} x s_{P1} x

E_{i}

E_{o}

let v_{1} = tm_{1} in
let v_{2} = tm_{2} in
P_{1} ⇒ P_{2} ⇒ (cp_{1} ↓ cp_{2}) ↓ cp_{3})

⟸

cp′_{1} cp′_{2} cp′_{3}

E_{o}

E_{d}

E_{c} E_{e}

E_{b}

E_{a}

E_{i}

Note, the nested let ins and the nested conditionals are each executed for themselves in one control step, whereas the ordering between the let ins and the conditionals is preserved. They are executed in series.

Let the general construction for this decomposition be called Ψ^{b}. Then Ψ^{b} is given by the definition in Fig. 2. A few explanations will be helpful to understand Ψ^{b}. The input structure is always of the form comps [E_{i}, E_{o}] where the computer structure comps is one of three possibilities, dealt 4.b.1 Ψ^{b} ((os = iss) [E_{i}, E_{o}]) ˆ= (os = iss) [E_{i}, E_{o}]

4.b.2 Ψ^{b} ((let A in cs) [E_{i}, E_{o}]) ˆ=

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

4.b.3 Ψ^{b} ((P ⇒ cs_{1} ↓ cs_{2}) [E_{i}, E_{o}]) ˆ=

(Ψ_{p1} (P ⇒ cs_{1} ↓ cs_{2}) ∧ iprt) [E_{i}, E_{m}] ∧

iprt [E_{i}, Ψ_{p2} (P ⇒ cs_{1} ↓ cs_{2})] ∧ Ψ_{p3} (P ⇒ cs_{1} ↓ cs_{2}, E_{o})

where iprt = (Ψ_{p3} (P ⇒ cs_{1} ↓ cs_{2}, E_{o}))^{i}.

4.b.4 Ψ_{l1} (let v = tm in cs) ˆ= s_{v} y = tm ∧ Ψ_{l1}(cs)

4.b.5 Ψ_{l1} (os = iss) ˆ= iss^{i}
4.b.6 Ψ_{l1} (P ⇒ cs_{1} ↓ cs_{2}) ˆ= P^{i} ∧ cs_{1}^{i} ∧ cs_{2}^{i}

4.b.7 Ψ_{l2} (let v = tm in cs, L) ˆ= Ψ_{l2} (cs, [s_{v} x/v] :: L)

4.b.8 Ψ_{l2} (os = iss, L) ˆ= os = (iss L) (do substitution L on iss)

4.b.9 Ψ_{l2} (P ⇒ cs_{1} ↓ cs_{2}, L) ˆ= (P L) ⇒ (cs_{1} L) ↓ (cs_{2} L) (do substitution)

4.b.10 Ψ_{p1} (P ⇒ cs_{1} ↓ cs_{2}) ˆ= s_{P} y = P ∧ Ψ_{p1} (cs_{1}) ∧ Ψ_{p1} (cs_{2})

4.b.11 Ψ_{p1} (os = iss) ˆ= T
4.b.12 Ψ_{p1} (let A in cs) ˆ= T

4.b.13 Ψ_{p2} (P ⇒ cs_{1} ↓ cs_{2}) ˆ= (s_{P} x) (Ψ_{p2} (cs_{1}), Ψ_{p2} (cs_{2}))

4.b.14 Ψ_{p2} (os = iss) ˆ= E_{iss}
4.b.15 Ψ_{p2} (let A in cs) ˆ= E_{cs}

4.b.16 Ψ_{p3} (P ⇒ cs_{1} ↓ cs_{2}, E_{o}) ˆ= Ψ_{p3} (cs_{1}, E_{o}) ∧ Ψ_{p3} (cs_{2}, E_{o})

4.b.17 Ψ_{p3} (os = iss, E_{o}) ˆ= (os = iss) [E_{iss}, E_{o}]

4.b.18 Ψ_{p3} (let A in cs, E_{o}) ˆ= Ψ^{b} ((let A in cs) [E_{cs}, E_{o}])

Figure 2: Construction Scheme Ψ^{b}

with by Ψ^{b} in the equations 4.b.1, 4.b.2 and 4.b.3: if comps is a computer comp, case 4.b.1, then nothing needs to be done. This is the base case of the construction. If it is a let in structure then 4.b.2 composes the result as the conjunction of two parts determined by the sub-constructions Ψ_{l1} and Ψ_{l2}: first Ψ_{l1} follows a consecutive sequence of nested let ins and realizes the bindings as a set of parallel transitions, by introducing fresh signals for the bound variables. It also computes the appropriate signal protections; Ψ_{l2} eliminates the let ins by substitution, the result of which is then continued to be decomposed by Ψ^{b}. If comps is a condition structure then equation 4.b.3 builds on the three sub-constructions Ψ_{p1}, Ψ_{p2}, and Ψ_{p3}. Here Ψ_{p1} follows a consecutive sequence of nested conditions and realizes the evaluation of all predicates in one parallel step. The second conjunct in 4.b.3 is the decision tree in the form of a leaving predicate structure. This is done by Ψ_{p2}. Finally, Ψ_{p3} deals with the decomposition of the continuation processes that are invoked by the decision tree. The construction is deterministic except for the generation of fresh variables and the choice of their names. In 4.b.4, 4.b.7, 4.b.10, and 4.b.13 new (existential) signal variables s_{v}, s_{P}, and in 4.b.2/3, 4.b.14/15, and 4.b.17/18 new (existential) entry and leaving predicate variables, E_{m}, E_{iss}, E_{cs}, are introduced. The choice of E_{m} in 4.b.2/3 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.b.4 and 4.b.7, and s_{P} in 4.b.10 and 4.b.13. The choice of s_{v} and s_{P}, however, must be functional, i.e. be uniquely determined by variable v and predicate P, respectively. Similarly, the choices of E_{iss} and E_{cs} in 4.b.14/15 and 4.17/18 must be functional, i.e. (in some way) uniquely depend on the sub-terms iss and cs, respectively.

Theorem 2 Assume that the trivial Boolean T is generally omitted in a conjunction. Then,

Ψ^{b} : ((tt^{+} ∪ comp) [E, lps])^{+} ⊢ comps [E, lps],

where ∪ denotes the ordinary set-theoretic union of sets (of languages.)

We can now combine our two constructions Ψ^{a} and Ψ^{b} to obtain a new construction Ψ^{c}, that first applies Ψ^{a} [E, lps] and then Ψ^{b}. Formally,

Ψ^{c} = Ψ^{b} ∘ (Ψ^{a} [E, lps]),

such that

Ψ^{c} : ((tt^{+} ∪ comp) [E, lps])^{+} ⊢ comp [E, lps].

Here ∘ is the functional composition of constructions. In general, if Θ_{1} : R ⊢ S and Θ_{2} : S ⊢ T , then (Θ_{1} ∘ Θ_{2}) : R ⊢ T is defined by (Θ_{1} ∘ Θ_{2})(T) = Θ_{1}(Θ_{2}(R)). Here, T ∈ T and R ∈ R.

The effect of Ψ^{c} as a refinement of the specification comp [E, lps] is to reach into comp up to a certain depth and to break out the appropriate control structure (by Ψ^{a} [E, lps].) This control structure is then implemented in terms of term transitions (by Ψ^{b}.) In the resulting specification, which is an instance of ((tt^{+} ∪ comp) [E, lps])^{+}, there may still be decomposable conjuncts of form comp [E, lps]. On these we could apply Ψ^{c} again, until there are no more of them left. We then end up in (tt^{+} [E, lps])^{+}. Let Ψ^{e} be this construction. Ψ^{e} can also be expressed using general combinators. The first combinator we need is the union operation: if Θ : S_{1} ⊢ S_{2} and T a specification scheme, then T ∪ Θ : T ∪ S_{1} ⊢ T ∪ S_{2}, where T ∪ Θ is defined in the obvious way as

\begin{matrix}(T ∪ Θ)(X) & ˆ= & Θ(X) & if X ∈ S_{2} \\ (T ∪ Θ)(X) & ˆ= & X & if X ∈ T . \end{matrix}

Notice, if S_{2} and T overlap, then we have a choice. This means that T ∪Θ may be nondeterministic even if Θ is not. Another combinator that is relevant is the conjunctive mapping: if Θ : S ⊢ T , then Θ^{+} : S^{+} ⊢ T^{+}, where Θ^{+} is defined by

Θ^{+}(X) ˆ= Θ(X)  if X ∈ S
Θ^{+}(X ∧ R) ˆ= Θ(X) ∧ Θ^{+}(R) otherwise.

With these two combinators we can now form the construction Ψ^{d} = (tt^{+} [E, lps] ∪ Ψ^{c})^{+}, by which we can apply Ψ^{c} to every conjunctive element of the form comp [E, lps] in an instance of ((tt^{+} ∪ comp) [E, lps])^{+}. For Ψ^{d} we obtain the specification

Ψ^{d} : (tt^{+} [E, lps] ∪ ((tt^{+} ∪ comp) [E, lps])^{+})^{+} ⊢ (tt^{+} [E, lps] ∪ comp [E, lps])^{+}.

It is now easy to verify that for the lhs (tt^{+} [E, lps] ∪ ((tt^{+} ∪ comp) [E, lps])^{+})^{+} = ((tt^{+} ∪ comp) [E, lps])^{+}, and also that for the rhs (tt^{+} [E, lps] ∪ comp [E, lps])^{+} = ((tt^{+} ∪ comp) [E, lps])^{+}. Thus, we get

Ψ^{d} : ((tt^{+} ∪ comp) [E, lps])^{+} ⊢ ((tt^{+} ∪ comp) [E, lps])^{+}.

All we need to do to get Ψ^{e} is to iterate Ψ^{d} until we reach a fixed-point, i.e. until there is no control structure left to be implemented. Formally, Ψ^{e} = μΨ^{d}, where

Y ∈ (μΨ^{d})(X) iff ∃X_{0}, …, X_{n}. X = X_{0} ∧ X_{n} = Y ∧

(∀i < n. X_{i+1} ∈ Ψ^{d}(X_{i})) ∧ (∀Y′ ∈ Ψ^{d}(X_{n}). Y′ = X_{n}).

For arbitrary constructions Θ : S ⊢ S, μΘ need not be total, i.e. for some X we may have (μΘ)(X) = ∅. However, for Ψ^{d} it can be shown that μΨ^{d} is indeed total. Viewing Ψ^{d} as a rewriting system, totality of μΨ^{d} corresponds to the condition of weak normalization. One can further show that Ψ^{e} satisfies the specification

Ψ^{e} : ((tt^{+} ∪ os = is) [E, lps])^{+} ⊢ ((tt^{+} ∪ comp) [E, lps])^{+}.

To round off our tool set we might come up with a further construction Ψ^{f}, using the logical equivalence

(sg_{1} y = tm_{1}) ∧ (sg_{2} y = tm_{2}) ≡ (sg_{1} y, sg_{2} y) = (tm_{1}, tm_{2}),

that implements the decomposition

Ψ^{f} : tt^{+} ⊢ os = is.

Now finally we can assemble our desired refinement Ψ from the machine instruction level to the term transition level as follows:

Ψ = ((tt^{+} ∪ Ψ^{f}) [E, lps])^{+} ∘ Ψ^{e}
= ((tt^{+} ∪ Ψ^{f}) [E, lps])^{+} ∘ (μΨ^{d})
= ((tt^{+} ∪ Ψ^{f}) [E, lps])^{+} ∘ (μ(tt^{+} [E, lps] ∪ Ψ^{c})^{+})
= ((tt^{+} ∪ Ψ^{f}) [E, lps])^{+} ∘ μ(tt^{+} [E, lps] ∪ (Ψ^{b} ∘ (Ψ^{a} [E, lps])))^{+}.

Here Ψ^{a}, Ψ^{b}, and Ψ^{f} are given directly, though they could be composed systematically from smaller pieces as well. For Ψ we derive the specification

Ψ : (tt^{+} [E, lps])^{+} ⊢ ((tt^{+} ∪ comp) [E, lps])^{+},

or by restriction, if we observe that comp [E, lps] is a sub-specification (subset of languages) of ((tt^{+} ∪ comp) [E, lps])^{+}:

Ψ : (tt^{+} [E, lps])^{+} ⊢ comp [E, lps]

as desired.

We should point out that the constructions presented above are just examples. Many more constructions are necessary to refine a computer from machine instruction level to, say, the register transfer level. Some other examples are mentioned later in Sec. 6. The gist of this section is to show that constructions can be treated in a way similar to functions in a functional language; and that specification schemes can be used to specify constructions rigorously, similar to the way types specify functions. However, since BNF specification schemes have a richer structure than ordinary functional types the expressibility is considerably higher. In this context it is useful to contrast our constructions with the tactics in a typical theorem prover: The only specification usually available for a tactic is that it has the type theorem → theorem, where the function arrow → means “partial function”. This is not extremely informative and the reason for the correctness leak mentioned in the introduction.

5 Constructing Logic, Space and Time Relations

Logic, space and time are the three primitive dimensions of hardware. Constructing hardware means constructing these three dimensions at different levels of abstraction. For hardware components the relation in logic is fundamental and can be reduced to the three basic operations: sequence, condition, and loop. The relation in space can be reduced to the three basic components: port-connection, bus, and register. The relation in time is accompanied by the relation in logic: through entry predicates we measure and define time points, time units, time clocks, time layers, and time refinements. We give a short summary, further details can be found in [39].

5.1 Constructing Logic Relation

Logic relation is constructed by introducing fresh entry predicate variables and dividing a specification into, for example, two sub-specifications. To preserve logic consistency, the variable always is made to appear in one sub-specification as the leaving and in the other one as the entry predicate. This leads to the logic structure of construction as follows.

1. Sequence: Through E_{m} compose α [E_{i}, E_{m}] and β [E_{m}, E_{o}]

2. Condition: Through leaving predicate structure, α [E_{a}, β (E_{b}, E_{c})]

3. Loop: Through a sequence of entry/leaving predicates with common start predicate E, α [E, E_{a}] ∧ ⋯ ∧ γ [E_{z}, E].

Thus, our extension of the traditional verification model by the entry predicate and leaving predicate structure, captures an elementary form of sequencing control. It allows us to separate control from function, and consequently to refine both aspects independently wherever appropriate. The notion of control here is still fairly abstract, however. It depends on the specific instantiation of the entry and leaving predicates; it can stand for synchronous or asynchronous control, single-clocked or multi-phase, pipelined or un-pipelined. This genericity justifies using the more general term ‘logic relation’ rather than ‘control’.

5.2 Constructing Space Relation

In a very general sense, the design process is stimulated by the aim to establish the consistency of a specification. This also applies to the construction in space. On the other hand, under the condition ensuring consistency there are various possible selections for the construction in space. We present a generic way based on the connection model to guarantee the consistency, while providing maximal flexibility to construct varied possible space relations. When a space relationship is needed we introduce a pair of ports: one, say r, as the output of a component and the other one, say s, as the input of another component. In this case we introduce a new connection formed as

(s y = r x) [E_{i}, E_{o}],

where s is the output and r the input of the connection. Like in introducing entry predicates, we always introduce fresh ports (signals). However, when allocating hardware we possibly assign two or more functions, e.g. Add and Sub, to be implemented by the same device. This leads to the unification of the corresponding ports. When allocation is done we distinguish three cases for a connection with output s:

1. Port-Connection: Signal s only appears once. In this case we can unify s with r and E_{i} with E_{o} and use the weakest implementation, the Boolean constant T:

(s y = s x) [E_{i}, E_{i}] ≡ T.

2. Bus: s is the common output of two or more connections.

(s y = r_{1} x) [E_{i1}, E_{o1}] ∧ ⋯ ∧ (s y = r_{k} x) [E_{ik}, E_{ok}] (k ≥ 2)

In this case a bus is introduced to realize signal s.

3. Register: If a time constraint is added, like in

(s y = r x ∧ y > x) [E_{i}, E_{o}] we can realize the connection by a register with input r and output s. Depending on the time level, a register may also be a simple delay.

5.3 Constructing Time Relation

We cannot directly catch time in hardware, it always is measured through its effect. In the construction model it is the entry predicates that measure time. When we construct the entry predicates we also construct time. The construction of time is always accompanied by the construction of entry predicates.

Definition 5.3.1 [time point]: A time point for entry predicate E is a t such that E t is true.□

Definition 5.3.2 [time clock & time layer]: If E_{i}, (i = 1, …, k), are entry predicates of a circuit specification at a given level of description, then the disjunction ∨_{k=1}^{n}E_{k} is called a(n) (abstract) clock of the circuit. The clock ticks if and when one and only one predicate in the disjunction becomes true. We call the set of all entry predicates of a circuit its time layer. Time clock and layer are relative to the specification level. The same circuit may have different time clocks and time layers at different specification levels. □

Definition 5.3.3 [time refinement]: The construction from a high-level specification, whose time layer is L_{i}, to the adjacent low-level specification, whose time layer is L_{i+1}, is through introducing a set Δ of new middle entry predicates. Therefore the time construction is L_{i} ∪ Δ = L_{i+1}. The time refinement of a circuit from top specification 1 to bottom implementation n is given as the sequence L_{1} ⊂ L_{2} ⊂ ⋯ ⊂ L_{n} of time layers. As the Δ for each step is non-empty, this is a proper hierarchy. □

Definition 5.3.4 [time unit]: We can introduce a specific time unit into a model by refining S (x, y) [E_{i}, E_{o}] into ∀x. E_{i} x ⇒ S (x, x + δ) ∧ E_{o} (x + δ). The δ is called the time unit of the model. □

In our methodology the process of introducing a time clock is a process of imposing more and more external constraints. So, we can have a various specific selections for the clocks of a circuit:

1. Non-Clock: Do not introduce clocks at all, use other forms of control.

2. Variable-Clock: Introduce clocks and time units.

3. Constant-Clock: Introduce clocks and time units, and moreover the constraint that the time units of all models are identical.

6 Case Study

In this section we describe briefly the main steps in the construction of a microprogrammed computer, Gordon’s computer [13], which was taken as a case study in [39]. It includes four main levels:

1. Machine Instruction (MIL): The programmer’s view of a computer as a global next-state transition. The specification scheme capturing MIL was introduced in Sec. 2. This level is characterized by complex data (next-state function) but simple control (single-transition loop) structure.

2. State Transition (STL): At this level the control structure has been separated from the data part, but not as yet implemented. Each instruction is decomposed into a set of concurrent state transitions. There is still one global control loop.

3. Term Transition (TTL): This is the mixed behaviour-structural specification at term transition level. The control structure is realized by entry/leaving predicates as an abstract microprogram, while the data functions appear as synchronized term transitions.

In contrast to the machine instruction level, the term transition level is characterized by a complex control structure of synchronized local state transformations, each of which is governed by a simple function term.

4. Register Transfer (RTL): A model in the register transfer specification is either a function, which is considered implementable at the register transfer level, a port-connection, bus, or register. The control has been flattened into a linear microprogram, microinstruction and microcode.

All description levels MIL, STL, TTL, RTL have been formalized rigorously as specification schemes [39, 40]. Let us illustrate the two main steps, viz. the construction from state transition level STL to term transition level TTL, and from TTL to register transfer level RTL, through rather simplified examples. The complete construction of Gordon’s computer, which applies our framework of specification and construction schemes, has been formalized in detail in [39].

Example 6.1. [from STL to TTL]: Our top-level specification describes a simple generic microcomputer:

Specification at STL:

( let v_{1} = tm_{1} in
let v_{2} = tm_{2} in
(P ⇒ (α ∧ Δ) ↓ (Q ⇒ (β ∧ Δ) ↓ γ))
) [E, E]

This computer has three machine instructions described through state transitions α ∧ Δ, β ∧ Δ and γ respectively. Δ is the common block in the state transition of the first two instructions. For instance, Δ might contain the incrementation of the program counter, pc y = pc x + 1. The three machine instructions are executed under different condition combinations led by P_{1} and P_{2}. Two let in sentences describe the common parts tm_{1} and tm_{2} bound to variables v_{1} and v_{2}, respectively. For instance, tm_{1} might stand for the opcode of the current instruction and tm_{2} for the operands. The entry and leaving predicate of the specification are the same, which describes an infinite loop for the repeated execution of the machine cycle. By applying refinement constructions similar to those in Sec. 4, we derive the following implementation at term transition level.

Implementation at TTL:

(r_{1} y = tm_{1} ∧ r_{2} y = tm_{2} ∧ K_{1}) [E, E_{1}] ∧ (b_{1} y = P′ ∧ b_{2} y = Q′ ∧ K_{2}) [E_{1}, E_{2}] ∧

K_{2} [E_{2}, (b_{1} x)(E_{3}, (b_{2} x)(E_{4}, E_{5}))] ∧ (α′ ∧ K_{3}) [E_{3}, E_{6}] ∧ (β′ ∧ K_{4}) [E_{4}, E_{6}] ∧
(Δ′ ∧ K_{5}) [E_{6}, E] ∧ γ′ [E_{5}, E],

where

K_{1} = P^{i} ∧ Q^{i} ∧ α^{i} ∧ β^{i} ∧ γ^{i} ∧ Δ^{i} K_{3} = K_{4} = Δ^{′i}
K_{2} = α^{′i} ∧ β^{′i} ∧ γ^{′i} ∧ Δ^{′i} K_{5} = α^{′o} ∧ β^{′o}

are the signal protections arising from decomposing atomic transitions. We write α′ for α[r_{1} x/v_{1}, r_{2} x/v_{2}], and similarly for P′, Q′, β′, γ′, and Δ′. The refinement can be depicted graphically as follows, where “SpBd” abbreviates the specification body of the initial STL specification:

E^{SpBd}  ⟸  ^{E}^{r_{1} y = tm_{1} ∧ r_{2} y = tm_{2} ∧ K_{1}}^{E_{1}}^{b_{1} y = P′ ∧ b_{2} y = Q′ ∧ K_{2}}^{E_{2}}^{K_{2} [E_{2}, (b_{1} x)(E_{3}, (b_{2} x)(E_{4}, E_{5}))]}^{E_{3}}  ^{E_{4}}  ^{E_{5}}^{α′ ∧ K_{3}}  ^{β′ ∧ K_{4}}^{E_{6}}^{Δ′ ∧ K_{5}}  ^{γ′}

The logical structure of the computer at term transition level gives us a clear picture of the computer’s global structure at a high level — each box corresponds to a set of parallel term transitions which are uninterpreted and abstract. With the term transition level our formal construction establishes a new and natural abstraction level of computer architecture, conveniently between microinstruction and register-transfer level. We call the implementation the abstract microprogram. 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 a synchronous or asynchronous circuit.

Example 6.2. [from TTL to RTL]: We now consider a part of the computer at TTL, for example the γ′ in the previous example 6.1.

Specification at TTL:

(s_{1} y = f (g (r_{1} x)) ∧ s_{2} y = h (r_{2} x)) [E_{i}, E_{o}].

We select a device D_{f} for function f and D_{gh} for both functions g and h. Assuming that r_{1} and r_{2} are distinct signals we need to introduce a bus or a multiplexer to feed D_{gf}. Let us say we use the bus, together with tristate gates to drive it. The devices are then defined as

D_{gh} (c_{g}, c_{h}, i, s_{2}) ≡ ∀t. s_{2} (t + 1) = (c_{g} t ⇒ g (i t) ↓ (c_{h} t ⇒ h (i t) ↓ i t)) D_{f} (c_{f}, s_{2}, s_{1}) ≡ ∀t. s_{1} (t + 1) = (c_{f} t ⇒ f (s_{2} t) ↓ s_{2} t)) Reg (c_{r}, r_{2}, s) ≡ ∀t. s (t + 1) = (c_{r} t ⇒ r_{2} t ↓ s t) Gate (c_{b1}, r_{1}, r′_{1}) ≡ ∀t. r′_{1} t = (c_{b1} t ⇒ Mk Tri (r_{1} t) ↓ Float) Gate (c_{b2}, s, s′) ≡ ∀t. s′ t = (c_{b2} t ⇒ Mk Tri (s t) ↓ Float) Bus (r′_{1}, s′, i) ≡ ∀t. i t = Dest Tri (r′_{1} t ∪ s′ t).

We could also work with more abstract versions of these devices, viz. simple instances of our scheme comp [E, E]. For example, instead of D_{f} as shown here we could use the model (s_{1} y = (c_{f} x ⇒ f (s_{2} x) ↓ s_{2} x)) [E_{i}, E_{o}]. To reflect the allocation we refine our TTL specification to

(r′_{1} x = r_{1} x ∧ i x = r′_{1} x ∧ s_{2} y = g (i x) ∧ s y = r_{2} x ∧ y > x) [E_{i}, E_{m}] ∧
(s_{1} y = f (s_{2} x) ∧ s′ x = s x ∧ i x = s′ x ∧ s_{2} y = h (i x)) [E_{m}, E_{o}].

Using appropriate symbols to distinguish the individual sub-state transitions, we get the following abstract control flow:

r_{1}  ^{r′_{1}}  ^{i}  ^{g} ^{s_{2}}  ^{f} ^{s_{1}}
r_{2}  ^{c} ^{s}  ^{s′}  ^{i}  ^{h} ^{s_{2}}_{E_{i}}  _{y > x} _{E_{m}}  _{E_{o}}

The control is effected by the three abstract control steps E_{i}, E_{m}, E_{o}. This can be viewed as a linear microprogram, which can be turned into a concrete microprogram, viz. through instantiating the entry predicates by the state of a microinstruction counter: E_{i} x ≡ addr x = 11, E_{m} x ≡ addr x = 12, and E_{o} x ≡ addr x = 13. We then obtain a concrete RTL structure.

Implementation at RTL:

Microprogram:

(∀x. addr x = 11 ⇒ c_{b1} x ∧ c_{g} x ∧ c_{r} x ∧ addr (x + 1) = 12) ∧

(∀x. addr x = 12 ⇒ c_{b2} x ∧ c_{h} x ∧ c_{f} x ∧ addr (x + 1) = 13)

Datapath:

Reg (c_{r}, r_{2}, s) ∧ Gate (c_{b1}, r_{1}, r′_{1}) ∧ Gate (c_{b2}, s, s′) ∧ Bus (r′_{1}, s′, i) ∧

D_{gh} (c_{g}, c_{h}, i, s_{2}) ∧ D_{f} (c_{f}, s_{2}, s_{1})

microprogram

c_{r}  c_{b1}  c_{b2}  c_{g} c_{h}  c_{f}

r_{1} G r{′ \atop 1}

r_{2} Reg s G s′

Bus i D_{gh} s_{2}

s_{2}

D_{f} s_{1}

In [39] a complete sequence of generic refinement steps has been worked out, which from the microinstruction level leads all the way down to a concrete implementation at register-transfer level. The refinements involve 10 major levels of specification schemes together with 9 major construction steps. All of these construction steps are rigorously defined and formally verified, using the framework of BNF specification schemes and constructions schemes described in this paper. The framework has been applied to construct several different versions of Gordon’s computer.

7 Conclusion and Further Work

The work reported in this paper is concerned with the formal synthesis of hardware, with the particular goal of achieving the rigour of formal verification while considerably increasing the amount of genericity and the level of formalization. The proposed framework is centered around the notion of a specification scheme, construction scheme, and construction model.

We argue that the traditional logic-centered approach to formal synthesis (based on theoremproving) in terms of formulas and rules employs too low a level of formalization. Instead of arbitrary formula schemes our calculus constructs specification schemes, each of which captures the generic structure of a class of hardware objects at a specific level of abstraction. This increases the level of formalization but also the amount of genericity: where formula schemes only exhibit vertical genericity a specification scheme also exploits the horizontal genericity of inductive BNF syntax. Construction schemes, then, generalize ordinary rule schemes in a natural way. They are logically correct refinements of one specification scheme to another one.

Yet another source of genericity in our approach lies in the use of the construction model. Besides the obvious signal parameters of the traditional verification model (components-as-relations paradigm) the construction model allows components to communicate via additional entry and leaving predicates. Through this extra dimension of logical communication we can separate functional from control aspects, and refine both independently whenever appropriate. In particular, we can concentrate on functional decomposition, even perform steps of abstract scheduling and allocation, without fixing the particular mode of control. We may instantiate to synchronous or asynchronous, micro-programmed or hard-wired control, at a fairly late stage in the design. We believe that the construction model is a natural and useful generalization of the traditional verification model.

The rather informal character of the presentation in this paper might be misleading. It should be stressed that the proposed construction framework is a rigorous calculus based on formally specified and verified construction schemes. How this can be done is demonstrated in [39], where a suite of concrete specification and construction schemes is presented to derive a class of computers. In this paper we concentrated essentially on motivating the basic ideas from a more general perspective.

Further work will be in two directions. We plan to develop a semi-automatic computer design system which can design a register-transfer level microprocessor from a specification at machine instruction level. It will be based on the ideas discussed in this paper. The user interaction consists in the selections for high-level allocation and scheduling, for which standard algorithms will be integrated. Exploiting the genericity of our approach the tool will be extendible to realize various alternative forms of control, such as multi-phase synchronous, pipelined, or asynchronous handshake. This is a long term goal, however. Other work aims at the theoretical foundations of our framework, in particular concerning the algebraic and logical properties of the construction model.

References

[1] 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.

[2] 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.

[3] G. Birtwistle and B. Graham, Verifying the SECD in HOL. In [32].

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

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

[6] H. Busch, Proof-based transformation of formal hardware models. In [22], pp. 271–296.

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

[8] L. Claesen, editor, IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 1+2, Elsevier/North-Holland, 1989.

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

[10] 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.

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

[12] M. P. Fourman, Formal System Design. In [32], pp 191-236.

[13] 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.

[14] 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, North-Holland, 1986, pp. 153-177.

[15] M. J. C. Gordon and T. F. Melham, Introduction to HOL. Cambridge University Press, 1993.

[16] 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.

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

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

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

[20] J. M. J. Herbert, Incremental Design and Formal Verification of Microcoded Microprocessors. In [34], pp. 157–174.

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

[22] G. Jones and M. Sheeran, Designing Correct Circuits. Springer, 1991.

[23] G. Jones and M. Sheeran, Circuit Design in Ruby. In [32].

[24] J. J. Joyce, Multi-Level Verification of Microprocessor-Based Systems, Ph.D. Thesis, Computer Laboratory, Cambridge University, December 1989 (Technical Report No. 195, May 1990).

[25] J. J. Joyce, Generic Specification of Digital Hardware. In [22], pp. 68–91.

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

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

[28] 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.

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

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

[31] M. Srivas and M. Bickford, Formal Verification of a Pipelined Microprocessor, In IEEE Software, September 1990, pp. 52–64.

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

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

[34] 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.

[35] 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.

[36] S. Tahar and R. Kumar, Towards a Methodology for the Formal Verification of RISC Processors. In Proceedings IEEE International Conference on Computer Design (ICCD’93), 1993, pp. 58–62.

[37] D. Verkest and L. Claesen and H. De Man, On the use of the Boyer-Moore theorem prover for correctness proofs of parametrized hardware modules. In [8], pp.405–422.

[38] Li-Guo Wang, Synthesis of Nondeterministic Logic Programs, Chinese Journal of Software, Vo. 1, No. 1, ISSN 1000-9825, CN 11 - 2560, January 1990.

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

[40] Li-Guo Wang and M. Mendler, Formal Derivation of A Class of Computers: Its high stage — abstract microprogramming. To appear in H. Eveking and P. Camurati, eds., Correct Hardware Design and Verification Methods (CHARME’95), Springer, 1995.

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

[42] P. J. Windley, A Theory of Generic Interpreters. In [29], pp. 122–134.