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
- data models,
- process models,
- structure and distribution models,
- state transition models,
- interface models.
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:
-
The resulting implementation is correct by construction.
-
The rules can be formulated schematically, independent of the
particular application area, and hence can be re-used for wide
classes of similar problems.
-
Since the rules are formal, the design process can be assisted
by machine.
-
Implementations can be constructed in a modular way, with
emphasis on correctness first and subsequent transformation
to increase performance.
-
The formal derivation also serves as a record of the design
decisions taken and hence is an explanatory documentation. Upon
modification of the system specification it eases revision
of the implementation.
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:
- How can we model structures present in modern microprocessors?
- How can we model time, and the relationship between times at different
levels of abstraction, in the presence of out-of-order execution?
- What does it mean for a microprocessor representation to be
correct? and
- How can we practically establish correctness?
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
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.
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.
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.
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