Formale Verifizierung auf SoC-Ebene schien lange Zeit eine unerreichbare Anforderung zu sein. Vielleicht sollten wir unsere Herangehensweise ändern. Könnte formal auf eine geeignete Abstraktion des SoC praktisch sein? Paul Cunningham (GM, Verification bei Cadence), Raúl Camposano (Silicon Catalyst, Unternehmer, ehemaliger CTO von Synopsys und jetzt CTO von Silvaco) und ich setzen unsere Reihe zu Forschungsideen fort. Feedback wie immer erwünscht.

Die Innovation

Die Auswahl dieses Monats ist Pfad-Prädikat-Abstraktion für Sound-System-Level-Modelle von RT-Level-Schaltungsdesigns. Das in den 2014 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems veröffentlichte Papier. Die Autoren stammen von der Universität Kaiserslautern in Deutschland.

Obwohl das Papier alt ist, ist dies ein würdiges Ziel und hat eine respektable Anzahl von Zitaten. Obwohl es eine begrenzte kommerzielle Entwicklung gegeben hat, ist das Thema für die meisten von uns immer noch ungewohnt. Die Autoren plädieren für eine andere Art der Abstraktion von bekannten Methoden in konventioneller Form. Sie schlagen Path Predicate Abstraction (PPA) vor. Dies zentriert sich um wichtige Staaten im Stufenübergangsdiagramm und Geschäftstätigkeit die mehrzyklische Übergänge zwischen wichtigen Zuständen sind.

Das Papier veranschaulicht die Top-Down-Konstruktion eines beispielhaften PPA als FSM, wobei Makros Zustände definieren und Eigenschaften Operationen als Sequenzen von Übergängen zwischen Zuständen definieren. Makros stellen über Signalnamenreferenzen eine Verbindung zur RTL-Implementierung her. Diese prüfen sie förmlich gegenüber RTL. Darüber hinaus zeigen sie, wie sich eine solche PPA-Zustandsmaschine als solide und vollständig erweisen kann. Sie behaupten, dies zeige eine formal vollständige Abdeckung des abstrakten Diagramms für den SoC.

Pauls Ansicht

Dieses Papier ist schwer zu lesen, aber es ist ein wichtiger Beitrag, der gut zitiert wurde. Das Konzept ist einfach zu verstehen. Erstellen Sie zunächst eine abstrakte Zustandsmaschine, um die Designfunktionalität auf Systemebene zu beschreiben, und beweisen Sie dann, dass eine RTL-Implementierung des Designs seiner Abstraktion entspricht. Die abstrakte Zustandsmaschine wird als Bündel zeitlicher Logikeigenschaften dargestellt, z. B. System Verilog Assertions (SVAs).

Der Nachweis, dass einige RTL einer SVA entsprechen, ist natürlich nicht neu und nicht der Beitrag des Papiers. Der Beitrag ist eine Methode, um das Gegenteil zu beweisen: dass eine Reihe von SVAs uneingeschränkt deckt alle mögliche Verhaltensweisen einiger RTL, relativ zu einer bestimmten Abstraktionsebene.

Das ist ein ziemlich cooles Konzept, und die Autoren öffnen sich mit einer eleganten Art, ihren Ansatz als Form der Farbgebung der Zustände in der RTL-Umsetzung eines Designs zu visualisieren. Sie schließen ihre Arbeit mit zwei ausgearbeiteten Beispielen ab – einem einfachen Busprotokoll und einem seriellen IO-Datenpaket-Framer.

Ich hätte gerne gesehen, dass eines der Beispiele ein rechenzentriertes Design im Vergleich zu einem protokollzentrierten Design ist. Protokollzentrische Designs haben immer eine klare und offensichtliche Zustandsmaschine auf Systemebene, gegen die verifiziert werden kann, und tatsächlich bieten wir bei Cadence eine Bibliothek formaler Protokoll-Proof-Kits an, die sehr ähnlich zu diesem Artikel sind, die wir als Assertion-Based Verification IPs (AB -VIPs kurz).

Aber für ein rechenzentriertes Design fanden wir es viel schwieriger, das beabsichtigte Verhalten mithilfe von Behauptungen und Zustandsmaschinen darzustellen. Ein sequenzieller Äquivalenzprüfungsansatz – entweder zwischen zwei RTL-Versionen oder zwischen einem C/C++-Modell und einer RTL-Implementierung – hat sich im Allgemeinen als besser skalierbar erwiesen.

Raúls Ansicht

Das Kernkonzept besteht darin, die Semantik eines Systemmodells zu definieren, indem Eigenschaften in einer Standard-Eigenschaftensprache wie SystemVerilog-Zusicherungen (SVA) formuliert werden. Wenn diese Eigenschaften unter Verwendung von Standardverfahren zur Eigenschaftsprüfung nachgewiesen werden können, dann ist das Systemmodell eine solide Abstraktion eines RTL-Designs. Es ist wichtig anzumerken, dass das Ziel des Papiers darin besteht, eine Methode aufzuzeigen, um die Äquivalenz zwischen einer Abstraktion und der Grund-RTL herzustellen. Es bietet keine Innovation, um zu einer soliden Abstraktion zu gelangen, beispielsweise um optimale Möglichkeiten zum Einfärben des Diagramms zu finden.

Die vorgeschlagene Methodik wird auf zwei Designs angewendet. Ein flexibler FPI-Bus (Peripheral Interconnect) mit insgesamt ~16,000 Codezeilen. Die Anzahl der Zustandsbits wurde von über 1500 auf nur 38 in 1850 Codezeilen (LoC) reduziert. Ein Property Checker prüfte alle Eigenschaften in 90 Sekunden. Die Autoren schätzten den Aufwand zur Erstellung eines vollständigen Satzes von Eigenschaften für die Verifizierung von SoC-Modulen auf etwa 2000 LoC pro Person und Monat, was ca. 8-Personen-Monat insgesamt.

Ein zweites Beispiel ist ein SONET/SDH-Framer (Tabelle III) mit etwa 27,000 LoC. Dies zeigt ebenso beeindruckende Ergebnisse und reduziert die Anzahl der Zustandsbits von über 47,000 auf nur 11. Der manuelle Gesamtaufwand einschließlich der formalen Überprüfung von 27k LoC in VHDL betrug in diesem Fall etwa sechs Personenmonate. Eigenschaften in weniger als zwei Minuten überprüft.

Die Etablierung „klingender Abstraktionen“ auf Ebenen oberhalb von RTL ist der Schlüssel, um die Abstraktionsebene anzuheben. Das Papier ist ein wichtiger Beitrag in diesem Bereich. Überraschenderweise sind die Kosten für den Nachweis der Solidität dieser Abstraktionen vernachlässigbar, nur wenige Minuten mit einem Model Checker. Was jedoch nicht zu vernachlässigen ist, ist der nicht automatisierte Aufwand, diese Abstraktionen zu erstellen. Viele Monate von Experten, die mit der nicht-trivialen Methodik vertraut sind. Es ist auch nicht klar, wie ausdrucksstark diese Abstraktionen sind. Die Anmerkung des Autors dazu: „Wir finden diesen abstrakten Graphen, indem wir eine Abbildungsfunktion konstruieren … In diesem Zusammenhang können wir beobachten, dass es immer triviale Färbefunktionen gibt, die jedem Knoten im Graphen eine andere Farbe zuweisen oder die allen Knoten dieselbe Farbe zuweisen (die resultierenden Pfadprädikat-Abstraktionen sind natürlich bedeutungslos) “. Ob und wie diese Methodik Eingang in praktische Designwerkzeuge findet, ist eine interessante Frage.

Meine Sicht

Eine Anmerkung dazu, wie ich an solche mathematischen Arbeiten herangehe. Unser Hauptinteresse gilt dem technischen Wert, daher konzentriere ich mich in erster Linie auf Eröffnungsvorschläge, Experimente und Ergebnisse. Eine dichte algebraische Begründung, die ich als Anhang behandle, ist vielleicht interessant, um sie später zu lesen, wenn dies gerechtfertigt ist. Das erleichtert das Lesen erheblich!

Teile diesen Beitrag über: