A signature-based approach to formal logic verification

Abstract

In der vorliegenden Arbeit untersuchen wir das Problem, für zwei Boolesche Funktionen zu testen, ob es eine Permutation ihrer Eingangsvariablen gibt, unter der diese Funktionen äquivalent sind. Eine Lösung für dieses Problem ist in verschiedenen Gebieten der Synthese und Verifikation kombinatorischer Schaltkreise von Nutzen. In der Logikverifikation findet es dann Verwendung, wenn die genaue Zuordnung der Eingangsvariablen der zu verifizierenden Schaltkreise nicht mehr bekannt ist. Das Problem ist NP-schwer, weshalb auf heuristische Lösungsansätze zurückgegriffen werden muß. Der Lösungsansatz, der in dieser Arbeit vorgestellt wird, berechnet für jede der Eingangsvariablen einer Booleschen Funktion Signaturen. Diese Signaturen sollen helfen, eine für Permutationsäquivalenz gültige Zuordnung der Variablen auszuwählen. Signaturen sind für eine große Anzahl der getesten Beispiele sehr wirkungsvoll. Leider gibt es auch oft Variablen, die nicht eindeutig identifiziert werden können. Interessanterweise gehören zu dieser Menge, für ein gegebenes Beispiel, immer nahezu dieselben Variablen - unabhängig von der verwendeten Signatur. In der vorliegenden Arbeit wird dieses Problem eingehend untersucht. Außerdem zeigen wir, wie die vorgestellten Methoden zur Lösung eines Problems der Verifikation sequentieller Schaltkreise herangezogen werden können, dem Problem, eine Zuordnung der Speicherelemente zweier sequentieller Schaltkreise zu finden, wenn diese nicht mehr bekannt ist, man aber weiß, daß die Zustände beider Schaltkreise mit der gleichen Methode kodiert wurden. Die Effizienz der in dieser Arbeit vorgestellten Methoden wird anhand einer Vielzahl von Experimenten veranschaulicht.

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 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.