Formele verificatie in VHDL met PSL

Bij het ontwerpen van VHDL voor veiligheidskritieke FPGA-toepassingen, is het niet voldoende om testbench te schrijven naar beste vermogen. Je moet bewijzen dat de module werkt zoals bedoeld en zonder ongewenste neveneffecten.

Formele verificatietechnieken kunnen u helpen een vereiste aan een test te koppelen, waarmee wordt aangetoond dat uw VHDL-module voldoet aan de specificatie. Het is een instrumenteel hulpmiddel voor het verifiëren van toepassingen in de gezondheidszorg of het verkrijgen van DO-254-certificering voor FPGA-oplossingen in de lucht.

Om formele verificatie te ontkrachten, roept VHDLwhiz de hulp in van Michael Finn Jørgensen om deze gastpost te schrijven. Michael heeft veel ervaring met het onderwerp en deelt veel tips op zijn GitHub-pagina.

Het apparaat dat in het downloadbare voorbeeld van dit artikel wordt getest, komt uit de bestaande tutorial:
Hoe maak je een AXI FIFO in blok-RAM met behulp van de kant-en-klare/geldige handshake

Ik laat Michael het vanaf hier overnemen en leg de formele verificatie aan je uit in de rest van deze blogpost.

Wat is formele verificatie?

Het doel van formele verificatie (FV) is ervoor te zorgen dat uw module werkt zoals bedoeld!

FV is iets dat u doet als onderdeel van uw ontwikkelingsproces voordat u uw module synthetiseert. Het wordt soms "Eigendomscontrole" genoemd, wat een betere omschrijving is, denk ik.

In FV specificeert u de eigenschappen uw module moet hebben, en dan zal de tool (een "Satisfiability Solver" genoemd) bewijzen dat uw module voldoet aan de eigenschappen voor alle mogelijke invoerreeksen .

Met andere woorden, de tool zoekt naar elke overgang van een geldige state (waar aan alle eigenschappen is voldaan) tot een ongeldige staat (waar een of meer eigenschappen worden geschonden). Als er geen dergelijke overgang is, d.w.z. er is geen manier om over te gaan naar een ongeldige staat, dan is bewezen dat aan de eigenschappen altijd wordt voldaan.

De uitdaging in FV is om de eigenschappen van je module uit te drukken in een taal die de tool kan begrijpen.

Formele verificatie is een alternatief voor handmatig geschreven testbanken. Het doel van zowel formele verificatie als handmatige testbanken is om bugs uit het ontwerp te verwijderen, maar formele verificatie doet dit door de eigenschappen te onderzoeken en automatisch veel verschillende testbanken te genereren.

De tools gebruiken twee verschillende methoden:

• Bounded Model Checking (BMC) . Begint vanaf reset en onderzoekt een vast aantal klokcycli.
• Inductiebestendig . Begint met een willekeurige geldige toestand en controleert of alle volgende toestanden ook geldig zijn.

Het inductiebewijs is moeilijker te bevredigen omdat het alle . vereist eigenschappen die moeten worden vermeld, terwijl BMC met slechts een paar eigenschappen kan worden uitgevoerd en toch bruikbare resultaten oplevert.

Waarom formele verificatie gebruiken?

Formele verificatie is erg goed in het opsporen van moeilijk te vinden bugs! Dat komt omdat formele verificatie automatisch de hele ruimte van mogelijke invoer doorzoekt.

Dit in tegenstelling tot traditioneel schrijven op een testbank, waarbij stimuli met de hand moeten worden gemaakt. Het is praktisch onmogelijk om de hele toestandsruimte te verkennen met behulp van handmatig geschreven testbanken.

Bovendien, wanneer formele verificatie een bug vindt, zal het een zeer korte golfvorm genereren die de bug laat zien en dit veel sneller doen dan wanneer een simulatie wordt uitgevoerd op basis van een handmatig geschreven testbench. Deze korte golfvorm is veel gemakkelijker te debuggen dan een zeer lange golfvorm die typisch voortkomt uit simulatie.

Formele verificatie is echter geen vervanging voor het schrijven van een testbank. In mijn ervaring is formele verificatie zeer geschikt voor unit-testen, terwijl het beter is om integratietests te doen met handgemaakte testbanken. Dat komt omdat de looptijd van de formele verificatie exponentieel toeneemt met de grootte van de module.

Er is inderdaad een leercurve verbonden aan formele verificatie, maar het is de tijd zeker waard, en ik hoop dat deze blogpost je helpt om over deze leercurve heen te komen. U bent sneller klaar met uw ontwerp en heeft minder bugs!

Eigenschappen schrijven in PSL

Wanneer u formele verificatie uitvoert, moet u de eigenschappen van uw module uitdrukken met behulp van de Property Specification Language (PSL). De eigenschappen bevinden zich meestal in een apart bestand met de uitgang .psl , en dit bestand wordt alleen gebruikt tijdens formele verificatie.

In dit gedeelte zal ik de belangrijkste kenmerken van de PSL-taal in algemene termen beschrijven, en in een later gedeelte zal ik u door een specifiek voorbeeld heen werken.

Er zijn drie uitspraken in PSL:

• assert
• assume
• cover

U bent misschien al bekend met het trefwoord assert bij het schrijven van testbanken. Hetzelfde trefwoord wordt ook in PSL gebruikt, maar met een iets andere syntaxis. De assert trefwoord wordt gebruikt om eigenschappen te beschrijven waaraan deze module altijd belooft te voldoen. In het bijzonder de assert trefwoord wordt toegepast op uitgangen van de module, of mogelijk ook op de interne status.

De assume trefwoord wordt gebruikt om alle vereisten te beschrijven die deze module aan de ingangen stelt. Met andere woorden, de assume trefwoord wordt toegepast op invoer in de module.

De cover trefwoord wordt gebruikt om eigenschappen te beschrijven die op de een of andere manier mogelijk moeten zijn.

U kunt ook gewone VHDL-code in het PSL-bestand schrijven, inclusief signaaldeclaraties en -processen (zowel synchroon als combinatorisch).

De eerste regel van het PSL-bestand moet zijn

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) {

Hier ENTITY_NAME en ARCHITECTURE_NAME raadpleeg de module die u verifieert. De INSTANCE_NAME kan alles zijn wat je wilt. Het bestand moet eindigen met een haakje sluiten:} .

De volgende regel in de .psl bestand moet zijn:

default clock is rising_edge(clk);

Dit vermijdt vervelend te moeten verwijzen naar het kloksignaal in elk van de eigenschappenverklaringen.

De syntaxis voor de assert en assume uitspraken is:

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

Deze verklaring luidt als volgt:Als de PRECONDITION houdt (in elke klokcyclus) dan de POSTCONDITION moet op dezelfde hetzelfde worden voldaan klokcyclus.

Er is nog een veelgebruikte vorm:

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

Deze verklaring luidt als volgt:Als de PRECONDITION houdt (in elke klokcyclus) dan de POSTCONDITION moet worden voldaan in de volgende klokcyclus.

Beide vormen worden veel gebruikt.

Binnen de PRE- en POST-CONDITIONS , kunt u het trefwoord stable . gebruiken . Dit zoekwoord betekent:De waarde in dit klokcyclus is hetzelfde als de waarde in de vorige klokcyclus.

Binnen de PRE- en POST-CONDITIONS , kunt u ook reeksen gebruiken door als volgt te schrijven:

{CONDITION_1 ; CONDITION_2}

Dit betekent dat CONDITION_1 moet worden voldaan in dit klokcyclus en dat CONDITION_2 moet worden voldaan op de volgende klokcyclus.

Het voorblad heeft de volgende syntaxis:

LABEL : cover {CONDITION}

We zullen veel voorbeelden van al deze uitspraken zien in het uitgewerkte voorbeeld verderop in deze blog.

De vereiste tools installeren

Formele verificatie wordt ondersteund door de toonaangevende leveranciers van tools, waaronder ModelSim. Helaas ondersteunt de Studenteneditie van ModelSim GEEN formele verificatie. U krijgt inderdaad de volgende foutmelding:

Dus om ModelSim te gebruiken voor formele verificatie is een betaalde licentie vereist.

In plaats daarvan zijn er open-source (gratis) tools waarmee u formele verificatie kunt uitvoeren. In dit gedeelte zal ik je door het installatieproces van deze tools leiden.

Deze handleiding gaat ervan uit dat je op een Linux-platform draait. Als u op een Windows-platform werkt, raad ik u aan het Windows-subsysteem voor Linux (WSL) te gebruiken. De volgende gids is geverifieerd met Ubuntu 20.04 LTS.

Vereisten

Eerst moeten we het systeem bijwerken om de nieuwste patches te krijgen:

sudo apt update
sudo apt upgrade

Dan moeten we enkele aanvullende ontwikkelpakketten installeren:

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.

Er zijn voorverpakte binaire bestanden voor GHDL, maar ik raad aan om de nieuwste bronbestanden te downloaden en als volgt te compileren:

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

Download het voorbeeldproject

De volgende sectie van dit artikel begeleidt u bij het implementeren van formele verificatie voor een bestaand VHDL-project. U kunt de volledige code downloaden door uw e-mailadres in het onderstaande formulier in te voeren.

Uitgewerkt voorbeeld met formele verificatie

In het volgende gedeelte wordt beschreven hoe u de axi_fifo-module waarover eerder op deze blog is geschreven, formeel kunt verifiëren.

Om te beginnen met de formele verificatie, moeten we ons afvragen, welke eigenschappen heeft de FIFO? Ik heb vier categorieën eigenschappen geïdentificeerd:

• Reset-afhandeling:dat de module ontwaakt in een goed gedefinieerde staat na reset.
• FIFO vol en leeg signalering:hiermee wordt gecontroleerd of de FIFO de vol- en leegcondities correct aangeeft.
• AXI protocol:Dat de module voldoet aan de eisen van de AXI valid/ready handshake.
• FIFO-bestelling:dat de FIFO geen elementen laat vallen/dupliceren/herordenen die er doorheen gaan.

Ik zal elk van deze eigenschappen hieronder bespreken.

Behandeling resetten

Eerst verklaren we dat de module verwacht dat de reset wordt uitgevoerd voor één klokcyclus:

f_reset : assume {rst};

Let hier op de afwezigheid van het trefwoord always . Zonder de always trefwoord, de instructie geldt alleen voor de allereerste klokcyclus.

Het is gebruikelijk (en zeer nuttig) om elke formele verklaring een label te geven. Bij het uitvoeren van de formele verificatie verwijst de tool naar deze labels bij het melden van eventuele fouten. Ik gebruik de conventie om al dergelijke labels vooraf te laten gaan met f_ .

Dan stellen we dat de FIFO leeg moet zijn na reset:

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

Merk op dat het mogelijk is om te verwijzen naar interne signalen in de module en niet alleen poorten. Hier verwijzen we naar count , wat het huidige vulniveau is, d.w.z. het aantal elementen dat zich momenteel in de FIFO bevindt. Dat is mogelijk omdat we verwijzen naar de architectuurnaam in de eerste regel van het PSL-bestand.

We kunnen ook een apart proces in het PSL-bestand hebben dat het aantal elementen telt dat in en uit de FIFO gaat. Hoewel dat de voorkeur heeft, ga ik het interne telsignaal gebruiken om deze blogpost kort en bondig te houden.

FIFO vol en leeg signalering

De manier waarop de AXI FIFO vol en leeg signaleert is met de out_valid en in_ready signalen. De out_valid signaal wordt bevestigd wanneer de FIFO niet leeg is, en de in_ready signaal wordt bevestigd wanneer de FIFO niet vol is. Laten we deze eigenschappen eens controleren:

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

AXI-protocol

De geldige/klaar AXI-handshake stelt dat gegevensoverdracht alleen plaatsvindt wanneer zowel valid en ready gelijktijdig worden beweerd. Een typische fout bij het werken met dit protocol is het bevestigen van geldige (en bijbehorende gegevens) en het niet controleren op gereedheid. Met andere woorden, als valid wordt bevestigd en ready niet is, dan valid moet de volgende klokcyclus gehandhaafd blijven en de gegevens moeten ongewijzigd blijven. Dat geldt zowel voor gegevens die de FIFO binnenkomen als voor de gegevens die uit de FIFO komen. Voor gegevens die de FIFO invoeren, gebruiken we de assume trefwoord, en voor gegevens die uit de FIFO komen, gebruiken we de assert zoekwoord.

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

Let hier op het gebruik van de stable trefwoord in combinatie met de |=> exploitant. Deze uitspraken verwijzen naar twee opeenvolgende klokcycli. Bij de eerste klokcyclus controleert het of valid wordt bevestigd en ready wordt niet beweerd. Dan op de volgende (tweede) klokcyclus (aangegeven door de |=> operator), de waarden van valid en data moet hetzelfde zijn als de vorige (d.w.z. eerste) klokcyclus.

Ten tweede vereisen we voor het AXI-protocol dat de ready signaal is stabiel. Dit betekent dat de FIFO gegevens kan accepteren (ready wordt bevestigd) maar er worden geen gegevens ingevoerd (valid wordt niet bevestigd), dan bij de volgende klokcyclus ready moet blijven gelden.

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

Een andere belangrijke eigenschap van een FIFO is dat gegevens niet worden gedupliceerd/verwijderd/verwisseld. Het uitdrukken van deze eigenschap in PSL is vrij complex, en dit is het moeilijkste deel van deze formele verificatie. Laten we deze woning stap voor stap zorgvuldig doornemen.

We kunnen in het algemeen zeggen dat als gegevens D1 de FIFO binnenkomen vóór andere gegevens D2, dan aan de uitvoerzijde dezelfde gegevens D1 de FIFO moeten verlaten voordat D2 dat doet.

Om dit in PSL uit te drukken hebben we enkele hulpsignalen nodig:f_sampled_in_d1 , f_sampled_in_d2 , f_sampled_out_d1 , en f_sampled_out_d2 . Deze signalen worden gewist bij reset en bevestigd wanneer D1 of D2 de FIFO binnenkomt of verlaat. Eenmaal bevestigd, blijven deze signalen gehandhaafd.

Dus we drukken de FIFO-bestellingseigenschap uit in twee delen:Eerst een aanname dat zodra D2 de FIFO binnenkomt, D1 al eerder is ingevoerd:

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

En ten tweede een bewering dat zodra D2 de FIFO verlaat, D1 al eerder is vertrokken:

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

We moeten nog steeds de hierboven genoemde bemonsteringssignalen declareren en invullen. We doen dit als volgt voor de ingangsbemonsteringssignalen:

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 verwijzen we naar twee andere signalen, f_value_d1 en f_value_d2 . Ze bevatten de gegevenswaarden D1 en D2. Deze signalen kunnen elke willekeurige . bevatten waarden, en er is een speciale manier om dit aan de formele verificatietool aan te geven:

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;

De anyconst kenmerk wordt herkend door de formele verificatietool. Het geeft aan dat de tool elke constante waarde op zijn plaats kan invoegen.

Met het bovenstaande hebben we de eigenschappen van de FIFO gespecificeerd.

Formele verificatie uitvoeren

Voordat we de formele verificatietool kunnen gebruiken, moeten we een klein script axi_fifo.sby . schrijven :

[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

De sectie [tasks] stelt dat we Bounded Model Checking willen. De sectie [options] specificeert dat BMC 10 klokcycli moet draaien. De standaard is 20. De sectie [engines] kiest welke van de verschillende oplossers moet worden gebruikt. Er kunnen verschillen zijn in uitvoeringssnelheid van de verschillende mogelijke motoren, afhankelijk van uw specifieke ontwerp. Laat deze waarde voorlopig ongewijzigd.

De [script] sectie is het interessante deel. Hier specificeren we de VHDL-standaard (2008), de waarden van de generieke geneesmiddelen, de bestanden die moeten worden verwerkt en de naam van de entiteit op het hoogste niveau. Eindelijk, de [files] sectie bevat opnieuw de bestandsnamen.

Als dit script gereed is, kunnen we de feitelijke formele verificatie uitvoeren met dit commando:

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

Het uitvoeren van de formele verificatietool eindigt met de niet-ceremoniële verklaring:

[axi_fifo_bmc] DONE (PASS, rc=0)

En dat betekent gewoon dat alle eigenschappen die we hebben gespecificeerd tevreden zijn met alle willekeurige ingangen voor maximaal 10 klokcycli. Het vergroten van de diepte leidt tot langere uitvoeringstijden voor de oplosser. Houd er echter rekening mee dat de diepte groter is dan de diepte van de FIFO, wat betekent dat de BMC voor sommige invoersequenties een FIFO-volledige situatie zal tegenkomen. Als we bijvoorbeeld maar 5 klokcycli hadden gekozen, zou de formele verificatie nooit een FIFO vol tegenkomen en geen bugs ontdekken die daarmee verband houden.

Het is mogelijk om aan te tonen dat de eigenschappen voor alle tevreden zijn klokcycli met behulp van de inductieproef. Dat vereist echter meer werk bij het schrijven van de eigenschappen. De uitdaging is dat we tot nu toe net sommige . hebben geschreven eigendommen. Maar voor inductie moeten we alle . specificeren eigenschappen (of in ieder geval voldoende veel). Dat zou behoorlijk tijdrovend zijn, dus in plaats daarvan zal ik een alternatieve strategie bespreken om ons vertrouwen te vergroten.

Mutatie

Dus nu hebben we enkele eigenschappen beschreven die de axi_fifo module moet voldoen, en onze tool bevestigt snel die eigenschappen, d.w.z. bewijst dat ze tevreden zijn. Maar misschien hebben we nog steeds dit ongemakkelijke gevoel:weten we zeker dat er geen bugs zijn? Hebben we echt alle eigenschappen van de axi_fifo . uitgedrukt? module?

Om deze vragen te helpen beantwoorden en meer vertrouwen te krijgen in de volledigheid van de gespecificeerde eigenschappen, kunnen we een techniek toepassen die mutatie wordt genoemd. :We brengen doelbewust een kleine wijziging in de implementatie aan, d.w.z. introduceren opzettelijk een bug, en kijken dan of de formele verificatie de bug zal opvangen!

Een dergelijke verandering zou kunnen zijn om een ​​deel van de logica te verwijderen die de out_valid . bestuurt signaal. We kunnen bijvoorbeeld deze drie regels van commentaar voorzien:

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

Wanneer we nu de formele verificatie uitvoeren, krijgen we een fout met het bericht

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

Met behulp van de tool GTKwave kunnen we de bijbehorende golfvorm bekijken en deze ziet er als volgt uit:

Hier zien we dat bij 40 ns de out_valid signaal zou naar nul moeten gaan, maar dat doet het niet. De bewering die mislukt is op 50 ns, waarbij out_valid blijft hoog, maar de out_data signaalveranderingen, wat duidt op dubbele gegevens. De gedupliceerde gegevens zijn niet daadwerkelijk verzonden in dit specifieke spoor omdat out_ready is laag bij 40 ns, maar de formele verificatie detecteert de bug niettemin.

Overzichtsverklaring

Laten we eindelijk eens kijken naar een andere toepassing van de formele verificatietool:Cover statement. Het doel van de omslagfoto is om te controleren of er een reeks invoer is die aan een bepaalde eigenschap voldoet. Aangezien we te maken hebben met een FIFO, laten we eens kijken of we deze volledig kunnen vullen en vervolgens weer kunnen legen. Dit kan worden uitgedrukt in een enkele dekkingsverklaring:

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

Dat is een hele mond vol! Let op de puntkomma's binnen de {} . Voor de leesbaarheid heb ik elke sectie op een aparte regel geplaatst. Deze algemene verklaring luidt als volgt:Zoek naar een reeks invoer die voldoet aan:

• Reset wordt uitgevoerd voor één klokcyclus.
• Een willekeurig aantal klokcycli (waarbij reset niet wordt uitgevoerd) kan dan voorbijgaan.
• Eén klokcyclus waarbij reset niet wordt uitgevoerd en de FIFO vol is.
• Een willekeurig aantal klokcycli (waarbij reset niet wordt uitgevoerd) kan dan voorbijgaan.
• Eén klokcyclus waarbij reset niet wordt uitgevoerd en de FIFO leeg is.

Dus de syntaxis [*] betekent herhaal (nul of meer keer) de voorgaande voorwaarde. In regel 3 hadden we de voorwaarde rst = '0' . kunnen verwijderen voor [*] . De resultaten zullen hetzelfde zijn. De reden is dat de formele verificateur zal proberen de kortste . te vinden volgorde die voldoet aan de coververklaring, en het bevestigen van reset tijdens het vullen van de FIFO zal dat alleen maar vertragen. Bij het legen van de FIFO in regel 5 is het echter essentieel dat reset niet wordt uitgevoerd.

Om de formele verificatie nu uit te voeren, moeten we een kleine wijziging aanbrengen in het script axi_fifo.sby . Vervang de bovenste secties door het volgende:

[tasks]
bmc
cover

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

Nu zal de oplosser de BMC uitvoeren en vervolgens de dekkingsanalyse uitvoeren. In de uitvoer zie je deze twee regels:

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

Dit betekent dat de coververklaring inderdaad kan worden voldaan met een reeks van 15 klokcycli, en de oplosser heeft specifiek voor deze coververklaring een golfvorm gegenereerd:

Hier zien we bij 80 ns dat de FIFO vol is en in_ready wordt ontkracht. En bij 150 ns is de FIFO leeg en out_valid wordt ontkracht. Merk op hoe tijdens de periode van 30 ns tot 80 ns dat out_ready laag wordt gehouden. Dat is nodig om ervoor te zorgen dat de FIFO vol raakt.

Als we de voorwaarde count = ram_depth-1 . vervangen met count = ram_depth , kan niet worden voldaan aan de dekkingsverklaring. De tool meldt dan een fout.

Unreached cover statement at i_axi_fifo.f_full_to_empty.

Het foutbericht bevat dus het label van het voorblad dat mislukt. Dat is een van de redenen waarom etiketten zo handig zijn! We interpreteren de bovenstaande fout als waarin staat dat de FIFO nooit ram_depth . kan bevatten aantal elementen. Dit is precies zoals vermeld in de originele AXI FIFO-blogpost.

Waar te gaan vanaf hier

• Een inleiding op de PSL-taal
• Een inleiding tot formele verificatie
• Een reeks kleinere video's om aan de slag te gaan met formele verificatie
• Een blog over formele verificatie
• Een serie artikelen met meer geavanceerde onderwerpen in formele verificatie
• Een verzameling kleine voorbeelden met formele verificatie