¿Qué es verificación formal?
La verificación formal (FV) consiste en el uso de herramientas que analizan matemáticamente el espacio de comportamientos posibles de un diseño, en lugar de calcular resultaos para valores particulares. Es decir, una herramienta de FV examina el conjunto completo de posibles simulaciones utilizando técnicas matemáticas, en contraste con la simulación, que evalúa puntos individuales en ese espacio.
Para definir qué estados del diseño son legales y cuáles no, se utilizan:
- «Assertions»: Una aserción es una declaración sobre el diseño, la cual se espera que siempre sea verdadera. Suelen definir el comportamiento de los outputs de DUT.
- «Assumptions»: Son parecidas a las aserciones, pero las asunciones especifican un comportamiento del DUT. Normalmente, definen condiciones que representan algún tipo de restricción. Suelen definir el comportamiento de los inputs del DUT.
- «Cover properties»: Mientras que las aserciones y las asunciones se espera que siempre sean verdaderas, los «cover properties» es algo que ocasionalmente es verdadero. Suele definir alguna condición interesante que se quiera confirmar que se está testando.
Simulación VS. Verificación formal
Este tipo de construcciones también se utilizan cuando se está verificando un diseño a través de simulaciones, pero la herramienta de simulación y la de verificación formal no tratan del mismo modo a las «assertions», «assumptions» y «cover properties». A continuación, vamos a ver qué diferencias hay con estas propiedades cuando se utilizan en un entorno de simulación y en un entorno de verificación formal.
| Verificación formal | Simulación tradicional | |
| «Assertions» | Define un estado ilegal. La herramienta prueba que el diseño nunca puede violar la aserción. Si falla, ofrece un contraejemplo de cómo ha fallado. | Si falla para la simulación con un error. |
| «Assumptions» | Restringe las entradas para eliminar estados irreales. | Si falla para la simulación con un error. |
| «Cover properties» | Comprueba si el estado definido se puede alcanzar. | La información se guarda en una base de datos y al final de la simulación se puede comprobar el coverage. |
Si observamos la siguiente imagen, dónde los círculos representan los posibles estados alcanzables en el diseño, podemos apreciar claramente la diferencia fundamental entre simulación y verificación formal.
- En simulación (izquierda), el proceso parte desde un estado inicial y avanza en función de los estímulos que recibe el diseño. Solo se exponen algunos estados específicos, dependiendo de los casos de prueba definidos. Como resultado, es difícil garantizar que se haya cubierto todo el rango de estados posibles, ya que solo se recorren trayectorias individuales dentro del espacio de estados.
- En verificación formal (derecha), en cambio, se analiza todo el espacio de estados de manera matemática y sistemática. Cada círculo representa los estados alcanzables en distintos ciclos de reloj, y el método permite explorarlos todos simultáneamente, sin necesidad de estímulos concretos
Por lo tanto, haciendo uso de la simulación tradicional puede que haya algún error en el diseño que no se llegue a cumplir porque puede que no se ha llegado a pensar en ese estado y no se ha hecho un test directo para verificarlo. En el siguiente supuesto, podemos ver como hay bugs en cinco estados distintos, pero que mediante las simulaciones realizadas solo se llega a cubrir uno de ellos. En la verificación formal, hay más posibilidades de que la herramienta sea capaz de detectar que estos estados contienen un error de comportamiento.
