Book contents
- Frontmatter
- Contents
- List of contributors
- Preface
- Introduction
- Part 1 Formal methods and verification
- Part 2 Theory and methodology of design
- 5 Formal specification of a digital correlator
- 6 Describing and reasoning about circuits using relations
- 7 The synthesis of VLSI signal processors: theory and example
- Part 3 Methods of circuits and complexity theory
5 - Formal specification of a digital correlator
Published online by Cambridge University Press: 06 November 2009
- Frontmatter
- Contents
- List of contributors
- Preface
- Introduction
- Part 1 Formal methods and verification
- Part 2 Theory and methodology of design
- 5 Formal specification of a digital correlator
- 6 Describing and reasoning about circuits using relations
- 7 The synthesis of VLSI signal processors: theory and example
- Part 3 Methods of circuits and complexity theory
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 GiddingABSTRACT
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.
- Type
- Chapter
- Information
- Theoretical Foundations of VLSI Design , pp. 161 - 262Publisher: Cambridge University PressPrint publication year: 1990
- 9
- Cited by