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: email@example.com -- Good health is merely the slowest rate at which one can die.