*Abstract:* The aim of this thesis is to investigate how to
use logic-based specification, construction, and proof methods to
formally derive a class of computers.

Differing from the traditional concepts of specification,
verification and synthesis, the emphasis will be on the *formal
design process* and the notion of derivation. A derivation is a
stepwise specification, construction and proof process. The
*specification* of derivation is a set of specifications which
is described by abstract syntax capturing the common structure of
the specifications in the set. The *construction* of
derivation is a mapping from the set of specifications to the power
set of specifications. The *proof* of derivation is a
guarantee that each construction is total and each constructed
specification is correct.

Computers are amongst the most complex hardware devices. Formal verification researchers have often used computers as their goals or case studies. But there are few reports of the formal construction and proof of a computer. There is no report about the formal derivation of a class of computers.

In this thesis we present the concepts and methods of
derivation, which includes, mainly, abstract-syntax-based
specification schemes for hierarchical specifications, formal and
nearly mechanical construction, and abstract and general
verification for a class of computers. The central concept is the
*unified derivation model*, developed from the predicate
model, used to describe the whole derivation process. The central
method is *logic structural refinement* which, complements
behavioral, data, temporal, and (spatial) structural abstraction.
It concentrates on describing the main aspect of construction:
logic decomposition. The key point is the concept of an *entry
predicate* which reveals the basic relationship in logic and
time betweeen a specification and its sub-specifications.

We use state-transition-based abstract syntax as the behavior specification scheme to describe a class of computers at the machine instruction level. Starting from the scheme we take nine steps of constructions and proofs to derive and obtain structural specifications at register transfer level. Each individual step, and thereby the whole construction, is proved to be total and correct.

Our work develops the basic view point that the hierarchical architecture of a computer can be organized through a dynamic formal construction and proof process, in a three-dimensional structure of logic, space and time. The aspect of relation and construction in logic is fundamental and novel. In addition to the traditional understanding of microprograms our work brings up three new levels in microprogramming: global loop, abstract microprogram structure, and linear microprogram. Also, there is a sequence of constructions of time layers in which the usual verification based on two time layers is only a special case. As a corollary we discuss no-clock, variable clock, and constant clock machines.

Gordon's computer is taken as a case study to illustrate our concepts and methods. We derive three different implementations and compare them with the original one of Gordon's paper.

**ECS-LFCS-95-329**, September 1995.

This report is available in the following formats:

Previous | Index | Next