Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Wed, 19 Apr 95 15:19:55 EDT
From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Message-Id: <9504191919.AA11507@ultrastar.EE.CORNELL.EDU>
To: info-hol@leopard.cs.byu.edu
Subject: Verifying SRT Dividers with BDDs


The following message was posted on comp.sys.intel and
comp.arch.arithmetic by Randy Bryant.  I thought people in the theorem
proving  community might be interested in this work.  

>From: bryant+@N3.SP.CS.CMU.EDU (Randy Bryant)
Newsgroups: comp.sys.intel,comp.arch.arithmetic
Subject: Verifying SRT Dividers with BDDs
Date: 19 Apr 1995 13:53:17 GMT
Organization: Carnegie-Mellon University, School of Computer Science
NNTP-Posting-Host: n3.sp.cs.cmu.edu
Originator: bryant@N3.SP.CS.CMU.EDU


Many months ago, I made several posts speculating that Binary Decision
Diagrams (BDDs) could be used for verifying one stage of an SRT
divider, and that this would have been an effective way to detect such
errors as an incorrectly designed PLA implementation of the PD table.

Several responded to the post with varying degrees of skepticism.  I
decided rather than trying to defend my speculations with more
speculations, that I should go off and try it.  Well, I finally did,
and the results are interesting.  I've prepared a CMU technical
report, CMU-CS-95-140.  You can retrieve it by anonymous FTP as
follows:

	Host:		n3.sp.cs.cmu.edu
	Directory: 	/usr/bryant/ftp
	File:		pentium-tr95-140.ps{.Z}

Let me highlight some key points:

GENERATING A DIVIDER CIRCUIT 

** I used Tim Coe's C model as the basis for creating a gate-level
   version of an SRT divider stage.  I first learned of Coe's program
   via his posts during the height of the Pentium excitement.  Check
   out his article in the April issue of Dr. Dobb's for more details. 
** I wrote a program to generate the PD table based on Coe's thresholds,
   ran the table through ESPRESSO to create an optimized PLA, and then
   converted the PLA into a gate-level equivalent, all automatically.
** I incorporated an "Intel compatibility mode" into my circuit so that
   I could selectively detect when one of the 5 bad table entries is
   hit and force a quotient digit of 0, instead of the normal 2.
** I'm sure my circuit does not exactly match Intel's, but it does
   reproduce its erroneous behavior and serves my objectives.
** The complete circuit has 1100 gates for a 70-bit word size (big
   enough for extended precision mantissas with multiple rounding bits).

VERIFICATION

** The biggest challenge is to convert the specification of one stage, 
   involving arithmetic expressions and inequalities, into a bit-level form.
** I did this by generating a gate-level "checker" circuit containing adders,
   comparators, etc.
** The checker is much larger than the actual divider stage, requiring
   around 4300 gates.  Its design style is more conservative and routine,
   however.
** There is no way to verify the correctness of the checker circuit
   using BDDs.  Still, it provides an independent test of the divider
   stage covering all possible operating conditions.
** The verification succeeds when compatibility mode is turned off,
   and fails when it is turned on, i.e., it would have detected the
   Intel error. 
** On a Sun Sparcstation 10, verification (good or bad) requires around
   112 MB and 10 minutes of CPU time (BDDs are real memory hogs.  We
   purchased a machine with lots of memory for tasks such as this.)

PD TABLE SYNTHESIS

** With this machinery in place, it's a small step to use BDDs to actually
   generate the PD table based on the specification and the rest of the
   circuitry.
** The set of allowable table entries is expressed as a Boolean function
   TAU(P, D, Q) yielding 1 if quotient digit Q is valid for table inputs
   P and D, where Q, P, and D are coded as bit vectors.
** Generation of the table requires 132 MB and 12 minutes of CPU time
** There are no surprises in the table, but it clearly shows that the
   entries Intel set to 0 must be set to 2.

CONCLUSIONS

** Although having to generate a checker circuit from the specification
   decreases the potential benefit and increases the cost of applying
   formal verification methods, it seems to be a worthwhile effort for
   critical and tricky circuits.
** Had Intel invested 1 person-month of effort (< $20,000), they would
   have avoided their estimated $475 million fiasco.  It's easy to say
   this in hindsight, of course, but I would argue that identifying
   regions of a circuit that are most prone to design error and applying
   this kind of verification would be a good policy.
** The utility would be much higher if we could express the specification
   at a higher level and have a program convert this into a bit-level
   check automatically.  That's something we're working on.

+--------------------------------+
| Randy Bryant                   |
| Computer Science Dept.         |
| Carnegie Mellon University     |
| Pittsburgh, PA 15213           |
| (412) 268-8821                 |
| Randy.Bryant@cs.cmu.edu        |
| http://www.cs.cmu.edu/~/bryant |
+--------------------------------+