Verifikation von Arithmetik-Schaltungen mit Word-Level Decision Diagrams

| project staff | cooperation partners | project description | publications |

The task of hardware verification is to prove that a given circuit implementation is conform with its specifiction. A popular method of proving that a combinational circuit corresponds to its specification is to transfer both specification and implementation into a normalform and then check their equivalence.

In this context BDDs have proved their value as compact normalform for certain circuit categories e.g. control logic or adders. For other circuits e.g. multipliers however, the BDD-based approach fails, because the design of multipliers with BDDs is of exponential size.

To face this problem so-called world-level DDs e.g. *BMDs, HDDs or K*BMDs were established, which can represent e.g multipliers in polynomial size. Unlike BDDs, world-level DDs represent functions with integer (or rational) image values. The question wether also division can be represented by world-level DDs in polynomial space was unanswered for quite a while and could be answered within the scope of this project.

After it turned out that certain world-level DDs are excellently suited for the verification of multiplieres, since it is possible to construct these world-level DDs in polynomial space and time for the multiplier function, the observation was expanded to dividers. In this connection the question whether or not also dividers can be represented by world-level DDs in polynomial space could be answered. With the help of the methods of linear algebra an exponential lower bound for the representation size of world-level DDs was specified for the division function. The proof is based on the construction of a “generic” world-level DD, for which the bound ist shown and which still allows the embedding of all current types of world-level DDs. Compared to other common techniques with DDs here the proof was shown directly for a whole class of DDs.

First continuative tests however make it expectable, that it is yet possible to verify dividers with the help of world-level DDs. Our approach tries to verify a transformed function instead of the division function itself. The transformation results out of an additional circuit, which is set behind the divider and reverses the division by multiplying the divisor and adding the rest of the division. The divider is considered as correct exactly then, when the whole circuit evaluates the identity function. Now firstly the evaluation of the world-level DD for the whole circuit is started by the (simple) construction of the world-level DD for the additional circuit. When the part of the circuit is reached, which corresponds to the divider, it is being worked with a representation, which doesn’t require the divider to be built up by backward substitution, but a transformation given by the additional circuit. Whether or not this transformation leads to (and in which cases it does) a polynomial limited representation is the object of current tests. Examinations for different kinds of common divider designs - e.g. the Pentium-Divider - shall be accomplished. The intention is to find a procedure, which, contrary to all other methods known so far, accomplishes a fully automated verification without having to fall back interactively on the knowledge of the developer about the implementation.