Conferencia magistral de Intel sobre formal A Mind-Stretcher

Reeditado por Platón

seguidores: 0

Synopsys ha publicado en el sitio SolvNet una fascinante charla impartida por el Dr. Theo Drane de Intel Graphics. El tema es la verificación de equivalencia de rutas de datos. Puede parecer simplemente otro respaldo formal de DPV de Synopsys VC, pero debería verlo de todos modos. Esta es una discusión que amplía la mente sobre los usos y consideraciones en el ámbito formal y que lo llevará más allá de la rutinaria presentación de la guía del usuario hacia un territorio más fascinante.

Conferencia magistral de Intel sobre formalidad

Comprensión intelectual versus pruebas de muestra

La simulación basada en pruebas en todas sus formas es excelente y, a menudo, insustituible para verificar la exactitud de una especificación o implementación de diseño. También es fácil empezar. Simplemente escriba un programa de prueba y comience a simular. Pero la otra cara de esa simplicidad es que no necesitamos completamente Entienda lo que estamos probando para comenzar. Nos convencemos de que hemos leído las especificaciones detenidamente y entendemos todos los casos extremos, pero no hace falta mucha complejidad para abrumar nuestra comprensión.

Formal lo alienta a comprender la funcionalidad en un nivel profundo (al menos si desea ofrecer un resultado valioso). En el ejemplo anterior, una pregunta simple (¿puede z alguna vez ser todo unos?) no logra demostrar un ejemplo en mil millones de ciclos en un simulador. No es sorprendente, ya que se trata de un caso extremo. Una prueba formal proporciona un ejemplo específico y muy poco obvio en 1 segundos y puede demostrar que este es el único caso así en un tiempo ligeramente menor.

OK, formal hizo lo que las pruebas dinámicas no pudieron hacer, pero lo más importante es que aprendió algo que el simulador quizás nunca le hubiera dicho. Que sólo había un caso posible en el que esa condición podía darse. Formal le ayudó a comprender mejor el diseño a nivel intelectual, no solo como un resumen probabilístico en un conjunto finito de casos de prueba.

Problemas de especificaciones

El siguiente ejemplo de Theo se basa en una máquina expendedora de errores (llamada así porque cuando presionas un botón aparece un error). Esto parece un problema de verificación de equivalencia de C a RTL bastante sencillo, modelo C a la izquierda, modelo RTL a la derecha. Una sorpresa para Theo en sus primeros días en el mundo formal fue que el comportamiento de desplazamiento a la derecha en el modelo C no está completamente definido en el estándar C, aunque gcc se comportará razonablemente. Sin embargo, DPV se quejará, como debería ser, de una discrepancia en la comparación con RTL. Es peligroso confiar en el comportamiento indefinido.

Formal como una máquina expendedora de insectos.

La comparación de especificaciones entre C y RTL conlleva otros peligros, especialmente en torno al ancho de las brocas. El truncamiento o la pérdida de un bit de acarreo en una señal intermedia (n.º 3 anterior) son buenos ejemplos. ¿Son estos problemas de especificaciones? Quizás haya un área gris entre las opciones de especificación e implementación.

Más allá de la verificación de equivalencia

Al parecer, el objetivo principal de DPV es comprobar la equivalencia entre una referencia C o RTL y una implementación RTL. Pero esa necesidad es relativamente infrecuente y hay otras maneras útiles en que se podría aplicar dicha tecnología, aunque un poco fuera de lo común. Primero, un clásico en el mundo de la implementación: hice un cambio, solucioné un error, ¿introduje algún error nuevo como resultado? Un poco como la verificación SEQ después de agregar la activación del reloj. El análisis de accesibilidad en salidas de bloques puede ser otra aplicación útil en algunos casos.

No sólo comprobación de equivalencia

Theo se vuelve aún más creativo y pide a los alumnos que utilicen contraejemplos para comprender mejor el diseño. resolver sudokus or factorizar números enteros. Reconoce que la DPV es una forma extraña de abordar estos problemas, pero señala que su intención es romper la ilusión de que la DPV sirve sólo para comprobar la equivalencia. Una idea interesante y, sin duda, un esfuerzo cerebral para pensar en estos desafíos. (Confieso que inmediatamente comencé a pensar en el problema del Sudoku tan pronto como lo mencionó).

Envolver

Theo concluye con una discusión sobre metodologías importantes en el uso de producción, en torno a restricciones, regresiones y comparaciones con modelos RTL heredados. También los desafíos de saber si lo que estás comprobando realmente coincide con la especificación de lenguaje natural de alto nivel.

Charla muy energizante, vale la pena verla. aquí en SolvNet!

Comparte esta publicación a través de: