Interaktive Open-Source-Schnittstelle zur formalen Verifikation von Chipdesigns

Die formale Verifikation ist eine zentrale Komponente der vollständigen Schaltungs-Entwurfsumgebung in der Halbleiter-Chipentwicklung. Das Hardware-Model-Checking, eine automatisierte Erreichbarkeitsprüfung von Schaltungszuständen, ist hierin eine Kerntechnologie der formalen Verifikation. Darüber hinaus wird Model-Checking für zahlreiche weitere tragende Anwendungen in der Chipentwicklung eingesetzt. Beispiele sind Teilprobleme der Synthese, Äquivalenzprüfungen, Informationsflussanalysen, Fehlertoleranzanalysen und Mutations-Testing. Das Ziel dieses Forschungs- und Entwicklungsprojektes ist die Entwicklung einer modernen Model-Checking API für Werkzeuge der Chipentwicklung und einer modernen grafischen Nutzerschnittstelle (GUI) für die formale Verifikation – unter Einbeziehung des Open-Source-Waveform-Viewers Surfer. Zudem soll der Funktionsumfang der API, neben konventioneller Funktionalitäten, um das für das Hardware-Model-Checking neue Konzept der inkrementellen API erweitert werden. Damit wird eine innovative inkrementelleund interaktive formale Verifikation (ININV) für Hardware-Designs ermöglicht, welche als integrierter Bestandteil der OSS-CAD-Suite - einer umfangreichen Open-Source-Entwurfsumgebung zum digitalen Halbleiter-Schaltungsentwurf - höchst effizient eingesetzt wird.