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; Thu, 26 May 1994 19:29:02 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26828; Thu, 26 May 1994 12:26:00 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from crl.dec.com by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA26824; Thu, 26 May 1994 12:25:56 -0600 Received: by crl.dec.com; id AA12563; Thu, 26 May 94 13:59:26 -0400 Received: by easynet.crl.dec.com; id AA01814; Thu, 26 May 94 13:59:09 -0400 Message-Id: <9405261759.AA01814@easynet.crl.dec.com> Received: from ricks.enet; by crl.enet; Thu, 26 May 94 13:59:25 EDT Date: Thu, 26 May 94 13:59:25 EDT From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" To: hol2000@leopard.cs.byu.edu Apparently-To: hol2000@leopard.cs.byu.edu Subject: What BDDs are A boolean decision diagram is a representation for a predicate over boolean variables, and has the advantages that the representation is compact enough, and performing operations on the representation (and, or, not, etc) is efficient enough, that BDDs can be used to perform automated verification of hardware structures of interesting size. See Randy Bryant's thesis and later papers at CMU. His tool, SMV, does model-checking using BDDs. See Carl Seger's papers on Voss (lower case --- it isn't an acronym), which does symbolic trajectory evaluation (and model checking) using BDDs. Tim