From owner-theorynt@LISTSERV.NODAK.EDU Wed Jul 23 21:49:59 1997 Received: from CS.Stanford.EDU (CS.Stanford.EDU [171.64.64.64]) by robotics.Stanford.EDU (8.8.5/8.8.5) with ESMTP id VAA14408 for ; Wed, 23 Jul 1997 21:49:59 -0700 (PDT) Received: from listserv.nodak.edu (listserv.NoDak.edu [134.129.111.8]) by CS.Stanford.EDU (8.8.6/8.8.6) with ESMTP id VAA10362; Wed, 23 Jul 1997 21:49:58 -0700 (PDT) Received: from listserv (134.129.111.8) by listserv.nodak.edu (LSMTP for Windows NT v1.1a) with SMTP id <0.19995F70@listserv.nodak.edu>; Wed, 23 Jul 1997 23:49:46 -0500 Received: from LISTSERV.NODAK.EDU by LISTSERV.NODAK.EDU (LISTSERV-TCP/IP release 1.8c) with spool id 2842555 for THEORYNT@LISTSERV.NODAK.EDU; Wed, 23 Jul 1997 23:49:40 -0500 Received: from listserv (134.129.111.8) by listserv.nodak.edu (LSMTP for Windows NT v1.1a) with SMTP id <0.155D46E0@listserv.nodak.edu>; Wed, 23 Jul 1997 23:49:39 -0500 Received: from LISTSERV.NODAK.EDU by LISTSERV.NODAK.EDU (LISTSERV-TCP/IP release 1.8c) with spool id 2842545 for THEORY-A@LISTSERV.NODAK.EDU; Wed, 23 Jul 1997 23:49:38 -0500 Received: from usc.edu by listserv.nodak.edu (LSMTP for Windows NT v1.1a) with SMTP id <0.14D71C70@listserv.nodak.edu>; Wed, 23 Jul 1997 23:49:38 -0500 Received: from pollux2.usc.edu (pollux2.usc.edu [128.125.253.192]) by usc.edu (8.8.4/8.7.2/usc) with ESMTP id VAA13620 for ; Wed, 23 Jul 1997 21:49:36 -0700 (PDT) Received: (from ierardi@localhost) by pollux2.usc.edu (8.8.4/8.8.4/usc) id VAA08389 for theory-a@listserv.nodak.edu; Wed, 23 Jul 1997 21:49:36 -0700 (PDT) X-Mailer: Microsoft Internet E-mail/MAPI - 8.0.0.4128 Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Status: RO Approved-By: Doug Ierardi Approved-By: Theory-A - TheoryNet World-Wide Events Message-ID: <01BC95E5.B8F19220.aboulham@iro.umontreal.ca> Date: Wed, 23 Jul 1997 21:49:35 PDT Reply-To: Theory-A - TheoryNet World-Wide Events , El Mostapha Aboulhamid Sender: TheoryNet List Comments: cc: "Denise St-Michel (E-mail)" From: El Mostapha Aboulhamid Organization: Université de Montréal Subject: CHARME'97 in Montreal in October 97 Comments: To: THEORY-A@LISTSERV.NODAK.EDU To: THEORYNT@LISTSERV.NODAK.EDU Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by robotics.Stanford.EDU id VAA14408 X-Mozilla-Status: 0001 Content-Length: 12181 ------------------------------------------------------------------ -------------- ******************** * CHARME '97 * ******************** PRELIMINARY PROGRAM AND REGISTRATION INFORMATION IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods Montreal, Quebec, Canada 16 - 18 October 1997 organized by the Groupe interuniversitaire en architecture des ordinateurs et VLSI (GRIAO) cosponsored by Nortel North America, Canadian Microelectronics Corporation, MICRONET Center of Excellence Up-to-date information available on the WEB : http://griao.iro.umontreal.ca/CHARME97/ OBJECTIVES CHARME 97 is the ninth in a series of working conferences devoted to the development and use of formal techniques in digital hardware design and verification. Previous meetings were held in Darmstadt (1984), Edinburgh (1985), Grenoble (1986), Glasgow (1988), Leuven (1989), Torino (1991), Arles (1993), and Frankfurt (1995). This conference series is sponsored by IFIP, and is organized in cooperation with IFIP WG 10.5. Formal verification is increasingly recognized as an appropriate tool for design acceptance (i.e., establishing correctness), and for detecting design errors and specification ambiguities. The validation of functional and timing behaviour is a major bottleneck in current VLSI design systems. Once an academic area, formal design and verification techniques are now beginning to attract serious attention from industry. Given this general increase in activity, our aim is to bring together researchers and users >From both communities. PRELIMINARY PROGRAM Thursday, October 16 7:30 p.m. Cocktail and registration Friday, October 17 9:00 - 9:15 Opening address 9:15 - 10:00 Session 1.1: Invited Presentation ASIC/System HW verification at Nortel: A view from the trenches, A. Silburt (Nortel Semiconductors) Abstract: The emergence of functional verification as the largest single component of the ASIC development cycle has come as a bit of a surprise to the design community. At Nortel we have had a group focusing on the methodologies used at this stage in the design for 4 years. Our involvement with some of the largest Nortel HW designs has provided us with first hand experience of the challenges in establishing confidense that ASICs will first time in a system. This talk will describe the scope of the problems faced in ASIC intesive telecom systems, the methodologies currently deployed and the emerging technologies that we are looking towards in the future to improve our ability to handle complex hardware systems. 10:30 - 12:00 Session 1.2: Advanced Processor Verification Proving the Correctness of the Interlock Mechanism in Processor Design, X. Li(1), A. Cau (2), B. Moszkowski (1), N. Coleman (1), and H. Zedan (2), (1) University of Newcastle, UK, (2) De Montfort University, UK Verifying Out-of-Order Executions, W. Damm and A. Pnueli, OFFIS, Weizmann Institute of Science Formal Modelling and Validation Applied to a Commercial, Coherent Bus, G. Gopalakrishnan, R. Ghughal, R. Hosabettu, and R. Nalumasu, University of Utah 13:00 - 14:30 Session 1.3: Semantics of Hardware-Description Languages An Approach to Verilog-VHDL Interoperability for Synchronous Designs, D. Borrione, F. Vestman, H. Bouamama, TIMA-UJF A Polymodal Semantics for VHDL, S. Shankar and J. Slagle, University of Minnesota A semantic model for VHDL-AMS, N. Martinez Madrid, P. Breuer, and C. Delgado Kloos, Universidad Carlos III de Madrid 15:00 - 16:30 Session 1.4: Model Checking Invited Presentation: Model Checking without Hardware Drivers, Carlos M. Roman, Gary De Palma, Robert Kurshan (Lucent Technologies, Inc.) Abstract: Regardless of whether a simulator or a model checker is used for functional verification, proper capture of the design environment is probably one of the most important steps. This step is not just limited to the proper definition of Clock and Reset pins but, it also includes the specification of input constraints in order to establish a reasonable habitat for the design. However, capturing the environment for a model checker does differ from the conventional approach used for simulators. In this paper, we address these fundamental differences as they are applicable to FormalCheck[Tm], an w-automata based, model checker being comerciallized by Bell-Labs Design Automation, a divisions of Lucent Technologies Inc. Drivers (input conditioners/controllers) and Monitors (output loggers/observers) are used in the simulation environment of virtually every design. These Drivers and Monitors, normally implemented with hardware surrounding the design entity, can invariably restrict the amount of non-determinism required to activate and detect a corner-case bug. In contrast, the level of expressiveness in FormalCheck's language containment constructs allows for accurate and efficient capture of design environments while eliminating the need for sophisticated Drivers and Monitors altogether. These language containment constructs cover the entire spectrum from assumptions and exclusions to eventualities thus, making the generation of safety and fairness constraints very simple. Efficient Model Checking for Analysis of Rainbow Designs, W. Visser, H. Barringer, D. Fellows, G. Gough, and A. Williams, University of Manchester Symbolic Model Checking for a Discrete-Clocked Temporal Logic with Intervals, J. Ruf and T. Kropf, University of Karlsruhe Saturday, October 18 8:30 - 10:00 Session 2.1: Decision Graphs A Parallel Approach to Symbolic Traversal Based on Set Partitioning, G. Cabodi (1), P. Camurati (2), A. Lioy (1), M. Poncino (1), and S. Quer (1), (1) Politecnico di Torino, (2) Universita di Udine Implementation of a Multiple-Domain Decision Package, S. Hoereth, University of Technology Darmstadt Using Induction and BDDs to Model Check Invariants, D. Deharbe and A. Martins Moreira, Universidade Federal do Rio Grande do Norte 10:30-12:00 Session 2.2: New verification techniques Invited Presentation: CheckOff-M - model checking and its role in IP, Roger Hughes (Abstract Inc. and Abstract Hardware Ltd.) On the Non-Termination of MDG-Based Abstract State Enumeration, O. Ait-Mohamed, X. Song, and E. Cerny, Universite de Montreal Verification of Correctness and Performance of Network Protocols via Simulation-Based Techniques, M. Baldi, M. Rebaudengo, P. Prinetto, M. SonzaReorda, and G. Squillero, Politecnico di Torino 13:00 - 14:30 Session 2.3: Issues in Formal Synthesis Integrated Reasoning Support in System Design: Design Derivation and Theorem Proving, S. Johnson (1) and P. Miner (2), (1) Indiana University, (2) NASA Langley Research Center Hardware Compilation Using Attribute Grammars, G. Economakos, G. Papakonstantinou, K. Pekmestzi, and P. Tsanakas, National Technical University of Athens Automatic Post-Synthesis Verification Support for a High-Level Synthesis Step Using the HOL Theorem-Proving System, M. Mutz, University of Passau 15:00 - 16:30 Session 2.4: Panel - Is there a crisis in HW verification Isadore Katz, VP, Chrysalis Symbolic Design, Inc. Carlos Roman (Lucent Inc.) Roger Hughes (Abstract Inc.) PROGRAM COMMITTEE Francois Anceau (CNAM, France) Dominique Borrione (TIMA, France) Paolo Camurati (Politecnico di Torino, Italy) Luc Claesen (IMEC, Belgium) Edmund Clarke (Carnegie Mellon University, USA) Francisco Corella (Hewlett-Packard, USA) Werner Damm (University of Oldenburg, Germany) Hans Eveking (University of Darmstadt, Germany) Ganesh Gopalakrishnan (University of Utah, USA) Mark Greenstreet (University of British Columbia, Canada) Steven Johnson (Indiana University, USA) Carlos Delgado Kloos (University Carlos III, Spain) Thomas Kropf (University of Karlsruhe, Germany) Michel Langevin (Nortel, Canada) Hon F. Li (Concordia University, Canada) Tiziana Margaria (University of Passau, Germany) Matthias Mutz (University of Passau, Germany) Laurence Pierre (Universite de Provence, France) Paolo Prinetto (Politecnico di Torino, Italy) Xiaoyu Song (Universite de Montreal, Canada) Jorgen Staunstrup (Technical University of Denmark, Lyngby) CONFERENCE CHAIR Eduard Cerny Dep. d'informatique et de recherche operationnelle (IRO) Universite de Montreal Tel: (514) 343-7472 Fax: (514) 343-5834 E-mail: cerny@iro.umontreal.ca PROGRAM CHAIR David K. Probst Department of Computer Science Concordia University Tel: (514) 848-3023 Fax: (514) 848-2830 E-mail: probst@iro.umontreal.ca -- conference e-mail address probst@vax2.concordia.ca -- alternate e-mail address PUBLICITY CHAIR El Mostapha Aboulhamid Dep. d'informatique et de recherche operationnelle (IRO) Universite de Montreal Tel: (514) 343-6822 Fax: (514) 343-5834 E-mail: aboulham@iro.umontreal.ca PUBLICATION CHAIR Hon F. Li Department of Computer Science, Room LB-941-3 Concordia University Tel: (514) 848-3020 Fax: (514) 848-2830 E-mail: hfli@vlsi.concordia.ca LOCAL ARRANGEMENTS, REGISTRATION CHAIR Denise St-Michel GRIAO-IRO Universite de Montreal Tel: (514) 343-7052 Fax: (514) 343-5834 E-mail: stmichel@iro.umontreal.ca ---------HOTEL RESERVATION AND CONFERENCE REGISTRATION FORMS -------- IFIP WG10.5 Advanced Research Working Conference on Correct Hardware Design and Verification (CHARME'97) Marriott Château Champlain Hotel 1, Place du Canada Montreal, Quebec, Canada October 16-18, 1997 CONFERENCE REGISTRATION FORM Please use BLOCK LETTERS. IFIP member - which working group: Last name: First name: Affiliation: Address: Country: Phone number: Fax number: E-mail: Registration fees Before September 10 After September 10 IFIP members 430$ CDN 550$ CDN Registration fees include cocktail, coffee breaks, lunches and banquet. Non IFIP members 480$ CDN 600$ CDN Registration fees include cocktail, coffee breaks, lunches and banquet. Students 300$ CDN 400$ CDN Registration fees include cocktail, coffee breaks, lunches. PAYMENT:Cheques labelled in Canadian currency ONLY to the order of CHARME '97. Note that we cannot accept credit cards for advance or on-site registration. Given the small size of the conference we apologize for not being able to provide such service. HOTEL RESERVATION FORM ---------------------- Marriott Chateau Champlain Hotel 1, Place du Canada Montreal, Quebec, Canada CHARME'97 Conference rate: 125.00$ CDN per night plus taxes (single or double occupancy) This rate is valid until September 10, 1997. Please use BLOCK LETTERS. Last name: First name: Affiliation: Address: Country: Phone number: Fax number: E-mail address: Single occupancy ( ) Double occupancy ( ) Last name: First name: Smoking ( ) Non smoking ( ) Number of nights: Arrival date: Departure date: Payment: Visa ( ) MasterCard ( ) Diners Club ( ) American Express ( ) Name of the cardholder: Card number: Expiry date: Signature: Send your hotel reservation and conference registration forms to: Denise St-Michel GRIAO Ð IRO, Andre-Aisenstadt Bldg., Room 3227 Universite de Montreal 2900 Edouard-Montpetit Montreal (Quebec), Canada H3C 3J7 Fax: (514) 343-5834 Phone: (514) 343-7052 e-mail: stmichel@iro.umontreal.ca