University:

Martin-Luther-Universitaet Halle-Wittenberg, Germany

Department:

Fachbereich Mathematik und Informatik

Informatik

Date: 12.02.1999

MSC:

68R99 None of the above but in this section

Language: written in ENG

Abstract: We consider the problem of checking the equivalence of two Boolean
functions under arbitrary input permutations. This problem has
several applications in the synthesis and verification of
combinational logic. In logic verification this is needed when the
exact correspondence of inputs between the two circuits is not
known. The problem is {\cal NP}--hard, thus recourse is taken to
heuristics that work well in practice. The approach presented in
this thesis computes signatures for each input variable that will
help to establish correspondence of variables. Signatures work well
for a large number of the investigated examples. However, for each
choice of signature, there remain variables that cannot be uniquely
identified. Our research has shown that, for a given example, this
set of problematic variables tends to be the same --- regardless of
the choice of signatures. In this thesis, we investigate this
problem. Furthermore, we demonstrate how the introduced techniques
can be applied to a problem in sequential logic verification, the
problem of establishing the unknown correspondence of the latches
(memory elements) of two sequential circuits which have the same
state encoding. Experimental results on a large number of examples
establish the efficacy of the introduced methods.