mrb@sei.cmu.edu (Mario Barbacci) (04/08/89)
Advanced Course on FORMAL VERIFICATION IN VLSI DESIGN L'Aquila (Italy), July 10-14, 1989 INTRODUCTION If we are to take full advantage of VLSI's enormous potentialities, zero-defect design is an essential goal. No designer will ever be able to verify the correctness of his work without the help of appropriate CAD tools. Simulation is the state of the art technique to prove correctness, but its drawbacks are widely known. An alternative approach is "formal verification", where the proof is mathematical, rather then experimental. Mathematical demonstration overcomes the limits of test case simulation, since it is valid for all input stimuli under specified assumptions. The course is aimed at introducing the most widely adopted formal verification techniques, outlining the related theories and their limits. The applicability of each approach will be shown in practice, through a series of guided experiments on different verification tools. Experiences from the real world will be presented, including some interesting industrial experiences and the verification of complex microprocessors. Critical assessment and the synergism between verification and synthesis toward zero-defect VLSI designs will be eventually analyzed. The course is mainly devoted to designers and engineers who want to investigate novel techniques to prove correctness of hardware designs. The course is directed by: Prof. Paolo PRINETTO Politecnico di Torino Dipartimento di Automatica e Informatica Corso Duca degli Abruzzi 24 I-10129 Torino TO Italy Telephone : + 39 11 556.7007 Fax : + 39 11 556.7099 Telex : 220646 POLITO I Bitnet : prinetto@itopoli.bitnet E-mail : prinetto@polpp.to.cnr.it Itapac (X25 net) : psi%0222 211 11 79 50::prinetto LECTURERS F. ANCEAU (BULL-CRG, Louveciennes, F) D. BORRIONE (IMAG/ARTEMIS, Grenoble, F) A. J. CAMILLERI (Hewlett Packard Labs., Bristol, UK) P. CAMURATI (Politecnico di Torino, Torino, I) H. EVEKING (Institut fur Datentechnik, Darmstad, D) P. PRINETTO (Politecnico di Torino, Torino, I) CONTENT OF THE COURSE The concept of Formal Verification Formal Verification within the scope of Design Automation The requirements of Formal Verification: - Formal Representation Systems - Automatic Proof Systems Formal Description Systems: - Taxonomy - First-Order Logic - Specific Calculi - Higher-Order Logic - Temporal Logic - Functional Languages Automatic Proof Systems: - Theorem Provers - Tautology Checkers Practical experiences on: - Use of Formal Systems - Use of Theorem Provers - Use of Tautology Checkers Verification of Microprogrammable Architectures The Industrial Impact of Formal Verification The Honeywell-Bull Experience Critical Assessment of Formal Verification: reality vs. utopia, applicability and trends. COST The registration fee is 3,400,000 Italian Lire. It includes transportation from Rome on July 9 and to Rome on July 14, lodging from the evening of July 9 till the afternoon of July 14, meals and reprints of lecture notes. REGISTRATION The enclosed registration form should be posted to: Mr. Renato CIAMPA SSGRR Strada Provinciale di Coppito, Km 0,300 I-67100 COPPITO (L'Aquila) Italy Tel. +39-862-76467 Fax. +39-862-76491 Telex 600870 SSGRR-I and received not later than June 16. Registrations made by telex or fax should contain the same information required in the registration form. Early registrations are highly recommended due to limits in the number of admittances. Applicants admitted will receive a more detailed program of the course, useful information on their staying at the School as well as details about transportation. No accompanying person can be lodged at the School. However participants can contact Mr. Ciampa for reservations in nearby hotels. PAYMENT Payment, required in Italian Lire, should be received before June 24, after the applicant has been notified of the admission to the course. It has to be made by bank transfer to "Credito Italiano - L'Aquila - Italy - account no. 16240-00", in favour of SSGRR. An invoice will be sent to the attendees after payment is received. It is advisable, however, to bring a copy of the receipt of payment and show it at our Reception Desk. Cancellations are accepted up to June 16, with full refund of the fee. No refund will be possible for later cancellations. Substitutions can be made at any time. DESCRIPTION OF SSGRR, L'AQUILA The Scuola Superiore G. Reiss Romoli (SSGRR) is a School for Engineers and Managers of STET, the Italian holding for Telecommunications and Electronics. The SSGRR is a modern and functional educational centre at about 5 km from L'Aquila. This town is famous for its history and for the beauty of its natural parks and mountains; It lies in the Appenines at about 100 Km east from Rome. Modern highways easily connect L'Aquila both to the west (Rome) and to the east side of the peninsula. REGISTRATION FORM Course / Date: FORMAL VERIFICATION TECHNIQUES IN VLSI DESIGN / July 10-14,1989 First Name Last Name Title Position Company Company Fiscal Code (Italian applicants only) Business Address Zip City Country Telex Fax Telephone