TY - THES AU - Brucker, Achim D. PY - 2000 DA - 2000/04/ TI - Verifikation von Dividierern mit Word-Level-Decision-Diagrams PB - Albert-Ludwigs-Universität Freiburg CY - Freiburg KW - formal verification, binary decision diagrams, K*BMD, BDD, nonrestoring division AB - 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. L1 - https://www.brucker.ch/bibliography/download/2000/brucker-verifikation-2000.pdf UR - https://www.brucker.ch/bibliography/abstract/brucker-verifikation-2000 LA - german ID - brucker:verifikation:2000 U1 - Masters thesis ER -