Formale Verifikation von VHDL-Modulen mit PSL meistern

Beim Design von VHDL für sicherheitskritische FPGA-Anwendungen reicht das bloße Schreiben von Testbenches nicht aus. Ingenieure müssen beweisen, dass ein Modul sich exakt wie spezifiziert verhält, frei von versteckten Seiteneffekten. Formale Verifikation liefert diese mathematische Absicherung.

Formale Verifikation schließt die Lücke zwischen Anforderungen und Implementierung, indem sie beweist, dass jede mögliche Eingabesequenz die Designeigenschaften erfüllt. Sie ist unverzichtbar für die Zertifizierung medizinischer Geräte, Avionik-Systeme oder jeder Domäne, in der DO‑254-Zertifizierung erforderlich ist.

In diesem Gastbeitrag teilt Michael Finn Jørgensen – erfahrener Formal-Verifikation-Praktiker – praktische Einblicke und umsetzbare Tipps. Das folgende Beispiel baut auf dem bekannten AXI FIFO Tutorial How to make an AXI FIFO in block RAM using the ready/valid handshake auf und demonstriert, wie PSL auf ein reales VHDL-Design angewendet wird.

Was ist formale Verifikation?

Formale Verifikation (FV) ist eine systematische Pre-Synthese-Methode, die die Korrektheit eines Designs für alle Eingangskombinationen garantiert. Im Gegensatz zu konventionellen Testbenches, die auf manuell erstellten Stimuli basieren, spezifiziert FV Eigenschaften, die an jedem Taktzyklus gelten müssen. Ein SAT-Solver beweist dann exhaustiv, dass diese Eigenschaften erfüllt sind – oder liefert ein Gegenbeispiel, falls nicht.

Zwei Kerntechniken treiben FV an:

• Bounded Model Checking (BMC) – prüft eine endliche Anzahl von Zyklen, beginnend vom Reset.
• Induktionsbeweis – verifiziert, dass wenn ein Zustand gültig ist, alle nachfolgenden Zustände gültig bleiben. Dies erfordert einen vollständigen Eigenschaftensatz, liefert aber Garantien für unendlich viele Zyklen.

Da BMC bereits mit wenigen Eigenschaften ausgeführt werden kann, ist es oft die erste Verteidigungslinie. Induktion ist zwar anspruchsvoller, liefert aber absolute Sicherheit.

Warum formale Verifikation nutzen?

FV glänzt beim Aufdecken schwer fassbarer Bugs, da sie den gesamten Eingangsraum automatisch erkundet. Wird ein Fehler entdeckt, produziert das Tool eine präzise Wellenform, die den exakten Zyklus markiert, in dem die Eigenschaft verletzt wurde – weit einfacher zu debuggen als ein langer Simulations-Trace.

Obwohl FV ein mächtiges Unit-Testing-Tool ist, ersetzt es keine handgefertigten Integrationstests. Mit wachsender Modulgröße kann die Laufzeit des Solvers prohibitiv werden. Dennoch reduziert Investition in FV den gesamten Debugging-Aufwand und beschleunigt Time-to-Market.

Eigenschaften in PSL schreiben

PSL (Property Specification Language) ist die Lingua Franca der formalen Verifikation in VHDL. Eigenschaften werden typischerweise in einer separaten .psl Datei gespeichert, die der Solver während der Verifikationsphase einliest.

Drei PSL-Schlüsselwörter beschreiben Eigenschaften:

• assert – garantiert, dass eine Bedingung immer gilt.
• assume – stellt Annahmen über die Eingänge auf.
• cover – prüft, ob ein bestimmtes Szenario jemals eintreten kann.

PSL-Dateien können auch gewöhnliche VHDL-Deklarationen und Prozesse enthalten, was die Erstellung Hilfssignale für komplexe Assertionen ermöglicht.

Jede PSL-Datei beginnt mit einem vunit Block, der die Datei an eine spezifische Entity bindet:

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) { } 

Gefolgt von einer Standard-Takt-Deklaration:

default clock is rising_edge(clk); 

Eigenschaftssyntax sieht so aus:

LABEL : assert always {PRECONDITION} |-> {POSTCONDITION} LABEL : assume always {PRECONDITION} |-> {POSTCONDITION} 

Nutzen Sie |=> für Next-Cycle-Assertionen:

LABEL : assert always {PRECONDITION} |=> {POSTCONDITION} 

Innerhalb von Bedingungen können Sie stable verwenden, um zu erzwingen, dass ein Signal zwischen Zyklen nicht wechselt, und Bedingungen mit {C1; C2} verketten, um sequentielle Constraints auszudrücken.

Benötigte Tools installieren

Führende kommerzielle Tools (z. B. ModelSim) unterstützen formale Verifikation, aber die kostenlose Student Edition bietet dieses Feature nicht. Glücklicherweise steht ein robuster Open-Source-Stack für Linux (und via WSL auf Windows) zur Verfügung. Die folgende Anleitung nutzt Ubuntu 20.04 LTS, funktioniert auf jedem aktuellen Debian-basierten Derivat.

Voraussetzungen

sudo apt update && sudo apt upgrade 

Essentielle Entwicklungsbibliotheken installieren:

sudo apt install build-essential clang bison flex libreadline-dev \ gawk tcl-dev libffi-dev git mercurial graphviz \ xdot pkg-config python python3 libftdi-dev gperf \ libboost-program-options-dev autoconf libgmp-dev \ cmake gnat gtkwave 

Yosys und SymbiYosys

git clone https://github.com/YosysHQ/yosys cd yosys make sudo make install cd .. git clone https://github.com/YosysHQ/SymbiYosys cd SymbiYosys sudo make install cd .. git clone https://github.com/SRI-CSL/yices2 cd yices2 autoconf ./configure make sudo make install cd .. 

GHDL und Yosys Plugin

git clone https://github.com/ghdl/ghdl cd ghdl ./configure --prefix=/usr/local make sudo make install cd .. git clone https://github.com/ghdl/ghdl-yosys-plugin cd ghdl-yosys-plugin make sudo make install cd .. 

Beispielprojekt herunterladen

Füllen Sie das untenstehende Formular aus, um ein ZIP-Archiv mit dem kompletten AXI FIFO Source, PSL-Datei und Verifikationsskripten zu erhalten.

Ausgearbeitetes Beispiel: Formale Verifikation eines AXI FIFO

Im Folgenden skizzieren wir die Schlüsseleigenschaftskategorien für ein FIFO und illustrieren, wie man sie in PSL kodiert.

Reset-Handling

f_reset : assume {rst}; 

Da das always Keyword fehlt, gilt diese Annahme nur für den ersten Zyklus nach Reset. Eine Label-Konvention (f_) hilft, Fehlschläge zu identifizieren.

f_after_reset_valid : assert always {rst} |=> {not out_valid}; f_after_reset_ready : assert always {rst} |=> {in_ready}; f_after_reset_head : assert always {rst} |=> {count = 0}; 

Beachten Sie, dass interne Signale wie count referenziert werden können, da die vunit Deklaration den Architecturenamen einschließt.

FIFO Full und Empty Signaling

f_empty : assert always {count = 0} |-> {not out_valid}; f_full : assert always {count = ram_depth-1} |-> {not in_ready}; 

AXI Protokoll-Compliance

f_in_data_stable : assume always {in_valid and not in_ready and not rst} |=> {stable(in_valid) and stable(in_data)}; f_out_data_stable : assert always {out_valid and not out_ready and not rst} |=> {stable(out_valid) and stable(out_data)}; 

Für die Ready-Signal-Stabilität:

f_out_ready_stable : assume always {out_ready and not out_valid and not rst} |=> {stable(out_ready)}; f_in_ready_stable : assert always {in_ready and not in_valid and not rst} |=> {stable(in_ready)}; 

FIFO Ordering

Ordering garantiert, dass frühere Schreibzugriffe vor späteren verlassen. Wir modellieren dies mit Hilfssignalen, die sich merken, wann bestimmte Datenwerte eingingen oder verließen.

signal f_sampled_in_d1 : std_logic := '0'; signal f_sampled_in_d2 : std_logic := '0'; p_sampled : process (clk) begin if rising_edge(clk) then if in_valid then if in_data = f_value_d1 then f_sampled_in_d1 <= '1'; end if; if in_data = f_value_d2 then f_sampled_in_d2 <= '1'; end if; end if; if out_valid then if out_data = f_value_d1 then f_sampled_out_d1 <= '1'; end if; if out_data = f_value_d2 then f_sampled_out_d2 <= '1'; end if; end if; if rst = '1' then f_sampled_in_d1 <= '0'; f_sampled_in_d2 <= '0'; f_sampled_out_d1 <= '0'; f_sampled_out_d2 <= '0'; end if; end if; end process p_sampled; 

Deklarieren Sie die Datenwerte als unconstrained Konstanten, damit der Solver jedes Bitmuster wählen kann:

signal f_value_d1 : std_logic_vector(ram_width - 1 downto 0); signal f_value_d2 : std_logic_vector(ram_width - 1 downto 0); attribute anyconst : boolean; attribute anyconst of f_value_d1 : signal is true; attribute anyconst of f_value_d2 : signal is true; 

Schließlich die Ordering-Constraints kodieren:

f_fifo_ordering_in : assume always {f_sampled_in_d2} |-> {f_sampled_in_d1}; f_fifo_ordering_out : assert always {f_sampled_out_d2} |-> {f_sampled_out_d1}; 

Formale Verifikation ausführen

Erstellen Sie ein axi_fifo.sby Skript für das sby Tool:

[tasks] bmc [options] bmc: mode bmc bmc: depth 10 [engines] smtbmc [script] ghdl --std=08 -gram_width=4 -gram_depth=8 axi_fifo.vhd axi_fifo.psl -e axi_fifo prep -top axi_fifo [files] axi_fifo.psl axi_fifo.vhd 

Verifikation starten:

sby --yosys ";yosys -m ghdl" -f axi_fifo.sby 

Ein erfolgreicher Lauf druckt:

[axi_fifo_bmc] DONE (PASS, rc=0) 

Das Erhöhen von depth über die FIFO-Tiefe hinaus stellt sicher, dass der Solver Vollkapazitätsszenarien erkundet.

Mutation Testing

Um die Vollständigkeit Ihres Eigenschaftensatzes zu prüfen, injizieren Sie absichtlich einen kleinen Bug – z. B. Entfernen der Logik, die out_valid treibt – und führen FV erneut aus. Meldet der Solver einen Assertion-Fehler, haben Sie verifiziert, dass Ihre Eigenschaften ausdrucksstark genug sind, um diesen Fehler zu erfassen.

Beispiel-Fehlermeldung:

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable 

Öffnen Sie das generierte trace.vcd in GTKWave, um den exakten Zyklus der Eigenschaftsverletzung zu lokalisieren.

Cover Statements

Cover-Statements sind nützlich, um zu beweisen, dass ein bestimmtes Szenario erreichbar ist. Zum Beispiel, um zu verifizieren, dass das FIFO gefüllt und dann geleert werden kann:

f_full_to_empty : cover { rst = '1'; rst = '0'[*]; rst = '0' and count = ram_depth-1; rst = '0'[*]; rst = '0' and count = 0}; 

Passen Sie das sby Skript an, um den Cover-Task einzuschließen:

[tasks] bmc cover [options] bmc: mode bmc bmc: depth 10 cover: mode cover 

Erfolgreiche Coverage ergibt:

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15. 

Ändert man count = ram_depth-1 zu count = ram_depth, wird der Cover unerreichbar, was die Sensitivität des Tools für Eigenschaftsgenauigkeit demonstriert.

Weiterführende Schritte

• Einführung in die PSL-Sprache
• Grundlagen formaler Verifikation
• Video-Serie: Einstieg in formale Verifikation
• Fortgeschrittene Artikel zur formalen Verifikation
• Mini-Projekt-Repository für formale Verifikation