
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/
@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,\newline In the area of the hardware
has increased.
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\newline In this work a new approach for
represent division.
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\glqq Pentium Bug\grqq. Seit dieser Zeit werden
mit dem \"a}rkt Verfahren zur Verifikation von arithmetischen
verst{\newline
Schaltkreisen, insbesondere der Division, untersucht.
Im Bereich der Hardwareverifikation sind
Entscheidungsdiagramme die wichtigsten Datenstrukturen zur\"a}sentation boolescher Funktionen. Allerdings konnte
Repr{\"a}rke der
1998 gezeigt werden, dass die Berechnungsst{
bekannten Entscheidungsdiagramme nicht ausreicht, um die\"o}nnen.\newline In dieser
Division effizient darstellen zu k{
Arbeit wird ein neuer Ansatz zur Verifikation von
Dividiererschaltkreisen vorgestellt, bei dem durch eine
Transformation vermieden wird, die Division als\"u}ssen. Mit diesem
Entscheidungsdiagramm darstellen zu m{\"a}ndig automatische
Verfahren ist erstmals eine vollst{
Verifikation der nonrestoring Division nur durch den Einsatz\"o}glich.},
von Entscheidungsdiagrammen m{note = {Author copy: \url{https://logicalhacking.com/publications/brucker-verifikation-2000/}},
pdf = {https://logicalhacking.com/publications/brucker-verifikation-2000/brucker-verifikation-2000.pdf},
}