Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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 07:46:10 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA28896;
          Mon, 21 Nov 1994 00:41:25 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA28892;
          Mon, 21 Nov 1994 00:41:24 -0700
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 4.1/3.26) 
          id AA27152; Sun, 20 Nov 94 23:38:17 PST
Message-Id: <9411210738.AA27152@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Re: FWD: The Pentium chip wasn't verified
Date: Sun, 20 Nov 94 23:38:16 PST
From: chou@cs.ucla.edu


By the way, I heard that BDD's breaks down when verifying multipliers.
Does this mean that theorem proving has a good chance of beating
model checking in the area of verifying multiplication and division
circuits?

- Ching Tsun