Digitale Hardware/ Software-Systeme - Part 21

Chia sẻ: Cong Thanh | Ngày: | Loại File: PDF | Số trang:8

Thêm vào BST

Báo xấu

70
lượt xem 3
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Digitale Hardware/ Software-Systeme- P21:Getrieben durch neue Technologien und Anwendungen wird der Entwurf eingebetteter Systeme zunehmend komplexer. Dabei ist eine Umsetzung als Hardware/Software- System heutzutage der Stand der Technik. Die Minimierung von Fehlern im Entwurf dieser Systeme ist aufgrund deren Komplexit¨at eine der zentralen Herausforderungen unserer heutigen Zeit. Bereits heute wird mehr Aufwand in die Verifikation, also in die U¨ berpru¨fung der Korrektheit, eines eingebetteten Systems gesteckt als in den eigentlichen Entwurf....

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Digitale Hardware/ Software-Systeme - Part 21

594 Sachverzeichnis relatives Komplement, 523 konstantes, 276 Mikroarchitektur 291 lineares, 276 mit Ausnahmebehandlung, 293, 311–312 Momentengraph mit dynamischer Instruktionsablaufpla- bin¨ rer, siehe BMD a nung, 293, 313–322 Monitor 103, 107, 189, 323 mit Fließbandverarbeitung, 293–308 Monitorschaltung 323 mit Multizyklen-Funktionseinheit, 293, MPSoC 2 308–311 MTBDD 275 mit Sprungvorhersage, 293, 312–313 Multi-Processor System-on-Chip 2 superskalare, 293 Multigraph 530 Miter 246 MoC 16 Nachbedingung Modallogik 24 st¨ rkste, 431 a model of computation siehe MoC Nebenl¨ uﬁgkeit 43 a Modell Netzwerk 531 heterogenes, 56 Boolesches, 525 Modellpr¨ fer u Interpretation 526 CBMC, 449 Netzwerkkalk¨ l 508 u CMC, 449 NFA 47 F-Soft, 450 Deﬁnition, 47 Java Pathﬁnder, 449 Normalform, konjunktive 247, 543 SATABS, 449 ¨ Null-Aquivalenzproblem 129 SLAM, 449 SPIN, 449 OBDD 535 VeriSoft, 449 reduziertes, siehe ROBDD ZING, 449 OBMD 277 Modellpr¨ fung 26, 106, 156, 178–207 u reduzierter, siehe ROBMD Abstraktionsverfeinerung OFDD 538 von Programmen 425 reduziertes, siehe ROFDD BDD-basierte, 156 Off-Testfall 137 CTL, 179–185 OIDD 460 existentielle, 200 reduziert, siehe ROIDD explizite, 106, 156, 178–188 OKFDD 539 implizite, 106, 185 reduziertes, siehe ROKFDD LTL, 185–188 On-Testfall 137 SAT-basierte, 156 open fault 6 von Hardware 331–345 Operandenbereich 382 von Programmen 422–425 Operator SE-LTL, 473–474 modellogischer, siehe Pfadquantor simulative, 27 temporaler, 73, 76 symbolische, 106, 156, 197–207 Finally 76 BDD-basierte 197–199 Globally 76 SAT-basierte 199–207 Next 76 TCTL, 211–222 Release 76 TLM, 476–484 Until 76 universelle, 200 von Programmen, 422–431 p-use 410, 412 Modulebene 14, 15 Pareto-Optimum 9, 18 Moment Partialordnung 524
Sachverzeichnis 595 Partialordnungsreduktion 158, 172–178 Modellpr¨ fung 211–214 u Partition Pr¨ fung des Zeitverhaltens 207–214 u einer Menge, 523 Zustandsklassen 208 Partitionsblock 523 Zustandsgleichung, 168 path segment simulation 436 PEUF 357 Periode 349 Pfad Petri-Netz 41, 91 deﬁnitionsfreier, 412 Anfangsmarkierung, 41 kritischer, 346 Beschr¨ nktheit, 44, 164 a l¨ ngster, 346 a Deﬁnition, 41 Pr¨ ﬁx, 74 a Dynamisierungsvorschrift, 41 Sufﬁx, 74 Erreichbarkeitsmenge, 44 Pfadberechnung 135 Flussrelation, 41 Pfadberechnungsanpassung 138 Folgemarkierung, 43 Pfadbereich 135 Grundzustand, 157, 165, 167 Pfadbereichsanpassung 138 Inzidenzmatrix eines, 168 Pfadbereichstest 134–139 Kanten, 41 Pfaderg¨ nzung 138 a Kantengewichte, 41 Pfadgewicht 531 Konﬂikt, 43 Pfadquantor 78 Konservativit¨ t, 45, 170 a existentieller, 78 Lebendigkeit, 44 universeller, 78 Marke, 42 Plattformmodell 17 Markierung, 42 point to analysis 449 Markierungsfunktion, 42 Polynom 117 Nachbereich eines Knotens, 42 sparse recursive representation, 118 Netzgraph, 41 verschwindendes, 291 Reversibilit¨ t, 45, 156, 165, 167, 171 a Polynomfunktion 119 Schaltregel, 43 polynomieller Algorithmus 542 schwache Lebendigkeit, 44 Potenzmenge 523 Sicherheit, 44, 156 Pr¨ dikatenabstraktion 426 a starke Lebendigkeit, 44, 167 Pr¨ dikatenintervall 462 a Stelle, 41 Pr¨ dikatenlogik 528 a Kapazit¨ t einer 41 a Alphabet, 528 totes, 44 Deﬁnitionen, 528–529 Transition, 41 erster Ordnung, 23, 528 nicht sichtbare 174 Formel, 528 Schalten einer 43 atomare 528 sichtbare 174 Terme, 528 unabh¨ ngige 172 a Pr¨ dikatensymbol 298 a Veriﬁkation Ordnung eines, 298 aufz¨ hlende 157–167 a uninterpretiertes, 298 strukturelle 157, 167–172 Pr¨ ﬁx a Verklemmungsfreiheit, 44, 164 L¨ nge, 90 a Vorbereich eines Knotens, 41 Latenz, 90 zeitbehaftetes, 45–47 prim¨ rer Ausgang 526 a Deﬁnition 45 prim¨ rer Eingang 526 a Erreichbarkeitsgraph 208 Problemgraph 348 Feuerbereich 208 iterativer, 349, 442 Latenz 213–214 Produktautomat 143, 187
596 Sachverzeichnis Programm Referenztestfall 132 Boolesches, 427 ¨ Regionen-Aquivalenz 216 Programmabh¨ ngigkeitsgraph 375 a Regionenautomat 217 Deﬁnition, 375 register transfer level siehe RTL Programmanalyse Registertransferebene siehe RTL statische, 416–422 Regressionstest 103, 131–132 Programmiersprache 59 regul¨ rer Ausdruck a Ausf¨ hrungsmodell, 59 u sequentiell erweiterter, siehe SERE control-driven 59 Rekonvergenzmodell 11 demand-driven 59 Relation 524 C, 59 antisymmetrische, 524 deklarative, 59 reﬂexive, 524 imperative, 59 symmetrische, 524 Programmveriﬁkation 26, 416–431 transitive, 524 Prototyp 100 requirement siehe Anforderung Prozesskalk¨ l 55 u Resolution 548 Prozessor Ressourcenauslastung 439 superskalarer, 313 RMS-Algorithmus 444 Pseudo-Boolesche Funktion ROBDD 150, 237, 535 Belegung, 274 Isomorphie, 535 PSL 72, 83–88, 188 ITE-Operator, 537 ¨ Uberdeckung, 192 ROBMD 277 Boolesche Ebene, 83–84 Robustheit 5 einfache Teilmenge, 85 ROFDD 538 Monitor, 192–197 ROIDD 460 temporale Ebene, 83–87 ROKFDD 237, 243, 539 Veriﬁkationsebene, 83, 87–88 round robin siehe Round-Robin- PSL-Eigenschaft 85 Algorithmus Ptolemy 91 Round-Robin-Algorithmus 446 RSM 453–454 QBF-Solver 430 Distanzvektor, 453 Qualit¨ t 8 a dynamische Transitionen, 454 Qualit¨ tsanforderung 8 a dynamische Zust¨ nde, 453 a Qualit¨ tsmaß 9, 17 a Indexmenge, 453 Qualit¨ tsmerkmal 8, 17, 18 a Pfad, 454 funktionales, 9 Pr¨ dikat, 453 a nichtfunktionales, 9 Semantik, 454 Quellknoten eines polaren Graphen 531 Zustandsdiagramm dynamisches 453 R¨ cksprungverfahren 545 u statisches 453 konﬂiktgetriebenes, 549 RTC 508–514 R¨ ckw¨ rtstraversierung 147 u a RTL 15 rate-monotonic scheduling siehe RMS-Algorithmus safety siehe Gefahrlosigkeit real time calculus siehe RTC SAT modulo theories siehe SMT Record&Play-Algorithmus 269 SAT-Problem 542 Referenzergebnis 107, 132 SAT-Solver 26, 113, 246, 356, 542–551 Referenzmodell 103 Schaltbereitschaft 43 Referenzstimulus 132 Deﬁnition, 43, 46
Sachverzeichnis 597 Schalten 43 shape analysis 449 Schaltnetz 236 Sicherheit 44 Schaltung sifting 536 asynchrone, 41 Signalverarbeitung 53 kombinatorische, 236, 242 Simulation 27, 101–105 Schaltungsmodell symbolische, 105, 237, 259, 357, 362 iteratives, 259, 331 zuf¨ llige a Schaltungsvereinfachung gesteuerte 102, 111–114 dynamische, 358 Simulator 104–105 Schaltvektor 168 ereignisgesteuerter, 104 Schaltwerk 236, 242 hybrider, 104 Schleifeninvariante 26 zyklenbasierter, 104 Schleifenkonstrukt 56 Sleep-Set-Methode 177–178 Schleifentransformation SMT 26, 365, 552 globale, 380 SMT-Solver 551–556 Schnitt 152 indirekte, 552 Schnittmenge 523 Software-Entwurfsprozess 14 Schnittpunkt 152, 369 Spannbaum 530 SDF-Graph 53 Speziﬁkation 15, 16, 37 Deﬁnition als Petri-Netz, 53 ausf¨ hrbare, 38, 39, 59 u Iteration, 226 Deﬁnition, 37 Konsumptionsrate, 53 eindeutige, 38 Produktionsrate, 53 formale, 37 Repetitionsvektor, 226 informale, 37 zeitbehafteter, siehe TSDF-Graph korrekte, 38 SDF-Modell 91 vollst¨ ndige, 38 a SE-LTL 472 Speziﬁkationsfehler 5 Modellpr¨ fung, 473–474 u Sprache Semantik, 472 einer temporalen Struktur, 467 Syntax, 472 eines B¨ chi-Automaten, 186 u Semaphore 30 Sprachinklusion 106 Senkeknoten eines polaren Graphen 531 state/event-LTL siehe SE-LTL sequential extended regular expression Stellen-Transitions-Netz 41 siehe SERE Stelleninvariante 171 Sequentialit¨ t 43 a Steuerbarkeit 109, 110 Sequenzautomat 358 Stimulation 101 SERE 84, 192 Strukturmodell 17 Abz¨ hlungswiederholung, 85 a Stubborn-Set-Methode 175–177 Bereichswiederholung, 85 stuck-at fault siehe Haftfehler Deﬁnition, 84 stuck-at fault model siehe Haftfehlermo- Fusion, 84 dell GOTO-Operator, 85 Subsumtion 548 Konkatenation, 84 SUV 102 L¨ ngendurchschnitt, 84 a synchroner Datenﬂussgraph siehe Servicefunktion 516 SDF-Graph Servicekennlinie 518 Synchronisation 43 obere, 510 synchronous dataﬂow graph siehe untere, 510 SDF-Graph Shannon-Zerlegung 243, 276, 534 Synthese 4, 15–18
598 Sachverzeichnis System Interpretation, 120 latenzinsensitives, 345 Kanonizit¨ t, 124 a system under veriﬁcation siehe SUV Kompositionsoperatoren, 284–286 Systemabh¨ ngigkeitsgraph 376 a Minimalit¨ t, 125 a SystemC 28, 60–67, 451 Multiplikation, 285–286 als LTS, 468–472 normalisiert, 123 Ereignis, 66 Normalisierung, 122 Kanal, 62, 63 Reduktion, 120 Methode, 62 reduziertes, 122 Modellpr¨ fung, 466–476 u Verschmelzungsregel, 122 Modul, 60 Teilmenge 523 Port, 60, 61 echte, 523 Prozess, 62 nichtnegative, 523 Signal, 62 positive, 523 Thread, 62 Teilmengenkonstruktion 191, 196 SystemCoDesigner 68 Temporale Struktur 73–75, 163 Systemebene 15 als B¨ chi-Automat, 186 u SysteMoC 60, 68–72 attributierte, siehe LTS Aktion, 68 Deﬁnition, 73 Anfangsmarke, 69 Pfad, 74, 467 Konsumptionsrate, 68 Sprache der, 467 Modellpr¨ fung, 452–466 u zeitbehaftete, siehe TTS Produktionsrate, 68 Temporallogik 25 Repr¨ sentation des Zustandsraums, a Test 5 452–464 Testbench 102 W¨ chterfunktion, 68 a Testfall 101 Zustand, 453 datenﬂussorientierter, 391, 400, 410–415 Systemsynthese 15 funktionsorientierter, 391–400 gerichteter, 102 Tableau-Technik 192, 233 kontrollﬂussorientierter, 391, 400–410 Taktdom¨ ne 334 a strukturorientierter, 391, 400–415 Taktzustand zuf¨ lliger, 102 a globaler, 336 zustandsorientierter, 396–400 tardiness 440 Testfallgenerierung 101–102 Tautologie 528 gerichtete, 102 Taylor-Expansions-Diagramm siehe TED zuf¨ llige, 102 a Taylor-Reihen-Entwicklung 118 zur Hardware-Veriﬁkation, 246 Taylorsches Theorem 124 zur Software-Veriﬁkation, 391–415 TCTL 89 Testmustergenerierung siehe ATPG Semantik, 90 Testvektor 253 Syntax, 89 Testvorschrift 112 Zeitschranke, 89 Theorembeweis TDMA-Ablaufplanung 447 automatischer, 25 TED 120–129, 283 Theorembeweiser 106–107 Addition, 284–285 Theorie Deﬁnition, 120 Hintergrund-, 26, 365, 551 Eindeutigkeit, 124 time division multiple access 447 Eliminationsregel, 121 timed computation tree logic siehe TCTL geordnetes, 122 TLM 28, 476
Sachverzeichnis 599 Deﬁnition, 478 strukturorientierte, 103 Eigenschaftspr¨ fung, 484–490 u Zustands-, 397 Initiatormodul, 478 Zweig-, 402 Modellpr¨ fung, 476–484 u ¨ Uberdeckungsmaß 103, 391 Targetmodul, 478 ¨ Uberdeckungstest 401 Transaktion, 476–478 all c-uses-, 414 Transaktion 20 all c-uses/some p-uses-, 414–415 blockierende, 476 all p-uses/some c-uses-, 415 nichtblockierende, 476 all defs-, 413 Transaktionsebene 452 all p-uses-, 414 Transaktionsebenenmodell siehe TLM all p-uses/some c-uses-, 415 Transferfunktion 515 all uses-, 415 Transferzeit 346 Anweisungs-, 401–402 Transition Bedingungs-, 404–406 Aktivierbarkeit, 44, 165 einfacher 404–405 Lebendigkeit, 44 Bedingungs-/Entscheidungs-, 405 neuaktivierte, 46 modiﬁzierter 448 Schaltbereitschaft, 43 Datenkontext-, 448 tote, 44 defs/uses-, 413–415 TSDF-Graph 222–232 Mehrfach-Bedingungs-, 406 Aktor, 222 einfache 406 Verz¨ gerungszeit 223 o Pfad-, 407–410 Aktordurchsatz, 226 strukturierter 408–410 Anfangsmarkierung, 223 required k-tuples, 448 Ausf¨ hrung, 225 u Zweig-, 402–404 selbstplanende 225 ¨ Ubereinstimmungsproblem 294 Durchsatz, 226–228 ¨ Ubergangsfunktion 48, 220, 295 Kanal, 222 erweiterte, 142 Konsumptionsrate, 223 ¨ Ubergangsrelation 47, 49 Pr¨ fung des Zeitverhaltens, 222–232 u ¨ Uberpr¨ fungsstrategien 103 u Produktionsrate, 223 ¨ Uberdeckung Zustand, 223 Zusicherungs-, 391 TTS 89, 213 UIP 550 minimale Latenz, 213 UML 91 mit exakten Verz¨ gerungen, 89 o Unabh¨ ngigkeitsintervall siehe II a ¨ Turing-Aquivalenz 55 Unabh¨ ngigkeitsintervallpartition siehe a Turing-Maschine 24 IIP unit propagtion 544 ¨ Uberapproximation 98, 344 Unterapproximation 342 ¨ Uberdeckung Unvollst¨ ndigkeitssatz 24 a ¨ Ubergangs-, 397 Ursache-Wirkungs-Analyse 392–396 Anweisungs-, 401 Ursache-Wirkungs-Graph 393 Bedingungs-/Entscheidungs-, 405 Ereignis-, 397 V-Modell 13 funktionsorientierte, 103 Validierung 5, 38, 109 Mehrfach-Bedingungs-, 406 Variablendeﬁnition minimale 406 globale, 412 Pfad-, 407 lokale, 412 strukturierte 408 Variablenordnung 119
600 Sachverzeichnis Variablenzugriff Architekturmodellierung, 436–438 globaler, 412 Programmpfadanalyse, 433–436 lokaler, 411 Wertebereich Vereinigungsmenge 523 abstrakter, 419 Verfeinerung 17, 18 lineare Kongruenzen 422 Verhalten 37 nichtrelationaler 419 Verhaltensmodell 16 relationaler 419, 421 ausf¨ hrbares, 59 u Intervall-, 419 formales, 41 Kongruenz-, 419, 421 Verhaltenssynthese 15 konkreter, 419 Veriﬁkation 5 Parit¨ ts-, 421 a Veriﬁkationsaufgabe 21, 95–97 Vorzeichen-, 419 Veriﬁkationsbereich 374 window permutation 536 Veriﬁkationsmethode 22, 99–107 worst case execution time siehe WCET diversiﬁzierende, 130 formale, 99, 105–107 X-Diagramm 35 hybride, 101, 107 der Synthese, 16 simulative, 100–105 f¨ r die Veriﬁkation, 20–22 u unvollst¨ ndige, 99, 100 a vollst¨ ndige, 99 a Y-Diagramm 35, 490 Veriﬁkationsmethodik 95 Veriﬁkationsprozess 11–22 Zeitanalyse 345 Veriﬁkationsvollst¨ ndigkeit 103–104, 400 a auf Systemebene, 490–520 Veriﬁkationsziel 95, 97–99 kompositionale 499–508 Verklemmung 44 modulare 508–520 Verschmelzungspunkt 271 dynamische, 348 Verschmelzungsregel 535, 538 f¨ r Hardware, 345 u Versetzungsfunktion 462 auf Architekturebene 348–351 inverse, 466 auf Logikebene 345–348 Verzweigung 53 Hardware, 356 als Kontrollstruktur, 56 kompositionale, 499–508 Verzweigungsliteral 544 Schaltung Verzweigungsstrategie synchroner 345–351 DLCS, 545 Software, 431–448 DLIS, 545 statische, 345 MOM, 546 symbolische, siehe SymTA/S VSIDS, 546 System Vielzweckrechner 1 latenzinsensitives 351–356 Volladdierer 29 Systemebene Vollst¨ ndigkeitskriterium 400 a simulative 492–499 Vorbedingung WCET, 432–436 schw¨ chste, 431 a Zeitschranke, 491 Vorw¨ rtstraversierung 145 a obere 491 VPC 492 untere 491 Zeitbewertungsmodell Wald 530 Zeitbewertungsnetzwerk, 512 Wartezeit 439 Zeitschranke 45 WCET 432 Zeitschrittsimulation 259 WCET-Analyse 432–438 Zeitstruktur 220
Sachverzeichnis 601 Zeitzone 219 regul¨ rer, siehe RSM a Zerlegung Zustandsdiagramm 48 momentenbasierte, 275 Zustandsexplosion 32 Zonenautomat 219 Zustandsraumexplosion 105, 172 Zur¨ ckverfolgung 249, 545 u Zustandsraumreduktion chronologische, 548 durch Schleifenabwicklung, 424–425 nichtchronologische, 545, 549 Zustandsraumtraversierung 144–151 Zusicherung 27, 88, 111, 391 r¨ ckw¨ rtsgerichtete, 147 u a Zusicherungssprache 92, 188 symbolische, 148–151 Zustand ablehnender, 190 vorw¨ rtsgerichtete, 145 a abstrakter, 427 Zuverl¨ ssigkeit 6 a akzeptierender, 186, 190 Zuweisungsfunktion 462 Zustands¨ quivalenz 142, 143 a inverse, 466 Zustands¨ bergang 48 u Zweig Zustandsautomat primitiver, 403