5 - Formal specification of a digital correlator

Summary

Since our concern was speech, and speech impelled us

To purify the dialect of the tribe

And urge the mind to aftersight and foresight

T. S. Eliot Little Gidding

ABSTRACT

We analyse theoretically the process of specifying the desired behaviour of a digital system and illustrate our theory with a case study of the specification of a digital correlator.

First, a general theoretical framework for specifications and their stepwise refinement is presented. A useful notion of the consistency of two general functional specifications is defined. The framework has three methodological divisions: an exploration phase, an abstraction phase, and an implementation phase.

Secondly, a mathematical theory for specifications based on abstract data types, streams, clocks and retimings, and recursive functions is developed. A specification is a function that transforms infinite streams of data. The mathematical theory supports formal methods and software tools.

Thirdly, a digital correlator is studied in considerable detail to demonstrate points of theoretical and practical interest.

INTRODUCTION

Overview

How can we precisely define the desired behaviour of a digital system? What role can such precise definitions have in the imprecise process of designing a digital system, and in its subsequent use?

We wish to formulate answers to these questions by theoretically analysing the first step of a design assignment, when it must be determined what is to be designed.