دانلود کتاب Verbessertes virtuelles Prototyping: Mit RISC-V-Fallstudien

فهرست مطالب :

Vorwort\nDanksagung\nInhaltsverzeichnis\nListe der Algorithmen\nAbbildungsverzeichnis\nTabellenverzeichnis\nKapital 1: Einführung\n 1.1 Auf virtuellen Prototypen basierender Entwurfsablauf\n 1.2 Buchbeitrag\n 1.3 Buchorganisation\nKapital 2: Präliminarien\n 2.1 SystemC TLM\n 2.1.1 TLM-basierte Kommunikation\n 2.1.2 Semantik der Simulation\n 2.2 RISC-V\n 2.2.1 ISA-Übersicht\n 2.2.2 Erweiterung des Atomic Instruction Set\n 2.3 Abdeckungsgesteuertes Fuzzing\n 2.3.1 LibFuzzer-Kern\n 2.3.2 LibFuzzer Erweiterungen\n 2.4 Symbolische Ausführung\n 2.4.1 Übersicht\n 2.4.2 Beispiel\nKapital 3: Eine Open-Source RISC-V Evaluierungsplattform\n 3.1 RISC-V-basierter virtueller Prototyp\n 3.1.1 RISC-V-basierte VP-Architektur\n 3.1.1.1 RV32/64 (Multi-)Core\n 3.1.1.2 TLM 2.0 Bus\n 3.1.1.3 Traps und Interrupts\n 3.1.1.4 Systemaufrufe\n 3.1.1.5 VP-Initialisierung\n 3.1.1.6 Timing-Modell\n 3.1.2 VP Interaktion mit SW und Umwelt\n 3.1.2.1 Unterbrechungsbehandlung und HW/SW-Interaktion\n 3.1.2.2 Interaktion mit der Umgebung: Syscall-Emulation und C/C++-Bibliothek\n 3.1.3 VP Leistungsoptimierungen\n 3.1.3.1 Direkte Speicherschnittstelle\n 3.1.3.2 Lokale Zeitquanten\n 3.1.4 Simulation von Multi-Core-Plattformen\n 3.1.4.1 Beispiel Bare-Metal Multi-Core SW\n 3.1.4.2 Implementierung der atomaren ISA-Erweiterung\n 3.1.5 VP Erweiterung und Konfiguration\n 3.1.5.1 Erweitern der VP mit einem Sensor-Peripheriegerät\n 3.1.5.2 Erweiterung der SW-Debugging-Unterstützung\n 3.1.5.3 HiFive1 Board Konfiguration\n 3.1.6 VP Bewertung\n 3.1.6.1 Prüfung\n 3.1.6.2 Leistungsbewertung\n 3.1.7 Diskussion und zukünftige Arbeit\n 3.2 Schnelle und akkurate Leistungsbewertung für RISC-V\n 3.2.1 Hintergrund: HiFive1-Karte\n 3.2.2 Kern-Timing-Modell\n 3.2.2.1 Übersicht\n 3.2.2.2 Zeitmodell für Pipelines\n 3.2.2.3 Zeitmodell für die Zweigvorhersage\n 3.2.2.4 Cache-Timing-Modell\n 3.2.3 Experimente\n 3.2.4 Diskussion und zukünftige Arbeit\n 3.3 Zusammenfassung\nKapitel 4: Formale Verifikation von SystemC-basierten Entwürfen durch symbolische Simulation\n 4.1 Zustandsbezogene symbolische Simulation\n 4.1.1 SystemC Intermediate Verification Language\n 4.1.2 Übersicht Symbolische Simulation\n 4.1.2.1 Ausführungsstatus\n 4.1.2.2 Symbolisches Ausführungssystem (SymEx)\n 4.1.2.3 Partial Order Reduction (POR)\n 4.1.2.4 Zustandsloser Scheduler\n 4.1.3 Zustand Subsumtionsreduzierung (SSR)\n 4.1.3.1 Motivierendes Beispiel\n 4.1.3.2 Schwache Erreichbarkeit\n 4.1.3.3 Zyklusvorbehalt\n 4.1.3.4 Zustandsabhängiger Scheduler\n 4.1.4 Überprüfung der symbolischen Subsumtion\n 4.1.4.1 Exakte symbolische Subsumtion (ESS)\n 4.1.4.2 Optimierungen\n 4.1.5 Experimente\n 4.1.5.1 Bewertung der ESS-Optimierungen\n 4.1.5.2 Vergleich mit KRATOS\n 4.1.6 Diskussion und zukünftige Arbeit\n 4.1.6.1 Pfadzusammenführung\n 4.1.6.2 Dynamische Reduktion von Teilaufträgen\n 4.1.6.3 Heuristiken zur Zustandsübereinstimmung\n 4.2 Formale Verifikation eines Interrupt-Controllers\n 4.2.1 TLM-Peripherie-Modellierung in SystemC\n 4.2.1.1 TLM-Register-Modellierung\n 4.2.1.2 TLM-Drahtmodellierung\n 4.2.2 Überbrückung der Modellierungslücke\n 4.2.3 Fallstudie\n 4.2.3.1 Unterbrechungssteuerung für mehrere Prozessoren\n 4.2.3.2 Formale Verifikation\n 4.2.3.3 Diskussion und zukünftige Arbeit\n 4.3 Kompilierte symbolische Simulation\n 4.3.1 Übersicht\n 4.3.1.1 Übersicht über das generierte C++-Programm\n 4.3.1.2 Datenstrukturen für den Ausführungszustand\n 4.3.1.3 Instrumentierter XIVL-Code\n 4.3.2 Optimierungen\n 4.3.2.1 Pfadzusammenführung\n 4.3.2.2 Native Ausführung\n 4.3.3 Experimente\n 4.3.3.1 Bewertung der nativen Ausführung\n 4.3.3.2 Vergleich mit existierenden SystemC-Verifikatoren\n 4.3.4 Diskussion und zukünftige Arbeit\n 4.4 Parallelisierte kompilierte symbolische Simulation\n 4.4.1 Details zur Implementierung\n 4.4.1.1 PCSS-Bibliothek\n 4.4.1.2 Fork/Join-basierte Zustandsraumuntersuchung\n 4.4.2 Bewertung und Schlussfolgerung\n 4.5 Zusammenfassung\nKapital 5: Abdeckungsgesteuertes Testen für skalierbare Verifikation virtueller Prototypen\n 5.1 Datenflusstests für virtuelle Prototypen\n 5.1.1 SystemC Laufendes Beispiel\n 5.1.2 Def-Use-Zuordnung und Datenflusstest\n 5.1.3 Datenflussprüfung für SystemC\n 5.1.3.1 Übersicht\n 5.1.3.2 Klassifizierung von Datenflussassoziationen\n 5.1.3.3 Erfassungsergebnis\n 5.1.3.4 Abbildung\n 5.1.4 Details zur Implementierung\n 5.1.4.1 Statische Analyse\n 5.1.4.2 Dynamische Analyse\n 5.1.4.3 Konstruktion von Datenflussassoziationen\n 5.1.5 Experimentelle Ergebnisse\n 5.2 Verifizierung von Befehlssatzsimulatoren mit Coverage-Guided Fuzzing\n 5.2.1 Abdeckungsgesteuertes Fuzzing für die ISS-Verifikation\n 5.2.1.1 Übersicht\n 5.2.1.2 Metrik für die funktionale Abdeckung\n 5.2.1.3 Instrumentierung zur Verfolgung der funktionalen Abdeckung\n 5.2.1.4 Benutzerdefinierte Mutationen\n 5.2.2 Fallstudie: RISC-V ISS-Verifikation\n 5.2.2.1 Bewertungseinstellungen und LibFuzzer-Integration\n 5.2.2.2 Evaluationsergebnisse\n 5.2.3 Diskussion und zukünftige Arbeit\n 5.3 Zusammenfassung\nKapitel 6: Verifizierung von eingebetteten Software-Binärdateien mit Hilfe virtueller Prototypen\n 6.1 Concolic Testing von eingebetteten Binärdateien\n 6.1.1 Hintergrund zur konkurrierenden Prüfung von SW\n 6.1.2 Concolic Testing Engine für eingebettete RISC-V-Binärdateien\n 6.1.2.1 Übersicht\n 6.1.2.2 Peripherie Modellierungskonzepte\n 6.1.2.3 Beispiel für Concolic Testing\n 6.1.3 Experimente\n 6.1.3.1 Leistungsbewertung\n 6.1.3.2 Testen des FreeRTOS TCP/IP-Stacks\n 6.1.4 Diskussion und zukünftige Arbeit\n 6.2 Verifikation von eingebetteten Binärdateien mit Coverage-Guided Fuzzing\n 6.2.1 VP-basiertes abdeckungsgeleitetes Fuzzing\n 6.2.1.1 Übersicht\n 6.2.1.2 Erfassung von Abdeckung der SW und Peripherie in dem VP\n 6.2.1.3 Beispiel für Fuzzing von eingebetteten Anwendungen\n 6.2.1.4 Diskussion: Kodierung der funktionalen Abdeckung für eingebettete Systeme\n 6.2.2 Experiment 1: Testen eingebetteter Anwendungen\n 6.2.2.1 Überblick über die Ergebnisse\n 6.2.2.2 Anwendung 1: Datenübertragung\n 6.2.2.3 Anwendung 2: Lüftersteuerung\n 6.2.3 Experiment 2: Testen des Zephyr-IP-Stacks\n 6.2.3.1 Testaufbau\n 6.2.3.2 Benutzerdefinierte IP-Paketmutation\n 6.2.3.3 Erkennung von Heap-Pufferüberläufen\n 6.2.3.4 Ergebnisse\n 6.2.4 Diskussion und zukünftige Arbeit\n 6.3 Zusammenfassung\nKapitel 7: Validierung von Firmware-basiertem Power Management mit virtuellen Prototypen\n 7.1 Ein Constraint-basierter Zufallsansatz für die Workload-Generierung\n 7.1.1 Frühzeitige Validierung von FW-basierten Power-Management-Strategien\n 7.1.1.1 Gesamte Vorgehensweise\n 7.1.1.2 Constraint-basierte Workload-Szenarien\n 7.1.1.3 Constraint-basierter Zufallsgenerator\n 7.1.2 SoCRocket Fallstudie\n 7.1.2.1 Erweiterungen der Energieverwaltung\n 7.1.2.2 Firmware-basierte Energieverwaltung\n 7.1.3 Ergebnisse\n 7.1.4 Diskussion und zukünftige Arbeit\n 7.2 Maximierung der Kreuzabdeckung von Powerzuständen\n 7.2.1 Maximierung der Kreuzabdeckung von Powerzuständen\n 7.2.1.1 Übersicht\n 7.2.1.2 Coverage – Schleife\n 7.2.1.3 Endgültige Testgenerierung\n 7.2.2 Fallstudie\n 7.2.2.1 Blockdefinition und Kalibrierung\n 7.2.2.2 Experimente\n 7.2.3 Diskussion und zukünftige Arbeit\n 7.3 Zusammenfassung\nKapital 8: Register-Transfer-Ebene Korrespondenzanalyse\n 8.1 Auf dem Weg zur vollautomatischen Verfeinerung von TLM-zu-RTL-Eigenschaften\n 8.1.1 UTOPIA Fallstudie\n 8.1.2 Statische Analyse von Transaktoren\n 8.1.2.1 Symbolische Ausführung\n 8.1.2.2 FSM Konstruktion\n 8.1.3 Eigenschaft Verfeinerung\n 8.1.3.1 Sprache zur Spezifikation von Eigenschaften\n 8.1.3.2 TLM-Eigenschaften zur Verfeinerung\n 8.1.3.3 Verfeinerungsprozess\n 8.1.4 Diskussion und zukünftige Arbeit\n 8.2 Automatisierte RTL-zu-TLM-Fehlerkorrespondenzanalyse\n 8.2.1 RTL-zu-TLM-Fehlerkorrespondenzanalyse\n 8.2.1.1 Übersicht und Algorithmus der Korrespondenzanalyse\n 8.2.1.2 Beispiel\n 8.2.2 Formale Analyse der Fehlerlokalisierung\n 8.2.2.1 Anmerkungen\n 8.2.2.2 Logik der symbolischen Fehlerinjektion\n 8.2.2.3 Testbench\n 8.2.3 Fallstudie\n 8.2.3.1 Experimente\n 8.3 Zusammenfassung\nKapital 9: Schlussfolgerung\nLiteratur