Die Münchner EDA-Firma OneSpin Solutions ist auf formale Verifikationslösungen spezialisiert, die den Funktionsnachweis vereinfachen und beschleunigen und dabei die bestmögliche funktionale Qualität für ASICs und FPGAs sicherstellen. Regelmäßig machen CEO Peter Feist und sein Team durch richtungsweisende Weiterentwicklungen auf sich aufmerksam. Nun ist ihnen einmal mehr ein technologischer Durchbruch gelungen, und zwar für die standardisierte Eigenschaftssprache SVA.

Die neue Software von OneSpin beinhaltet eine SVA-Timing Diagram Assertion Library (kurz TIDAL), mit der es sehr einfach ermöglich ist, Timing-Diagramme in SVA-Eigenschaften umzusetzen. Timing-Diagramme werden häufig angewendet, um auf Modulebene Operationen und Verhalten zu spezifizieren. Benutzer des 360 Module Verifier (360 MV) von OneSpin können damit auch deren GapFreeVerification-Prozess mit SVA einsetzen und dadurch den Verifikationsaufwand bei gleichzeitiger Gewähr höchstmöglicher Qualität reduzieren.

„Unsere Kunden verlangten einen Verifikationsprozess, der die automatische Lückenauffindung für standardisierte SystemVerilog Assertions ermöglicht“, konstatiert Peter Feist, President und CEO von OneSpin, „durch die Kombination aus TIDAL-Bibliothek, 360 MV mit Unterstützung von SVA und dem GapFreeVerification-Prozess bieten wir nun die industrieweit einzige lückenlose SVA-basierte Verifikationslösung an. Sie verbessert Produktivität, Anwendbarkeit und Kapazität formaler Verifikationswerkzeuge und sichert die höchstmögliche Verifikationsqualität.“

Ab Ende Juni sind die SVA-basierte GapFreeVerification und TIDAL ohne Zusatzkosten in der Version 5.0 von 360 MV integriert. Bisher unterstützte 360 MV vollautomatische RTL-Überprüfungen und die Verifikation von implementationsnahen SVA-Zusicherungen sowie in SVA geschriebenen funktionalen Anforderungen. Die aktuellen Innovationen machen 360 MV und den GapFreeVerification-Prozess zur derzeit umfassendsten formalen SVA-Verifikationslösung, „die den Verifikationsaufwand im Vergleich zu Testansätzen, die auf hohe Qualität abzielen, um bis zu 80 Prozent reduziert und ist auf Designs mit einer Größe von weit über 100.000 Zeilen RTL-Code anwendbar. 360 MV verfügt damit über die höchste Kapazität unter allen in der EDA-Industrie derzeit verfügbaren formalen Verifikationslösungen“ (Feist).

Die neue, auf SVA anwendbare Version des GapFreeVerification-Prozesses ist laut OneSpin der erste in sich geschlossene SVA-basierte Verifikationsprozess. Durch das patentierte, automatische Auffinden von Verifikationslücken mit Hilfe von 360 MV werden sowohl nicht verifizierte RTL-Funktionalität als auch Lücken oder Fehler in der Spezifikation aufgedeckt, sodass sich Verifikationsplanung und Eigenschaftenerstellung erheblich vereinfachen. Es werden außerdem keine Abdeckungsmodelle (Coverage) mehr benötigt, und es entfallen die Sammlung und die zeitaufwändige Analyse von Abdeckungsdaten, um die erreichte Verifikationsqualität zu bestimmen und zu verbessern. Mit dem automatischen Auffinden von Verifikationslücken durch 360 MV werden erstmals die Verifikationsplanung, die Ausführung der Verifikation und die Analyse der Verifikationsqualität in einem geschlossenen, hoch-automatisierten Prozess zusammengeführt, um gleichzeitig die Produktivität und Qualität der Verifikation signifikant zu erhöhen.

TIDAL unterstützt den intuitiven Operations-basierten Verifikationsansatz von 360 MV. Benutzer können Timing-Diagramme, die das erwartete Verhalten von Operationen auf Modulebene beschreiben, direkt in entsprechende SVA-Eigenschaften umsetzen. Anschließend können Benutzer durch die Verwendung der automatischen Lückenauffindung systematisch die Qualität des Eigenschaftssatzes untersuchen und verbessern. Die TIDAL-Sprachelemente, die im standardisierten SVA-Sprachumfang implementiert sind, erlauben es Anwendern, das gewohnte Konzept der Timing-Diagramme in der formalen Verifikation einzusetzen, wodurch der GapFreeVerification-Prozess sowohl für Neulinge als auch erfahrene Anwender der formalen Verifikation leicht erlernbar und einsetzbar ist.