Skip navigation
Please use this identifier to cite or link to this item: http://dx.doi.org/10.25673/2993
Title: A signature-based approach to formal logic verification
Author(s): Mohnke, Janett
Granting Institution: Martin-Luther-Universität Halle-Wittenberg
Issue Date: 1999
Extent: Online Ressource, Text + Image
Type: Hochschulschrift
Language: English
Publisher: Universitäts- und Landesbibliothek Sachsen-Anhalt
URN: urn:nbn:de:gbv:3-000000270
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.
URI: https://opendata.uni-halle.de//handle/1981185920/9778
http://dx.doi.org/10.25673/2993
Open access: Open access publication
Appears in Collections:Hochschulschriften bis zum 31.03.2009

Files in This Item:
File Description SizeFormat 
prom.pdf688.76 kBAdobe PDFThumbnail
View/Open
Show full item record BibTeX EndNote


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.