Formale Verifizierung in VHDL mit PSL

Bei der Entwicklung von VHDL für sicherheitskritische FPGA-Anwendungen reicht es nicht aus, nach bestem Wissen und Gewissen Testbenches zu schreiben. Sie müssen nachweisen, dass das Modul bestimmungsgemäß und ohne unerwünschte Nebeneffekte funktioniert.

Formale Verifikationstechniken können Ihnen dabei helfen, eine Anforderung einem Test zuzuordnen und zu beweisen, dass Ihr VHDL-Modul der Spezifikation entspricht. Es ist ein Instrument zur Verifizierung von Anwendungen im Gesundheitswesen oder zur Erlangung der DO-254-Zertifizierung für luftgestützte FPGA-Lösungen.

Um die formale Verifizierung zu entmystifizieren, bittet VHDLwhiz die Hilfe von Michael Finn Jørgensen um diesen Gastbeitrag zu schreiben. Michael hat umfangreiche Erfahrung mit dem Thema und gibt viele Tipps auf seiner GitHub-Seite.

Das zu testende Gerät im herunterladbaren Beispiel dieses Artikels stammt aus dem vorhandenen Tutorial:
How to make an AXI FIFO in block RAM using the ready/valid handshake

Ich lasse Michael ab hier übernehmen und erkläre Ihnen im Rest dieses Blogbeitrags die formelle Überprüfung.

Was ist eine formale Verifizierung?

Das Ziel der formalen Verifizierung (FV) ist sicherzustellen, dass Ihr Modul wie vorgesehen funktioniert!

FV ist etwas, das Sie als Teil Ihres Entwicklungsprozesses tun, bevor Sie Ihr Modul synthetisieren. Es wird manchmal „Property Checking“ genannt, was meiner Meinung nach eine bessere Beschreibung ist.

In FV spezifizieren Sie die Eigenschaften Ihr Modul muss dies haben, und dann wird das Tool (das als „Satisfiability Solver“ bezeichnet wird) beweisen dass Ihr Modul die Eigenschaften für alle möglichen Folgen von Eingaben erfüllt .

Mit anderen Worten, das Tool sucht nach jedem Übergang von einem gültigen Zustand (bei dem alle Eigenschaften erfüllt sind) auf ungültig Zustand (wo eine oder mehrere Eigenschaften verletzt werden). Wenn es keinen solchen Übergang gibt, d. h. es gibt keine Möglichkeit, in einen ungültigen Zustand überzugehen, dann sind die Eigenschaften erwiesenermaßen immer erfüllt.

Die Herausforderung bei FV besteht darin, die Eigenschaften Ihres Moduls in einer Sprache auszudrücken, die das Tool verstehen kann.

Formale Verifikation ist eine Alternative zu manuell geschriebenen Testbenches. Das Ziel sowohl der formalen Verifizierung als auch der manuellen Testbenches besteht darin, Fehler aus dem Design zu eliminieren, aber die formale Verifizierung tut dies, indem sie die Eigenschaften untersucht und automatisch viele verschiedene Testbenches generiert.

Die Tools verwenden zwei verschiedene Methoden:

• Bounded Model Checking (BMC) . Startet ab Reset und prüft eine feste Anzahl von Taktzyklen.
• Induktionsbeweis . Beginnt mit einem beliebigen gültigen Zustand und überprüft, ob alle nachfolgenden Zustände ebenfalls gültig sind.

Der Induktionsbeweis ist schwieriger zu erfüllen, da er alles erfordert Eigenschaften angegeben werden, während BMC mit nur wenigen Eigenschaften ausgeführt werden kann und dennoch nützliche Ergebnisse liefert.

Warum formale Verifizierung verwenden?

Formale Verifizierung ist sehr gut darin, schwer zu findende Fehler zu finden! Das liegt daran, dass die formale Verifizierung automatisch den gesamten Raum möglicher Eingaben durchsucht.

Dies steht im Gegensatz zum traditionellen Testbench-Schreiben, das das manuelle Erstellen von Stimuli erfordert. Es ist praktisch unmöglich, den gesamten Zustandsraum mit manuell geschriebenen Testbenches zu erkunden.

Wenn die formale Überprüfung einen Fehler findet, generiert sie außerdem eine sehr kurze Wellenform, die den Fehler zeigt, und zwar viel schneller als beim Ausführen einer Simulation, die auf einer manuell geschriebenen Testbench basiert. Diese kurze Wellenform ist viel einfacher zu debuggen als eine sehr lange Wellenform, die normalerweise aus der Simulation entsteht.

Die formale Verifikation ist jedoch kein Ersatz für das Schreiben auf der Testbench. Meiner Erfahrung nach eignet sich die formale Verifikation gut für Unit-Tests, während es besser ist, Integrationstests mit handgefertigten Testbenches durchzuführen. Denn die Laufzeit der formalen Verifikation steigt exponentiell mit der Größe des Moduls.

Es gibt tatsächlich eine Lernkurve, die mit der formalen Verifizierung verbunden ist, aber es lohnt sich, und ich hoffe, dieser Blogbeitrag hilft Ihnen, diese Lernkurve zu überwinden. Sie werden Ihr Design früher fertigstellen und es wird weniger Fehler enthalten!

Wie schreibt man Eigenschaften in PSL

Bei der formalen Verifikation müssen Sie die Eigenschaften Ihres Moduls mit der Property Specification Language (PSL) ausdrücken. Die Eigenschaften befinden sich typischerweise in einer separaten Datei mit der Endung .psl , und diese Datei wird nur während der formalen Überprüfung verwendet.

In diesem Abschnitt beschreibe ich die Hauptmerkmale der PSL-Sprache allgemein und in einem späteren Abschnitt werde ich Sie durch ein spezifisches Beispiel arbeiten.

Es gibt drei Anweisungen in PSL:

• assert
• assume
• cover

Das Schlüsselwort assert ist Ihnen vielleicht schon bekannt beim Schreiben von Testbenches. Dasselbe Schlüsselwort wird auch in PSL verwendet, jedoch mit einer etwas anderen Syntax. Die assert Das Schlüsselwort wird verwendet, um Eigenschaften zu beschreiben, die dieses Modul verspricht, immer erfüllt zu sein. Insbesondere die assert Das Schlüsselwort wird auf die Ausgänge des Moduls oder möglicherweise auch auf den internen Zustand angewendet.

Die assume Das Schlüsselwort wird verwendet, um alle Anforderungen zu beschreiben, die dieses Modul an die Eingänge stellt. Mit anderen Worten, die assume Schlüsselwort wird auf Eingaben in das Modul angewendet.

Die cover Das Schlüsselwort wird verwendet, um Eigenschaften zu beschreiben, die auf irgendeine Weise erreichbar sein müssen.

Sie können auch regulären VHDL-Code in die PSL-Datei schreiben, einschließlich Signaldeklarationen und -prozesse (sowohl synchron als auch kombinatorisch).

Die erste Zeile der PSL-Datei sollte

sein

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) {

Hier ENTITY_NAME und ARCHITECTURE_NAME beziehen Sie sich auf das Modul, das Sie überprüfen. Die INSTANCE_NAME kann alles sein, was du magst. Die Datei sollte mit einer schließenden Klammer enden:} .

Die nächste Zeile im .psl Datei sollte sein:

default clock is rising_edge(clk);

Dies vermeidet das mühsame Verweisen auf das Taktsignal in jedem der Property-Statements.

Die Syntax für assert und assume Anweisungen ist:

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

Diese Anweisung lautet wie folgt:Wenn der PRECONDITION hält (in jedem Taktzyklus) dann die POSTCONDITION muss im gleichen erfüllt werden Taktzyklus.

Es gibt noch eine andere häufig verwendete Form:

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

Diese Anweisung lautet wie folgt:Wenn die PRECONDITION hält (in jedem Taktzyklus) dann den POSTCONDITION muss im nächsten erfüllt werden Taktzyklus.

Beide Formen werden häufig verwendet.

Innerhalb des PRE- und POST-CONDITIONS können Sie das Schlüsselwort stable verwenden . Dieses Schlüsselwort bedeutet:Der Wert in this Taktzyklus ist derselbe wie der Wert im vorherigen Taktzyklus.

Innerhalb des PRE- und POST-CONDITIONS , können Sie auch Sequenzen verwenden, indem Sie wie folgt schreiben:

{CONDITION_1 ; CONDITION_2}

Das bedeutet, dass CONDITION_1 muss damit zufrieden sein Taktzyklus und das CONDITION_2 muss am nächsten erfüllt werden Taktzyklus.

Die Cover-Anweisung hat die folgende Syntax:

LABEL : cover {CONDITION}

Wir werden später in diesem Blog viele Beispiele für all diese Aussagen in dem ausgearbeiteten Beispiel sehen.

Installieren der erforderlichen Tools

Die formale Verifizierung wird von den führenden Toolanbietern unterstützt, einschließlich ModelSim. Leider unterstützt die Student Edition von ModelSim KEINE formale Verifizierung. Tatsächlich erhalten Sie die folgende Fehlermeldung:

Um ModelSim für die formelle Verifizierung zu verwenden, ist also eine kostenpflichtige Lizenz erforderlich.

Stattdessen gibt es (kostenlose) Open-Source-Tools, mit denen Sie eine formale Überprüfung durchführen können. In diesem Abschnitt führe ich Sie durch den Installationsprozess dieser Tools.

In diesem Handbuch wird davon ausgegangen, dass Sie auf einer Linux-Plattform arbeiten. Wenn Sie auf einer Windows-Plattform arbeiten, empfehle ich die Verwendung des Windows-Subsystems für Linux (WSL). Die folgende Anleitung wurde mit Ubuntu 20.04 LTS verifiziert.

Voraussetzungen

Zuerst müssen wir das System aktualisieren, um die neuesten Patches zu erhalten:

sudo apt update
sudo apt upgrade

Dann müssen wir einige zusätzliche Entwicklungspakete 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 et al.

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 et al.

Es gibt vorgefertigte Binärdateien für GHDL, aber ich empfehle, die neuesten Quelldateien herunterzuladen und sie wie folgt zu kompilieren:

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

Der nächste Abschnitt dieses Artikels führt Sie durch die Implementierung der formalen Überprüfung für ein vorhandenes VHDL-Projekt. Sie können den vollständigen Code herunterladen, indem Sie Ihre E-Mail-Adresse in das untenstehende Formular eingeben.

Arbeitsbeispiel mit formaler Verifikation

Der folgende Abschnitt beschreibt, wie das axi_fifo-Modul, über das zuvor in diesem Blog geschrieben wurde, formal verifiziert wird.

Um mit der formalen Verifikation zu beginnen, müssen wir uns fragen, welche Eigenschaften hat der FIFO? Ich habe vier Kategorien von Eigenschaften identifiziert:

• Reset-Handhabung:Dass das Modul nach dem Reset in einem wohldefinierten Zustand aufwacht.
• FIFO-Voll- und -Leer-Signalisierung:Dies verifiziert, dass der FIFO die Voll- und Leer-Zustände korrekt anzeigt.
• AXI-Protokoll:Dass das Modul die Anforderungen des AXI-Gültig/Bereit-Handshakes erfüllt.
• FIFO-Ordnung:Dass das FIFO Elemente, die es durchlaufen, nicht fallen lässt/dupliziert/neu ordnet.

Ich werde jede dieser Eigenschaften im Folgenden besprechen.

Handhabung zurücksetzen

Zuerst deklarieren wir, dass das Modul erwartet, dass ein Reset für einen Taktzyklus bestätigt wird:

f_reset : assume {rst};

Beachten Sie hier das Fehlen des Schlüsselworts always . Ohne always Stichwort gilt die Aussage nur für den allerersten Taktzyklus.

Es ist üblich (und sehr nützlich), jeder formalen Aussage ein Label zu geben. Beim Ausführen der formalen Überprüfung greift das Tool auf diese Bezeichnungen zurück, wenn es Fehler meldet. Ich verwende die Konvention, allen solchen Labels f_ voranzustellen .

Dann geben wir an, dass der FIFO nach dem Zurücksetzen leer sein muss:

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 es möglich ist, intern zu referenzieren Signale im Modul und nicht nur Ports. Hier verweisen wir auf count , das ist der aktuelle Füllstand, d. h. die Anzahl der Elemente, die sich derzeit im FIFO befinden. Das ist möglich, weil wir in der ersten Zeile der PSL-Datei auf den Architekturnamen verweisen.

Wir könnten alternativ einen separaten Prozess in der PSL-Datei haben, der die Anzahl der Elemente zählt, die in den FIFO hinein- und hinausgehen. Obwohl dies zu bevorzugen ist, werde ich das interne Zählsignal verwenden, um diesen Blogbeitrag kurz und auf den Punkt zu bringen.

FIFO-Voll- und -Leer-Signalisierung

Voll und leer signalisiert das AXI FIFO mit out_valid und in_ready Signale. Der out_valid Signal wird aktiviert, wann immer der FIFO nicht leer ist, und der in_ready Signal wird aktiviert, wann immer der FIFO nicht voll ist. Lassen Sie uns diese Eigenschaften überprüfen:

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

AXI-Protokoll

Der gültige/bereite AXI-Handshake besagt, dass die Datenübertragung nur dann erfolgt, wenn beide valid und ready werden gleichzeitig geltend gemacht. Ein typischer Fehler bei der Arbeit mit diesem Protokoll besteht darin, gültige (und begleitende Daten) zu behaupten und nicht bereit zu prüfen. Mit anderen Worten, wenn valid wird bestätigt und ready nicht, dann valid sollten im nächsten Taktzyklus geltend gemacht bleiben, und die Daten sollten unverändert bleiben. Das gilt sowohl für Daten, die in den FIFO gehen, als auch für Daten, die aus dem FIFO kommen. Für Daten, die in den FIFO gelangen, verwenden wir den assume Schlüsselwort, und für Daten, die aus dem FIFO kommen, verwenden wir den assert Schlüsselwort.

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)};

Beachten Sie hier die Verwendung des stable Schlüsselwort in Kombination mit dem |=> Operator. Diese Anweisungen beziehen sich auf zwei aufeinanderfolgende Taktzyklen. Beim ersten Taktzyklus prüft es, ob valid wird bestätigt und ready wird nicht behauptet. Dann beim nächsten (zweiten) Taktzyklus (angezeigt durch |=> Operator), die Werte von valid und data sollte derselbe wie der vorherige (d. h. erste) Taktzyklus sein.

Zweitens benötigen wir für das AXI-Protokoll den ready Signal ist stabil. Das bedeutet, wenn der FIFO Daten annehmen kann (ready wird bestätigt), aber es werden keine Daten eingegeben (valid nicht aktiviert), dann beim nächsten Taktzyklus ready sollte bestehen bleiben.

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-Ordnung

Eine weitere wichtige Eigenschaft eines FIFO ist, dass Daten nicht dupliziert/gelöscht/ausgetauscht werden. Das Ausdrücken dieser Eigenschaft in PSL ist ziemlich komplex, und dies ist der schwierigste Teil dieser formalen Überprüfung. Lassen Sie uns diese Immobilie Schritt für Schritt sorgfältig durchgehen.

Wir können allgemein sagen, dass, wenn irgendwelche Daten D1 vor einigen anderen Daten D2 in den FIFO gelangen, dann auf der Ausgangsseite die gleichen Daten D1 den FIFO verlassen müssen, bevor D2 dies tut.

Um dies in PSL auszudrücken, benötigen wir einige Hilfssignale:f_sampled_in_d1 , f_sampled_in_d2 , f_sampled_out_d1 , und f_sampled_out_d2 . Diese Signale werden beim Rücksetzen gelöscht und aktiviert, wann immer D1 oder D2 den FIFO betreten oder verlassen. Einmal aktiviert, bleiben diese Signale aktiviert.

Also drücken wir die FIFO-Ordnungseigenschaft in zwei Teilen aus:Zuerst eine Annahme dass, sobald D2 in den FIFO eintritt, D1 bereits zuvor eingetreten ist:

f_fifo_ordering_in : assume always
   {f_sampled_in_d2} |->
   {f_sampled_in_d1};

Und zweitens eine Behauptung dass, sobald D2 den FIFO verlässt, D1 bereits vorher gegangen ist:

f_fifo_ordering_out : assert always
   {f_sampled_out_d2} |->
   {f_sampled_out_d1};

Wir müssen noch die oben genannten Sampling-Signale deklarieren und füllen. Für die Eingangs-Sampling-Signale gehen wir wie folgt vor:

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;

Hier beziehen wir uns auf zwei andere Signale, f_value_d1 und f_value_d2 . Sie enthalten die Datenwerte D1 und D2. Diese Signale können beliebige beliebige enthalten Werte, und es gibt eine spezielle Möglichkeit, dies dem formalen Verifizierungstool anzuzeigen:

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;

Der anyconst -Attribut wird vom formalen Verifizierungstool erkannt. Es zeigt an, dass das Tool einen beliebigen konstanten Wert an seiner Stelle einfügen kann.

Damit haben wir die Eigenschaften des FIFO spezifiziert.

Formale Verifizierung läuft

Bevor wir das formelle Überprüfungstool tatsächlich ausführen können, müssen wir ein kleines Skript axi_fifo.sby schreiben :

[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

Der Abschnitt [tasks] gibt an, dass wir Bounded Model Checking durchführen wollen. Der Abschnitt [options] gibt an, dass BMC für 10 Taktzyklen laufen soll. Der Standardwert ist 20. Der Abschnitt [engines] wählt aus, welcher von mehreren verschiedenen Solvern verwendet werden soll. Abhängig von Ihrem speziellen Design kann es Unterschiede in der Ausführungsgeschwindigkeit der verschiedenen möglichen Engines geben. Lassen Sie diesen Wert vorerst unverändert.

Der [script] Abschnitt ist der interessante Teil. Hier geben wir den VHDL-Standard (2008), die Generics-Werte, die zu verarbeitenden Dateien und den Namen der Entität der obersten Ebene an. Schließlich die [files] Abschnitt enthält wieder die Dateinamen.

Wenn dieses Skript fertig ist, können wir die eigentliche formale Überprüfung mit diesem Befehl ausführen:

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

Das Ausführen des formalen Überprüfungstools endet mit der unzeremoniellen Anweisung:

[axi_fifo_bmc] DONE (PASS, rc=0)

Und das bedeutet nur, dass alle von uns angegebenen Eigenschaften mit allen willkürlichen Eingaben für bis zu 10 Taktzyklen erfüllt sind. Eine Erhöhung der Tiefe führt zu längeren Ausführungszeiten für den Solver. Beachten Sie jedoch, dass die Tiefe größer ist als die FIFO-Tiefe, was bedeutet, dass der BMC bei einigen Eingabesequenzen auf eine FIFO-Voll-Situation stoßen wird. Wenn wir nur, sagen wir, 5 Taktzyklen gewählt hätten, würde die formale Verifizierung niemals auf ein volles FIFO stoßen und keine diesbezüglichen Fehler finden.

Es ist möglich zu beweisen, dass die Eigenschaften für alle erfüllt sind Taktzyklen mit dem Induktionsbeweis. Das erfordert jedoch mehr Arbeit beim Schreiben der Eigenschaften. Die Herausforderung besteht darin, dass wir bisher nur einige geschrieben haben Eigenschaften. Aber für die Induktion müssen wir all angeben Eigenschaften (oder zumindest ausreichend viele). Das wäre ziemlich zeitaufwändig, also werde ich stattdessen eine alternative Strategie zur Stärkung unseres Vertrauens erörtern.

Mutation

So, jetzt haben wir einige der Eigenschaften beschrieben, die der axi_fifo Modul erfüllen muss, und unser Tool bestätigt diese Eigenschaften schnell, d. h. beweist, dass sie erfüllt sind. Aber wir haben vielleicht immer noch dieses ungute Gefühl:Sind wir sicher, dass es keine Fehler gibt? Haben wir wirklich alle Eigenschaften des axi_fifo ausgedrückt Modul?

Um diese Fragen zu beantworten und mehr Vertrauen in die Vollständigkeit der angegebenen Eigenschaften zu bekommen, können wir eine Technik namens Mutation anwenden :Wir nehmen absichtlich eine kleine Änderung in der Implementierung vor, d. h. führen absichtlich einen Fehler ein und sehen dann, ob die formale Überprüfung den Fehler findet!

Eine solche Änderung könnte darin bestehen, einen Teil der Logik zu entfernen, die out_valid steuert Signal. Wir könnten zum Beispiel diese drei Zeilen auskommentieren:

if count = 1 and read_while_write_p1 = '1' then
  out_valid_i <= '0';
end if;

Wenn wir jetzt die formale Überprüfung durchführen, erhalten wir einen Fehler mit der Meldung

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable
Writing trace to VCD file: engine_0/trace.vcd

Mit dem Tool GTKwave können wir die begleitende Wellenform anzeigen, und sie sieht wie folgt aus:

Hier sehen wir das bei 40 ns, die out_valid Das Signal sollte auf Null gehen, tut es aber nicht. Die fehlgeschlagene Assertion liegt bei 50 ns, wobei out_valid bleibt hoch, aber die out_data Signaländerungen, was auf doppelte Daten hinweist. Die duplizierten Daten wurden in diesem speziellen Trace nicht übertragen, weil out_ready ist mit 40 ns niedrig, aber die formale Überprüfung erkennt den Fehler trotzdem.

Cover-Statement

Kommen wir abschließend zu einer anderen Anwendung des formellen Verifizierungstools:Deckblatt. Der Zweck der Cover-Anweisung besteht darin, zu prüfen, ob es eine Folge von Eingaben gibt, die eine bestimmte Eigenschaft erfüllt. Da wir es mit einem FIFO zu tun haben, schauen wir mal, ob wir es komplett füllen und dann wieder leeren können. Dies kann in einer einzigen Cover-Anweisung ausgedrückt werden:

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

Das ist ein ziemlicher Mund voll! Beachten Sie die Semikolons innerhalb des {} . Zur besseren Lesbarkeit habe ich jeden Abschnitt in einer separaten Zeile platziert. Diese Cover-Anweisung lautet wie folgt:Suchen Sie nach einer Folge von Eingaben, die Folgendes erfüllt:

• Reset wird für einen Taktzyklus aktiviert.
• Jede Anzahl von Taktzyklen (wo Reset nicht bestätigt wird) kann dann vergehen.
• Ein Taktzyklus, in dem das Zurücksetzen nicht bestätigt wird und der FIFO voll ist.
• Jede Anzahl von Taktzyklen (wo Reset nicht bestätigt wird) kann dann vergehen.
• Ein Taktzyklus, in dem das Zurücksetzen nicht bestätigt wird und der FIFO leer ist.

Also die Syntax [*] bedeutet, die vorhergehende Bedingung (null oder mehrmals) zu wiederholen. In Zeile 3 hätten wir die Bedingung rst = '0' entfernen können vor [*] . Die Ergebnisse werden die gleichen sein. Der Grund dafür ist, dass der formale Verifizierer versuchen wird, den kürzesten zu finden Sequenz, die die Cover-Anweisung erfüllt, und das Setzen von Reset während des Füllens des FIFO wird dies nur verzögern. Beim Leeren des FIFOs in Zeile 5 ist es jedoch wichtig, dass kein Reset aktiviert wird.

Um den formalen Prüfer jetzt auszuführen, müssen wir eine kleine Änderung am Skript axi_fifo.sby vornehmen . Ersetzen Sie die oberen Abschnitte durch Folgendes:

[tasks]
bmc
cover

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

Jetzt führt der Solver die BMC und dann die Abdeckungsanalyse aus. In der Ausgabe sehen Sie diese beiden Zeilen:

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15.
Writing trace to VCD file: engine_0/trace5.vcd

Das bedeutet, dass die Cover-Anweisung tatsächlich mit einer Folge von 15 Taktzyklen erfüllt werden kann und der Solver speziell für diese Cover-Anweisung eine Wellenform generiert hat:

Hier sehen wir bei 80 ns, dass der FIFO voll ist und in_ready ist deaktiviert. Und bei 150 ns ist das FIFO leer und out_valid ist deaktiviert. Beachten Sie, wie während des Zeitraums von 30 ns bis 80 ns out_ready wird niedrig gehalten. Das ist notwendig, um sicherzustellen, dass sich der FIFO füllt.

Wenn wir die Bedingung count = ram_depth-1 ersetzen mit count = ram_depth , kann die Deckungsaussage nicht erfüllt werden. Das Tool meldet dann einen Fehler.

Unreached cover statement at i_axi_fifo.f_full_to_empty.

Die Fehlermeldung enthält also das Label der fehlgeschlagenen Cover-Anweisung. Das ist einer der Gründe, warum Etiketten so nützlich sind! Wir interpretieren den obigen Fehler so, dass er besagt, dass der FIFO niemals ram_depth enthalten kann Anzahl der Elemente. Dies ist genau wie im ursprünglichen AXI FIFO-Blogbeitrag angegeben.

Wohin es von hier aus geht

• Eine Einführung in die PSL-Sprache
• Eine Einführung in die formale Verifizierung
• Eine Reihe kleinerer Videos für den Einstieg in die formelle Überprüfung
• Ein Blog zum Thema formelle Verifizierung
• Eine Artikelserie mit fortgeschritteneren Themen zur formalen Verifizierung
• Eine Sammlung kleiner Beispiele mit formaler Verifizierung