jorgen@daimi (J|rgen Staunstrup) (12/04/89)
IFIP WG 10.5
SUMMER SCHOOL on FORMAL METHODS FOR VLSI DESIGN
June 24 - June 30, 1990
Technical University of Denmark, Lyngby
At this one week summer school, lectures and laboratories will present the
latest developments in formal methods for VLSI design.
Such design techniques aim at unifying hardware and software design for
dedicated and special purpose chips (ASIC's).
A further motivation for these techniques is formal verification/analysis
of VLSI designs. The focus will be on design and verification using
behavioral descriptions of circuits.
Students attending the summer school will learn to design and verify
VLSI chips using high-level behavioral languages.
The lecturers will present different approaches
which will give students an overview of alternative techniques.
Although the summer school will not focus directly on synthesis
techniques, all lecturers will include material on how
their approach can be useful for designing ``real'' chips.
Overview of lectures:
Graham Birtwistle and Brian Graham, Calgary:
In these lectures we will describe the design and verification of
an SECD chip using HOL. After presenting the specification of
an abstract machine, it is shown how it may be realized at the
RTL and logic levels. In particular we will focus on the abstraction
problems between the levels. Some of the interesting proofs from
the verification of the SECD chip are presented.
Michael Fourman, Edinburgh:
We discuss the roles of specification, verification and simulation in
the design cycle, and briefly review models of behaviour at various
levels. Top-down design involves both data and temporal abstraction. We
show how logic may be used to describe and relate behaviours at
different levels of abstraction, using some representative examples.
Mark Greenstreet, Princeton and J\ orgen Staunstrup, Lyngby:
VLSI circuits are highly concurrent. Accordingly, parallel programming
provides a natural paradigm for specifying, designing, and analyzing
VLSI circuits. These lectures will present ``Synchronized Transitions,''
a simple, language for parallel programming that is well-suited for
use in the VLSI design process. The use of ``Synchronized Transitions''
throughout the design process of practical chips will be described.
Warren Hunt, Computational Logic Inc.:
A representation for hardware circuits has been developed for digital
logic which allows various circuit properties to be specified and
verified. A "good" circuit predicate has been defined which precisely
characterizes allowed circuits. An interpreter has been defined which
evaluates hardware circuit descriptions and makes it possible to
verify the logical properties of circuits. Other functions have been
defined to facilitate the verification of timing constraints, fan-out
conditions, and power requirements. These techniques are being employed
in the specification and verification of a microprocessor which we
are having manufactured.
Alain Martin, CALTECH:
We present a synthesis method for the design of delay-insensitive VLSI
circuits, i.e. VLSI circuits whose correct operation is independent of
the delays in operators and wires, with the exception of so-called
``isochronic forks.'' A circuit is first designed as a concurrent
program in a communicating-processes notation inspired by CSP.
It is then compiled into a network of digital gates by a series of
semantics-preserving program transformations. The network of gates is
transformed into a layout for the chosen technology---usually CMOS---
by an automatic placement and routing program. Hence, the circuits
obtained are correct by construction. The method has been
applied both with ``hand compilation'' and automatic
compilation to a series of non-trivial problems. All fabricated chips
have been found correct on ``first silicon.''
Mary Sheeran, Glasgow University and Geraint Jones, Oxford:
We introduce the Ruby design language and calculus. We show how Ruby
is used to design regular array architectures. We demonstrate the use
of standard array design methods by designing a regular Digital Signal
Processing circuit. Next, we show how our methods can be used to
derive the classic Fast Fourier Transform algorithm from a
specification of the Discrete Fourier Transform.
We consider recursive networks, concentrating on butterfly networks
which have very interesting properties. We show how the FFT can be
implemented on a butterfly-like network.
Each lecturer will give approximately 6 lectures. In addition there will
be a laboratory with various tools supporting the formal design techniques.
Attendants will be able to experiment with some of the techniques
discussed in the lectures.
LOCATION
The summer school will be held at the Technical University of Denmark,
Lyngby is a pleasant suburb of Copenhagen with convenient access to
the cultural attractions of the city and the lakes, parks and beaches
of the Danish countryside.
REGISTRATION
The summer school is supported by the Danish Research Academy.
The cost of registration including accommodation will be approx.
D.Kr. 4000 (approx. $600 U.S.).
Participants from the Nordic countries may apply for scholarships
covering travel expenses and attendance. The number of participants will
be limited to 40. First priority will be given to Ph.D. students.
The application deadline is April 1, 1990.
------------------------------------
Please send me further information on the IFIP WG 10.5
SUMMER SCHOOL on FORMAL METHODS FOR VLSI DESIGN:
name:
address:
e-mail:
Return to J\o rgen Staunstrup,
Department of Computer Science, Building 344,
Technical University of Denmark,
DK-2800 Lyngby,
Denmark
tel. (45) 42 88 15 66, e-mail: jst@iddth.dk
--
Good health is merely the slowest rate at which one can die.