Preprocessing for property checking of sequential circuits on the register transfer level [Elektronische Ressource] = Vorverarbeitung für die Überprüfung von Eigenschaften sequentieller Schaltungen auf der Register-Transfer-Ebene / von Raik Brinkmann

Sujets

• Informatik

Informations

• Publié par: technische_universitat_kaiserslautern
• Publié le: 01 janvier 2004
• Nombre de lectures: 16
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

Preprocessing for Property Checking of Sequential
Circuits on the Register Transfer Level
Vorverarbeitung fur die Uberprufung von Eigenschaften Sequentieller
Schaltungen auf der Register-Transfer-Ebene
Vom Fachbereich Elektrotechnik und Informationstechnik
der Universit at Kaiserslautern
zur Verleihung des akademischen Grades
Doktor der Ingenieurwissenschaften (Dr.-Ing.)
genehmigte Dissertation
von
Dipl.-Inf. Raik Brinkmann
geboren in Brehna
Tag der Einreichung: 2. Juli 2003
Tag der mundlic hen Prufung: 21. November 2003
Dekan des Fachbereichs: Prof. Dr.-Ing. Gerhard Huth
Vorsitzender der
Prufungsk ommission: Prof. Dr.-Ing. Norbert Wehn
Erster Berichterstatter: Prof. Dr.-Ing. Wolfgang Kunz
Zweiter Berich Prof. Dr. Wolfram Buttner
D386, Universit at Kaiserslautern, 2003This work is dedicated to Christiane.iii
Zusammenfassung
Motivation
Integrierte digitale Schaltkreise (ICs) realisieren seit langem schnell und kompakt Schlus-
selfunktionen, besonders in der Informations-, Unterhaltungs- und Kommunikationstech-
nik, sowie in der Fertigungs- und Automobilindustrie. Der Trend, immer gr o ere vollst an-
dige Systeme auf einem einzigen IC zu integrieren, ist in allen Gebieten zu beobachten. Die
Verfugbark eit von solchen ’Systems on a Chip’ (SoC) wird einerseits durch die fortschrei-
tende Erh ohung der Integrationsdichten der verwendeten Halbleiter bestimmt, anderer-
seits von der M oglichkeit vorentwickelte Schaltungsteile, als sog. ’Intellectual-Property-’
(IP-) Bl ocke, zu integrieren.
Sprunge in der technologischen Entwicklung von einer Halbleitergeneration zur n ach-
sten, fuhren bei traditionellen Hableiterprodukten, wie Speichern, zu Phasen des Nach-
fragemangels einerseits und Versorgungsengp assen andererseits. Diese treten als sog.
’Halbleiter-Zyklen’ hervor, welche die Industrie ok onomisch belasten. Da die Nachfrage
nach Systemen weniger stark schwankt als beispielsweise bei Speicherprodukten, versucht
die Halbleiterindustrie durch Fokussierung auf SoC, diese Zyklen zu ub erbruc ken.
Aus technologischer Perspektive k onnen bereits 20 Millionen Gatter und mehr auf
einem IC integriert werden. Es sind bereits ICs mit einer Milliarde Gattern in Sicht. Die
F ahigkeiten, sequentielle Schaltungen solcher Gr o enordn ung im Zeit- und Kostenrahmen
zu entwerfen, begrenzt aber das Potential der SoC-Technik. Um diese Produktivit atsluc ke
zu schlie en, mu fur die verwendeten Bl ocke dabei extreme Qualit at erzielt werden.
Angenommen ein SoC besteht aus sechs Bl ocken, deren korrekte Funktion nach gegen-
w artiger Methodik rudiment ar durch Simulation ub erpruft wurde. Da sich Fehler in den
Komponenten im Gesamtsystem fortp anzen, ist dessen korrekte Funktion wahrscheinlich
nicht gew ahrleistet (Sind beispielsweise die Bl ocke mit einer Wahrscheinlichkeit von 90%
korrekt, ergeben sich nur etwa 50% fur das System.). Dieses potentielle Fehlverhalten muss
dann im Systemtest muhsam ausgeschlossen werden. Abgesehen davon, dass Fehler in den
Bl ocken durch Systemsimulation oft schwierig zu nden sind, sind die Sytemtests sehr
zeitaufwendig, da sie sich nicht auf die Sytemaspekte der Funktion konzentrieren k onnen.
Sollen nun Systeme mit 50 oder gar 100 Bl ocken integriert werden, ist dies nur noch
m oglich, wenn sie den h ochstm oglichen Qualit atsanspruc hen bezuglic h ihrer Funktion
genugen. Andernfalls w are die Systemveri k ation und damit die gesamte Entwicklung zu
kostspielig.
Heute wird die Funktion eines Blocks zumeist durch Simulation ub erpruft. Dies kann
jedoch aufgrund der inherenten Unvollst andigkeit des Ansatzes praktisch nicht zur er-
forderlichen Qualit at fuhren. Um nur einfache Qualit atsstandards zu gew ahrleisten, wer-
den zwischen 60 { 80% des gesamten Entwicklungsaufwandes auf die Simulation verwen-
det. Die Produktivit atsluc ke ist daher vor allem eine Veri k ationskrise.
Formale Methoden bieten die einzige M oglichkeit, die erforderliche Qualit at zu erzie-
len, da sie vollst andig sind. Insbesondere die automatische Uberprufung von formal spezi-
zierten Eigenschaften durch ’Bounded-Model-Checking’ hat in der letzten Zeit an Bedeu-
tung gewonnen, da es die automatische Veri k ation ganzer Bl ocke erlaubt. Dabei bieten
die verwendeten Eigenschaften eine orthogonale Sicht auf die Funktion der Schaltung.
Diese sind jedem Hardware-Entwickler zug anglich, da sie kompakt und, im Gegensatz zu
anderen formalen Methoden, leicht verst andlich sind.iv
Dieser Technik sind jedoch aus Komplexit atsgrunden noch nicht alle Klassen von se-
quentiellen Schaltungen zug anglich. Dies betri t insbesondere gr o ere Schaltungen mit
regul arer Struktur, die beispielsweise durch die Verwendung von Speichern und Bussys-
temen hervor tritt. Ziel der vorliegenden Arbeit ist es, die Anwendbarkeit von Bounded-
Model-Checking auf diese Klasse von Schaltungen auszudehnen.
Uberblick
Die Arbeit beschreibt einen neuen Ansatz zur Vereinfachung von aussagenlogischen Be-
weisproblemen, wie sie beim Bounded-Model-Cheking (BMC) ublic herweise auftreten.
Dieser Ansatz erm oglicht es, bisher unl osbare Beweisaufgaben aus dem BMC in der in-
dustriellen Praxis zu l osen, sowie bereits l osbare Bewen wesentlich e zien ter zu
bew altigen.
Eine Beweisaufgabe besteht darin, zu ub erprufen, ob eine Bool’sche Funktion konstant
wahr ist, bzw. ob eine diese Funktion repr asentierende aussagenlogische Formel allge-
mein gultig ist. Derartige Uberprufungen lassen sich zwar mit Techniken wie Bool’scher
Erfullbark eit (SAT) oder Bin aren Entscheidungsdiagrammen (BDDs) im Prinzip l osen,
doch sto en diese Verfahren in der industriellen Praxis regelm a 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 ndet auf einer dem Ursprungsproblem nahen Repr asentation der
Bool’schen Funktion als sog. Bitvektor-Term statt, da dies eine besonders e zien te und
weitreichende Reduktion begunstigt. Die Reduktion basiert einerseits darauf, die Term-
Repr asentation zu vereinfachen, andererseits auf einer speziellen Zerlegung des Beweis-
problems in Co-Faktoren der repr asentierten Funktion. Diese Co-Faktoren werden je-
weils einzeln vereinfacht und wenn m oglich durch automatische Symmetriebetrachtun-
gen zu Aquivalenzklassen zusammengefasst. In vielen F allen gelingt das Zusammen-
fassen zu einer einzigen Aquivalenzklasse. Es ist im Folgenden ausreichend, aus jeder
Aquivalenzklasse einen beliebigen Repr asentanten auszuw ahlen und fur diesen den Beweis
durchzufuhren. Alternativ k onnen die Repr asentanten ihrerseits weiter zerlegt, verein-
facht und zu neuen Aquivalenzklassen zusammengefasst werden. Auf diese Weise werden
nacheinander Variable eliminiert, und die resultierenden Beweisprobleme massiv verein-
facht.
Reduktion und Zusammenfassung basieren auf Heuristiken und Semi-Entscheidungs-
verfahren fur Aquivalenz und Permutations aquivalenz von Bitvektortermen bzw. den
repr asentierten Bool’schen Funktionen. Diese Verfahren beruhen ihrerseits auf Term-
Rewriting- und Graphenalgorithmen.
Die vorgestellte Reduktionsmethode erm oglicht bereits in einer prototypischen Im-
plementierung die Demonstration messbarer Verbesserungen der Gesamtperformanz fur
BMC in praktisch relevanten Beispielen um ein bis zwei Gr o enordn ungen. Weitere
Steigerung durch Verbesserung der Implementierung und der Heuristiken scheinen durch-
aus m oglich, bedurfen jedoch eines gewissen Implementierungsaufwandes, der den Rah-
men dieser Arbeit gesprengt h atte.
Der entwickelte Ansatz sowie die erzielten Resultate werden im Folgenden beschrieben.v
Problemkonstruktion auf der Register-Transfer-Ebene
In dieser Arbeit wird die Methode des sog. Bounded-Interval-Model-Checking, die eine Ab-
wandlung des bekannten BMC-Ansatzes darstellt, zur Veri k ation sequentieller (digitaler)
Schaltungen benutzt. Sequentielle (digitale) Schaltungen werden zur Uberprufung von
Eigenschaften vermittels BIMC durch Mealy-Maschinen modelliert. Mealy-Maschinen
sind endliche Automaten mit Ausgabe- und Zustandsub ergangsfunktion ub er ein Ein-
und Ausgabealphabet. Eine bestimmte Teilmenge der Zust ande des Automaten wird als
Menge der Startzust ande angesehen. Eine Schaltung mit n Eing angen, m Ausg angen
n mund k Latches hat dann als Ein- und Ausgabealphabet die Mengen B und B , sowie
kdie Zustandsmenge B . Die Bool’schene- und Zustandsub ergangsfunktionen f :O
n k m n k kB B ! B und f : B B ! B werden gew ohnlich als Bool’sche Terme ub erS
Bool’sche Ein-, Ausgabe- und Zustandsvariablen { = (i ;:::;i ), o = (o ;:::;o ) und1 n 1 m
s = (s ;:::;s ) repr asentiert. Basierend auf einem diskreten Zeitmodell ist das sequen-1 k
tielle Verhalten der Mealy-Maschine durch die Bedingungen8t2 N :o =f ({;s ), und0 t O t t
8t2 N :s =f ({;s ) de niert, wobei eine Abarbeitungsfolge am Zeitpunkt t = 0 mit0 t+1 S t t
einem Startzustand beginnt.
Fur die Uberprufung der korrekten Funktion werden zun achst Eigenschaften der Form
p({ ;:::;{ ;o ;:::;o ;s ;:::;s ) ub er beschr ankte Zeitintervalle [t;t + n] durcht+0 t+n t+0 t+n t+0 t+n
eine Eigenschaftssprache spezi ziert, die einer Hardware-Beschreibungssprache (HDL)
ahnlic h ist. Durch rekursives Einsetzen obiger Ausgabe- und Zustandsub ergangsbeding-
0 0ungen wird eine Bool’sche Funktion p ({ ;:::;{ ;s ) konstruiert, so dass au