Verifikation von Dividierern mit Word-Level-Decision-Diagrams

By Achim D. Brucker.

Da die späte Entdeckung von Fehlern in einem Schaltkreisdesign hohe Kosten verursacht, nimmt die Bedeutung der Verifikation und Validierung zu. Deutlich wurde dies 1994 mit dem Pentium Bug. Seit dieser Zeit werden verstärkt Verfahren zur Verifikation von arithmetischen Schaltkreisen, insbesondere der Division, untersucht. Im Bereich der Hardwareverifikation sind Entscheidungsdiagramme die wichtigsten Datenstrukturen zur Repräsentation boolescher Funktionen. Allerdings konnte 1998 gezeigt werden, dass die Berechnungsstärke der bekannten Entscheidungsdiagramme nicht ausreicht, um die Division effizient darstellen zu können.In dieser Arbeit wird ein neuer Ansatz zur Verifikation von Dividiererschaltkreisen vorgestellt, bei dem durch eine Transformation vermieden wird, die Division als Entscheidungsdiagramm darstellen zu müssen. Mit diesem Verfahren ist erstmals eine vollständig automatische Verifikation der nonrestoring Division nur durch den Einsatz von Entscheidungsdiagrammen möglich.

Keywords:
Formale Verifikation, Binary Decision Diagrams, K*BMD, BDD, Nonrestoring Division, Pentium Bug

Please cite this work as follows:
A. D. Brucker, Verifikation von Dividierern mit Word-Level-Decision-Diagrams,” Diplomarbeit, Albert-Ludwigs-Universität Freiburg, Freiburg, 2000. Author copy: https://logicalhacking.com/publications/brucker-verifikation-2000/

BibTeX
@MastersThesis{ brucker:verifikation:2000,
  language    = {german},
  author      = {Achim D. Brucker},
  title       = {{Verifikation von Dividierern mit
                 Word-Level-Decision-Diagrams}},
  school      = {{Albert-Ludwigs-Universit{\"a}t Freiburg}},
  month       = {apr},
  year        = {2000},
  address     = {Freiburg},
  keywords    = {Formale Verifikation, Binary Decision Diagrams, K*BMD, BDD,
                 Nonrestoring Division, Pentium Bug},
  areas       = {formal methods, hardware},
  abstract_en = {Late detection of design errors typically results in higher
                 costs, therefore the importance of design verification and
                 validation increases. This was especially shown in 1994 by the
                 ``Pentium bug''. Since then the effort put into the
                 verification of arithmetic circuits, particularly division,
                 has increased.\newline In the area of the hardware
                 verification decision diagrams are the most important data
                 structures for the representation of boolean functions.
                 However, in 1998 was shown that the representational power of
                 any known decision diagram is too weak to efficiently
                 represent division.\newline In this work a new approach for
                 the verification of divider circuits is introduced, which by a
                 transformation avoids the representation of the division
                 operation as decision diagram. With this approach it was the
                 first time possible to verify the non-restoring division
                 automatically only by the application of decision diagrams.},
  abstract    = {Da die sp{\"a}te Entdeckung von Fehlern in einem
                 Schaltkreisdesign hohe Kosten verursacht, nimmt die Bedeutung
                 der Verifikation und Validierung zu. Deutlich wurde dies 1994
                 mit dem \glqq Pentium Bug\grqq. Seit dieser Zeit werden
                 verst{\"a}rkt Verfahren zur Verifikation von arithmetischen
                 Schaltkreisen, insbesondere der Division, untersucht. \newline
                 Im Bereich der Hardwareverifikation sind
                 Entscheidungsdiagramme die wichtigsten Datenstrukturen zur
                 Repr{\"a}sentation boolescher Funktionen. Allerdings konnte
                 1998 gezeigt werden, dass die Berechnungsst{\"a}rke der
                 bekannten Entscheidungsdiagramme nicht ausreicht, um die
                 Division effizient darstellen zu k{\"o}nnen.\newline In dieser
                 Arbeit wird ein neuer Ansatz zur Verifikation von
                 Dividiererschaltkreisen vorgestellt, bei dem durch eine
                 Transformation vermieden wird, die Division als
                 Entscheidungsdiagramm darstellen zu m{\"u}ssen. Mit diesem
                 Verfahren ist erstmals eine vollst{\"a}ndig automatische
                 Verifikation der nonrestoring Division nur durch den Einsatz
                 von Entscheidungsdiagrammen m{\"o}glich.},
  note        = {Author copy: \url{https://logicalhacking.com/publications/brucker-verifikation-2000/}},
  pdf         = {https://logicalhacking.com/publications/brucker-verifikation-2000/brucker-verifikation-2000.pdf},
}