Lückenlose Prüfung komplexer Chip-Designs im Post-Silicon-Debugging durch Tools der formalen Verifikation

Anbieter zum Thema

MicroConsult Academy GmbH

MES Electronic Connect GmbH & Co. KG

Cadlog Group

Jasper Design Automation

Formale Verifikation als Rettung

Benötigt wird das passende formale Verifikations-Tool mit hochkarätigen Fähigkeiten: hohe Kapazität für die lückenlose Prüfung umfangreicher Designs mit Tausenden von Blöcken, Fähigkeit zum Prüfen der Integrität von Datentransfers in einem Design (geboten beispielsweise von Jasper Formal Scoreboard und Proof Accelerators). Mehrere Ein- und Ausgangs-Ports ermöglichen die Verifikation vieler verschiedener Arten von Datentransfers.

Zu den entscheidenden Vorteilen formaler Verifikations-Technologien beim Post-Silicon Debugging gehört die Schnelligkeit, mit der Fehler gefunden werden. Das Finden von Gegenbeispielen etwa geht mit formalen Methoden in der Regel deutlich schneller und eignet sich hervorragend für die Fehlersuche. Ein leistungsfähiges Formal-Verification-Tool ermöglicht es dem Anwender, einen bestimmten Zustand in einem bestimmten Zyklus einzufrieren und setzt die Analyse dann an diesem Punkt fort. Es ist deshalb nicht notwendig, das ganze Design auf einmal zu analysieren.

Die Fehlersuche mit formalen Verfahren läuft nahezu nach demselben Muster ab wie die formale Verifikation in der Pre-Silicon-Phase. Es gibt jedoch einige wichtige Unterschiede: Die Suche bezieht sich auf einen bestimmten Fehler und genau ein Szenario. Eine vollständige Abdeckung wird nicht angestrebt. Gesucht wird das Szenario, das zu dem illegalen Verhalten führt. Es ist zulässig, das Szenario aus Einfachheitsgründen künstlich einzuschränken (zum Beispiel können Schreib-Transaktionen unterbunden werden, wenn der Fehler nur im Lesebetrieb auftritt).

Ein IP-Bug mit potenziell katastrophalen Folgen

Hier geht es um das Debugging eines Speicher-Controllers, der sich nicht an das vorgegebene Busprotokoll hielt (Bild 2). Das große SoC mit einem Prozessor und mehreren Peripheriefunktionen hängte sich unter bestimmten Bedingungen auf und wurde deshalb vom Hersteller zurückgerufen.

Es dauerte über drei Monate, bis mit der gerichteten Zufallssimulation die Ursache gefunden war. Sie lag im Speicher-Controller, der seine Daten in einem ganz besonderen Muster an den Wrapper schickte, damit einen Bug in eben diesem Wrapper aktivierte und letztendlich die Protokollverletzung auslöste (Bild 3). Da sich diese ganz besondere zeitliche Beziehung zwischen verschiedenen Ereignissen mithilfe von Zufallssimulationen nur unter größten Schwierigkeiten nachvollziehen ließ, blieb der Fehler unentdeckt und war auch mit Post-Silicon-Simulationen nur extrem schwierig nachweisbar.

Der dreimonatige Zeitaufwand zum Aufdecken der Fehlerquelle stellte ein gravierendes Problem dar, weil sich die mit dem Chip bestückten Produkte bereits in Kundenhand befanden und man somit um einen Rückruf nicht herum kam.

Man brachte anschließend formale Verfahren ein und gab dem zuständigen Ingenieur dieselben Informationen, die auch das Simulations-Team bekommen hatte. Binnen zweieinhalb Wochen war der Fehler gefunden. Allerdings ging der weitaus größte Teil der Zeit auf das Konto der vorbereitenden Arbeiten. Die eigentliche Laufzeit zum Finden des Gegenbeispiels betrug weniger als eine Minute!

Unerwartet war dies keineswegs, denn die formale Methode arbeitet sich auf mathematischem Weg rückwärts den Trace entlang und geht nicht nach dem Zufallsprinzip vor, auch wenn dieses hier etwas zielgerichteter angewandt wird, weil die Betonung von Lese-Transaktionen gelegt wird.

Die formale Verifikation des nachgebesserten RTL-Codes förderte zwei neue, von den Post-Silicon-Simulationen nicht entdeckte, Bugs zutage und ersparte dem Hersteller damit eine weitere Iteration.

(ID:336406)