Verificação formal em VHDL usando PSL

Ao projetar VHDL para aplicativos FPGA de segurança crítica, não é suficiente escrever testbenches com o melhor esforço. Você deve apresentar prova de que o módulo funciona como pretendido e sem efeitos colaterais indesejáveis.

As técnicas de verificação formal podem ajudá-lo a mapear um requisito para um teste, provando que seu módulo VHDL está em conformidade com a especificação. É uma ferramenta instrumental para verificar aplicações de saúde ou obter a certificação DO-254 para soluções FPGA aerotransportadas.

Para desmistificar a verificação formal, VHDLwhiz pede a ajuda de Michael Finn Jørgensen para escrever este guest post. Michael tem experiência substancial no assunto e compartilha muitas dicas em sua página do GitHub.

O dispositivo em teste no exemplo para download deste artigo vem do tutorial existente:
Como fazer um AXI FIFO em bloco de RAM usando o handshake pronto/válido

Vou deixar Michael assumir a partir daqui e explicar a verificação formal para você no restante desta postagem do blog.

O que é verificação formal?

O objetivo da verificação formal (FV) é garantir que seu módulo funcione conforme o esperado!

FV é algo que você faz como parte de seu processo de desenvolvimento antes de sintetizar seu módulo. Às vezes é chamado de “Verificação de propriedades”, que é uma descrição melhor, eu acho.

Em FV você especifica as propriedades seu módulo deve ter, e então a ferramenta (chamada de “Solucionador de Satisfação”) irá provar que seu módulo satisfaz as propriedades para todas as sequências possíveis de entradas .

Em outras palavras, a ferramenta procurará qualquer transição de um válido state (onde todas as propriedades são satisfeitas) para um invalid estado (onde uma ou mais propriedades são violadas). Se não houver tal transição, ou seja, não há como fazer a transição para um estado inválido, as propriedades provaram ser sempre satisfeitas.

O desafio em FV é expressar as propriedades do seu módulo em uma linguagem que a ferramenta possa entender.

A verificação formal é uma alternativa aos testbenches escritos manualmente. O objetivo da verificação formal e dos testbenches manuais é eliminar bugs do design, mas a verificação formal faz isso examinando as propriedades e gerando muitos testbenches diferentes automaticamente.

As ferramentas usam dois métodos diferentes:

Verificação de modelo limitado (BMC) . Inicia da reinicialização e examina um número fixo de ciclos de clock.
Prova de indução . Inicia a partir de um estado válido arbitrário e verifica se todos os estados subsequentes também são válidos.

A prova de indução é mais difícil de satisfazer porque requer todos propriedades a serem declaradas, enquanto o BMC pode ser executado com apenas algumas propriedades e ainda fornecer resultados úteis.

Por que usar a verificação formal?

A verificação formal é muito boa para capturar bugs difíceis de encontrar! Isso porque a verificação formal pesquisa automaticamente todo o espaço de entradas possíveis.

Isso contrasta com a escrita tradicional em bancada que exige a criação manual de estímulos. É praticamente impossível explorar todo o espaço de estado usando testbenches escritos manualmente.

Além disso, quando a verificação formal encontrar um bug, ela gerará uma forma de onda muito curta mostrando o bug e fará isso muito mais rápido do que ao executar uma simulação baseada em um testbench escrito manualmente. Essa forma de onda curta é muito mais fácil de depurar do que uma forma de onda muito longa que normalmente surge da simulação.

No entanto, a verificação formal não é um substituto para a redação do testbench. Na minha experiência, a verificação formal é adequada para testes de unidade, enquanto é melhor fazer testes de integração usando testbenches feitos à mão. Isso porque o tempo de execução da verificação formal aumenta exponencialmente com o tamanho do módulo.

De fato, existe uma curva de aprendizado associada à verificação formal, mas vale a pena o tempo, e espero que esta postagem no blog ajude você a superar essa curva de aprendizado. Você concluirá seu design mais cedo e terá menos bugs!

Como escrever propriedades em PSL

Ao fazer a verificação formal, você deve expressar as propriedades do seu módulo usando a Property Specification Language (PSL). As propriedades geralmente estão localizadas em um arquivo separado com o final .psl , e esse arquivo é usado apenas durante a verificação formal.

Nesta seção, descreverei os principais recursos da linguagem PSL em termos gerais e, em uma seção posterior, mostrarei um exemplo específico.

Existem três declarações no PSL:

assert
assume
cover

Você já deve estar familiarizado com a palavra-chave assert ao escrever testbenches. Essa mesma palavra-chave também é usada no PSL, mas com uma sintaxe ligeiramente diferente. O assert palavra-chave é usada para descrever propriedades que este módulo promete sempre satisfazer. Em particular, o assert A palavra-chave é aplicada às saídas do módulo, ou possivelmente também ao estado interno.

O assume palavra-chave é usada para descrever quaisquer requisitos que este módulo impõe às entradas. Em outras palavras, o assume palavra-chave é aplicada às entradas no módulo.

O cover palavra-chave é usada para descrever propriedades que devem ser possíveis de alcançar de alguma forma.

Você também pode escrever código VHDL regular no arquivo PSL, incluindo declarações e processos de sinal (tanto síncronos quanto combinatórios).

A primeira linha do arquivo PSL deve ser

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) {

Aqui ENTITY_NAME e ARCHITECTURE_NAME consulte o módulo que você está verificando. O INSTANCE_NAME pode ser o que você quiser. O arquivo deve terminar com uma chave de fechamento:} .

A próxima linha no .psl arquivo deve ser:

default clock is rising_edge(clk);

Isso evita ter que se referir ao sinal de clock em cada uma das declarações de propriedade.

A sintaxe para o assert e assume declarações é:

LABEL : assert always {PRECONDITION} |-&gt; {POSTCONDITION}
LABEL : assume always {PRECONDITION} |-&gt; {POSTCONDITION}

Esta declaração é a seguinte:Se o PRECONDITION detém (em qualquer ciclo de clock) então o POSTCONDITION deve ser satisfeito no mesmo ciclo do relógio.

Existe outra forma comumente usada:

LABEL : assert always {PRECONDITION} |=&gt; {POSTCONDITION}

Esta declaração é a seguinte:Se o PRECONDITION detém (em qualquer ciclo de clock) então o POSTCONDITION deve ser satisfeito no próximo ciclo do relógio.

Ambas as formas são amplamente utilizadas.

Dentro do PRE- e POST-CONDITIONS , você pode usar a palavra-chave stable . Esta palavra-chave significa:O valor em this ciclo de clock é o mesmo que o valor no anterior ciclo do relógio.

Dentro do PRE- e POST-CONDITIONS , você também pode usar sequências, escrevendo da seguinte forma:

{CONDITION_1 ; CONDITION_2}

Isso significa que CONDITION_1 deve ser satisfeito neste ciclo de clock e que CONDITION_2 deve ser satisfeito no próximo ciclo do relógio.

A declaração de capa tem a seguinte sintaxe:

LABEL : cover {CONDITION}

Veremos muitos exemplos de todas essas declarações no exemplo trabalhado mais adiante neste blog.

Instalando as ferramentas necessárias

A verificação formal é suportada pelos principais fornecedores de ferramentas, incluindo ModelSim. Infelizmente, a Student Edition do ModelSim NÃO suporta verificação formal. Na verdade, você recebe o seguinte erro:

Portanto, usar o ModelSim para verificação formal requer uma licença paga.

Em vez disso, existem ferramentas de código aberto (gratuitas) que permitem a verificação formal. Nesta seção, vou guiá-lo pelo processo de instalação dessas ferramentas.

Este guia pressupõe que você esteja executando em uma plataforma Linux. Se você estiver em uma plataforma Windows, recomendo usar o Windows Subsystem for Linux (WSL). O guia a seguir é verificado usando o Ubuntu 20.04 LTS.

Pré-requisitos

Primeiro, devemos atualizar o sistema para obter os patches mais recentes:

sudo apt update
sudo apt upgrade

Em seguida, devemos instalar alguns pacotes de desenvolvimento adicionais:

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.

Existem binários pré-empacotados para GHDL, mas eu recomendo baixar os arquivos de origem mais recentes e compilá-los da seguinte forma:

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

Faça o download do projeto de exemplo

A próxima seção deste artigo orienta você na implementação da verificação formal para um projeto VHDL existente. Você pode baixar o código completo digitando seu endereço de e-mail no formulário abaixo.

Exemplo trabalhado com verificação formal

A seção a seguir descreverá como verificar formalmente o módulo axi_fifo descrito anteriormente neste blog.

Para começar a verificação formal, precisamos nos perguntar:quais propriedades o FIFO possui? Identifiquei quatro categorias de propriedades:

Manuseio de redefinição:que o módulo acorde em um estado bem definido após a redefinição.
Sinalização FIFO cheia e vazia:isso verifica se a FIFO indica corretamente as condições cheias e vazias.
Protocolo AXI:se o módulo atende aos requisitos do handshake válido/pronto do AXI.
Ordenação FIFO:que o FIFO não descarte/duplica/reordene os elementos que passam por ele.

Discutirei cada uma dessas propriedades a seguir.

Redefinir manuseio

Primeiro, declaramos que o módulo espera que o reset seja declarado por um ciclo de clock:

f_reset : assume {rst};

Observe aqui a ausência da palavra-chave always . Sem o always palavra-chave, a instrução é válida apenas para o primeiro ciclo de clock.

É costume (e muito útil) dar um rótulo a cada declaração formal. Ao executar a verificação formal, a ferramenta fará referência a esses rótulos ao relatar quaisquer falhas. Eu uso a convenção de preceder todos esses rótulos com f_ .

Em seguida, afirmamos que o FIFO deve estar vazio após o reset:

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

Observe que é possível fazer referência a internos sinais no módulo e não apenas nas portas. Aqui fazemos referência a count , que é o nível de preenchimento atual, ou seja, o número de elementos atualmente no FIFO. Isso é possível porque nos referimos ao nome da arquitetura na primeira linha do arquivo PSL.

Alternativamente, poderíamos ter um processo separado no arquivo PSL contando o número de elementos que entram e saem do FIFO. Embora isso deva ser preferido, vou usar o sinal de contagem interno para manter esta postagem no blog curta e direta.

Sinalização FIFO cheia e vazia

A forma como o AXI FIFO sinaliza cheio e vazio é com o out_valid e in_ready sinais. O out_valid sinal é afirmado sempre que o FIFO não está vazio, e o in_ready sinal é afirmado sempre que o FIFO não está cheio. Vamos verificar essas propriedades:

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

Protocolo AXI

O handshake AXI válido/pronto afirma que a transferência de dados só acontece quando os dois valid e ready são afirmados simultaneamente. Um erro típico ao trabalhar com este protocolo é declarar válido (e acompanhar os dados) e não verificar pronto. Em outras palavras, se valid é afirmado e ready não é, então valid devem permanecer ativos no próximo ciclo de clock, e os dados devem permanecer inalterados. Isso se aplica tanto aos dados que entram no FIFO quanto aos dados que saem do FIFO. Para dados que entram no FIFO, usamos o assume palavra-chave, e para dados que saem do FIFO, usamos o assert palavra-chave.

f_in_data_stable : assume always
   {in_valid and not in_ready and not rst} |=&gt;
   {stable(in_valid) and stable(in_data)};

f_out_data_stable : assert always
   {out_valid and not out_ready and not rst} |=&gt;
   {stable(out_valid) and stable(out_data)};

Observe aqui o uso do stable palavra-chave em combinação com o |=> operador. Essas instruções fazem referência a dois ciclos de clock consecutivos. No primeiro ciclo de clock, ele verifica se valid é afirmado e ready não é afirmado. Em seguida, no próximo (segundo) ciclo de clock (indicado pelo |=> operador), os valores de valid e data deve ser o mesmo que o ciclo de clock anterior (ou seja, o primeiro).

Em segundo lugar, para o protocolo AXI, exigimos que o ready sinal é estável. O que isto significa é se o FIFO pode aceitar dados (ready é afirmado), mas nenhum dado é inserido (valid não é afirmado), então no próximo ciclo de clock ready deve permanecer afirmado.

f_out_ready_stable : assume always
   {out_ready and not out_valid and not rst} |=&gt;
   {stable(out_ready)};

f_in_ready_stable : assert always
   {in_ready and not in_valid and not rst} |=&gt;
   {stable(in_ready)};

Pedido FIFO

Outra propriedade importante de um FIFO é que os dados não são duplicados/excluídos/trocados. Expressar esta propriedade em PSL é bastante complexo, e esta é a parte mais difícil desta verificação formal. Vamos percorrer esta propriedade cuidadosamente passo a passo.

Podemos dizer em geral que se algum dado D1 entra no FIFO antes de algum outro dado D2, então no lado de saída o mesmo dado D1 deve sair do FIFO antes que D2 o faça.

Para expressar isso em PSL precisamos de alguns sinais auxiliares:f_sampled_in_d1 , f_sampled_in_d2 , f_sampled_out_d1 e f_sampled_out_d2 . Esses sinais são apagados no reset e ativados sempre que D1 ou D2 entra ou sai da FIFO. Uma vez ativados, esses sinais permanecem ativos.

Assim, expressamos a propriedade de ordenação FIFO em duas partes:Primeiro, uma suposição que uma vez que D2 entra no FIFO, então D1 já entrou anteriormente:

f_fifo_ordering_in : assume always
   {f_sampled_in_d2} |-&gt;
   {f_sampled_in_d1};

E em segundo lugar uma asserção que uma vez que D2 sai do FIFO, então D1 já saiu anteriormente:

f_fifo_ordering_out : assert always
   {f_sampled_out_d2} |-&gt;
   {f_sampled_out_d1};

Ainda precisamos declarar e preencher os sinais de amostragem mencionados acima. Fazemos isso da seguinte forma para os sinais de amostragem de entrada:

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 &lt;= '1';
         end if;
         if in_data = f_value_d2 then
            f_sampled_in_d2 &lt;= '1';
         end if;
      end if;

      if out_valid then
         if out_data = f_value_d1 then
            f_sampled_out_d1 &lt;= '1';
         end if;
         if out_data = f_value_d2 then
            f_sampled_out_d2 &lt;= '1';
         end if;
      end if;

      if rst = '1' then
         f_sampled_in_d1  &lt;= '0';
         f_sampled_in_d2  &lt;= '0';
         f_sampled_out_d1 &lt;= '0';
         f_sampled_out_d2 &lt;= '0';
      end if;
   end if;
end process p_sampled;

Aqui estamos referenciando dois outros sinais, f_value_d1 e f_value_d2 . Eles contêm os valores de dados D1 e D2. Esses sinais podem conter qualquer sinal arbitrário valores, e há uma maneira especial de indicar isso para a ferramenta de verificação formal:

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;

O anyconst atributo é reconhecido pela ferramenta de verificação formal. Indica que a ferramenta pode inserir qualquer valor constante em seu lugar.

Com o acima, especificamos as propriedades do FIFO.

Executando verificação formal

Antes de podermos executar a ferramenta de verificação formal, precisamos escrever um pequeno script axi_fifo.sby :

[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

A seção [tasks] afirma que queremos a Verificação de Modelo Limitado. A seção [options] especifica que o BMC deve ser executado por 10 ciclos de clock. O padrão é 20. A seção [engines] escolhe qual dos vários solucionadores diferentes usar. Pode haver diferenças na velocidade de execução dos diferentes motores possíveis, dependendo do seu projeto específico. Por enquanto, apenas deixe esse valor inalterado.

O [script] seção é a parte interessante. Aqui especificamos o padrão VHDL (2008), os valores dos genéricos, os arquivos a serem processados e o nome da entidade de nível superior. Por fim, o [files] seção contém os nomes dos arquivos novamente.

Com este script pronto, podemos executar a verificação formal real usando este comando:

sby --yosys &quot;;yosys -m ghdl&quot;; -f axi_fifo.sby

A execução da ferramenta de verificação formal termina com a declaração sem cerimônia:

[axi_fifo_bmc] DONE (PASS, rc=0)

E isso significa apenas que todas as propriedades que especificamos são satisfeitas com todas as entradas arbitrárias por até 10 ciclos de clock. Aumentar a profundidade leva a tempos de execução mais longos para o solver. No entanto, observe que a profundidade é maior que a profundidade do FIFO, o que significa que o BMC encontrará uma situação FIFO completa para algumas sequências de entrada. Se tivéssemos escolhido apenas, digamos, 5 ciclos de clock, a verificação formal nunca encontraria um FIFO completo e não detectaria nenhum bug relacionado a isso.

É possível provar que as propriedades são satisfeitas para todos ciclos de clock usando a prova de indução. No entanto, isso requer mais trabalho escrevendo as propriedades. O desafio é que, até agora, acabamos de escrever algumas propriedades. Mas para indução, precisamos especificar todos propriedades (ou pelo menos o suficiente). Isso consumiria bastante tempo, então, em vez disso, discutirei uma estratégia alternativa para aumentar nossa confiança.

Mutação

Então, agora descrevemos algumas das propriedades que o axi_fifo módulo deve satisfazer, e nossa ferramenta rapidamente confirma essas propriedades, ou seja, prova que elas estão satisfeitas. Mas ainda podemos ter essa sensação desconfortável:temos certeza de que não há bugs? Nós realmente expressamos todas as propriedades do axi_fifo módulo?

Para ajudar a responder a essas perguntas e obter mais confiança na integridade das propriedades especificadas, podemos aplicar uma técnica chamada mutação :Propositalmente fazemos uma pequena mudança na implementação, ou seja, introduzimos deliberadamente um bug e, em seguida, vemos se a verificação formal detectará o bug!

Uma dessas mudanças pode ser remover parte da lógica que controla o out_valid sinal. Por exemplo, poderíamos comentar estas três linhas:

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

Quando executamos a verificação formal agora recebemos uma falha com a mensagem

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

Usando a ferramenta GTKwave, podemos visualizar a forma de onda que a acompanha e se parece com o seguinte:

Aqui vemos que em 40 ns, o out_valid sinal deve ir para zero, mas isso não acontece. A asserção que falha é em 50 ns, onde out_valid permanece alto, mas o out_data alterações de sinal, indicando dados duplicados. Os dados duplicados não foram realmente transmitidos neste rastreamento específico porque out_ready é baixo em 40 ns, mas a verificação formal detecta o bug mesmo assim.

Declaração de capa

Vamos finalmente voltar para uma aplicação diferente da ferramenta de verificação formal:Declaração de capa. O objetivo da declaração de capa é verificar se existe uma sequência de entradas que satisfaça uma propriedade específica. Como estamos lidando com um FIFO, vamos ver se podemos preenchê-lo completamente e depois esvaziá-lo novamente. Isso pode ser expresso em uma única declaração de capa:

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

Isso é um bocado cheio! Observe os pontos e vírgulas dentro do {} . Para facilitar a leitura, coloquei cada seção em uma linha separada. Esta declaração de capa tem a seguinte redação:Procure uma sequência de entradas que satisfaça:

A reinicialização é confirmada por um ciclo de clock.
Qualquer número de ciclos de clock (onde a redefinição não é declarada) pode passar.
Um ciclo de clock em que a reinicialização não é confirmada e o FIFO está cheio.
Qualquer número de ciclos de clock (onde a redefinição não é declarada) pode passar.
Um ciclo de clock em que a reinicialização não é confirmada e o FIFO está vazio.

Portanto, a sintaxe [*] significa repetir (zero ou mais vezes) a condição anterior. Na linha 3, poderíamos ter removido a condição rst = '0' na frente de [*] . Os resultados serão os mesmos. A razão é que o verificador formal tentará encontrar o mais curto seqüência que satisfaça a declaração de capa, e afirmando reset enquanto preenche o FIFO apenas atrasará isso. No entanto, ao esvaziar o FIFO na linha 5, é essencial que o reset não seja ativado.

Para executar o verificador formal agora, precisamos fazer uma pequena modificação no script axi_fifo.sby . Substitua as seções superiores pelas seguintes:

[tasks]
bmc
cover

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

Agora, o solver executará o BMC e, em seguida, executará a análise de cobertura. Na saída você verá estas duas linhas:

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

Isso significa que a declaração de capa pode realmente ser satisfeita com uma sequência de 15 ciclos de clock, e o solver gerou uma forma de onda especificamente para esta declaração de capa:

Aqui vemos em 80 ns que o FIFO está cheio e in_ready é desativada. E em 150 ns o FIFO está vazio e out_valid é desativada. Observe como durante o período de 30 ns a 80 ns que out_ready é mantido baixo. Isso é necessário para garantir que o FIFO esteja sendo preenchido.

Se substituirmos a condição count = ram_depth-1 com count = ram_depth , a declaração de capa não pode ser satisfeita. A ferramenta então relata um erro.

Unreached cover statement at i_axi_fifo.f_full_to_empty.

Portanto, a mensagem de erro contém o rótulo da declaração de capa que falha. Essa é uma das razões pelas quais os rótulos são tão úteis! Interpretamos o erro acima como afirmando que o FIFO nunca pode conter ram_depth número de elementos. Isso é exatamente como afirmado na postagem original do blog AXI FIFO.

Para onde ir a partir daqui

Uma cartilha sobre a linguagem PSL
Uma introdução à verificação formal
Uma série de vídeos menores para dar os primeiros passos na verificação formal
Um blog relacionado à verificação formal
Uma série de artigos com tópicos mais avançados em verificação formal
Uma coleção de pequenos exemplos usando verificação formal

Introdução ao VUnit Usando Integrated Logic Analyzer (ILA) e Virtual Input/Output (VIO)

VHDL