Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 9 Sep 1993 21:27:29 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA25798; Thu, 9 Sep 93 13:16:51 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from crl.dec.com by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA25794; Thu, 9 Sep 93 13:16:46 -0700 Received: by crl.dec.com; id AA26437; Thu, 9 Sep 93 16:16:48 -0400 Received: by easynet.crl.dec.com; id AA17394; Thu, 9 Sep 93 16:16:31 -0400 Message-Id: <9309092016.AA17394@easynet.crl.dec.com> Received: from ricks.enet; by crl.enet; Thu, 9 Sep 93 16:16:47 EDT Date: Thu, 9 Sep 93 16:16:47 EDT From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" To: info-hol@cs.uidaho.edu Apparently-To: info-hol@cs.uidaho.edu Subject: EE Times article on formal verification There's a front-page article in Electronic Engineering Times this week (Sep 6) about formal verification. It's mostly fluff, but will make more engineers aware that something called formal verification is coming. It says FV is slowly moving into commercial tools, waves large numbers around potential market size, mentions several tools and companies, and hints at underlying technology (mentioning, without defining, BDDs and higher-order logic.) People from each company make one-line comments, and many mention the size of circuits they've verified, varying from 2000 to 100,000 gates. Tools mentioned (and companies quoted): VFormal Compass Design Automation Design Verifyer Chrysalis Symbolic Design BoolesEye IBM (marketed by Altium) Lambda Abstract Hardware Ltd part of Design Compiler synthesizer Synopsys future part of synthesis tool set AT&T (sold by Intergraph Electronics)