Verifikation von Dividierern mit Word-Level-Decision-Diagrams

@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},
}