Skip to main content

2022 | Buch

Verbessertes virtuelles Prototyping

Mit RISC-V-Fallstudien

share
TEILEN
insite
SUCHEN

Über dieses Buch

Dieses Buch stellt eine umfassende Reihe von Techniken vor, die alle wichtigen Aspekte eines modernen Virtual Prototype (VP)-basierten Entwurfsablaufs verbessern. Die Autoren legen den Schwerpunkt auf automatisierte formale Verifikationsmethoden sowie auf fortgeschrittene, abdeckungsgeleitete Analyse- und Testtechniken, die auf SystemC-basierte VP und die zugehörige Software (SW) zugeschnitten sind. Die Abdeckung umfasst auch VP-Modellierungstechniken, die sowohl funktionale als auch nicht-funktionale Aspekte behandeln, und beschreibt zudem Korrespondenzanalysen zwischen der Hardware- und VP-Ebene, um die auf verschiedenen Abstraktionsebenen verfügbaren Informationen zu nutzen. Alle Ansätze werden ausführlich diskutiert und anhand mehrerer Experimente evaluiert, um ihre Effektivität bei der Verbesserung des VP-basierten Entwurfsablaufs zu demonstrieren. Darüber hinaus legt das Buch einen besonderen Schwerpunkt auf den modernen RISC-V ISA, mit mehreren Fallstudien, die sowohl Aspekte der Modellierung als auch der VP- und SW-Verifikation abdecken.

Inhaltsverzeichnis

Frontmatter
1. Einführung
Zusammenfassung
Virtuelle Prototypen (VPs) spielen eine sehr wichtige Rolle bei der Bewältigung der steigenden Komplexität im Entwurfsablauf von eingebetteten Geräten. Ein VP ist im Wesentlichen ein ausführbares abstraktes Modell der gesamten Hardware (HW) Plattform und wird überwiegend in SystemC TLM (Transaction Level Modeling) erstellt. Im Gegensatz zu einem traditionellen Entwurfsablauf, bei dem zuerst die HW und dann die Software (SW) entwickelt wird, ermöglicht ein VP-basierter Entwurfsablauf die parallele Entwicklung von HW und SW, indem der VP für die frühe SW-Entwicklung und als Referenzmodell für die nachfolgenden Entwurfsablaufschritte genutzt wird. Dieser moderne VP-basierte Entwurfsablauf hat jedoch immer noch Schwächen, insbesondere aufgrund des erheblichen manuellen Aufwands für die Verifizierung und Analyse sowie für Modellierungsaufgaben, der sowohl zeitaufwändig als auch fehleranfällig ist. In diesem Kapitel wird der VP-basierte Entwurfsablauf detaillierter vorgestellt und die wichtigsten Beiträge des Buches, die den VP-basierten Entwurfsablauf stark verbessern, werden vorgestellt.
Vladimir Herdt, Daniel Große, Rolf Drechsler
2. Präliminarien
Zusammenfassung
Dieses Kapitel bietet Hintergrundinformationen zu relevanten und allgemeinen Themen für dieses Buch. Zunächst wird SystemC TLM (Transaction Level Modeling) vorgestellt, die Sprache der Wahl zur Erstellung von virtuellen Prototypen (VPs). Dann werden die Hauptkonzepte der RISC-V-Befehlssatzarchitektur (ISA) beschrieben. RISC-V wird in mehreren Evaluierungen und Fallstudien in diesem Buch verwendet und ist die ISA, die in unserem vorgeschlagenen Open-Source RISC-V-basierten VP implementiert ist. Schließlich werden in diesem Kapitel die wichtigsten Konzepte des Coverage-guided Fuzzing (CGF) und der symbolischen Ausführung vorgestellt. Beides sind sehr effektive Techniken für das Testen und Verifizieren von Software und dienen als Grundlage für mehrere in diesem Buch entwickelte Verifikationsansätze.
Vladimir Herdt, Daniel Große, Rolf Drechsler
3. Eine Open-Source RISC-V Evaluierungsplattform
Zusammenfassung
In diesem Kapitel wird ein quelloffener RISC-V virtueller Prototyp (VP) vorgestellt, der in SystemC TLM (Transaction Level Modeling) implementiert ist und das Ziel verfolgt, das RISC-V-Ökosystem zu erweitern. Der VP bietet einen 32/64-Bit-RISC-V-Kern mit einem wesentlichen Satz von Peripheriegeräten und Unterstützung für Multi-Core-Simulationen. Darüber hinaus bietet der VP auch SW-Debugging (über die Eclipse IDE) und Abdeckungsmessungen und unterstützt die Betriebssysteme FreeRTOS, Zephyr und Linux. Der VP ist als erweiterbare und konfigurierbare Plattform konzipiert (als Beispiel stellen wir eine Konfiguration zur Verfügung, die dem RISC-V HiFive1 Board von SiFive entspricht), mit einem generischen Bussystem und in standardkonformem SystemC implementiert. Der letzte Punkt ist sehr wichtig, da er die Nutzung modernster SystemC-basierter Modellierungstechniken ermöglicht, die für die genannten Anwendungsfälle auf Systemebene benötigt werden. Schließlich ermöglicht der VP eine deutlich schnellere Simulation im Vergleich zu RTL und ist dabei genauer als bestehende ISSs. Darüber hinaus integriert der VP ein effizientes Kern-Timing-Modell, das eine schnelle und genaue Leistungsbewertung für RISC-V-basierte Systeme ermöglicht. Das Timing-Modell ist mit dem Kern über eine Reihe klar definierter Schnittstellen verbunden, die die funktionalen von den nicht-funktionalen Aspekten entkoppeln und eine einfache Rekonfiguration des Timing-Modells ermöglichen.
Vladimir Herdt, Daniel Große, Rolf Drechsler
4. Formale Verifikation von SystemC-basierten Entwürfen durch symbolische Simulation
Zusammenfassung
In diesem Kapitel werden neuartige formale Verifikationsmethoden vorgestellt, die auf SystemC-basierte Entwürfe zugeschnitten sind, um den Verifikationsfluss von virtuellen Prototypen (VPs) zu verbessern. Formale Verifikationsmethoden können die Korrektheit eines SystemC-Entwurfs in Bezug auf eine Reihe von Eigenschaften beweisen. Die formale Verifikation von SystemC-Entwürfen stellt jedoch eine große Herausforderung dar, da sie alle möglichen Eingaben sowie Prozessausführungsreihenfolgen berücksichtigen muss, was den Verifikationsprozess aufgrund des Problems der Zustandsraumexplosion sehr schnell unlösbar machen kann. In diesem Buch wurden fortgeschrittene symbolische Simulationstechniken für SystemC entwickelt, um die Zustandsraumexplosion zu entschärfen. Neben der grundlegenden symbolischen Simulationstechnik, die die Grundlage für eine effiziente Exploration des Zustandsraums bildet, werden in diesem Buch mehrere wichtige Erweiterungen und Optimierungen vorgestellt, wie SSR (State Subsumption Reduction) und CSS (Compiled Symbolic Simulation). SSR unterstützt die Verifikation von zyklischen Zustandsräumen, indem es den erneuten Aufruf symbolischer Zustände verhindert und somit die Verifikation vollständig macht. CSS ist eine ergänzende Technik, die die symbolische Simulations-Engine eng in das zu verifizierende SystemC-Design integriert, um die Verifikationsleistung durch die Unterstützung der nativen Ausführung drastisch zu steigern. Die entwickelten formalen Techniken verbessern den derzeitigen Stand der Technik bei der formalen Verifikation von SystemC-Designs erheblich.
Vladimir Herdt, Daniel Große, Rolf Drechsler
5. Abdeckungsgesteuertes Testen für skalierbare Verifikation virtueller Prototypen
Zusammenfassung
In diesem Kapitel werden fortgeschrittene abdeckungsorientierte Testverfahren vorgestellt, die auf Testfallgenerierung und Simulation beruhen, um formale Verifikationsmethoden zu ergänzen, die immer noch anfällig für eine Explosion des Zustandsraums sein können. Im Vergleich zum bestehenden simulationsbasierten Verifikationsablauf werden in diesem Kapitel stärkere Überdeckungsmetriken sowie fortgeschrittene automatische Testfallgenerierung und -verfeinerungstechniken untersucht. Insbesondere werden die Data Flow Testing (DFT)-Abdeckung und das Coverage-guided Fuzzing (CGF) betrachtet, die sich beide im SW-Bereich als sehr effektiv erwiesen haben und auf die Verifikation von VPs zugeschnitten sind. Für DFT wurde eine Reihe von SystemC-spezifischen Abdeckungskriterien entwickelt, die die SystemC-Semantik der Verwendung von nicht-präemptivem Thread-Scheduling mit Shared-Memory-Kommunikation und ereignisbasierter Synchronisation berücksichtigen. CGF wird für die Verifikation von Instruktionssatzsimulatoren (ISSs) eingesetzt, d. h. ein abstraktes Modell eines Prozessorkerns, und wird durch die Integration von funktionaler Abdeckung und einem auf die ISS-Verifikation zugeschnittenen Mutationsverfahren weiter verbessert.
Vladimir Herdt, Daniel Große, Rolf Drechsler
6. Verifizierung von eingebetteten Software-Binärdateien mit Hilfe virtueller Prototypen
Zusammenfassung
In diesem Kapitel werden effiziente, auf virtuellen Prototypen (VP) basierende Ansätze für die Verifikation von Software (SW) vorgestellt. Sie verbessern den bestehenden VP-basierten SW-Verifikationsablauf durch die Integration stärkerer Überdeckungsmetriken und die Bereitstellung automatischer Testfallgenerierungstechniken sowie die Nutzung formaler Methoden. Die Gewährleistung eines korrekten funktionalen Verhaltens ist sehr wichtig, um Fehler und Sicherheitslücken (wie Pufferüberläufe) zu vermeiden. Der erste Ansatz integriert konkolische Tests in den VP. Im Wesentlichen ist das konkolische Testen eine automatisierte Technik, die sukzessive neue Pfade durch das SW-Programm erkundet, indem sie symbolische Beschränkungen löst, die parallel zur konkreten Ausführung verfolgt werden. Die Integration von konkolischen Tests in VPs ist jedoch aufgrund der komplexen HW/SW-Interaktionen und Peripheriegeräte eine Herausforderung. Die vorgeschlagene Lösung ermöglicht eine hohe Simulationsleistung mit genauen Ergebnissen und vergleichsweise geringem Aufwand für die Integration von Peripheriegeräten mit konkolischen Ausführungsfunktionen. Der zweite Ansatz nutzt modernste CGF in Kombination mit VPs, um eine skalierbare und effiziente Verifikation von eingebetteten SW-Binärprogrammen zu ermöglichen. Zur Steuerung des Fuzzing-Prozesses wird die Abdeckung der eingebetteten SW mit der Abdeckung der SystemC-basierten Peripherie des VPs kombiniert.
Vladimir Herdt, Daniel Große, Rolf Drechsler
7. Validierung von Firmware-basiertem Power Management mit virtuellen Prototypen
Zusammenfassung
Neben einem korrekten Funktionsverhalten ist eine hohe Leistung in Kombination mit einem geringen Stromverbrauch eine wichtige Anforderung für viele eingebettete Systeme. Power-Management-Strategien (PM) können einen großen Beitrag zur allgemeinen Energieeinsparung leisten, indem sie ungenutzte Komponenten in einen stromsparenden Zustand versetzen und sie auf intelligente Art und Weise wieder aufwecken. Aufgrund ihrer Benutzerfreundlichkeit und Flexibilität werden PM-Strategien häufig in SW implementiert. PM-Strategien werden analysiert, indem das nicht-funktionale Verhalten des VPs neben der SW-Ausführung beobachtet wird. In diesem Kapitel werden neuartige VP-basierte Techniken vorgestellt, die auf die Validierung von SW-basierten PM-Strategien zugeschnitten sind. Der Beitrag ist zweifach: Erstens eine eingeschränkte Zufallscodierung zur Spezifizierung abstrakter Workloads, die die Generierung einer großen Testsuite mit verschiedenen Anwendungs-Workload-Merkmalen ermöglicht. Und zweitens ein automatisierter, abdeckungsgesteuerter Ansatz zur Generierung von Workloads, die die Abdeckung im Hinblick auf die PM-Strategien maximieren.
Vladimir Herdt, Daniel Große, Rolf Drechsler
8. Register-Transfer-Ebene Korrespondenzanalyse
Zusammenfassung
In diesem Kapitel werden zwei Ansätze vorgestellt, die eine Korrespondenzanalyse zwischen TLM (Transaction Level Modeling) und RTL (Register-Transfer Level) durchführen, um die auf verschiedenen Abstraktionsebenen verfügbaren Informationen zu nutzen. Der erste Ansatz ermöglicht eine automatisierte TLM-zu-RTL-Eigenschaftsverfeinerung. Er ermöglicht die Umwandlung von High-Level-TLM-Eigenschaften in RTL-Eigenschaften, die als Ausgangspunkt für die Prüfung von RTL-Eigenschaften dienen. Dadurch wird die fehleranfällige und zeitraubende manuelle Umwandlung von Eigenschaften von TLM in RTL vermieden. Der zweite vorgeschlagene Ansatz führt eine RTL-zu-TLM-Fehlerkorrespondenzanalyse durch. Er ermöglicht es, entsprechende TLM-Fehler für transiente Bitflips auf RTL zu identifizieren. Die erzielten Ergebnisse können die Genauigkeit einer VP-basierten Fehlereffektsimulation verbessern. Eine Fehlereffektsimulation funktioniert im Wesentlichen durch das Einbringen von Fehlern in die VP während der SW-Ausführung, um die Robustheit der SW gegenüber verschiedenen HW-Fehlern zu prüfen. Eine solche Analyse ist sehr wichtig für eingebettete Systeme, die in gefährdeten Umgebungen arbeiten oder sicherheitskritische Aufgaben ausführen, um sie z. B. vor Strahlung und Alterung zu schützen.
Vladimir Herdt, Daniel Große, Rolf Drechsler
9. Schlussfolgerung
Zusammenfassung
In den letzten Jahren hat die Komplexität von eingebetteten Geräten stetig zugenommen, wobei verschiedene gegensätzliche Anforderungen bestehen. Einerseits müssen IoT-Geräte intelligente Funktionen mit hoher Leistung bieten, einschließlich Echtzeit-Rechenleistung, Konnektivität und Fernzugriff, sowie Sicherheit und hohe Zuverlässigkeit. Gleichzeitig müssen sie kostengünstig sein, mit extrem wenig Speicher und begrenzten Ressourcen auskommen und sollten darüber hinaus nur eine minimale Energiemenge verbrauchen, um eine sehr lange Laufzeit zu gewährleisten. Um die steigende Komplexität des Entwurfs zu bewältigen, wird ein auf virtuellen Prototypen (VP) basierender Entwurfsablauf eingesetzt. Im Gegensatz zu einem traditionellen Entwurfsablauf, bei dem zuerst die Hardware (HW) und dann die Software (SW) entwickelt wird, ermöglicht ein VP-basierter Entwurfsablauf ein HW/SW-Co-Design, indem der VP für die frühe SW-Entwicklung und als Referenzmodell für die nachfolgenden Entwurfsablaufschritte genutzt wird. Dieser moderne VP-basierte Entwurfsablauf hat jedoch noch Schwächen, insbesondere aufgrund des erheblichen manuellen Aufwands für Verifikations- und Analyseaufgaben, der sowohl zeitaufwändig als auch fehleranfällig ist. Dieses Kapitel fasst die wichtigsten Beiträge des Buches zusammen, die den VP-basierten Entwurfsablauf stark verbessern, und skizziert vielversprechende Ideen für zukünftige Arbeiten zur weiteren Verbesserung des VP-basierten Entwurfsablaufs.
Vladimir Herdt, Daniel Große, Rolf Drechsler
Backmatter
Metadaten
Titel
Verbessertes virtuelles Prototyping
verfasst von
Vladimir Herdt
Daniel Große
Rolf Drechsler
Copyright-Jahr
2022
Electronic ISBN
978-3-031-18174-0
Print ISBN
978-3-031-18173-3
DOI
https://doi.org/10.1007/978-3-031-18174-0