Formal Derivation of a Class of Computers

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.