Digitale Hardware/Software-Systeme: Spezifikation und Verifikation

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

eXamen.press

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

eXamen.press ist eine Reihe, die Theorie und

Praxis aus allen Bereichen der Informatik fur¨

die Hochschulausbildung vermittelt.

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

Christian Haubelt · Jurgen Teich ¨

Digitale Hardware/

Software-Systeme

Spezifikation und Verifikation

123

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

ISSN 1614-5216

ISBN 978-3-642-05355-9 e-ISBN 978-3-642-05356-6

DOI 10.1007/978-3-642-05356-6

Springer Heidelberg Dordrecht London New York

Die Deutsche Nationalbibliothek verzeichnet diese Publikation in der Deutschen Nationalbibliografie;

detaillierte bibliografische Daten sind im Internet uber http://dnb.d-nb.de abrufbar. ¨

c Springer-Verlag Berlin Heidelberg 2010

Dieses Werk ist urheberrechtlich geschutzt. Die dadurch begr ¨ undeten Rechte, insbesondere die der ¨

Ubersetzung, des Nachdrucks, des Vortrags, der Entnahme von Abbildungen und Tabellen, der ¨

Funksendung, der Mikroverfilmung oder der Vervielfaltigung auf anderen Wegen und der Speicherung in ¨

Datenverarbeitungsanlagen, bleiben, auch bei nur auszugsweiser Verwertung, vorbehalten. Eine

Vervielfaltigung dieses Werkes oder von Teilen dieses Werkes ist auch im Einzelfall nur in den Grenzen ¨

der gesetzlichen Bestimmungen des Urheberrechtsgesetzes der Bundesrepublik Deutschland vom 9.

September 1965 in der jeweils geltenden Fassung zulassig. Sie ist grunds ¨ atzlich verg ¨ utungspflichtig. ¨

Zuwiderhandlungen unterliegen den Strafbestimmungen des Urheberrechtsgesetzes.

Die Wiedergabe von Gebrauchsnamen, Handelsnamen, Warenbezeichnungen usw. in diesem Werk

berechtigt auch ohne besondere Kennzeichnung nicht zu der Annahme, dass solche Namen im Sinne der

Warenzeichen- und Markenschutz-Gesetzgebung als frei zu betrachten waren und daher von jedermann ¨

benutzt werden durften. ¨

Einbandentwurf: KuenkelLopka GmbH

Gedruckt auf saurefreiem Papier ¨

Springer ist Teil der Fachverlagsgruppe Springer Science+Business Media (www.springer.com)

Christian Haubelt

Universitat Erlangen-N ¨ urnberg ¨

Lehrstuhl Hardware-Software-Co-Design

Am Weichselgarten 3

91058 Erlangen

Deutschland

[email protected]

Jurgen Teich ¨

Universitat Erlangen-N ¨ urnberg ¨

Lehrstuhl Hardware-Software-Co-Design

Am Weichselgarten 3

91058 Erlangen

Deutschland

[email protected]

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

Vorwort

Getrieben durch neue Technologien und Anwendungen wird der Entwurf eingebet￾teter Systeme zunehmend komplexer. Dabei ist eine Umsetzung als Hardware/Soft￾ware-System heutzutage der Stand der Technik. Die Minimierung von Fehlern im

Entwurf dieser Systeme ist aufgrund deren Komplexitat eine der zentralen Heraus- ¨

forderungen unserer heutigen Zeit. Bereits heute wird mehr Aufwand in die Verifika￾tion, also in die Uberpr ¨ ufung der Korrektheit, eines eingebetteten Systems gesteckt ¨

als in den eigentlichen Entwurf. Um so erstaunlicher ist es, dass das Thema Veri￾fikation eingebetteter Systeme in der Ausbildung und Lehre nach wie vor keinen

entsprechenden Stellenwert besitzt. Ein uberwiegender Anteil der Lehrveranstaltun- ¨

gen zu diesem Thema konzentriert sich dabei ausschließlich auf die Verifikation von

Hardware oder Software. Aber gerade das Zusammenspiel beider Bestandteile ga￾rantiert die Realisierbarkeit komplexer Systeme und bedarf selbstverstandlich, wie ¨

andere Aspekte, auch der Verifikation.

Dieses Lehrbuch widmet sich der Verifikation digitaler Hardware/Software￾Systeme. Es ist als zweiter Band zu dem Buch ”

Digitale Hardware/Software-Systeme

– Synthese und Optimierung“ [426] konzipiert mit dem Ziel, grundlegende Metho￾den und Verfahren zur Verifikation digitaler Hardware, Software, aber auch von gan￾zen Systemen zu vermitteln. Der Leser wird damit in die Lage versetzt, die Kom￾plexitat und Grenzen der Verifikation zu verstehen sowie Verifikation durchzuf ¨ uhren ¨

und dabei ihre Effektivitat einzusch ¨ atzen. Dies ist die Voraussetzung, um im prak- ¨

tischen Einsatz geeignete Verifikationsziele zu setzen, passende Verifikationsmetho￾den auszuwahlen sowie die damit verbundenen Risiken abzusch ¨ atzen. ¨

Im Gegensatz zu vielen anderen Lehrbuchern, welche oftmals den Schwerpunkt ¨

auf den Aspekt Hardware oder Software legen, zielt der vorliegende Band darauf

ab, dem Leser genau die notwendigen Methoden an die Hand zu geben, um mo￾derne eingebettete Systeme bestehend aus Hardware- und Software-Komponenten

auf ihren korrekten Entwurf hin zu uberpr ¨ ufen. Hierzu geh ¨ ort sowohl die funktiona- ¨

le Verifikation als auch die Verifikation des Zeitverhaltens. Der Stoff ist Lehrinhalt

von Vorlesungen, die teilweise seit mehreren Jahren vom Lehrstuhl fur Hardware- ¨

Software-Co-Design angeboten und mit großer Resonanz von den Studierenden der

Friedrich-Alexander-Universitat Erlangen-N ¨ urnberg angenommen werden. ¨

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

VI Vorwort

Beim Lesen dieses Buches kann man feststellen, dass Verifikationsmethoden fur¨

Hardware und Software auf identischen Prinzipien aufsetzen und ahnliche L ¨ osun- ¨

gen hervorbringen. Dies ist eine analoge Erkenntnis zu der im ersten Band aufge￾zeigten Dualitat f ¨ ur den Entwurf von Hardware und Software. Als gemeinsames ¨

Modell fur beide B ¨ ande dient deshalb das Doppeldachmodell, welches den ideali- ¨

sierten Entwurfsfluss fur digitale Hardware/Software-Systeme darstellt. In diesem ¨

Band wird ein Doppeldachmodell fur den Verifikationsprozess vorgestellt, das zur ¨

Definition grundlegender Verifikationsaufgaben in der Entwicklung von digitalen

Hardware/Software-Systemen dient. Die verwendeten Modellierungsansatze f ¨ ur di- ¨

gitale Systeme, namentlich Petri-Netze, endliche Automaten, Datenflussmodelle so￾wie ausgewahlte heterogene Modelle, bilden eine weitere Gemeinsamkeit beider ¨

Bande. Eine dritte Gemeinsamkeit, die beide B ¨ ande verbindet, ist eine Entwurfsum- ¨

gebung mit dem Namen SystemCoDesigner, welche als aktuelles Forschungsprojekt

am Lehrstuhl fur Hardware-Software-Co-Design an der Universit ¨ at Erlangen-N ¨ urn- ¨

berg entwickelt wird. SystemCoDesigner setzt die im Band Synthese und Optimie￾rung beschriebenen Synthese- und Optimierungsverfahren um und unterstutzt die in ¨

diesem Band beschriebenen Spezifikations- und Verifikationsmethodiken.

Die Autoren mochten Ihren Dank den anonymen Gutachtern des Springer- ¨

Verlags aussprechen, die maßgeblich geholfen haben, die Idee zu diesem Buch zu

fokussieren. Daruber hinaus m ¨ ochten wir uns bei den wissenschaftlichen Mitarbei- ¨

tern bedanken, die durch ihre Ideen und ihr Mitwirken geholfen haben, die Entwurf￾sumgebung SystemCoDesigner zu verwirklichen. Insbesondere mochten wir uns bei ¨

Dipl.-Inf. Michael Glaß, Dipl.-Inf. Martin Streubuhr und Dipl.-Inf. Christian Zebe- ¨

lein bedanken, die durch ihre zahlreichen Vorschlage geholfen haben, das vorliegen- ¨

de Buch zu verbessern. Unserer besonderer Dank gilt Prof. Dr. rer. nat. Rolf Wanka,

der uns in langen Diskussionen geholfen hat, Ergebnisse aus dem Bereich der Theo￾retischen Informatik zu interpretieren. Schließlich mochten wir uns bei Dipl.-Inf. ¨

Jens Gladigau bedanken, der durch seine Kommentare und Anregungen maßgeblich

zum Gelingen dieses Buches beigetragen hat.

Erlangen, im Fr ¨uhjahr 2010 C. Haubelt und J. Teich

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

Inhaltsverzeichnis

1 Einleitung ..................................................... 1

1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

1.2 Der Verifikationsprozess . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

1.2.1 Das V-Modell . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

1.2.2 Das Doppeldachmodell des Entwurfsprozesses . . . . . . . . . . . 14

1.2.3 Das Doppeldachmodell des Verifikationsprozesses . . . . . . . . 18

1.3 Eine kurze Geschichte der Verifikation . . . . . . . . . . . . . . . . . . . . . . . . . 22

1.4 Beispiele . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

1.5 Ausblick . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

1.6 Literaturhinweise . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

2 Spezifikation digitaler Systeme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

2.1 Wie spezifiziert man ein System? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

2.2 Formale Verhaltensmodelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

2.2.1 Petri-Netze . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

2.2.2 Endliche Automaten . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

2.2.3 Datenflussgraphen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

2.2.4 Heterogene Modelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56

2.3 Ausfuhrbare Verhaltensmodelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 ¨

2.3.1 SystemC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

2.3.2 SysteMoC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68

2.4 Formale Spezifikation funktionaler Anforderungen . . . . . . . . . . . . . . 72

2.4.1 Temporale Strukturen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

2.4.2 Temporale Aussagenlogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

2.4.3 Die Zusicherungssprache PSL . . . . . . . . . . . . . . . . . . . . . . . . . 83

2.5 Formale Spezifikation nichtfunktionaler Anforderungen . . . . . . . . . . 88

2.6 Literaturhinweise . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91

3 Verifikation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95

3.1 Verifikationsaufgabe, -ziel und -methode . . . . . . . . . . . . . . . . . . . . . . . 95

3.1.1 Verifikationsziel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

VIII Inhaltsverzeichnis

3.1.2 Verifikationsmethode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99

3.2 Beobachtbarkeit und Steuerbarkeit . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107

3.3 Gesteuerte zufallige Simulation . . ¨ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111

4 Aquivalenzpr ¨ ufung ¨ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115

4.1 Implizite Aquivalenzpr ¨ ufung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 ¨

4.1.1 Kanonische Funktionsreprasentationen . . . ¨ . . . . . . . . . . . . . . . 117

4.1.2 Taylor-Expansions-Diagramme . . . . . . . . . . . . . . . . . . . . . . . . 120

4.1.3 Reduktion und Normalisierung von TEDs. . . . . . . . . . . . . . . . 120

4.1.4 Kanonizitat von TEDs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124 ¨

4.1.5 Implizite Aquivalenzpr ¨ ufung mit TEDs . . . . . . . . . . . . . . . . . . 125 ¨

4.2 Explizite Aquivalenzpr ¨ ufung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 ¨

4.2.1 Regressionstest . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131

4.2.2 Bereichstest . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133

4.2.3 Pfadbereichstest . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134

4.2.4 Fehleroffenbarende Unterbereiche . . . . . . . . . . . . . . . . . . . . . . 139

4.3 Sequentielle Aquivalenzpr ¨ ufung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141 ¨

4.3.1 Automaten-Aquivalenz . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 ¨

4.3.2 Zustandsraumtraversierung . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144

4.3.3 Symbolische Zustandsraumtraversierung . . . . . . . . . . . . . . . . 148

4.3.4 Erzeugung von Gegenbeispielen . . . . . . . . . . . . . . . . . . . . . . . . 151

4.4 Strukturelle Aquivalenzpr ¨ ufung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 ¨

4.5 Literaturhinweise . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154

5 Eigenschaftsprufung ¨ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155

5.1 Prufung funktionaler Eigenschaften . . . . . ¨ . . . . . . . . . . . . . . . . . . . . . . 156

5.1.1 Eigenschaftsprufung auf Erreichbarkeitsgraphen . . . . . . ¨ . . . . 158

5.1.2 Strukturelle Eigenschaftsprufung von Petri-Netzen . . . . . . . . 167 ¨

5.1.3 Partialordnungsreduktion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172

5.2 Explizite Modellprufung. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178 ¨

5.2.1 CTL-Modellprufung. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179 ¨

5.2.2 LTL-Modellprufung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185 ¨

5.2.3 Zusicherungsbasierte Eigenschaftsprufung . . . . . . . . . . . . . . . 188 ¨

5.3 Symbolische Modellprufung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 197 ¨

5.3.1 BDD-basierte CTL-Modellprufung . . . . . . . . . . . . . . . . . . . . . 197 ¨

5.3.2 SAT-basierte Modellprufung . . . . . . . . . . . . . . . . . . . . . . . . . . . 199 ¨

5.4 Prufung nichtfunktionaler Eigenschaften . ¨ . . . . . . . . . . . . . . . . . . . . . . 207

5.4.1 Zeitbehaftete Petri-Netze . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207

5.4.2 Zeitbehaftete Automaten . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 214

5.4.3 Zeitbehaftete SDF-Graphen . . . . . . . . . . . . . . . . . . . . . . . . . . . 222

5.5 Literaturhinweise . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 232

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

Inhaltsverzeichnis IX

6 Hardware-Verifikation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 235

6.1 Aquivalenzpr ¨ ufung kombinatorischer und sequentieller Schaltungen 236 ¨

6.1.1 Implizite Aquivalenzpr ¨ ufung auf der Logikebene . . . . . . ¨ . . . . 236

6.1.2 Explizite Aquivalenzpr ¨ ufung auf der Logikebene . . . . . . ¨ . . . . 246

6.1.3 Formale explizite Aquivalenzpr ¨ ufung von Schaltwerken . . . . 258 ¨

6.1.4 Strukturelle Aquivalenzpr ¨ ufung auf der Logikebene . . . ¨ . . . . 263

6.2 Aquivalenzpr ¨ ufung arithmetischer Schaltungen . . ¨ . . . . . . . . . . . . . . . 273

6.2.1 Implizite Aquivalenzpr ¨ ufung auf der Architekturebene . ¨ . . . . 273

6.2.2 Aquivalenzpr ¨ ufung zwischen Architektur- und Logikebene . 280 ¨

6.2.3 Aquivalenzpr ¨ ufung auf der Architekturebene . . ¨ . . . . . . . . . . . 283

6.3 Formale Verifikation von Prozessoren. . . . . . . . . . . . . . . . . . . . . . . . . . 291

6.3.1 Aquivalenzpr ¨ ufung f ¨ ur Prozessoren mit ¨

Fließbandverarbeitung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 293

6.3.2 Berucksichtigung von Multizyklen-Funktionseinheiten, ¨

Ausnahmebehandlung und Sprungvorhersage. . . . . . . . . . . . . 308

6.3.3 Aquivalenzpr ¨ ufung f ¨ ur Prozessoren mit dynamischer ¨

Instruktionsablaufplanung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 313

6.4 Funktionale Eigenschaftsprufung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 323 ¨

6.4.1 Zusicherungsbasierte Eigenschaftsprufung . . . . . . . . . . . . . . . 323 ¨

6.4.2 SAT-basierte Modellprufung . . . . . . . . . . . . . . . . . . . . . . . . . . . 331 ¨

6.5 Zeitanalyse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 345

6.5.1 Zeitanalyse synchroner Schaltungen . . . . . . . . . . . . . . . . . . . . 345

6.5.2 Zeitanalyse latenzinsensitiver Systeme . . . . . . . . . . . . . . . . . . 351

6.6 Literaturhinweise . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 356

7 Software-Verifikation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 361

7.1 Formale Aquivalenzpr ¨ ufung eingebetteter Software . . . ¨ . . . . . . . . . . . 362

7.1.1 Aquivalenzpr ¨ ufung von Assemblerprogrammen . . . . . . . . . . . 362 ¨

7.1.2 Strukturelle Aquivalenzpr ¨ ufung von Assemblerprogrammen 368 ¨

7.1.3 Aquivalenzpr ¨ ufung von C-Programmen . . . . . . . . . . . . . . . . . 373 ¨

7.2 Testfallgenerierung zur simulativen Eigenschaftsprufung . . . . . . . . . 391 ¨

7.2.1 Funktionsorientierte Testfalle . . . . . . . . . . . . . . . . . . . . . . . . . . 391 ¨

7.2.2 Kontrollflussorientierte Testfalle . . . . . . . . . . . . . . . . . . . . . . . . 400 ¨

7.2.3 Datenflussorientierte Testfalle . . . . . . . . . . . . . . . . . . . . . . . . . . 410 ¨

7.3 Formale funktionale Eigenschaftsprufung von Programmen . . . . . . . 416 ¨

7.3.1 Statische Programmanalyse . . . . . . . . . . . . . . . . . . . . . . . . . . . . 416

7.3.2 SAT-basierte Modellprufung von C-Programmen . . . . . . . . . . 422 ¨

7.3.3 Modellprufung durch Abstraktionsverfeinerung . . . . . . . . . . . 425 ¨

7.4 Zeitanalyse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 431

7.4.1 BCET- und WCET-Analyse . . . . . . . . . . . . . . . . . . . . . . . . . . . 432

7.4.2 Echtzeitanalyse fur Einprozessorsysteme . . . . . . . . . . . . . . . . 438 ¨

7.5 Literaturhinweise . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 448

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

X Inhaltsverzeichnis

8 Systemverifikation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 451

8.1 Funktionale Eigenschaftsprufung von SystemC-Modellen . . . . . . . . . 452 ¨

8.1.1 Symbolische CTL-Modellprufung von SysteMoC-Modellen 452 ¨

8.1.2 Modellprufung von SystemC-Modellen . . . . . . . . . . . . . . . . . . 466 ¨

8.1.3 Formale Modellprufung von Transaktionsebenenmodellen . . 476 ¨

8.1.4 Zusicherungsbasierte Eigenschaftsprufung f ¨ ur¨

Transaktionsebenenmodelle . . . . . . . . . . . . . . . . . . . . . . . . . . . 484

8.2 Zeitanalyse auf Systemebene . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 490

8.2.1 Simulative Zeitbewertung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 492

8.2.2 Kompositionale Zeitanalyse uber Ereignisstr ¨ ome . . . . . . . . . . 499 ¨

8.2.3 Modulare Zeitanalyse mit RTC . . . . . . . . . . . . . . . . . . . . . . . . . 508

8.3 Literaturhinweise . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 520

Anhang . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 523

Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 523

A.1 Mengen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 523

A.2 Relationen und Funktionen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 524

A.3 Aussagenlogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 527

A.4 Pradikatenlogik erster Ordnung . . ¨ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 528

A.5 Graphen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 529

Binare Entscheidungsdiagramme ¨ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 533

B.1 Entscheidungsdiagramme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 533

B.2 Binare Entscheidungsdiagramme ¨ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 534

B.3 Verallgemeinerte binare Entscheidungsdiagramme . . . . ¨ . . . . . . . . . . . 537

Algorithmen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 541

C.1 Klassifikation von Algorithmen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 541

C.2 SAT-Solver . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 542

C.3 SMT-Solver . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 551

C.4 CTL-Fixpunktberechnung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 556

Literatur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 561

Sachverzeichnis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 587

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

1

Einleitung

Dieses einleitende Kapitel vermittelt einen Einblick, warum die Verifikation ein un￾verzichtbarer Bestandteil des Entwurfs von digitalen Hardware/Software-Systemen

darstellt. Dabei werden die wesentlichen Aspekte der Verifikation vorgestellt.

1.1 Motivation

Digitale Hardware/Software-Systeme sind aus der heutigen Gesellschaft nicht mehr

wegzudenken. Oftmals treten sie in Form sog. eingebetteter Systeme auf. Eingebette￾te Systeme sind Computer, die fur einen speziellen Einsatz konzipiert und optimiert ¨

sind. Heutzutage sorgen eingebettete Systeme dafur, dass wir mobil auf Daten zu- ¨

greifen konnen, Autos fahren, Flugzeuge fliegen, Patienten ¨ uberwacht werden etc. ¨

Im Unterschied zu eingebetteten Systemen werden Vielzweckrechner, wie bei￾spielsweise Server und PCs, vorrangig auf deren Rechengeschwindigkeit optimiert.

Wahrend Verlustleistung, Platzbedarf und Kosten bei Vielzweckrechnern eher un- ¨

tergeordnete Ziele sind, werden eingebettete Systeme primar bez ¨ uglich dieser nicht- ¨

funktionalen Ziele optimiert. Eine ausreichende Rechengeschwindigkeit gilt ledig￾lich als Randbedingung, die es zu erfullen gilt. Beispielsweise ist es nicht tolerier- ¨

bar, dass ein Mobiltelefon bereits nach wenigen Minuten oder gar Sekunden die ge￾samte, in einem vollstandig geladenen Akku gespeicherte Energie verbraucht. Auch ¨

gibt es die Kundenanforderungen, dass Mobiltelefone klein und leicht zu sein haben.

Diesen Zielen entgegen stehen allerdings die Forderungen nach immer komplexeren

Anwendungen, die auf dem eingebetteten System ausgefuhrt werden. Ein modernes ¨

Mobiltelefon sollte heutzutage neben den Sprach- und Datendiensten zumindest mit

einer integrierte Digitalkamera, einem MP3-Player und einem Internet-Zugang aus￾gestattet sein. Auch das Abspielen von Videos auf dem Mobiltelefon gehort bereits ¨

zum Standard.

Auch in anderen Bereichen kann man eine zunehmende Komplexitat der An- ¨

wendungen sehen: Ein prominentes Beispiel sind Fahrerassistenzsysteme in heutigen

Fahrzeugen mit gehobener Ausstattung. Neben ABS (Antiblockiersystem) und ESP

C. Haubelt, J. Teich, Digitale Hardware/Software-Systeme, eXamen.press,

DOI 10.1007/978-3-642-05356-6 1, c Springer-Verlag Berlin Heidelberg 2010

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

2 1 Einleitung

(elektronisches Stabilitatsprogramm) geh ¨ oren heutzutage Spur- und Personenerken- ¨

nung sowie Einparksysteme zum Funktionsumfang. Die steigende Komplexitat ist ¨

hierbei auch der Grund, warum immer haufiger eingebettete Systeme aus speziali- ¨

sierten, interagierenden Hardware- und Software-Komponenten bestehen.

Durch den steigenden Funktionsumfang wird auch die Implementierung einge￾betteter Systeme immer komplexer. Zukunftige Systeme werden nicht mehr ledig- ¨

lich aus einem zentralen Prozessor und etwas Zusatzhardware, sondern aus vielen

zusammenwirkenden Prozessorkernen und Hardware-Beschleunigern, die auf einem

einzelnen Chip integriert werden (engl. Multi-Processor System-on-Chip, MPSoC),

bestehen. Ein Beispiel hierfur ist in Abb. 1.1 zu sehen: Man sieht im oberen Teil meh- ¨

rere Prozessoren zu einem Prozessorsubsystem zusammengefasst. Jeder einzelne

Prozessor verfugt ¨ uber einen eigenen Cache f ¨ ur Daten und Instruktionen. Hardware- ¨

Beschleuniger sind in einer eigenen Einheit zusammengefasst. Die Kommunikation

zwischen Prozessoren und Hardware-Beschleunigern erfolgt uber ein blockierungs- ¨

freies Verbindungsnetzwerk. Der Datentransport zwischen Prozessoren und Haupt￾speicher wird durch ein spezielles Speichersubsystem mit eigenem Cache gesteuert,

welches ebenfalls uber das Verbindungsnetzwerk an die anderen Komponenten des ¨

MPSoC angebunden ist. Schließlich ist eine weitere Kommunikationseinheit (I/O)

direkt auf dem Chip integriert, um Daten schnell mit Komponenten außerhalb des

Chips austauschen zu konnen. ¨

L3 Cache

Prozessor-Subsystem

Hardware-Beschleuniger

L2 Cache L2 Cache L2 Cache L2 Cache

Prozessor￾kern kern kern kern

Prozessor- Prozessor- Prozessor￾Speicher-Subsystem

I/O

Verbindungs￾netzwerk

Port Port Port

Beschleunigereinheit

Beschleunigereinheit

Beschleunigereinheit

Beschleunigereinheit

Abb. 1.1. Beispiel eines Mehrprozessorsystems (MPSoC) nach [240]

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

1.1 Motivation 3

Wahrend in Abb. 1.1 noch eine recht ¨ uberschaubare Anzahl an Prozessoren und ¨

Hardware-Beschleunigern zu sehen ist, wird dies in zukunftigen Systemen nicht ¨

mehr so sein. Die International Technology Roadmap for Semiconductors (ITRS)

[240] geht in ihrem Bericht von 2007 davon aus, dass sich das Mooresche Ge￾setz auch auf zukunftige MPSoCs ¨ ubertragen l ¨ asst, d. h. man wird einen exponen- ¨

tiellen Anstieg der Prozessoren auf einem einzelnen Chip feststellen konnen (sie- ¨

he Abb. 1.2). Das Mooresche Gesetz besagt, dass sich die Komplexitat integrierter ¨

Schaltungen etwa alle zwei Jahre verdoppelt. Das Gesetz wurde 1965 von George

Moore aufgestellt [332] und gilt bis heute, wobei Moore mit Komplexitat die Anzahl ¨

der Gatter meinte.

2007

1.000

1.200

2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021 2022

1.400

1.600

800

600

400

200

0

# Prozessoren

Abb. 1.2. Die ITRS geht davon aus, dass im Jahr 2020 nahezu 1.000 Prozessoren auf einem

einzelnen Chip integrierbar sind [240]

Mit steigendem Funktionsumfang erobern eingebettete Systeme immer neue An￾wendungsgebiete in unserem taglichen Leben, so dass sie h ¨ aufig gar nicht mehr als ¨

solche wahrgenommen werden. Diese oftmals unauffalligen Helfer treten h ¨ aufig erst ¨

in unser Bewusstsein, wenn sie ihre Aufgabe nicht mehr zu unserer Zufriedenheit

erfullen oder sich nicht mehr entsprechend ihrer Vorgaben verhalten. Betrachtet man ¨

die enorme Anzahl solcher Systeme, mit denen wir tagtaglich interagieren, so ver- ¨

wundert es nicht, dass es hin und wieder zu Storungen kommt. Aber gerade wegen ¨

dieser ”

wenigen Storungen“ ist es ein beeindruckendes Ph ¨ anomen unserer Gesell- ¨

schaft, dass wir solchen Systemen immer ofter unser Geld oder sogar unser Leben ¨

anvertrauen.

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com

4 1 Einleitung

Korrektheit und Fehler

Als Benutzer eines eingebetteten Systems geht man davon aus, dass dieses korrekt

funktioniert. Diese Erwartung ist aber leider so schwierig zu erfullen, wie sie trivi- ¨

al scheint. Dies beginnt bereits damit, wie sich Korrektheit eigentlich definiert. Der

IEEE-Standard 610.12 [232] definiert die Korrektheit eines Systems auf drei unter￾schiedliche Arten:

1. Korrektheit ist der Grad der Fehlerfreiheit eines Systems in seiner Spezifikation,

in seinem Entwurf und seiner Implementierung.

2. Korrektheit ist der Grad, mit dem ein System die spezifizierten Anforderungen

erfullt. ¨

3. Korrektheit ist der Grad, mit dem ein System die Kundenanforderungen und

Kundenerwartungen erfullt. Unabh ¨ angig davon, ob diese spezifiziert sind oder ¨

nicht.

Hier kann man zumindest bereits erahnen, wie umfangreich der Spielraum bei der

Interpretation von Korrektheit eines Systems ausfallen kann.

Genau dies wird deshalb im Folgenden genauer betrachtet. Hierzu wird zunachst ¨

die Entwicklung eines eingebetteten Systems naher untersucht. Die Entwicklung ei- ¨

nes digitalen Hardware/Software-Systems (siehe Abb. 1.3) beginnt mit der Produk￾tidee. Nach der Anforderungsanalyse entsteht eine Spezifikation, welche die Grund￾lage fur den Entwurfsprozess bildet. Die Umsetzung der Spezifikation in eine Imple- ¨

mentierung wird als Entwurf bezeichnet. Erfolgt die Umsetzung einer Spezifikation

in eine Implementierung automatisch, so spricht man von Synthese [426]. Die Im￾plementierung wiederum ist die Basis fur die Herstellung eines Produktes, welches ¨

anschließend in Betrieb geht.

Spezifikation

Implementierung

Idee

Produkt

Anforderungsanalyse

Entwurf

Herstellung

Betrieb

Abb. 1.3. Entwicklung eines eingebetteten Systems

Simpo PDF Merge and Split Unregistered Version - http://www.simpopdf.com