From owner-colloq-ext@lists.stanford.edu Thu Nov 11 00:53 PST 1999 Return-Path: owner-colloq-ext@lists.stanford.edu Received: from CS.Stanford.EDU (CS.Stanford.EDU [171.64.64.64]) by pedigree.cs.ubc.ca (8.8.8/8.6.9) with ESMTP id AAA19054 for ; Thu, 11 Nov 1999 00:53:09 -0800 (PST) Received: from lists.Stanford.EDU (lists.Stanford.EDU [171.64.14.232]) by CS.Stanford.EDU (8.9.3/8.9.3) with ESMTP id AAA05249; Thu, 11 Nov 1999 00:48:43 -0800 (PST) Received: (from daemon@localhost) by lists.Stanford.EDU (8.9.3/8.9.3) id AAA20677 for colloq-ext-out705929; Thu, 11 Nov 1999 00:44:45 -0800 (PST) Received: from CS.Stanford.EDU (CS.Stanford.EDU [171.64.64.64]) by lists.Stanford.EDU (8.9.3/8.9.3) with ESMTP id AAA20672 for ; Thu, 11 Nov 1999 00:44:44 -0800 (PST) Received: from alpha.xerox.com (firewall-user@alpha.Xerox.COM [13.1.64.93]) by CS.Stanford.EDU (8.9.3/8.9.3) with SMTP id AAA04978; Thu, 11 Nov 1999 00:44:11 -0800 (PST) Received: from Dove.Parc.Xerox.xns by alpha.xerox.com via XNS id <61137(5)>; Thu, 11 Nov 1999 00:37:19 PST Received: from idea.parc.xerox.com ([13.2.19.79]) by alpha.xerox.com with SMTP id <61128(3)>; Wed, 10 Nov 1999 23:56:21 PST Received: by idea.parc.xerox.com id <834562>; Wed, 10 Nov 1999 23:55:18 PST X-NS-Transport-ID: 08002088459301204205 Date: Wed, 10 Nov 1999 23:55:15 PST From: Drew Dean Subject: PARC Forum 11/11: Alan Hu -- The Amazing Commercial Success of Formal Verification To: OpenPARCForum.PARC@xerox.com Message-ID: <99Nov10.235518pst."834562"@idea.parc.xerox.com> Sender: owner-colloq-ext@lists.stanford.edu Precedence: bulk Content-Type: text Content-Length: 2533 Status: RO XEROX PARC FORUM Thursday, November 11, 1999 4:00 - 5:00 p.m. The Amazing Commercial Success of Formal Verification Alan J. Hu Department of Computer Science University of British Columbia Most people still think of formal verification as an impractical, ivory tower pipedream (if they think of formal verification at all). Yet, in the past decade, automated formal verification of hardware has gained considerable industrial importance. Today, formal verification conferences draw industrial sponsorship and mainly industrial attendees, every major company that designs microprocessors employs formal verification experts, and all major VLSI CAD companies as well as several start-ups sell formal verification tools. In this talk, I will give a cocktail-party-level introduction to some of the formal verification techniques that have achieved commercial significance, e.g., BDDs, symbolic simulation, combinational equivalence checking, model checking, and directed search. I will also present my wild, unfounded speculation as to the underlying research principles that made this research area so quickly and successfully commercializable. This Forum is OPEN to the public. Refreshments will be served from 3:45 to 4:00. The George Pake Auditorium is located at Xerox PARC, 3333 Coyote Hill Road in Palo Alto, off of Page Mill Road. From Page Mill Road, turn South on Foothill Expressway, then right on Hillview, and take the second entrance to the right. Park in the large parking lot and enter the auditorium at the upper level of the building. The auditorium is located to the left of and down the stairs from the main entrance. There is a map to PARC at: http://www.parc.xerox.com/images/maptoparc.gif. Note to Xerox employees and contractors: remember to bring your badge for re-entry to building 35. Forum Coordinator: Drew Dean Phone: 650 812-4415 Xerox employees may purchase a copy of the forum videotape by contacting Mimi Gardner, mgardner@parc.xerox.com. A circulation copy will be available to Palo Alto employees through the PARC Information Center, library@parc.xerox.com. PARC Forum Web addresses: External: http://www.parc.xerox.com/forum Internal: http://parcweb.parc.xerox.com/events/forum [-- For mailing list administrative requests, please send mail to Drew Dean . Please understand that the PARC Forum announcements get forwarded via many mailing lists, and I may be unable to help you. Thanks. --DD]