Verifikation von Dividierern mit Word-Level-Decision-Diagrams

by Achim D. Brucker

Cover for brucker:verifikation:2000.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.
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 ist too weak to efficiently represent division.
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 nonrestoring division automatically only by the application of decision diagrams.

Keywords: formal verification, binary decision diagrams, K*BMD, BDD, nonrestoring division
Categories: ,
Documents: (full text as PDF file)

QR Code for brucker:verifikation:2000.Please cite this article as follows:
Achim D. Brucker. Verifikation von Dividierern mit Word-Level-Decision-Diagrams. Diplomarbeit, Albert-Ludwigs-Universität Freiburg, 2000.
Keywords: formal verification, binary decision diagrams, K*BMD, BDD, nonrestoring division
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@MastersThesis{ brucker:verifikation:2000,
abstract = {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.\\ 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 ist too weak to efficiently represent division.\\ 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 nonrestoring division automatically only by the application of decision diagrams.},
abstract_de = {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. \\ 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.\\ 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.},
address = {Freiburg},
author = {Achim D. Brucker},
bibkey = {brucker:verifikation:2000},
keywords = {formal verification, binary decision diagrams, K*BMD, BDD, nonrestoring division},
language = {german},
month = {apr},
pdf = {https://www.brucker.ch/bibliography/download/2000/brucker-verifikation-2000.pdf},
school = {{Albert-Ludwigs-Universit{\"a}t Freiburg}},
title = {{Verifikation von Dividierern mit Word-Level-Decision-Diagrams}},
type = {Diplomarbeit},
url = {https://www.brucker.ch/bibliography/abstract/brucker-verifikation-2000},
year = {2000},
}