Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 21 Nov 1994 09:31:06 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA00756; Mon, 21 Nov 1994 02:23:35 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from gmdzi.gmd.de by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA00752; Mon, 21 Nov 1994 02:23:30 -0700 Received: from borneo.gmd.de (borneo) by gmdzi.gmd.de with SMTP id AA14754 (5.65c8/IDA-1.4.4 for ); Mon, 21 Nov 1994 10:20:24 +0100 Received: from borneo.gmd.de by borneo.gmd.de with SMTP id AA23298 (5.67b8/IDA-1.5); Mon, 21 Nov 1994 10:20:20 +0100 Message-Id: <199411210920.AA23298@borneo.gmd.de> To: chou@cs.ucla.edu Cc: info-hol@leopard.cs.byu.edu From: Matthew Morley Subject: Re: FWD: The Pentium chip wasn't verified In-Reply-To: Your message of "Sun, 20 Nov 94 23:38:16 PST." <9411210738.AA27152@maui.cs.ucla.edu> Date: Mon, 21 Nov 94 10:20:20 +0100 - -By the way, I heard that BDD's breaks down when verifying multipliers. Yes, they break down and cry when they can't find a good variable ordering. There is a proof that no good variable ordering exists for such circuits. Conjecture #1. No good BDD variable ordering exists for circuits having multiplier sub-circuits. Conjecture #2. BDDs break down almost always! -Does this mean that theorem proving has a good chance of beating -model checking in the area of verifying multiplication and division -circuits? It's interesting to here on the one hand the theorem provers opine that model checking's no good in general as "it only handles diddy circuits", and model checkers, on the other, opine that theorem proving's no good as "it's just too inefficient". Reality is likely to be somewhere in between, when the clouds of hype disperse. M