Preprocessing for Property Checking of Sequential Circuits on the Register Transfer Level
Vorverarbeitung für die Überprüfung von Eigenschaften Sequentieller Schaltungen auf der Register-Transfer-Ebene
- As the sustained trend towards integrating more and more functionality into systems on a chip can be observed in all fields, their economic realization is a challenge for the chip making industry. This is, however, barely possible today, as the ability to design and verify such complex systems could not keep up with the rapid technological development. Owing to this productivity gap, a design methodology, mainly using pre designed and pre verifying blocks, is mandatory. The availability of such blocks, meeting the highest possible quality standards, is decisive for its success. Cost-effective, this can only be achieved by formal verification on the block-level, namely by checking properties, ranging over finite intervals of time. As this verification approach is based on constructing and solving Boolean equivalence problems, it allows for using backtrack search procedures, such as SAT. Recent improvements of the latter are responsible for its high capacity. Still, the verification of some classes of hardware designs, enjoying regular substructures or complex arithmetic data paths, is difficult and often intractable. For regular designs, this is mainly due to individual treatment of symmetrical parts of the search space by backtrack search procedures used. One approach to tackle these deficiencies, is to exploit the regular structure for problem reduction on the register transfer level (RTL). This work describes a new approach for property checking on the RTL, preserving the problem inherent structure for subsequent reduction. The reduction is based on eliminating symmetrical parts from bitvector functions, and hence, from the search space. Several approaches for symmetry reduction in search problems, based on invariance of a function under permutation of variables, have been previously proposed. Unfortunately, our investigations did not reveal this kind of symmetry in relevant cases. Instead, we propose a reduction based on symmetrical values, as we encounter them much more frequently in our industrial examples. Let \(f\) be a Boolean function. The values \(0\) and \(1\) are symmetrical values for a variable \(x\) in \(f\) iff there is a variable permutation \(\pi\) of the variables of \(f\), fixing \(x\), such that \(f|_{x=0} = \pi(f|_{x=1})\). Then the question whether \(f=1\) holds is independent from this variable, and it can be removed. By iterative application of this approach to all variables of \(f\), they are either all removed, leaving \(f=1\) or \(f=0\) trivially, or there is a variable \(x'\) with no such \(\pi\). The latter leads to the conclusion that \(f=1\) does not hold, as we found a counter-example either with \(x'=0\), or \(x'=1\). Extending this basic idea to vectors of variables, allows to elevate it to the RTL. There, self similarities in the function representation, resulting from the regular structure preserved, can be exploited, and as a consequence, symmetrical bitvector values can be found syntactically. In particular, bitvector term-rewriting techniques, isomorphism procedures for specially manipulated term graphs, and combinations thereof, are proposed. This approach dramatically reduces the computational effort needed for functional verification on the block-level and, in particular, for the important problem class of regular designs. It allows the verification of industrial designs previously intractable. The main contributions of this work are in providing a framework for dealing with bitvector functions algebraically, a concise description of bounded model checking on the register transfer level, as well as new reduction techniques and new approaches for finding and exploiting symmetrical values in bitvector functions.
- Die Arbeit beschreibt einen neuen Ansatz zur Vereinfachung von aussagenlogischen Beweisproblemen, wie sie beim Bounded-Model-Cheking (BMC) üblicherweise auftreten. Dieser Ansatz ermöglicht es, bisher unlösbare Beweisaufgaben aus dem BMC in der industriellen Praxis zu lösen, sowie bereits lösbare Beweisaufgaben wesentlich effizienter zu bewältigen. Eine Beweisaufgabe besteht darin, zu überprüfen, ob eine Bool'sche Funktion konstant wahr ist, bzw. ob eine diese Funktion repräsentierende aussagenlogische Formel allgemein gültig ist. Derartige Überprüfungen lassen sich zwar mit Techniken wie Bool'scher Erfüllbarkeit (SAT) oder Binären Entscheidungsdiagrammen (BDDs) im Prinzip lösen, doch stoßen diese Verfahren in der industriellen Praxis regelmäßig an Grenzen. Ziel der Arbeit ist es, diese Grenzen zu erweitern. Dies wird erreicht, indem das Beweisproblem vor einem Beweisversuch auf eine neuartige Weise reduziert wird. Die Reduktion findet auf einer dem Ursprungsproblem nahen Repräsentation der Bool'schen Funktion als sog. Bitvektor-Term statt, da dies eine besonders effiziente und weitreichende Reduktion begünstigt. Die Reduktion basiert einerseits darauf, die Term-Repräsentation zu vereinfachen, andererseits auf einer speziellen Zerlegung des Beweisproblems in Co-Faktoren der repräsentierten Funktion. Diese Co-Faktoren werden jeweils einzeln vereinfacht und wenn möglich durch automatische Symmetriebetrachtungen zu Äquivalenzklassen zusammengefasst. In vielen Fällen gelingt das Zusammenfassen zu einer einzigen Äquivalenzklasse. Es ist im Folgenden ausreichend, aus jeder Äquivalenzklasse einen beliebigen Repräsentanten auszuwählen und für diesen den Beweis durchzuführen. Alternativ können die Repräsentanten ihrerseits weiter zerlegt, vereinfacht und zu neuen Äquivalenzklassen zusammengefasst werden. Auf diese Weise werden nacheinander Variable eliminiert, und die resultierenden Beweisprobleme massiv vereinfacht. Reduktion und Zusammenfassung basieren auf Heuristiken und Semi-Entscheidungsverfahren für Äquivalenz und Permutationsäquivalenz von Bitvektortermen bzw. den repräsentierten Bool'schen Funktionen. Diese Verfahren beruhen ihrerseits auf Term-Rewriting- und Graphenalgorithmen. Die vorgestellte Reduktionsmethode ermöglicht bereits in einer prototypischen Implementierung die Demonstration messbarer Verbesserungen der Gesamtperformanz für BMC in praktisch relevanten Beispielen um ein bis zwei Größenordnungen. Weitere Steigerung durch Verbesserung der Implementierung und der Heuristiken scheinen durchaus möglich, bedürfen jedoch eines gewissen Implementierungsaufwandes, der den Rahmen dieser Arbeit gesprengt hätte.
Author: | Raik Brinkmann |
---|---|
URN: | urn:nbn:de:bsz:386-kluedo-16675 |
Advisor: | Wolfgang Kunz |
Document Type: | Doctoral Thesis |
Language of publication: | English |
Year of Completion: | 2003 |
Year of first Publication: | 2003 |
Publishing Institution: | Technische Universität Kaiserslautern |
Granting Institution: | Technische Universität Kaiserslautern |
Acceptance Date of the Thesis: | 2003/11/21 |
Date of the Publication (Server): | 2004/02/02 |
Tag: | Bitvektor; Permutationsäquivalenz RTL; bitvector; bounded model checking; preprocessing; property cheking; satisfiability; sequential circuit; symmetry; verification |
GND Keyword: | Verifikation; Model checking; Symmetrie; Symmetriebrechung; Vorverarbeitung; Zugesicherte Eigenschaft; System-on-Chip; Schaltwerk; Erfüllbarke |
Faculties / Organisational entities: | Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik |
CCS-Classification (computer science): | B. Hardware / B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION / B.5.2 Design Aids |
DDC-Cassification: | 6 Technik, Medizin, angewandte Wissenschaften / 620 Ingenieurwissenschaften und Maschinenbau |
Licence (German): | Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011 |