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

An drei Projekten verdeutlicht der vorliegende Beitrag, wie sich mit Verfahren der formalen Verifikation die unterschiedlichsten Ursachen von Funktionsfehlern ermitteln lassen.

Anbieter zum Thema

MicroConsult Academy GmbH

MES Electronic Connect GmbH & Co. KG

Cadlog Group

Jasper Design Automation

Die Verifikation heutiger Superchips, wie etwa Telecom-Halbleiter, verlangt nach dem Einsatz der bestmöglichen Methodiken und Tools. Unter anderem muss während des gesamten Design-Flows (vom ersten Sondieren der Architektur bis zum Post-Silicon Debugging) auf kapazitätsstarke formale Verifikationstechniken gesetzt werden. Beim Post-Silicon Debugging können formale Verfahren den Teams auch dann einen erheblichen Nutzen bieten, wenn in den bis dahin absolvierten Phasen des Designs kein Gebrauch von formalen Technologien gemacht wurde. Die im vorliegenden Artikel angeführten Fallstudien belegen anschaulich, wie sich mit formalen Verfahren Fehler finden und beheben lassen und wie es außerdem möglich ist, auch die gefundenen Abhilfemaßnahmen zu verifizieren.

Es geht dabei um viel. Am günstigsten kommt man weg, wenn Fehler bereits beim Testen des Modells entdeckt werden, denn bereits im Komponententest schlagen Fehler mit zehnmal höheren Kosten zu Buche und im Systemtest liegen die noch einmal zehnmal höher. Am teuersten wird es für alle, wenn der schlimmste Fall eintritt und ein Bug erst im Feld zutage kommt.

Das Post-Silicon Debugging kann äußerst stressintensiv sein. Wenn der Abgabetermin näher rückt und der Chip immer noch fehlerhaft ist, steht unter Umständen das Unternehmen und damit der eigene Arbeitsplatz auf dem Spiel. Das Management erwartet deshalb, dass Post-Silicon-Bugs schnell eingekreist werden und möchte hierüber von den Design- und Debug-Teams ständig auf dem Laufenden gehalten werden.

Man kann versuchen, die im Labor entdeckten Fehler mit gesteuerten Zufallssimulationen und Emulationen nachzubilden, doch häufig ist dies mit solchen traditionellen Methoden nicht möglich, ohne den gesteckten Zeitrahmen zu sprengen. Hier bewährt sich die formale Verifikation. Sie kann die ursprüngliche Ursache von Bugs eingrenzen und Abhilfemaßnahmen gründlich validieren, auch wenn andere Verfahren nicht zum Ziel geführt haben.

An drei Projekten verdeutlicht der vorliegende Beitrag, wie sich mit formalen Verfahren die Ursachen von Funktionsfehlern ermitteln lassen.

(ID:336406)