Formale Verifikation

OneSpin beschleunigt mit automatischer Fehleranalyse formale Assertion-basierte Verifikation

31.07.2009 | Redakteur: Gerd Kucera

Peter Feist, OneSpin: „Mit dem RootCauseAnalyzer können Ingenieure nun alle Sprachmittel von SVA ausnutzen.“

Bis um den Faktor 10 bescheunigt das automatische Werkzeug RootCauseAnalyzer von OneSpin die Fehleranalyse in Assertions und Designs. Der Entwickler hat damit ein Hilfsmittel, um die Ursache zu finden, warum eine Zusicherung bei der funktionalen Verifikation eines RTL-Designs fehlgeschlagen ist.

Das auf umfassende formale Verifikationslösungen spezialisierte EDA-Unternehmen OneSpin Solutions präsentiert ihre neue Technologie: RootCauseAnalyzer. Dieses automatische Fehleranalyse-Tool erleichtert und beschleunigt die Fehlersuche in SystemVerilog-Zusicherungen (Assertions) und RTL-Designs bis um den Faktor 10 und erhöht damit die Produktivität der formalen Assertion-Based Verification (ABV).

RootCauseAnalyzer ist integraler Bestandteil der 360 MV-Lösung und bietet die leistungsstärkste automatische Fehleranalyse, die heute in der formalen ABV verfügbar ist. Das Tool automatisiert einen Großteil der sonst erforderlichen, zeitintensiven manuellen Analyse, um die eigentliche Ursache zu finden, warum eine Zusicherung bei der funktionalen Verifikation eines RTL-Designs fehlgeschlagen ist.

RootCauseAnalyzer reduziert den Aufwand

Peter Feist, President und CEO von OneSpin konstatiert: „Die Suche nach Fehlern in Zusicherungen und Designs verschlingt zwischen 30 und 40 Prozent des gesamten Aufwandes in der funktionalen Verifikation. Mit dem RootCauseAnalyzer können Ingenieure nun alle Sprachmittel von SVA ausnutzen, um zunehmend komplexere Designanforderungen effizient zu verifizieren. Dies ermöglicht signifikante Produktivitätssteigerungen und Qualitätsverbesserungen, beispielsweise beim Erfassen und Verifizieren von komplexen Design-Eigenschaften, -Operationen und -Transaktionen. Hochentwickelte Fehleranalysetechnologie ist der Schlüssel zu diesen Fortschritten.“

RootCauseAnalyzer besteht aus vier eng miteinander verknüpften Analysekomponenten. Diese bilden einen branchenweit einmaligen Analyseablauf, der es ermöglicht, hochautomatisiert die Ursache für fehlgeschlagene Zusicherungen zu ermitteln. Ursachen können Fehler in den Zusicherungen, Fehler im RTL-Quellcode oder fehlende Einschränkungen (Constraints) sein.

Der RootCauseAnalyzer besteht aus vier Komponenten: WaveformAnalyzer, StructuralAssertionAnalyzer, TemporalFaninAnalyzer und ActiveCodeAnalyzer.

Automatische Analyse der Ursachen

• Der WaveformAnalyzer erzeugt Diagnoseinformationen, um die Untersuchung von Gegenbeispielen zu beschleunigen, die das Fehlschlagen einer Zusicherung bewirken.
• Der StructuralAssertionAnalyzer ist ein automatischer SVA-Code-Debugger, der die fehlschlagenden Teile einer Zusicherung präzise lokalisiert. Er zeigt somit dem Benutzer an, welche Teile für die weitere Fehleranalyse relevant sind und identifiziert alle zum Fehler beitragenden Signale und Taktzyklen. Außerdem erzeugt er für alle relevanten Taktzyklen Werteannotationen für alle Teile der Zusicherung (einschließlich der Objekte in referenzierten Sequenzen und Eigenschaften).

Dadurch ermöglicht er erstmalig eine effiziente Fehleranalyse in Zusicherungen, die zur verbesserten Lesbarkeit und Wiederverwendbarkeit hierarchisch mittels Sequenzen und Eigenschaften beschrieben sind. Solche hierarchischen SVA-Zusicherungen verursachen ohne diese Automatisierung sehr hohe manuelle Aufwaende bei der Fehlersuche.

Erstmals eine effiziente Fehleranalyse

• Der TemporalFaninAnalyzer automatisiert die Rückverfolgung kritischer Signale in der Zusicherung auf für die Fehlersuche relevante Signale im Design. Dadurch lassen sich Signalabhängigkeiten über Taktzyklen und Modulgrenzen hinweg automatisch untersuchen.
• Der ActiveCodeAnalyzer kennzeichnet dann die Bereiche im RTL-Quellcode, die für das Fehlschlagen der Zusicherung verantwortlich sind und automatisiert die Identifikation dieser Quellcodebereiche über die entsprechenden Taktzyklen hinweg. Die Fehlersuche im RTL-Quellcode wird dadurch wesentlich zielgerichteter und somit beschleunigt.

Kommentar zu diesem Artikel abgeben

Schreiben Sie uns hier Ihre Meinung ...
(nicht registrierter User)

Spamschutz 

Bitte geben Sie das Resultat dieser Rechenaufgabe (Addition) ein:

Kommentar abschicken

Dieser Beitrag ist urheberrechtlich geschützt. Sie wollen ihn für Ihre Zwecke verwenden? Infos finden Sie unter www.mycontentfactory.de (ID: 312949)