Formale Äquivalenzprüfung - Formal equivalence checking

Der Prozess der formalen Äquivalenzprüfung ist Teil der elektronischen Entwurfsautomatisierung (EDA), die üblicherweise bei der Entwicklung digitaler integrierter Schaltungen verwendet wird , um formal zu beweisen, dass zwei Darstellungen eines Schaltungsentwurfs genau dasselbe Verhalten aufweisen.

Äquivalenzprüfung und Abstraktionsebenen

Im Allgemeinen gibt es eine breite Palette möglicher Definitionen der funktionalen Äquivalenz, die Vergleiche zwischen verschiedenen Abstraktionsebenen und unterschiedlicher Granularität von Zeitdetails abdecken .

  • Der gebräuchlichste Ansatz besteht darin, das Problem der Maschinenäquivalenz zu betrachten, das zwei synchrone Entwurfsspezifikationen definiert, die funktional äquivalent sind, wenn sie Takt für Takt genau dieselbe Folge von Ausgangssignalen für jede gültige Folge von Eingangssignalen erzeugen.
  • Mikroprozessorentwickler verwenden die Äquivalenzprüfung, um die für die Befehlssatzarchitektur (ISA) angegebenen Funktionen mit einer RTL-Implementierung ( Register Transfer Level ) zu vergleichen und sicherzustellen, dass jedes auf beiden Modellen ausgeführte Programm eine identische Aktualisierung des Hauptspeicherinhalts bewirkt. Dies ist ein allgemeineres Problem.
  • Ein Systemdesignfluss erfordert einen Vergleich zwischen einem TLM (Transaction Level Model), z. B. in SystemC geschrieben, und seiner entsprechenden RTL-Spezifikation. Eine solche Überprüfung wird in einer System-on-a-Chip-Entwurfsumgebung (SoC) immer interessanter.

Synchronmaschinenäquivalenz

Das RTL-Verhalten ( Register Transfer Level ) eines digitalen Chips wird normalerweise mit einer Hardwarebeschreibungssprache wie Verilog oder VHDL beschrieben . Diese Beschreibung ist das goldene Referenzmodell, das detailliert beschreibt, welche Operationen während welchem Taktzyklus und von welcher Hardware ausgeführt werden. Sobald die Logikdesigner durch Simulationen und andere Verifizierungsmethoden die Registerübertragungsbeschreibung verifiziert haben, wird der Entwurf normalerweise von einem Logiksynthesewerkzeug in eine Netzliste umgewandelt . Die Gleichwertigkeit ist nicht mit der Funktionskorrektheit zu verwechseln, die durch Funktionsüberprüfung ermittelt werden muss .

Die anfängliche Netzliste wird normalerweise einer Reihe von Transformationen unterzogen, z. B. Optimierung, Hinzufügen von DFT-Strukturen ( Design For Test ) usw., bevor sie als Grundlage für die Platzierung der Logikelemente in einem physischen Layout verwendet wird . Zeitgemäße physische Entwurfssoftware nimmt gelegentlich auch wesentliche Änderungen an der Netzliste vor (z. B. Ersetzen von Logikelementen durch gleichwertige ähnliche Elemente mit einer höheren oder niedrigeren Antriebsstärke und / oder Fläche ). Während jedes Schritts eines sehr komplexen, mehrstufigen Verfahrens müssen die ursprüngliche Funktionalität und das im ursprünglichen Code beschriebene Verhalten beibehalten werden. Wenn das endgültige Tape-Out aus einem digitalen Chip besteht, haben viele verschiedene EDA-Programme und möglicherweise einige manuelle Änderungen die Netzliste geändert.

Theoretisch garantiert ein Logiksynthesewerkzeug, dass die erste Netzliste logisch dem RTL-Quellcode entspricht. Alle Programme, die später im Prozess Änderungen an der Netzliste vornehmen, stellen theoretisch auch sicher, dass diese Änderungen logisch einer früheren Version entsprechen.

In der Praxis weisen Programme Fehler auf, und es besteht ein großes Risiko anzunehmen, dass alle Schritte von RTL bis zur endgültigen Tape-Out-Netzliste fehlerfrei ausgeführt wurden. Im wirklichen Leben ist es außerdem üblich, dass Designer manuelle Änderungen an einer Netzliste vornehmen, die allgemein als Engineering Change Orders oder ECOs bezeichnet wird, wodurch ein wichtiger zusätzlicher Fehlerfaktor eingeführt wird. Anstatt blind anzunehmen, dass keine Fehler gemacht wurden, ist daher ein Überprüfungsschritt erforderlich, um die logische Äquivalenz der endgültigen Version der Netzliste mit der ursprünglichen Beschreibung des Entwurfs (goldenes Referenzmodell) zu überprüfen.

In der Vergangenheit bestand eine Möglichkeit zur Überprüfung der Äquivalenz darin, die Testfälle, die zur Überprüfung der Richtigkeit der RTL entwickelt wurden, mithilfe der endgültigen Netzliste erneut zu simulieren. Dieser Prozess wird als Logiksimulation auf Gate-Ebene bezeichnet . Das Problem dabei ist jedoch, dass die Qualität der Prüfung nur so gut ist wie die Qualität der Testfälle. Außerdem sind Simulationen auf Gate-Ebene notorisch langsam auszuführen, was ein großes Problem darstellt, da die Größe digitaler Designs weiterhin exponentiell zunimmt .

Eine alternative Möglichkeit, dies zu lösen, besteht darin, formal zu beweisen, dass der RTL-Code und die daraus synthetisierte Netzliste in allen (relevanten) Fällen genau dasselbe Verhalten aufweisen. Dieser Prozess wird als formale Äquivalenzprüfung bezeichnet und ist ein Problem, das im breiteren Bereich der formalen Verifikation untersucht wird .

Eine formale Äquivalenzprüfung kann zwischen zwei beliebigen Darstellungen eines Entwurfs durchgeführt werden: RTL <> Netzliste, Netzliste <> Netzliste oder RTL <> RTL, obwohl letztere im Vergleich zu den ersten beiden selten ist. In der Regel zeigt ein formales Äquivalenzprüfwerkzeug auch mit großer Genauigkeit an, an welchem ​​Punkt ein Unterschied zwischen zwei Darstellungen besteht.

Methoden

Es gibt zwei grundlegende Technologien, die für das boolesche Denken in Äquivalenzprüfprogrammen verwendet werden:

  • Binäre Entscheidungsdiagramme oder BDDs: Eine spezielle Datenstruktur, die das Denken über boolesche Funktionen unterstützt. BDDs sind aufgrund ihrer Effizienz und Vielseitigkeit sehr beliebt geworden.
  • Konjunktive Normalform-Erfüllbarkeit: SAT- Löser geben eine Zuordnung zu den Variablen einer Satzformel zurück , die diese erfüllt, wenn eine solche Zuordnung vorliegt. Fast jedes boolesche Argumentationsproblem kann als SAT-Problem ausgedrückt werden.

Kommerzielle Anwendungen zur Äquivalenzprüfung

Hauptprodukte im Bereich Logic Equivalence Checking ( LEC ) von EDA sind:

Verallgemeinerungen

  • Äquivalenzprüfung von Schaltkreisen mit zeitgesteuerter Schaltung: Manchmal ist es hilfreich, die Logik von einer Seite eines Registers auf eine andere zu verschieben, was das Überprüfungsproblem kompliziert.
  • Sequentielle Äquivalenzprüfung: Manchmal sind zwei Maschinen auf kombinatorischer Ebene völlig unterschiedlich, sollten jedoch bei gleichen Eingaben die gleichen Ausgaben liefern. Das klassische Beispiel sind zwei identische Zustandsautomaten mit unterschiedlichen Codierungen für die Zustände. Da dies nicht auf ein Kombinationsproblem reduziert werden kann, sind allgemeinere Techniken erforderlich.
  • Äquivalenz von Softwareprogrammen, dh Überprüfen, ob zwei genau definierte Programme, die N Eingaben verwenden und M Ausgaben erzeugen, äquivalent sind: Konzeptionell können Sie Software in eine Zustandsmaschine verwandeln (genau das macht die Kombination eines Compilers, da ein Computer plus Speicher bilden eine sehr große Zustandsmaschine.) Dann können theoretisch verschiedene Formen der Eigenschaftsprüfung sicherstellen, dass sie die gleiche Ausgabe erzeugen. Dieses Problem ist noch schwieriger als die sequentielle Äquivalenzprüfung, da die Ausgaben der beiden Programme zu unterschiedlichen Zeiten angezeigt werden können. aber es ist möglich und Forscher arbeiten daran.

Siehe auch

Verweise

  • Handbuch zur elektronischen Entwurfsautomatisierung für integrierte Schaltkreise von Lavagno, Martin und Scheffer, ISBN  0-8493-3096-3 Eine Übersicht über das Gebiet. Dieser Artikel wurde mit Genehmigung von Fabio Somenzi und Andreas Kuehlmann aus Band 2, Kapitel 4, Äquivalenzprüfung , abgeleitet.
  • RE Bryant, Graphbasierte Algorithmen zur Manipulation boolescher Funktionen , IEEE Transactions on Computers., C-35, S. 677–691, 1986. Die ursprüngliche Referenz zu BDDs.
  • Sequentielle Äquivalenzprüfung für RTL-Modelle. Nikhil Sharma, Gagan Hasteer und Venkat Krishnaswamy. EE Times .

Externe Links