[dk.general] Summer School on Formal Methods for VLSI Design

jorgen@daimi (J|rgen Staunstrup) (12/04/89)

                          IFIP WG 10.5

                    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.

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.

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




Return to   J\o rgen Staunstrup,
            Department of Computer Science, Building 344,
            Technical University of Denmark,
            DK-2800 Lyngby,
            tel. (45) 42 88 15 66,   e-mail: jst@iddth.dk
Good health is merely the slowest rate at which one can die.