Dominando la verificación formal de módulos VHDL con PSL

Al diseñar VHDL para aplicaciones FPGA críticas de seguridad, simplemente escribir testbenches no basta. Los ingenieros deben probar que un módulo se comporta exactamente como se especifica, libre de efectos laterales ocultos. La verificación formal proporciona esa certeza matemática.

La verificación formal cierra la brecha entre requisitos e implementación probando que toda secuencia posible de entradas satisface las propiedades del diseño. Es indispensable para certificar dispositivos médicos, sistemas aviónicos o cualquier dominio donde se requiera certificación DO‑254.

En este artículo invitado, Michael Finn Jørgensen —practicante experimentado en verificación formal— comparte insights prácticos y consejos accionables. El ejemplo abajo se basa en el conocido tutorial de FIFO AXI How to make an AXI FIFO in block RAM using the ready/valid handshake y demuestra cómo aplicar PSL a un diseño VHDL real.

¿Qué es la verificación formal?

La verificación formal (FV) es un método sistemático pre‑síntesis que garantiza la corrección de un diseño para todas las combinaciones de entrada. A diferencia de testbenches convencionales, que dependen de estímulos manuales, FV especifica propiedades que deben cumplirse en cada ciclo de reloj. Un solver SAT entonces prueba exhaustivamente que estas propiedades se satisfacen —o señala un contra‑ejemplo si no lo hacen.

Dos técnicas centrales impulsan la FV:

• Bounded Model Checking (BMC) – verifica un número finito de ciclos, partiendo de reset.
• Prueba por inducción – verifica que si un estado es válido, todos los estados subsiguientes permanecen válidos. Requiere un conjunto completo de propiedades pero garantiza corrección para un número infinito de ciclos.

Como BMC puede ejecutarse con solo unas pocas propiedades, suele ser la primera línea de defensa. La inducción, aunque más exigente, entrega certeza absoluta.

¿Por qué usar verificación formal?

La FV destaca en descubrir bugs elusivos porque explora el espacio de entradas completo automáticamente. Cuando se descubre un fallo, la herramienta produce una forma de onda concisa que señala el ciclo exacto donde la propiedad falló —mucho más fácil de depurar que una traza de simulación larga.

Aunque la FV es una potente herramienta de test unitario, no reemplaza tests de integración hechos a mano. A medida que el tamaño del módulo crece, el tiempo de ejecución del solver puede volverse prohibitivo. No obstante, invertir tiempo en FV reduce el esfuerzo global de depuración y acelera time‑to‑market.

Escribir propiedades en PSL

PSL (Property Specification Language) es la lingua franca de la verificación formal en VHDL. Las propiedades se almacenan típicamente en un archivo .psl aparte que el solver lee durante la fase de verificación.

Tres palabras clave PSL describen propiedades:

• assert – garantiza que una condición siempre se cumplirá.
• assume – establece suposiciones sobre las entradas.
• cover – verifica si un escenario particular puede ocurrir alguna vez.

Los archivos PSL también pueden contener declaraciones y procesos VHDL ordinarios, permitiendo crear señales auxiliares para aserciones complejas.

Todo archivo PSL comienza con un bloque vunit que vincula el archivo a una entidad específica:

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) { } 

Seguido de una declaración de clock por defecto:

default clock is rising_edge(clk); 

La sintaxis de propiedad se ve así:

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

Use |=> para aserciones de ciclo siguiente:

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

Dentro de condiciones puede usar stable para forzar que una señal no cambie entre ciclos, y encadenar condiciones usando {C1; C2} para expresar restricciones secuenciales.

Instalación de herramientas requeridas

Herramientas comerciales líderes (p. ej., ModelSim) soportan verificación formal, pero la edición Student gratuita carece de esta característica. Afortunadamente, un stack open‑source robusto está disponible para Linux (y vía WSL en Windows). La siguiente guía usa Ubuntu 20.04 LTS pero funciona en cualquier distro basada en Debian reciente.

Prerrequisitos

sudo apt update && sudo apt upgrade 

Instalar librerías de desarrollo esenciales:

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

Descargar el proyecto de ejemplo

Complete el formulario abajo para recibir un archivo ZIP conteniendo el código fuente completo AXI FIFO, archivo PSL y scripts de verificación.

Ejemplo trabajado: Verificación formal de un FIFO AXI

A continuación esbozamos las categorías clave de propiedades para un FIFO e ilustramos cómo codificarlas en PSL.

Manejo de reset

f_reset : assume {rst}; 

Como se omite la palabra clave always, esta suposición aplica solo al primer ciclo tras reset. Una convención de etiquetas (f_) ayuda a identificar fallos.

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

Observe que señales internas como count pueden referenciarse porque la declaración vunit incluye el nombre de la arquitectura.

Señalización de FIFO lleno y vacío

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

Cumplimiento 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 la estabilidad de la señal 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)}; 

Ordenación FIFO

La ordenación garantiza que escrituras previas salgan antes que posteriores. Modelamos esto con señales auxiliares que recuerdan cuándo valores de datos particulares entraron o salieron.

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; 

Declarar los valores de datos como constantes no restringidas para que el solver pueda elegir cualquier patrón 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, codificar las restricciones de ordenación:

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

Ejecutando verificación formal

Crear un script axi_fifo.sby para la herramienta 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 

Ejecutar la verificación:

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

Una ejecución exitosa imprime:

[axi_fifo_bmc] DONE (PASS, rc=0) 

Ajustar depth más allá de la profundidad del FIFO asegura que el solver explore escenarios de capacidad completa.

Test de mutación

Para medir la completitud de su conjunto de propiedades, inyecte deliberadamente un pequeño bug —como eliminar la lógica que conduce out_valid— y vuelva a ejecutar FV. Si el solver reporta un fallo de aserción, ha verificado que sus propiedades son lo suficientemente expresivas para capturar ese error.

Mensaje de fallo ejemplo:

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable 

Abra el trace.vcd generado en GTKWave para señalar el ciclo exacto donde la propiedad violó.

Sentencias cover

Las sentencias cover son útiles para afirmar que un escenario particular es alcanzable. Por ejemplo, para verificar que el FIFO puede llenarse y luego vaciarse:

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

Ajustar el script sby para incluir la tarea cover:

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

Cobertura exitosa produce:

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15. 

Cambiar count = ram_depth-1 a count = ram_depth hará la cover inalcanzable, demostrando la sensibilidad de la herramienta a la precisión de la propiedad.

Próximos pasos

• Introducción al lenguaje PSL
• Fundamentos de verificación formal
• Serie de vídeo: Primeros pasos con verificación formal
• Artículos avanzados de verificación formal
• Repositorio mini‑proyecto para verificación formal