TOLEDO'97

Tutorial M-A:
Formal Methods in Hardware Design

Speakers

Abstracts

Part I

M. Broy: Mathematical Methods in System Engineering

We present a mathematical, scientific, descriptional and methodological basis for system engineering. In its core, there is a mathematical model of a system and formal techniques to describe it. We outline representative examples of diagrammatic description techniques as they are used in system engineering approaches in practice and show how they are formally related to the system model. These description techniques include in particular

We define a translation of the description techniques into predicate logic. This allows us to combine techniques of formal specification and verification with pragmatic system description techniques. We show how to develop systems with the help of these description techniques in refinement steps. By this, we demonstrate how system engineering methods can be backed up by mathematics.

Part II

B. Möller: Towards Deductive Hardware Design

The term Deductive Design means the systematic construction of a system implementation, starting from its behavioural specification, according to formal, provably correct rules. The main advantages of this approach are:

This paradigm has successfully been applied to sequential and, to a lesser extent, also to parallel programs. The tutorial demonstrates its application to hardware design. We present various case studies dealing with basic combinational and sequential circuits. Special emphasis is laid on parametrization and re-usability aspects.

Part III

N. Harman: Algebraic Models of Microprocessors

The usefulness of formal methods is limited by the accuracy of the mathematical models of hardware that are available. Important questions in formally representing microprocessors are:

We introduce a set of algebraic techniques for representing microprocessors, readily implementable within a range of available software tools. The techniques introduced are suitable for representations of microprocessors at a number of levels of abstraction, including ISA and RT. The techniques are readily applicable to modern microprocessor implementations, including pipelined and superscalar processors. We consider the precise concept of the correctness of one level of abstraction with respect to another, and how we can simplify the resulting proof obligations. We discuss how these algebraic tools relate to, and may be integrated with, techniques developed by other groups working on formal methods for microprocessor representation. We illustrate our tools with a small superscalar example, supporting out-of-order issue and retirement, with precise architectural state maintained by a reorder buffer.

Part IV

A. Ponse: Grid protocols based on synchronous communication

A specification format for networks based on synchronous communication, modeling parallel computation, will be presented. This approach starts from the work done on Synchronous Concurrent Algorithms (SCAs) in Swansea (Thompson and Tucker, 1994). The specification format is ACP-based (Algebra of Communicating Processes, Bergstra and Klop). Main technical construct is the process prefix (generalizing Milner's action prefix), with which parallel input can be easily specified and analyzed. For certain classes of networks, I/O behaviour (comprising absence of deadlock) can be easily characterized by a recursive equation. The specification format and characterization results are illustrated by some examples (Fibonacci sequence, numerical approximation of a one-dimensional wave equation).

Curricula Vitarum

M. Broy

Prof. Dr. Manfred Broy is full professor of computing science at the Technical University of Munich. His research interests are software and systems engineering comprising both theoretical and practical aspects. This includes system models, specification and refinement of system components, specification techniques, development methods and verification. He is leading a research group working in a number of industrial projects that try to apply mathematically based techniques and to combine practical approaches to software engineering with mathematical rigor. Professor Broy is a member of the European Academy of Sciences. In 1994 he received the Leibniz Award by the Deutsche Forschungs Gemeinschaft.

B. Möller

Prof. Dr. Bernhard Möller studied informatics and mathematics at the Technical University Munich and Cornell University. He holds an M.S. degree from Cornell and completed his doctorate and habilitation at TU Munich. He has been involved in the project CIP - Computer Aided, Intuition-Guided Programming at TU Munich, where he worked on the design of the language CIP-L and of the transformation system CIP-S, as well as on the methodology of deductive design. Since 1990 he has been Professor of Informatics at the University of Augsburg. He is a member of IFIP WG 2.1 on Algorithmic Languages and Calculi; since 1994 he has been the coordinator of Esprit WG 8533 NADA - New Hardware Design Methods.

N. Harman

Dr Neal A Harman received a BSc and a PhD in Computer Science from the University of Leeds. His thesis was on the formal representation of digital system. He has worked on a range of formal models of hardware since 1985, specializing in microprocessors since 1993.

A. Ponse

Dr. Alban Ponse completed the study of Mathematics (Logics and Foundations, extended version) at the University of Amsterdam in 1987. From 1988 to 1992 he was employed at CWI, Department of Software Technology, and worked on his Ph.D. at the University of Amsterdam. Currently, he is Lecturer at the Univ. of Amsterdam, Programming Research Group. His Research interests are in process algebra and correctness issues.
ifip@it.uc3m.es