Un enfoque diferente para verificar formalmente funciones de ruta de datos muy desafiantes. Paul Cunningham (GM, Verificación en Cadence), Raúl Camposano (Silicon Catalyst, emprendedor, ex CTO de Synopsys y ahora CTO de Silvaco) y yo continuamos nuestra serie sobre ideas de investigación. Como siempre, los comentarios son bienvenidos. Estamos planeando agregar un aspecto a nuestra exploración de verificación este año. ¡Detalles a seguir!
La innovación
La elección de este mes es Verificación formal polinómica de sumadores de coma flotante. Este artículo fue publicado en la Conferencia DATE 2023. Los autores son de la Universidad de Bremen, Alemania.
Se debe demostrar que las implementaciones de elementos de Datapath son absolutamente correctas (recuerde el infame error de punto flotante de Pentium), lo que exige pruebas formales. Sin embargo, los gráficos de estado BDD para elementos de punto flotante explotan rápidamente, mientras que las pruebas SAT a menudo están limitadas y, por lo tanto, no son realmente completas.
La solución popular hoy en día es utilizar la verificación de equivalencia con un modelo de referencia C/C++, que funciona muy bien pero, por supuesto, depende de una referencia confiable. Sin embargo, algunas almas valientes todavía están intentando encontrar un camino con BDD. Estos autores sugieren métodos para utilizar la división de casos para limitar la explosión del gráfico de estado, pasando de una complejidad limitada exponencial a polinómica. ¡Veamos qué piensan nuestros críticos!
Punto de vista de pablo
Documento compacto de fácil lectura para el inicio de 2024, y sobre un problema clásico en informática: gestionar la explosión del tamaño de BDD en la verificación formal.
La contribución clave del artículo es un nuevo método para la "división de casos" en la verificación formal de sumadores de punto flotante. Tradicionalmente, la división de casos significa elegir una variable booleana que hace que un BDD aumente de tamaño y simplemente ejecutar dos pruebas formales separadas, una para el "caso" en el que esa variable es verdadera y otra para el caso en el que esa variable es falsa. Si ambas pruebas pasan, significa que la prueba general para el BDD completo, incluida esa variable, necesariamente también debe pasar. Por supuesto, la división de casos para n variables significa 2^n casos, por lo que si lo usa en todas partes, simplemente cambia una explosión exponencial por otra.
Este artículo observa que la división de casos no necesita basarse únicamente en variables booleanas individuales. Cualquier subdivisión exhaustiva del problema es válida. Por ejemplo, antes de normalizar el exponente base, se puede realizar una división del caso según el número de ceros iniciales en la base, es decir, cero ceros iniciales en la base, un cero inicial en la base, etc. Esta elección particular de división combinada con otra división astuta en el paso de cambio de alineación logra un compromiso mágico tal que la prueba general para una suma de punto flotante pasa de ser exponencial a polinómica en complejidad. Ahora se puede demostrar formalmente que un circuito de suma de coma flotante de doble precisión es correcto en 10 segundos. ¡Lindo!
La mirada de Raúl
Este breve artículo presenta un enfoque novedoso para gestionar el problema de la explosión de tamaño en la verificación formal de sumadores de punto flotante utilizando BDD, un problema clásico en la verificación de equivalencia. Tradicionalmente, esto se aborda mediante la división de casos, es decir, dividiendo el problema en función de los valores de variables booleanas individuales (0, 1), lo que también conduce a un crecimiento exponencial de la complejidad con el número de variables divididas. Con base en observaciones sobre dónde ocurre la explosión de tamaño al construir los BDD, el artículo propone tres métodos innovadores de división de casos. No se basan en variables booleanas individuales y son específicos para sumadores de punto flotante (por supuesto, no simplifican la verificación de equivalencia general a P).
- División de casos de cambio de alineación: el documento sugiere dividir con respecto a la cantidad de cambio o diferencia de exponente, reduciendo significativamente la cantidad de casos necesarios para la verificación.
- División de casos con ceros a la izquierda: para abordar la explosión en el cambio de normalización, el artículo propone crear casos basados en el número de ceros a la izquierda en el resultado de la suma.
- Números subnormales y redondeo: los números subnormales se manejan agregando una simplificación en los casos en que puedan ocurrir; El redondeo no provoca una explosión en el tamaño de BDD.
Al elegir estratégicamente estas divisiones de casos, la complejidad general de la prueba para la suma de punto flotante se puede reducir de exponencial a polinómica. Como resultado, la verificación formal de circuitos de suma de punto flotante de precisión doble y cuádruple, que en la simulación simbólica clásica tiene un tiempo de espera de dos horas, ahora se puede completar en 10 a 300 segundos.
Comparte esta publicación a través de:
- Distribución de relaciones públicas y contenido potenciado por SEO. Consiga amplificado hoy.
- PlatoData.Network Vertical Generativo Ai. Empodérate. Accede Aquí.
- PlatoAiStream. Inteligencia Web3. Conocimiento amplificado. Accede Aquí.
- PlatoESG. Carbón, tecnología limpia, Energía, Ambiente, Solar, Gestión de residuos. Accede Aquí.
- PlatoSalud. Inteligencia en Biotecnología y Ensayos Clínicos. Accede Aquí.
- Fuente: https://semiwiki.com/eda/342214-bdd-based-formal-for-floating-point-innovation-in-verification/
