Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <03163-0@swan.cl.cam.ac.uk>; Fri, 3 Apr 1992 22:25:32 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01367; Fri, 3 Apr 92 13:01:35 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from enet-gw.pa.dec.com by ted.cs.uidaho.edu (16.6/1.34) id AA01363; Fri, 3 Apr 92 13:00:15 -0800 Received: by enet-gw.pa.dec.com; id AA23875; Fri, 3 Apr 92 12:58:53 -0800 Message-Id: <9204032058.AA23875@enet-gw.pa.dec.com> Received: from hpsrad.enet; by decwrl.enet; Fri, 3 Apr 92 12:59:09 PST Date: Fri, 3 Apr 92 12:59:09 PST From: "HEMENDRA TALESARA, VSS FT SYSTEMS, 297-5541 03-Apr-1992 1602" To: info-hol@com.dec.Pa Apparently-To: info-hol@ted.cs.uidaho.edu Subject: FWD: Hardware Verification course, July 6 - 10 ------------------Forwarded item dated 3-APR-1992 15:50:53.54------------------ From: DECWRL::"kaufmann@CLI.COM" "Matt Kaufmann" To: theorem-provers@ai.mit.edu, technical@CLI.COM, nqthm-users@CLI.COM CC: PRINETTO@POLITO.IT Subj: Hardware Verification course, July 6 - 10 I've been asked to forward the following course announcement. Feel free to forward it further as you see fit. I've been told: >> People in L'Aquila will be able to confirm the course 2-3 weeks before, not >> earlier. Please forward the program to people on your mailing list that >> are probably interested in formal techniques. Date: Tue, 24 Mar 1992 19:42 GMT+1 From: PRINETTO@POLITO.IT Subject: summer course program: please forward To: borrione@imag.imag.fr, ac@hplb.hpl.hp.com, camurati@POLITO.IT, claesen@imec.be, Edmund_Clarke@G.GP.CS.CMU.EDU, denicola@icnucevm.cnuce.cnr.it, xbr4d75r%DDATHD21.bitnet@CUNYVM.CUNY.EDU, kaufmann@cli.com, milne@computer-science.strathclyde.ac.uk, prinetto@polpp.TO.CNR.IT, fabio@duke.Colorado.EDU, soulas@rem63ax.edf.fr X-Envelope-To: kaufmann@cli.com X-Vms-To: @LECTURER.DIS Advanced Course on Formal Verification Techniques in VLSI Design ---------------------------------------------------------------- SSGRR - L'Aquila, Italy 6 - 10 July 1992 Objectives ---------- 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 than experimental. Mathematical demonstration overcomes the limits of test case simulation, since it is valid for all input stimuli under specified assumptions. Formal techniques are getting out of their infancy and we already witness their introduction in industrial environments. The course aims at introducing the most widely adopted formal veri- fication techniques, outlining the related theories and their limits. State-of-the-art techniques and novel research efforts will be considered, as well as their relationship with VHDL. The applicability of each ap- proach will be shown in practice during demos, guided and hands-on experi- ments on popular tools. Formal verification's merits and limits will be critically assessed, the synergy between verification and synthesis toward zero-defect VLSI de- signs will be analyzed, and industrial experience will be discussed. The main topics of this course are: high-level description and validation of hardware designs with process algebras (the Circal system), Petri Nets (the EVAL system), and VHDL (the Prevail proof environment); propositional logic (BDD's and tautology checking); first-order logic (the Boyer-Moore and OTTER theorem provers); higher-order logic (the HOL system); temporal logic and model checking (the SMV system). As application examples, switch- level descriptions, control-dominated FSM's, data paths & control units, and properties of communicating FSM's will be considered. The impact of formal verification techniques on synthesis and testing will be analyzed. Target Audience --------------- The course is mainly devoted to managers, designers, engineers, and students who want to get acquainted with novel techniques and tools to formally specify, validate, and prove hardware designs. Faculty ------- Course Director Prof. Paolo PRINETTO Politecnico di Torino, Turin (I) Lecturers D. BORRIONE (IMAG/Artemis, Grenoble (F)) A.J. CAMILLERI (Hewlett Packard Labs, Bristol (UK)) P. CAMURATI (Politecnico di Torino, Turin (I)) L. CLAESEN (IMEC / Kath. Univ. Leuven, Leuven (B)) E.M. CLARKE (Carnegie-Mellon University, Pittsburgh (USA)) R. DE NICOLA (Universita' di Roma "La Sapienza", Rome (I)) H. EVEKING (Technische Hochschule Darmstadt, Darmstadt (D)) M. KAUFMANN (CLI, Austin (USA)) G.J. MILNE (Strathclyde University, Glasgow (UK)) P. PRINETTO (Politecnico di Torino, Turin (I)) F. SOMENZI (University of Colorado, Boulder (USA)) B. SOULAS (Electricite' de France, Paris (F)) Course Contents --------------- ------------------- Monday, July 6 1992 ------------------- 09.00 - 09.30 Course presentation (P. Prinetto) 09.30 - 11.00 Towards zero-defect designs (P. Prinetto) 11.00 - 13.00 The Boyer-Moore theorem prover: basic principles (M. Kaufmann) 14.30 - 16.30 Verification from transistor switch level upwards (L. Claesen) 16.30 - 17.30 Guided hands-on experience: the Boyer-Moore theorem prover (M. Kaufmann) 17.30 - 18.30 Guided hands-on experience: switch-level verification (L. Claesen) 18.30 - 20.00 Optional hands-on experience: the Boyer-Moore theorem prover (M. Kaufmann, P.Camurati, P. Prinetto) Optional hands-on experience: switch-level verification (L. Claesen, P.Camurati, P. Prinetto) -------------------- Tuesday, July 7 1992 -------------------- 09.00 - 11.00 BDDs, tautology checking & demo (H. Eveking) 11.00 - 13.00 Temporal Logic & Model Checking: basic principles (E.M. Clarke) 14.30 - 16.30 Higher-order logic & HOL (A. Camilleri) 16.30 - 17.30 Guided hands-on experience: the SMV system (E.M. Clarke) 17.30 - 18.30 Guided hands-on experience: the HOL system (A. Camilleri) 18.30 - 20.00 Optional hands-on experience: the SMV system (E.M. Clarke, P. Camurati, P. Prinetto) Optional hands-on experience: the HOL system (A. Camilleri, P. Camurati, P. Prinetto) ---------------------- Wednesday, July 8 1992 ---------------------- 09.00 - 11.00 First-order logic & OTTER (P. Camurati) 11.00 - 13.00 Formal verification of designs described in VHDL (D. Borrione) 14.30 - 16.30 Predicate/Transition Petri Nets and the EVAL system (B. Soulas) 16.30 - 17.30 Guided hands-on experience: the PREVAIL VHDL proof environment (D. Borrione) 17.30 - 18.30 Guided hands-on experience: the EDF approach to communication protocol specification, validation, verification, and test (B. Soulas) 18.30 - 20.00 Optional hands-on experience: the PREVAIL VHDL proof environment (D. Borrione, P.Camurati, P. Prinetto) Optional hands-on experience: the EVAL system (B. Soulas, P.Camurati, P. Prinetto) --------------------- Thursday, July 9 1992 --------------------- 09.00 - 13.00 Process Algebras (R. De Nicola) 14.30 - 16.30 The Circal System: basic principles (G.J. Milne) 16.30 - 17.30 Guided hands-on experience: the Circal System (G.J. Milne) 17.30 - 18.30 Guided hands-on experience: the OTTER theorem prover (P. Prinetto) 18.30 - 20.00 Optional hands-on experience: the Circal System (G.J. Milne, P.Camurati, P. Prinetto) Optional hands-on experience: the OTTER theorem prover (P.Camurati, P. Prinetto) -------------------- Friday, July 10 1992 -------------------- 09.00 - 12.00 FSM verification and its application to synthesis and testing \ demo (F. Somenzi) 12.00 - 13.00 Roundatble Affiliations ------------ prof. Dominique BORRIONE Institut IMAG Laboratoire Artemis B.P. 53X F-38041 Grenoble Cedex France Tel: + 33 76 514604 ext 5240 Fax: + 33 76 519637 E-mail: borrione@imag.imag.fr dr. Albert J. CAMILLERI Hewlett Packard Labs. Information Systems Centre Filton Road Stoke Gifford Bristol BS12 6QZ UK Tel: + 44 272 799910 ext 24196 Fax: + 44 272 790554 E-mail: ac@hplb.hpl.hp.com dr. Paolo CAMURATI Politecnico di Torino Dip. di Automatica e Informatica Corso Duca degli Abruzzi 24 I-10129 Turin Italy Tel: + 39 11 564.7009 Fax: + 39 11 564.7099 E-mail: camurati@polito.it prof. Luc CLAESEN IMEC / Kath. Univ. Leuven Kapeldreef 75 B-3001 Leuven Belgium Tel: + 32 16 281.203 Fax: + 32 16 229.515 E-mail: claesen@imec.be prof. Edmund M. CLARKE Dept. of Computer Science Carnegie-Mellon University Schenley Park Pittsburgh PA 15213 USA Tel: + 1 412 268 2628 Fax: + 1 412 268 5016 E-mail: Edmund_Clarke@G.GP.CS.CMU.EDU prof. Rocco DE NICOLA Universita' di Roma "La Sapienza" Dip. Matematica Via Salaria 113 I-00184 Rome Italy Tel: + 39 6 884.1957 Fax: + 39 6 884.1964 E-mail: denicola@icnucevm.cnuce.cnr.it dr. Hans EVEKING Institut fuer Datentechnik Technische Hochschule Darmstadt Merckstrasse 25 D-6100 Darmstadt Fed. Rep. Germany Tel: + 49 6151 16.2075 Tel: + 49 6151 16.2076 Fax: + 49 6151 16.4976 E-mail: xbr4d75r@ddathd21.bitnet dr. Matt KAUFMANN Computational Logic, Inc. 1717 W. Sixth St. Suite 290 Austin, TX 78703 USA Tel: + 1 512 322-9951 Fax: + 1 512 322-0656 E-mail: kaufmann@cli.com dr. George J. MILNE Dept. of Computer Science University of Strathclyde 26 Richmond Street Livingstone Tower Glasgow G1 1XQ UK Tel: + 44 41 552 4400 ext 3551 Fax: + 44 41 552 0775 E-mail: milne@computer-science.strathclyde.ac.uk prof. Paolo PRINETTO Politecnico di Torino Dip. di Automatica e Informatica Corso Duca degli Abruzzi 24 I-10129 Turin Italy Tel: + 39 11 564.7007 Fax: + 39 11 564.7099 E-mail: prinetto@polpp.to.cnr.it prof. Fabio SOMENZI University of Colorado at Boulder Dept. of Elec. and Com. Eng. Eng. Center, Campus Box 425 Boulder, CO 80309-0425 USA Tel: + 1 303 492.3466 Fax: + 1 303 492.2758 E-mail: fabio@duke.Colorado.EDU dr. Bernard SOULAS Electricite' de France Direction des Etudes et Recherches Service Materiel Electrique Dept. C.I.M.A. Les Renardieres Boite Postale n. 1 F-77250 Moret sur Loing France Tel: + 33 1 60706343 Fax: + 33 1 60706543 E-mail: soulas@rem63ax.der.edf.fr  % ====== Internet headers and postmarks (see DECWRL::GATEWAY.DOC) ====== % Received: by enet-gw.pa.dec.com; id AA22977; Fri, 3 Apr 92 12:46:23 -0800 % Received: by CLI.COM (4.1/1); Fri, 3 Apr 92 14:20:49 CST % Date: Fri, 3 Apr 92 14:22:32 CST % From: Matt Kaufmann % Message-Id: <9204032022.AA05809@thunder.CLI.COM> % Received: by thunder.CLI.COM (4.1/CLI-1.2) id AA05809; Fri, 3 Apr 92 14:22:32 CST % To: theorem-provers@ai.mit.edu, technical@CLI.COM, nqthm-users@CLI.COM % Cc: PRINETTO@POLITO.IT % Subject: Hardware Verification course, July 6 - 10