Funktionsüberprüfung - Functional verification

In Electronic Design Automation , funktionale Verifikation ist die Aufgabe, die der Überprüfung Logik - Design Konform Spezifikation. Im Alltag versucht die Funktionsüberprüfung, die Frage zu beantworten: "Tut dieses vorgeschlagene Design, was beabsichtigt ist?" Dies ist eine komplexe Aufgabe, die bei den meisten großen Projekten zum Entwurf elektronischer Systeme den größten Teil der Zeit und Mühe kostet. Die Funktionsüberprüfung ist Teil einer umfassenderen Entwurfsüberprüfung , bei der neben der Funktionsüberprüfung auch nichtfunktionale Aspekte wie Timing, Layout und Leistung berücksichtigt werden.

Die Funktionsüberprüfung ist aufgrund der Vielzahl möglicher Testfälle, die selbst in einem einfachen Design vorhanden sind, sehr schwierig. Häufig gibt es mehr als 10 ^ 80 mögliche Tests, um ein Design umfassend zu verifizieren - eine Zahl, die in einem Leben unmöglich zu erreichen ist. Dieser Aufwand entspricht der Programmüberprüfung und ist NP-hart oder sogar noch schlimmer - und es wurde keine Lösung gefunden, die in allen Fällen gut funktioniert. Es kann jedoch mit vielen Methoden angegriffen werden. Keiner von ihnen ist perfekt, aber jeder kann unter bestimmten Umständen hilfreich sein:

  • Die Logiksimulation simuliert die Logik, bevor sie erstellt wird.
  • Die Simulationsbeschleunigung wendet spezielle Hardware auf das Logiksimulationsproblem an.
  • Die Emulation erstellt eine Version des Systems unter Verwendung programmierbarer Logik. Dies ist teuer und immer noch viel langsamer als die reale Hardware, aber um Größenordnungen schneller als die Simulation. Es kann beispielsweise verwendet werden, um das Betriebssystem auf einem Prozessor zu starten.
  • Die formale Überprüfung versucht mathematisch zu beweisen, dass bestimmte Anforderungen (auch formal ausgedrückt) erfüllt sind oder dass bestimmte unerwünschte Verhaltensweisen (wie z. B. Deadlock) nicht auftreten können.
  • Bei der intelligenten Überprüfung wird die Testbench mithilfe der Automatisierung an Änderungen im Code der Registerübertragungsebene angepasst .
  • HDL-spezifische Versionen von Flusen und andere Heuristiken werden verwendet, um häufige Probleme zu finden.

Die simulationsbasierte Verifizierung (auch als " dynamische Verifizierung " bezeichnet) wird häufig verwendet, um das Design zu "simulieren", da diese Methode sehr einfach skaliert werden kann. Es wird ein Stimulus bereitgestellt, um jede Zeile im HDL-Code zu trainieren. Ein Prüfstand dient zur funktionalen Überprüfung des Entwurfs, indem aussagekräftige Szenarien bereitgestellt werden, um zu überprüfen, ob der Entwurf bei bestimmten Eingaben den Spezifikationen entspricht.

Eine Simulationsumgebung besteht normalerweise aus mehreren Arten von Komponenten:

  • Der Generator generiert Eingabevektoren, mit denen nach Anomalien gesucht wird, die zwischen der Absicht (Spezifikationen) und der Implementierung (HDL-Code) bestehen. Dieser Generatortyp verwendet einen NP-vollständigen SAT-Solver-Typ, der rechenintensiv sein kann. Andere Arten von Generatoren umfassen manuell erstellte Vektoren und proprietäre Generatoren für graphbasierte Generatoren (GBMs). Moderne Generatoren erzeugen gerichtete zufällige und zufällige Stimuli, die statistisch gesteuert werden, um zufällige Teile des Designs zu verifizieren. Die Zufälligkeit ist wichtig, um eine hohe Verteilung über den riesigen Raum der verfügbaren Eingangsreize zu erreichen. Zu diesem Zweck geben Benutzer dieser Generatoren die Anforderungen für die generierten Tests absichtlich zu wenig an. Es ist die Aufgabe des Generators, diese Lücke zufällig zu füllen. Dieser Mechanismus ermöglicht es dem Generator, Eingaben zu erstellen, die Fehler aufdecken, nach denen der Benutzer nicht direkt sucht. Generatoren richten die Stimuli auch auf Design-Eckfälle aus, um die Logik weiter zu betonen. Vorspannung und Zufälligkeit dienen unterschiedlichen Zielen und es gibt Kompromisse zwischen ihnen, daher haben verschiedene Generatoren eine unterschiedliche Mischung dieser Eigenschaften. Da die Eingabe für das Design gültig (legal) sein muss und viele Ziele (wie z. B. Vorspannung) beibehalten werden sollten, verwenden viele Generatoren die CSP-Technik ( Constraint Zufriedenheitsproblem ), um die komplexen Testanforderungen zu lösen. Die Legalität der Design-Inputs und das Biasing-Arsenal werden modelliert. Die modellbasierten Generatoren verwenden dieses Modell, um die richtigen Stimuli für das Zieldesign zu erzeugen.
  • Die Treiber übersetzen die vom Generator erzeugten Reize in die tatsächlichen Eingaben für das zu überprüfende Design. Generatoren erstellen Eingaben auf einem hohen Abstraktionsniveau, nämlich als Transaktionen oder Assemblersprache. Die Treiber konvertieren diese Eingabe in tatsächliche Designeingaben, wie in der Spezifikation der Designschnittstelle definiert.
  • Der Simulator erzeugt die Ausgänge des Entwurfs basierend auf dem aktuellen Zustand des Entwurfs (dem Zustand der Flip-Flops) und den eingespeisten Eingängen. Der Simulator enthält eine Beschreibung der Entwurfsnetzliste. Diese Beschreibung wird erstellt, indem die HDL zu einer Netzliste mit niedrigem Gate-Level synthetisiert wird.
  • Der Monitor konvertiert den Status des Entwurfs und seiner Ausgaben in eine Transaktionsabstraktionsebene, damit er in einer Datenbank mit Anzeigetafeln gespeichert und später überprüft werden kann.
  • Der Prüfer bestätigt, dass der Inhalt der Anzeigetafeln legal ist. Es gibt Fälle, in denen der Generator zusätzlich zu den Eingaben erwartete Ergebnisse erzielt. In diesen Fällen muss der Prüfer überprüfen, ob die tatsächlichen Ergebnisse mit den erwarteten übereinstimmen.
  • Der Arbitration Manager verwaltet alle oben genannten Komponenten zusammen.

Es werden verschiedene Abdeckungsmetriken definiert, um zu bewerten, ob das Design angemessen ausgeführt wurde. Dazu gehören die funktionale Abdeckung (wurde jede Funktionalität des Designs ausgeübt?), Die Anweisungsabdeckung (wurde jede HDL-Zeile ausgeübt?) Und die Zweigstellenabdeckung (wurde jede Richtung jeder Zweigstelle ausgeübt?).

Werkzeuge

Siehe auch

Verweise