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

Fehlersuche durch Post-Silicon-Partnerschaft

Im zweiten Fall wurde das für die formale Verifikation zuständige Team zu Hilfe gerufen, als im Labor ein Fehler entdeckt wurde. Dieser trat in einer im Chip enthalten Reihe von vier Blöcken auf, deren Aufgabe es ist, Daten an ihren Eingängen entgegenzunehmen, zu verarbeiten und an den jeweils nächsten Block weiterzureichen. Der eingebaute Logikanalysator des Chips kann zwar eine Gruppe von Signalen an den Ausgang herausführen, doch bedeutete es für das Laborteam stets eine echte Herausforderung, die richtigen Signale zu ermitteln. Da der Fehler am Ausgang von Block D aufgetreten war, konzentrierte das Team seine Bemühungen auf diesen Schaltungsteil und der Logikanalysator tastete diesen Block ab. Das Formal-Team schrieb auf Basis des illegalen Trace eine End-to-End Property (Bild 4), die von den Eingängen von Block B zu den Ausgängen von Block D reichte. Dabei wurden nur jene Eingangssignale zugelassen, die den Bug verursachten.

Aufgrund des Umfangs der drei Blöcke konvergierte die Property nicht und musste demzufolge in kleinere Abschnitte zerlegt werden. Es galt somit, die nun geschriebene Property von den Eingängen zum Ausgang von Block D mit Eingangs-Constraints zu versehen, die das legale Verhalten am Eingang definieren (Bild 5). Diese Property erwies sich sehr schnell als richtig, womit belegt war, dass sich Block D niemals illegal verhält, solange an seinen Eingängen legale Zustände vorliegen.

Block D wurde auf diese Weise bescheinigt, dass er den gesuchten Bug nicht enthält. Das Post-Silicon-Debug-Team widmete sich nun auf die gleiche Weise Block C und das formal vorgehende Team verifizierte diesen Block, indem zunächst die Prämissen zu den Eingängen von Block D in Ausgangszustände von Block C umgesetzt wurden. Darüber hinaus wurden neue Constraints geschrieben, die nur legale Eingänge an Block C zuließen. Auch hier waren die Propertys binnen Minuten überprüft, sodass nun Block B zum Hauptverdächtigen avancierte. Der Trace am Ausgang dieses Blocks führte das Post-Silicon-Team erwartungsgemäß schnell ans Ziel und brachte den Bug ans Tageslicht.

Deutlich wird an diesem Beispiel vor allem, wie sinnvoll zwei Teams Hand in Hand arbeiten und sich gegenseitig mit Informationen versorgen können, um einen Fehler rasch einzukreisen.

(ID:336406)