Verifikation von Dividierern mit Word-Level-Decision-Diagrams
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.
Schlüsselwörter: formal verification, binary decision diagrams, K*BMD, BDD, nonrestoring division
Kategorien: ,
Dokumente: (Artikel als PDF Datei)
Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker.
Verifikation von Dividierern mit Word-Level-Decision-Diagrams. Diplomarbeit, Albert-Ludwigs-Universität Freiburg, 2000.
Schlüsselwörter: formal verification, binary decision diagrams, K*BMD, BDD, nonrestoring division
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (
)
| 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}, | |
| = | {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}, |