Dominando Verificação Formal de Módulos VHDL com PSL

Ao projetar VHDL para aplicações FPGA críticas de segurança, simplesmente escrever testbenches não basta. Engenheiros devem provar que um módulo comporta-se exatamente como especificado, livre de efeitos colaterais ocultos. Verificação formal fornece essa garantia matemática.

Verificação formal preenche a lacuna entre requisitos e implementação provando que toda sequência possível de entradas satisfaz as propriedades do design. É indispensável para certificar dispositivos médicos, sistemas avionicos, ou qualquer domínio onde certificação DO‑254 é requerida.

Neste artigo convidado, Michael Finn Jørgensen — praticante experiente em verificação formal — compartilha insights práticos e dicas acionáveis. O exemplo abaixo baseia-se no tutorial familiar de FIFO AXI How to make an AXI FIFO in block RAM using the ready/valid handshake e demonstra como aplicar PSL a um design VHDL real.

O que é Verificação Formal?

Verificação formal (FV) é um método sistemático, pré-síntese, que garante correção do design para todas combinações de entrada. Diferente de testbenches convencionais, que dependem de estímulos manualmente criados, FV especifica propriedades que devem valer a cada ciclo de clock. Um solver SAT então prova exaustivamente que estas propriedades são satisfeitas — ou aponta um contra-exemplo se não forem.

Duas técnicas centrais impulsionam FV:

• Bounded Model Checking (BMC) — verifica número finito de ciclos, partindo do reset.
• Prova por Indução — verifica que se um estado é válido, todos estados subsequentes permanecem válidos. Requer conjunto completo de propriedades mas garante para número infinito de ciclos.

Como BMC pode rodar com apenas algumas propriedades, é frequentemente a primeira linha de defesa. Indução, embora mais exigente, entrega certeza absoluta.

Por que Usar Verificação Formal?

FV se destaca em descobrir bugs elusivos porque explora todo espaço de entrada automaticamente. Quando uma falha é descoberta, a ferramenta produz waveform conciso que aponta o ciclo exato onde a propriedade foi violada — muito mais fácil de debugar que trace de simulação longo.

Embora FV seja poderosa ferramenta de teste unitário, não substitui testes de integração artesanais. Conforme tamanho do módulo cresce, tempo de execução do solver pode tornar-se proibitivo. Ainda assim, investir tempo em FV reduz esforço geral de debug e acelera time-to-market.

Escrevendo Propriedades em PSL

PSL (Property Specification Language) é a lingua franca da verificação formal em VHDL. Propriedades são tipicamente armazenadas em arquivo .psl separado que o solver lê durante fase de verificação.

Três palavras-chave PSL descrevem propriedades:

• assert — garante que condição sempre valerá.
• assume — declara suposições sobre as entradas.
• cover — verifica se cenário particular pode ocorrer.

Arquivos PSL também podem conter declarações e processos VHDL ordinários, permitindo criar sinais auxiliares para asserções complexas.

Todo arquivo PSL começa com bloco vunit que vincula arquivo a entidade específica:

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) { } 

Seguido por declaração de clock padrão:

default clock is rising_edge(clk); 

Sintaxe de propriedade parece assim:

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

Use |=> para asserções de próximo ciclo:

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

Dentro de condições pode usar stable para forçar que sinal não mude entre ciclos, e encadear condições usando {C1; C2} para expressar restrições sequenciais.

Instalando Ferramentas Necessárias

Ferramentas comerciais líderes (ex.: ModelSim) suportam verificação formal, mas a Student Edition gratuita carece deste recurso. Felizmente, stack open-source robusto está disponível para Linux (e via WSL no Windows). O guia a seguir usa Ubuntu 20.04 LTS mas funciona em qualquer distro baseada em Debian recente.

Pré-requisitos

sudo apt update && sudo apt upgrade 

Instale bibliotecas de desenvolvimento essenciais:

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 e 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 e Plugin Yosys

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

Baixe o Projeto Exemplo

Preencha o formulário abaixo para receber arquivo ZIP contendo fonte completo AXI FIFO, arquivo PSL e scripts de verificação.

Exemplo Prático: Verificação Formal de FIFO AXI

Abaixo descrevemos categorias-chave de propriedades para FIFO e ilustramos como codificá-las em PSL.

Tratamento de Reset

f_reset : assume {rst}; 

Como palavra-chave always é omitida, esta suposição aplica-se apenas ao primeiro ciclo após reset. Convenção de label (f_) ajuda identificar falhas.

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

Note que sinais internos como count podem ser referenciados porque declaração vunit inclui nome da arquitetura.

Sinalização FIFO Cheio e Vazio

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

Conformidade Protocolo AXI

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

Para estabilidade do sinal ready:

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

Ordenação FIFO

Ordenação garante que escritas anteriores saiam antes de escritas posteriores. Modelamos isso com sinais auxiliares que lembram quando valores de dados particulares entraram ou saíram.

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; 

Declare os valores de dados como constantes não-restritas para que o solver possa escolher qualquer padrão de bits:

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; 

Finalmente, codifique as restrições de ordenação:

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

Executando Verificação Formal

Crie script axi_fifo.sby para ferramenta 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 

Execute a verificação:

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

Execução bem-sucedida imprime:

[axi_fifo_bmc] DONE (PASS, rc=0) 

Ajustando depth além da profundidade do FIFO garante que solver explore cenários de capacidade total.

Teste de Mutação

Para avaliar completude do seu conjunto de propriedades, injete deliberadamente pequeno bug — como remover lógica que aciona out_valid — e rode FV novamente. Se solver reportar falha de asserção, você verificou que suas propriedades são expressivas o suficiente para pegar aquele erro.

Exemplo de mensagem de falha:

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable 

Abra trace.vcd gerado no GTKWave para pinpointar ciclo exato onde propriedade violou.

Declarações Cover

Declarações cover são úteis para afirmar que cenário particular é alcançável. Por exemplo, para verificar que FIFO pode ser preenchido e depois esvaziado:

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

Ajuste script sby para incluir tarefa cover:

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

Cobertura bem-sucedida produz:

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15. 

Alterando count = ram_depth-1 para count = ram_depth tornará cover inalcançável, demonstrando sensibilidade da ferramenta à precisão da propriedade.

Próximos Passos

• Introdução à Linguagem PSL
• Fundamentos de Verificação Formal
• Série de Vídeos: Começando com Verificação Formal
• Artigos Avançados de Verificação Formal
• Repositório Mini-Projeto para Verificação Formal