Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <9504200401.AA16541@maui.cs.ucla.edu>
To: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Subject: Re: Verifying SRT Dividers with BDDs
Cc: info-hol@leopard.cs.byu.edu
Date: Wed, 19 Apr 95 21:01:03 PDT
From: chou@cs.ucla.edu


The following announcement might be relevant to this thread .....

- Ching Tsun


From: "M. Vilma Lorenzana-Feliciano" <vilma@cs.usc.edu>

              COMPUTER SCIENCE & COMPUTER ENGINEERING
                    DISTINGUISHED LECTURE SERIES

             Formal Verification of Arithmetic Circuits
                     with Binary Moment Diagrams

                            Randy Bryant
                     Carnegie-Mellon University

The  advent  of  symbolic  Boolean manipulation using Binary Decision
Diagrams (BDDs) has made it possible to automatically verify a wide
range of digital circuits.Typically,  verification  proceeds  by
deriving and comparing BDD representations of the Boolean functions
for a circuit (e.g., a  combinational logic network) and the
specification (e.g., a known good implementation of the desired
function.)  BDD-based methods are in widespread use for verifying both
combinational and sequential circuits.

This  approach  has  two  weaknesses.  First, some circuit functions cannot
be represented efficiently by BDDs.  For example, it has been shown that the
BDDs representing  the  outputs  of  a multiplier circuit grow exponentially
in the word size.  To date, no multiplier with a word size greater
than 16  bits has been  verified  using  BDDs, and even these require
special tricks to overcome the exponential memory requirement
(approximately 0.5 gigabytes for 16 bits.) Second,  generating  a "known  
good"
implementation can prove challenging---the user must essentially create a
prototype circuit from the specification.

We present an approach to verifying arithmetic circuits that  overcomes
these limitations.    It is based on a hierarchical methodology in which the
circuit is given at a block level (e.g, adders,  add-step  stages),
with  each  block having  a  bit-level  structure  (e.g.,  as  logic
gates),  and  a word-level specification.  The overall specification
is also given  at  the  word  level. Verification  involves  showing
that the blocks implement their specifications and that the
composition of word-level block  functions  matches  the  overall
specification. A new data structure, called Binary Moment Diagrams
(BMDs) is used  to  represent  both  bit-level  and  word-level
functions.    BMDs  can efficiently  represent  a  wide  variety  of 
numeric encodings and functions. Using BMDs we have verified a number
of different multiplier designs with word sizes up to 256 bits.

                Date:           April 21, 1995, Friday
                Time:           10:30 a.m.
                Place:          Gerontology Auditorium

                   (Refreshments at 10:00 a.m.)

Randal Bryant received his B.S. degree from the University of Michigan in
1973, and his S.M. and PhD degrees from MIT in 1977 and 1981,
respectively.  From 1981 to 1984 he was an Assistant Professor at
Caltech.  Since 1984 he has been on the faculty of Carnegie Mellon
University, where he is now a Professor of Computer Science.