Verificación formal en VHDL usando PSL

Al diseñar VHDL para aplicaciones FPGA críticas para la seguridad, no es suficiente escribir bancos de prueba al máximo. Debe presentar una prueba de que el módulo funciona según lo previsto y sin efectos secundarios no deseados.

Las técnicas de verificación formal pueden ayudarlo a asignar un requisito a una prueba, lo que demuestra que su módulo VHDL cumple con la especificación. Es una herramienta fundamental para verificar aplicaciones de atención médica u obtener la certificación DO-254 para soluciones FPGA aerotransportadas.

Para desmitificar la verificación formal, VHDLwhiz solicita la ayuda de Michael Finn Jørgensen para escribir esta publicación de invitado. Michael tiene una gran experiencia en el tema y comparte muchos consejos en su página de GitHub.

El dispositivo bajo prueba en el ejemplo descargable de este artículo proviene del tutorial existente:
Cómo hacer un AXI FIFO en un bloque de RAM usando el protocolo de enlace listo/válido

Dejaré que Michael se haga cargo a partir de aquí y te explique la verificación formal en el resto de esta publicación de blog.

¿Qué es la verificación formal?

¡El objetivo de la verificación formal (FV) es asegurarse de que su módulo funcione según lo previsto!

FV es algo que haces como parte de tu proceso de desarrollo antes de sintetizar tu módulo. A veces se le llama "Comprobación de propiedad", que es una mejor descripción, creo.

En FV especificas las propiedades su módulo debe tener, y luego la herramienta (llamada "Solucionador de satisfacción") probará que su módulo satisfaga las propiedades para todas las posibles secuencias de entradas .

En otras palabras, la herramienta buscará cualquier transición desde un válido estado (donde se cumplen todas las propiedades) a un inválido estado (donde se violan una o más propiedades). Si no existe tal transición, es decir, no hay forma de pasar a un estado inválido, entonces se ha demostrado que las propiedades siempre se cumplen.

El desafío en FV es expresar las propiedades de su módulo en un lenguaje que la herramienta pueda entender.

La verificación formal es una alternativa a los bancos de pruebas escritos manualmente. El objetivo tanto de la verificación formal como de los bancos de pruebas manuales es eliminar errores del diseño, pero la verificación formal lo hace examinando las propiedades y generando muchos bancos de pruebas diferentes automáticamente.

Las herramientas utilizan dos métodos diferentes:

Comprobación de modelos acotados (BMC) . Comienza desde el reinicio y examina un número fijo de ciclos de reloj.
Prueba de inducción . Comienza desde un estado válido arbitrario y verifica que cualquier estado subsiguiente también sea válido.

La prueba de inducción es más difícil de satisfacer porque requiere todos establecer propiedades, mientras que BMC se puede ejecutar con solo unas pocas propiedades y seguir dando resultados útiles.

¿Por qué usar la verificación formal?

¡La verificación formal es muy buena para detectar errores difíciles de encontrar! Eso es porque la verificación formal busca automáticamente todo el espacio de posibles entradas.

Esto contrasta con la escritura tradicional del banco de pruebas que requiere la elaboración manual de estímulos. Es prácticamente imposible explorar todo el espacio estatal utilizando bancos de pruebas escritos manualmente.

Además, cuando la verificación formal encuentra un error, generará una forma de onda muy corta que muestra el error y lo hará mucho más rápido que cuando se ejecuta una simulación basada en un banco de pruebas escrito manualmente. Esta forma de onda corta es mucho más fácil de depurar que una forma de onda muy larga que normalmente surge de la simulación.

Sin embargo, la verificación formal no sustituye a la escritura en el banco de pruebas. En mi experiencia, la verificación formal es adecuada para las pruebas unitarias, mientras que es mejor hacer pruebas de integración utilizando bancos de pruebas hechos a mano. Esto se debe a que el tiempo de ejecución de la verificación formal aumenta exponencialmente con el tamaño del módulo.

De hecho, existe una curva de aprendizaje asociada con la verificación formal, pero vale la pena el tiempo, y espero que esta publicación de blog lo ayude a superar esta curva de aprendizaje. ¡Completará su diseño antes y tendrá menos errores!

Cómo escribir propiedades en PSL

Al realizar la verificación formal, debe expresar las propiedades de su módulo utilizando el lenguaje de especificación de propiedades (PSL). Las propiedades normalmente se encuentran en un archivo separado con la terminación .psl , y este archivo se usa solo durante la verificación formal.

En esta sección, describiré las características principales del lenguaje PSL en términos generales y, en una sección posterior, lo explicaré con un ejemplo específico.

Hay tres declaraciones en PSL:

assert
assume
cover

Es posible que ya esté familiarizado con la palabra clave assert al escribir bancos de pruebas. Esta misma palabra clave también se usa en PSL, pero con una sintaxis ligeramente diferente. El assert La palabra clave se utiliza para describir las propiedades que este módulo promete cumplir siempre. En particular, el assert La palabra clave se aplica a las salidas del módulo, o posiblemente también al estado interno.

El assume La palabra clave se utiliza para describir los requisitos que este módulo impone a las entradas. En otras palabras, el assume la palabra clave se aplica a las entradas en el módulo.

El cover La palabra clave se utiliza para describir propiedades que deben ser posibles de lograr de alguna manera.

También puede escribir código VHDL regular en el archivo PSL, incluidas las declaraciones de señales y los procesos (tanto sincrónicos como combinatorios).

La primera línea del archivo PSL debería ser

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) {

Aquí ENTITY_NAME y ARCHITECTURE_NAME consulte el módulo que está verificando. El INSTANCE_NAME puede ser lo que quieras. El archivo debe terminar con una llave de cierre:} .

La siguiente línea en el .psl el archivo debe ser:

default clock is rising_edge(clk);

Esto evita el tedioso tener que referirse a la señal del reloj en cada una de las declaraciones de propiedad.

La sintaxis del assert y assume declaraciones es:

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

Esta declaración dice lo siguiente:Si el PRECONDITION contiene (en cualquier ciclo de reloj) entonces el POSTCONDITION debe ser satisfecho en el mismo ciclo de reloj.

Hay otra forma de uso común:

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

Esta declaración dice lo siguiente:Si el PRECONDITION contiene (en cualquier ciclo de reloj) entonces el POSTCONDITION debe ser satisfecho en el siguiente ciclo de reloj.

Ambas formas se usan ampliamente.

Dentro del PRE- y POST-CONDITIONS , puede usar la palabra clave stable . Esta palabra clave significa:El valor en esto el ciclo del reloj es el mismo que el valor en el anterior ciclo de reloj.

Dentro del PRE- y POST-CONDITIONS , también puede usar secuencias, escribiendo lo siguiente:

{CONDITION_1 ; CONDITION_2}

Esto significa que CONDITION_1 debe estar satisfecho en esto ciclo de reloj y que CONDITION_2 debe ser satisfecho en el siguiente ciclo de reloj.

La declaración de portada tiene la siguiente sintaxis:

LABEL : cover {CONDITION}

Veremos muchos ejemplos de todas estas declaraciones en el ejemplo resuelto más adelante en este blog.

Instalación de las herramientas necesarias

La verificación formal cuenta con el respaldo de los principales proveedores de herramientas, incluido ModelSim. Desafortunadamente, la edición para estudiantes de ModelSim NO es compatible con la verificación formal. De hecho, obtienes el siguiente error:

Entonces, para usar ModelSim para la verificación formal, se requiere una licencia paga.

En cambio, existen herramientas de código abierto (gratuitas) que le permiten realizar una verificación formal. En esta sección, lo guiaré a través del proceso de instalación de estas herramientas.

Esta guía asume que está ejecutando en una plataforma Linux. Si está en una plataforma Windows, le recomiendo usar el Subsistema de Windows para Linux (WSL). La siguiente guía se verifica usando Ubuntu 20.04 LTS.

Requisitos

Primero, debemos actualizar el sistema para obtener los últimos parches:

sudo apt update
sudo apt upgrade

Luego debemos instalar algunos paquetes de desarrollo adicionales:

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 otros

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 otros

Hay binarios preempaquetados para GHDL, pero recomiendo descargar los archivos fuente más recientes y compilarlos de la siguiente manera:

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

La siguiente sección de este artículo lo guía a través de la implementación de la verificación formal para un proyecto VHDL existente. Puede descargar el código completo ingresando su dirección de correo electrónico en el siguiente formulario.

Ejemplo resuelto con verificación formal

La siguiente sección describirá cómo verificar formalmente el módulo axi_fifo escrito anteriormente en este blog.

Para comenzar con la verificación formal, debemos preguntarnos, ¿qué propiedades tiene el FIFO? He identificado cuatro categorías de propiedades:

Manejo de reinicio:que el módulo se active en un estado bien definido después del reinicio.
Señalización de FIFO lleno y vacío:Verifica que el FIFO indique correctamente las condiciones de lleno y vacío.
Protocolo AXI:Que el módulo cumpla con los requisitos del protocolo de enlace AXI valid/ready.
Ordenamiento FIFO:Que el FIFO no suelte/duplique/reordene elementos que pasan por él.

Discutiré cada una de estas propiedades a continuación.

Manejo de restablecimiento

Primero, declaramos que el módulo espera que se confirme el restablecimiento durante un ciclo de reloj:

f_reset : assume {rst};

Nótese aquí la ausencia de la palabra clave always . Sin el always palabra clave, la declaración solo es válida para el primer ciclo de reloj.

Es habitual (y muy útil) dar a cada declaración formal una etiqueta. Al ejecutar la verificación formal, la herramienta se referirá a estas etiquetas cuando informe cualquier falla. Uso la convención de preceder todas esas etiquetas con f_ .

Luego indicamos que el FIFO debe estar vacío después del reinicio:

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

Tenga en cuenta que es posible hacer referencia a interno señales en el módulo y no solo puertos. Aquí hacemos referencia a count , que es el nivel de llenado actual, es decir, el número de elementos actualmente en el FIFO. Eso es posible porque nos referimos al nombre de la arquitectura en la primera línea del archivo PSL.

Alternativamente, podríamos tener un proceso separado en el archivo PSL que cuente la cantidad de elementos que entran y salen del FIFO. Si bien eso es preferible, voy a utilizar la señal de conteo interno para que esta publicación de blog sea breve y vaya al grano.

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

La forma en que AXI FIFO señala lleno y vacío es con el out_valid y in_ready señales El out_valid la señal se afirma siempre que el FIFO no esté vacío, y el in_ready la señal se afirma cada vez que el FIFO no está lleno. Revisemos estas propiedades:

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

Protocolo AXI

El protocolo de enlace AXI válido/listo establece que la transferencia de datos solo ocurre cuando ambos valid y ready se afirman simultáneamente. Un error típico cuando se trabaja con este protocolo es afirmar que es válido (y los datos que lo acompañan) y no comprobar que está listo. En otras palabras, si valid se afirma y ready no lo es, entonces valid debe permanecer afirmado el próximo ciclo de reloj, y los datos deben permanecer sin cambios. Eso se aplica tanto a los datos que ingresan al FIFO como a los datos que salen del FIFO. Para los datos que ingresan al FIFO, usamos el assume palabra clave, y para los datos que salen del FIFO, usamos el assert palabra clave.

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

Nótese aquí el uso del stable palabra clave en combinación con |=> operador. Estas declaraciones hacen referencia a dos ciclos de reloj consecutivos. En el primer ciclo de reloj, comprueba si valid se afirma y ready no se afirma. Luego, en el siguiente (segundo) ciclo de reloj (indicado por el |=> operador), los valores de valid y data debe ser igual que el ciclo de reloj anterior (es decir, el primero).

En segundo lugar, para el protocolo AXI requerimos que el ready la señal es estable. Lo que esto significa es si FIFO puede aceptar datos (ready se afirma) pero no se ingresan datos (valid no se afirma), luego en el siguiente ciclo de reloj ready debe 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

Otra propiedad importante de FIFO es que los datos no se duplican/eliminan/intercambian. Expresar esta propiedad en PSL es bastante complejo y esta es la parte más difícil de esta verificación formal. Repasemos esta propiedad cuidadosamente paso a paso.

Podemos decir en general que si algún dato D1 ingresa al FIFO antes que algún otro dato D2, entonces en el lado de salida, el mismo dato D1 debe salir del FIFO antes que D2.

Para expresar esto en PSL necesitamos algunas señales auxiliares:f_sampled_in_d1 , f_sampled_in_d2 , f_sampled_out_d1 y f_sampled_out_d2 . Estas señales se borran en el reinicio y se confirman cada vez que D1 o D2 ingresan o salen de FIFO. Una vez afirmadas, estas señales permanecen afirmadas.

Entonces, expresamos la propiedad de ordenamiento FIFO en dos partes:Primero, una suposición que una vez que D2 ingresa al FIFO, entonces D1 ya ha ingresado previamente:

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

Y en segundo lugar una afirmación que una vez que D2 sale del FIFO, entonces D1 ya se ha ido previamente:

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

Todavía tenemos que declarar y completar las señales de muestreo a las que se hace referencia anteriormente. Hacemos esto de la siguiente manera para las señales de muestreo 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;

Aquí estamos haciendo referencia a otras dos señales, f_value_d1 y f_value_d2 . Contienen los valores de datos D1 y D2. Estas señales pueden contener cualquier arbitrario valores, y hay una manera especial de indicar esto a la herramienta de verificación 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;

El anyconst atributo es reconocido por la herramienta de verificación formal. Indica que la herramienta puede insertar cualquier valor constante en su lugar.

Con lo anterior, hemos especificado las propiedades del FIFO.

Ejecutar verificación formal

Antes de que podamos ejecutar la herramienta de verificación formal, necesitamos escribir un pequeño 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

La sección [tasks] indica que queremos la comprobación de modelos acotados. La sección [options] especifica que BMC debe ejecutarse durante 10 ciclos de reloj. El valor predeterminado es 20. La sección [engines] elige cuál de varios solucionadores diferentes usar. Puede haber diferencias en la velocidad de ejecución de los diferentes motores posibles, dependiendo de su diseño particular. Por ahora, deja este valor sin cambios.

El [script] sección es la parte interesante. Aquí especificamos el estándar VHDL (2008), los valores de los genéricos, los archivos a procesar y el nombre de la entidad de nivel superior. Finalmente, el [files] contiene los nombres de los archivos nuevamente.

Con este script listo, podemos ejecutar la verificación formal real usando este comando:

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

La ejecución de la herramienta de verificación formal termina con la declaración sin ceremonias:

[axi_fifo_bmc] DONE (PASS, rc=0)

Y eso solo significa que todas las propiedades que hemos especificado se satisfacen con todas las entradas arbitrarias hasta por 10 ciclos de reloj. Aumentar la profundidad conduce a tiempos de ejecución más prolongados para el solucionador. Sin embargo, tenga en cuenta que la profundidad es mayor que la profundidad de FIFO, lo que significa que el BMC encontrará una situación de FIFO completo para algunas secuencias de entrada. Si solo hubiéramos elegido, digamos, 5 ciclos de reloj, la verificación formal nunca encontraría un FIFO completo y no detectaría ningún error relacionado con eso.

Es posible probar que las propiedades se cumplen para todos ciclos de reloj utilizando la prueba de inducción. Sin embargo, eso requiere más trabajo escribiendo las propiedades. El desafío es que hasta ahora, solo hemos escrito algunos propiedades. Pero para la inducción, necesitamos especificar todos propiedades (o al menos suficientes). Eso llevaría bastante tiempo, por lo que, en su lugar, analizaré una estrategia alternativa para aumentar nuestra confianza.

Mutación

Así que ahora hemos descrito algunas de las propiedades que el axi_fifo El módulo debe satisfacer, y nuestra herramienta confirma rápidamente esas propiedades, es decir, demuestra que están satisfechos. Pero aún podemos tener esta sensación incómoda:¿estamos seguros de que no hay errores? ¿Realmente hemos expresado todas las propiedades del axi_fifo módulo?

Para ayudar a responder estas preguntas y tener más confianza en la integridad de las propiedades especificadas, podemos aplicar una técnica llamada mutación :¡Hacemos a propósito un pequeño cambio en la implementación, es decir, introducimos deliberadamente un error y luego vemos si la verificación formal detecta el error!

Uno de esos cambios podría ser eliminar parte de la lógica que controla el out_valid señal. Por ejemplo, podríamos comentar estas tres líneas:

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

Cuando ejecutamos la verificación formal ahora obtenemos un error con el mensaje

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

Usando la herramienta GTKwave podemos ver la forma de onda que lo acompaña, y se ve de la siguiente manera:

Aquí vemos que a los 40 ns, el out_valid la señal debería ir a cero, pero no lo hace. La afirmación que falla está en 50 ns, donde out_valid sigue siendo alto, pero el out_data cambios de señal, lo que indica datos duplicados. Los datos duplicados en realidad no se transmitieron en este seguimiento en particular porque out_ready es bajo a 40 ns, pero la verificación formal detecta el error de todos modos.

Declaración de portada

Pasemos finalmente a una aplicación diferente de la herramienta de verificación formal:declaración de portada. El propósito de la declaración de cobertura es verificar si hay una secuencia de entradas que satisfaga una propiedad particular. Ya que estamos tratando con un FIFO, veamos si podemos llenarlo por completo y luego vaciarlo nuevamente. Esto se puede expresar en una sola declaración de portada:

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

¡Eso es una boca llena! Tenga en cuenta los puntos y coma dentro del {} . Para facilitar la lectura, he colocado cada sección en una línea separada. Esta declaración de portada dice lo siguiente:Busque una secuencia de entradas que satisfaga:

El restablecimiento se afirma durante un ciclo de reloj.
Puede pasar cualquier número de ciclos de reloj (donde no se afirma el restablecimiento).
Un ciclo de reloj en el que no se confirma el restablecimiento y el FIFO está lleno.
Puede pasar cualquier número de ciclos de reloj (donde no se afirma el restablecimiento).
Un ciclo de reloj en el que no se confirma el restablecimiento y el FIFO está vacío.

Entonces la sintaxis [*] significa repetir (cero o más veces) la condición anterior. En la línea 3, podríamos haber eliminado la condición rst = '0' delante de [*] . Los resultados serán los mismos. La razón es que el verificador formal intentará encontrar el más corto secuencia que satisfaga la declaración de portada, y afirmar el reinicio mientras se llena el FIFO solo retrasará eso. Sin embargo, al vaciar el FIFO en la línea 5, es esencial que no se confirme el restablecimiento.

Para ejecutar el verificador formal ahora, tenemos que hacer una pequeña modificación en el script axi_fifo.sby . Reemplace las secciones superiores con lo siguiente:

[tasks]
bmc
cover

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

Ahora el solucionador ejecutará el BMC y luego ejecutará el análisis de cobertura. En el resultado verás estas dos líneas:

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

Esto significa que la declaración de cobertura puede satisfacerse con una secuencia de 15 ciclos de reloj, y el solucionador ha generado una forma de onda específica para esta declaración de cobertura:

Aquí vemos a los 80 ns el FIFO está lleno y in_ready es desestimado. Y a los 150 ns el FIFO está vacío y out_valid es desestimado. Observe cómo durante el período de 30 ns a 80 ns que out_ready se mantiene bajo. Eso es necesario para garantizar que el FIFO se esté llenando.

Si reemplazamos la condición count = ram_depth-1 con count = ram_depth , la declaración de portada no se puede cumplir. La herramienta luego informa un error.

Unreached cover statement at i_axi_fifo.f_full_to_empty.

Entonces, el mensaje de error contiene la etiqueta de la declaración de portada que falla. ¡Esa es una de las razones por las que las etiquetas son tan útiles! Interpretamos el error anterior como que indica que FIFO nunca puede contener ram_depth número de elementos Esto es exactamente como se indica en la publicación original del blog AXI FIFO.

Adónde ir desde aquí

Una introducción al lenguaje PSL
Una introducción a la verificación formal
Una serie de videos más pequeños para comenzar con la verificación formal
Un blog relacionado con la verificación formal
Una serie de artículos con temas más avanzados en verificación formal
Una colección de pequeños ejemplos usando verificación formal

Primeros pasos con VUnit Uso del analizador lógico integrado (ILA) y entrada/salida virtual (VIO)

VHDL