SystemC Verifikation mittels symbolischer Simulation einer Zwischensprache

Abstract:
Beim Entwurf elektronischer Systeme ist die funktionale Verifikation eine zentrale Aufgabe. Insbesondere gilt es die Korrektheit verschiedener Modelle bereits auf hohen Abstraktionsebenen sicherzustellen, welche häufig in der Systembeschreibungssprache SystemC beschrieben werden. Nur so ist es möglich Fehler frühzeitig zu entdecken (und zu korrigieren) und so enorme Folgekosten zu vermeiden, die sonst durch das „Weitertragen“ eines Fehlers und seiner Auswirkungen (beispielsweise bei Verfeinerungsschritten) entstehen. Die meisten Verifikationsmethoden für SystemC Modelle auf Transaktionsebene (TLM) basieren auf Simulation mit konkretenWerten. Sie können deshalb nur einen kleinen Teil der Funktionalität abdecken, d.h. es können weder alle Fehler entdeckt noch kann die Korrektheit nachgewiesen werden. Darüberhinaus gibt es eine überschaubare Anzahl von formalen Ansätzen, die zwar den Suchraum vollständig explorieren, aber größtenteils für komplexe Modelle nicht skalieren. In dieser Arbeit stellen wir einen neuen Ansatz zur symbolischen Simulation für SystemC vor. Die Basis bildet eine kompakte Zwischensprache, auf die SystemC Modelle abgebildet werden können. Der entwickelte symbolische Simulator integriert zudem verschiedene Such- und Optimierungsstrategien zur Performanzsteigerung. Durch die vollständige Suchraumexploration ist der Simulator in der Lage, alle vorhandenen Fehler (u.a. Zusicherung- und Speicherzugriffsverletzungen) zu finden. Experimentelle Ergebnisse bestätigen die Überlegenheit unseres Verfahrens im Vergleich zu State-of-the-Art Ansätzen.