deutsch  |  english  |  svenska

FPGA Verifikation

ChecklistBei der Entwicklung von IP-Cores und anspruchsvollen FPGA-Systemen stellt die Verifikation der vorgegebenen Funktion eine Herausforderung dar. Oft wird der Projektanteil der Verifikation auf 70% des Gesamtaufwands eines Projekts geschätzt, Tendenz steigend [1]. Es gibt verschiedene Möglichkeiten die Korrektheit eines FPGA-Designs zu verifizieren. Um sicherzustellen, dass das entwickelte System die gewünschte Funktionalität korrekt umsetzt, werden die Methoden der Simulation und der formalen Verifikation eingesetzt.

Simulation

Bei der Simulation kann das Verhalten eines Systems auf verschiedenen Abstraktionsebenen überprüft werden. In einem Simulator können die entwickelten HDL-Komponenten (HDL steht für Hardware Description Language) mit Testvektoren stimuliert und Ausgangsvektoren sowie interne Zustände mittels einer sogenannten Testbench (häufig ebenfalls als HDL-Komponente ausgeführt) überprüft werden.Waveform Die Simulation ist heute ein unerlässlicher Bestandteil des Verifikationsprozesses, um die Funktionalität eines FPGA-Designs zu überprüfen. Es bleibt allerdings, trotz Code Coverage Funktionen, schwierig abzuschätzen an welchem Punkt genug Fälle getestet worden sind, um bestimmte Eigenschaften des Systems wirklich garantieren zu können. Hier kann eine formale Verifikation nützlich sein.

Formale Verifikation

Bei der formalen Verifikation werden nicht Stimuli angelegt um ein Systemverhalten zu simulieren, sondern es wird mathematisch analysiert, ob eine Aussage über ein System zutrifft oder nicht. In den letzten Jahren sind erhebliche Fortschritte in der Entwicklung von leistungsfähigen Softwaretools für die vollautomatische Analyse von Systemen gelungen, die das Problem der sogenannten "Zustandsexplosion" abmildert. Diesem Problem muss begegnet werden um eine Aussage über ein System mit sehr vielen Zuständen zu ermöglichen.Temporal logic In der Regel muss der HDL-Code als RTL-Code (Register Transfer Level), bzw. als endlicher Automat vorliegen, um eine formale Verifikation durchführen zu können. Zwei in der EDA Industrie verbreitete Vorgehensweisen der formalen Verifikation sind Model Checking und Equivalence Checking.

Model Checking

Beim Model Checking, auch bekannt als Property Checking, wird überprüft ob eine Systembeschreibung bestimmte logische Eigenschaften (Spezifikationen) erfüllt. Die Systembeschreibung sollte als Modell in einer formalen Sprache vorliegen und wird einem sogenannten Model Checker übergeben, der überprüft ob das Modell der Spezifikation genügt. Diese Überprüfung erfolgt vollautomatisch und liefert entweder die Aussage, dass das System die Spezifikation erfüllt, oder ein Gegenbeispiel.

Equivalence Checking

Bei dieser Vorgehensweise werden zwei Modelle mit derselben Funktionalität verglichen und es wird mathematisch festgestellt ob die Modelle logisch wirklich identisch sind.

Assertion-Based Verification

Assertion-Based Verification (ABV) ist ein Begriff für die Verifikation durch Aussagen-Überprüfung, die sowohl für die Simulation als auch die formale Verifikation verwendet werden kann. Die Property Specification Language (PSL) ist eine von Accellera entwickelte Beschreibungssprache die für die Verifikation von Hardware geschaffen wurde. In PSL lassent sich Aussagen über das Verhalten von Signalen in einem System sehr kompakt beschreiben.

[1] Grant Martin Blog

Wir beantworten gerne Ihre Fragen zum Thema Verifikation oder Simulation.
Kontaktieren Sie uns!