Intel-Keynote über Formal A Mind-Stretcher

Neuauflage von Plato

Verfolger: 0

Synopsys hat auf der SolvNet-Site einen faszinierenden Vortrag von Dr. Theo Drane von Intel Graphics veröffentlicht. Das Thema ist die Äquivalenzprüfung von Datenpfaden. Klingt vielleicht nach einer weiteren formalen DPV-Empfehlung für Synopsys VC, aber Sie sollten es sich trotzdem ansehen. Dies ist eine bewusstseinserweiternde Diskussion über die Verwendung von und Überlegungen in formaler Form, die Sie über die Art der routinemäßigen Benutzerführung hinaus in ein faszinierenderes Gebiet führen wird.

Intel Keynote zum Formalen

Intellektuelles Verständnis versus Stichprobenprüfung

Testgetriebene Simulation in all ihren Formen ist hervorragend und oft unersetzlich, wenn es darum geht, die Korrektheit einer Designspezifikation oder -implementierung zu überprüfen. Auch der Einstieg ist einfach. Schreiben Sie einfach ein Testprogramm und beginnen Sie mit der Simulation. Aber die Kehrseite dieser Einfachheit ist, dass wir es nicht müssen voll verstehen, was wir testen, um loszulegen. Wir überzeugen uns selbst, dass wir die Spezifikation sorgfältig gelesen und alle Eckfälle verstanden haben, aber es braucht nicht viel komplexe Komplexität, um unser Verständnis zu überwältigen.

Formal ermutigt Sie, die Funktionalität auf einer tiefen Ebene zu verstehen (zumindest wenn Sie ein wertvolles Ergebnis liefern möchten). Im obigen Beispiel zeigt eine einfache Frage – kann z jemals nur 1 sein – kein Beispiel in einer Milliarde Zyklen auf einem Simulator. Kein Wunder, denn dies ist ein extremer Eckfall. Ein formaler Test liefert in 188 Sekunden ein spezifisches und sehr nicht offensichtliches Beispiel und kann in etwas kürzerer Zeit beweisen, dass dies der einzige derartige Fall ist.

OK formal hat getan, was dynamisches Testen nicht konnte, aber was noch wichtiger ist, Sie haben etwas gelernt, das Ihnen der Simulator möglicherweise nie gesagt hat. Dass es nur einen möglichen Fall gab, in dem dieser Zustand eintreten konnte. Formal hat Ihnen geholfen, das Design auf intellektueller Ebene besser zu verstehen, nicht nur als probabilistische Zusammenfassung über eine endliche Menge von Testfällen.

Spezifikationsprobleme

Theos nächstes Beispiel basiert auf einem Käferautomaten (so genannt, weil man einen Käfer bekommt, wenn man auf einen Knopf drückt). Dies sieht aus wie ein ziemlich einfaches C-zu-RTL-Äquivalenzprüfungsproblem, C-Modell links, RTL-Modell rechts. Eine Überraschung für Theo in seinen frühen formalen Tagen war, dass das Rechtsverschiebungsverhalten im C-Modell nicht vollständig im C-Standard definiert ist, obwohl gcc sich vernünftig verhalten wird. Allerdings wird DPV wie es sich gehört eine Diskrepanz im Vergleich mit RTL beklagen. Undefiniertes Verhalten ist eine gefährliche Sache, auf die man sich verlassen kann.

Formal wie ein Käferautomat

Der Spezifikationsvergleich zwischen C und RTL birgt andere Gefahren, insbesondere bei Bitbreiten. Das Abschneiden oder der Verlust eines Übertragsbits in einem Zwischensignal (Nr. 3 oben) sind gute Beispiele. Sind das Spezifikationsprobleme? Vielleicht eine Grauzone zwischen Spezifikations- und Implementierungsoptionen.

Jenseits der Äquivalenzprüfung

Der Hauptzweck von DPV scheint es zu sein, die Äquivalenz zwischen einer C- oder RTL-Referenz und einer RTL-Implementierung zu überprüfen. Aber dieser Bedarf ist relativ selten und es gibt andere nützliche Möglichkeiten, wie eine solche Technologie angewendet werden könnte, wenn auch ein wenig out of the box. Zuerst ein Klassiker in der Implementierungswelt – ich habe eine Änderung vorgenommen, einen Fehler behoben – habe ich dadurch neue Fehler eingeführt? Ein bisschen wie die SEQ-Überprüfung, nachdem Sie Clock-Gating hinzugefügt haben. Die Erreichbarkeitsanalyse in Blockausgaben kann in einigen Fällen eine weitere nützliche Anwendung sein.

Nicht nur Gleichwertigkeitsprüfung

Theo wird noch kreativer und bittet die Auszubildenden, Gegenbeispiele zu verwenden, um das Design besser zu verstehen. Sudokus lösen or ganze Zahlen faktorisieren. Er räumt ein, dass DPV eine seltsame Herangehensweise an solche Probleme darstellt, weist jedoch darauf hin, dass seine Absicht darin besteht, die Illusion zu brechen, dass DPV nur zur Überprüfung der Äquivalenz dient. Interessante Idee und sicherlich anstrengend, solche Herausforderungen zu durchdenken. (Ich gestehe, ich fing sofort an, über das Sudoku-Problem nachzudenken, sobald er es erwähnte.)

Wrap up

Theo schließt mit einer Diskussion über Methoden, die für die Produktionsnutzung wichtig sind, rund um Einschränkungen, Regressionen und Vergleiche mit älteren RTL-Modellen. Auch die Herausforderungen, zu wissen, ob das, was Sie überprüfen, tatsächlich mit der Spezifikation der natürlichen Sprache auf oberster Ebene übereinstimmt.

Sehr anregender Vortrag, sehr sehenswert hier auf SolvNet!

Teile diesen Beitrag über: