¿Está seguro de que su RISC-V RTL no contiene sorpresas?

Dada la relativa novedad y complejidad de los diseños RISC-V RTL, ya sea que esté comprando un núcleo compatible comercialmente o descargando una oferta popular de código abierto, existe el riesgo pequeño pero no nulo de que se escapen sorpresas no deseadas sin ser detectadas en su producto final. En orden de probabilidad de mayor a menor, considere:

• La presencia de un error de caso de esquina extraño pero completamente posible
• Errores "dentro" de las instrucciones personalizadas que usted o su proveedor están creando para su aplicación
• Errores "en los bordes" de una instrucción personalizada, por ejemplo, la instrucción se ejecuta correctamente, pero de alguna manera deja la máquina en un estado corrupto.
• Relacionado: nuevas características no documentadas y/o mal especificadas que, sin darse cuenta, abren agujeros en el diseño
• Lógica troyana maliciosa insertada subrepticiamente a través de un ataque a la cadena de suministro

Enfoques comunes de mitigación

Naturalmente, la primera línea de defensa es la inspección experta del código RTL entrante o en desarrollo. Obviamente, esto debe hacerse; pero debería ser igualmente obvio que esta técnica, como dicen en el mundo matemático, "es necesaria pero no suficiente" (incluso si el propio profesor Patterson revisara su código).

La siguiente línea de defensa es aplicar enfoques basados ​​en simulación: Simulación de conjunto de instrucciones (ISS), comparación automatizada de su DUT con modelos dorados maduros, bancos de prueba UVM aleatorios restringidos para simulación DUT RTL e incluso canalización de estímulos del mundo real en emulación asistida por hardware del DUT. Una vez más, todos estos enfoques son valiosos y deben realizarse; pero todos adolecen del mismo defecto: son intrínsecamente incompletos ya que dependen de la generación de estímulos. Por ejemplo, en el caso extremo, pero posible, de un ataque a la cadena de suministro, el desarrollador de lógica troyana ha creado deliberadamente una secuencia desencadenante de señales y datos que probablemente escapará a la detección incluso por parte del hacker de sombrero blanco más creativo. Y, por supuesto, los errores funcionales tienen su propia forma de utilizar la entropía natural para permanecer ocultos.

La conclusión es que la única forma de estar completamente seguro de que su RISC-V RTL está libre de sorpresas naturales o maliciosas es aplicar métodos formales y exhaustivos para verificar el diseño.

Es mas facil decirlo que hacerlo. ¿verdad?

Sí y no: hace 14 años, este tipo de análisis solo lo podían hacer investigadores con nivel de doctorado que usaban sus propios programas hechos a mano. Pero desde 2008, las herramientas y técnicas se han desarrollado de tal manera que cualquier persona que esté familiarizada con los conceptos básicos de la verificación formal y la redacción del estándar IEEE System Verilog Assertions (SVA) puede aplicar rápidamente y tener éxito aquí.

Un proceso formal de tres etapas

El flujo recomendado de base formal se desarrolla de la siguiente manera:

1. Cree un banco de pruebas formal que "modele" la especificación DUT
2. Defina las restricciones de entrada y las comprobaciones que se ejecutarán contra el DUT
3. Ejecutar análisis

Paso 1: cree un banco de pruebas formal que "modele" la especificación DUT

La base de esta metodología es escribir un conjunto de propiedades que representen el comportamiento de cada instrucción en su diseño RISC-V. La tarea es capturar el efecto de una instrucción dada en las salidas de IP y los estados arquitectónicos internos (en el mundo RISC-V, este es el contador de programa (PC) y el archivo de registro (RF)) para cualquier secuencia de entrada arbitrariamente larga. Esto se hace utilizando una extensión especialmente diseñada para IEEE SVA llamada Operational SVA. En pocas palabras, se trata de una biblioteca que se envía con la herramienta de verificación del procesador de base formal; y desde el punto de vista del ingeniero de verificación, parece un subconjunto intuitivo del código SVA familiar. La figura 1 muestra la estructura genérica:

propiedad instrucción_A; // estado conceptual t ##0 ready_to_issue() y // disparador t ##0 opcode==instr_A_opc implica // estado conceptual t ##0 ready_to_issue() y // salidas de interfaces de memoria // lectura de la siguiente instrucción t ##0 imem_access(instr_A_opc) y // carga/almacenamiento de datos t ##1 dmem_access(instr_A_opc) y // registros arquitectónicos t ##1 RF_update(instr_A_opc) y t ##1 PC_update(instr_A_opc) endproperty 

Fig. 1: Estructura del código SVA operativo que captura la especificación de una instrucción del procesador. [1]

Con referencia a la figura 1, el lado izquierdo de la participación (la porción de código arriba la palabra clave implica) identifica cuándo la máquina está lista para emitir una nueva instrucción y la instrucción que se está emitiendo. La aserción captura los valores actuales de los estados arquitectónicos y, en el lado derecho de la implicación (parte del código a continuación la palabra clave implica), demuestra sus siguientes valores.

Además, se debe demostrar que las salidas del procesador son correctas; en este caso, para asegurarse de que la instrucción acceda a las ubicaciones de memoria de datos e instrucciones esperadas. La afirmación también prueba que la máquina está lista para emitir una nueva instrucción en el siguiente ciclo. Esto es crucial para desvincular la verificación de una instrucción de la secuencia de instrucciones de la que podría ser parte. Por ejemplo, la instrucción A podría ejecutarse correctamente, pero dejar la máquina en un estado corrupto. Este estado erróneo podría causar que la siguiente instrucción B produzca resultados incorrectos sin culpa propia. Por lo tanto, con el enfoque SVA operativo, la instrucción de verificación de aserción B pasaría, mientras que la instrucción de verificación de aserción A fallaría (donde las operaciones de memoria de lectura y escritura podrían durar varios ciclos).

En pocas palabras: las funciones que representan estados arquitectónicos en el código SVA operativo deben asignarse a las señales de implementación y deben reflejar la microarquitectura del procesador. El estado de la RF, por ejemplo, podría depender de la activación de las rutas de reenvío. [1]

[Nota: para aquellos que estén familiarizados con la simulación o la cobertura funcional formal, esta noción de integridad no se basa en métricas de cobertura estructural ni en la creación y recopilación de métricas para un modelo de cobertura funcional. En cambio (y adelantándose un poco a los pasos y resultados restantes), el resultado del análisis aquí se trata de obtener pruebas completas para todas las propiedades. Las pruebas completas también muestran implícitamente que no hay ninguna otra funcionalidad, que no haya sido especificada o inesperada (error de especificación o codificación), o insertada maliciosamente, que no esté capturada por este conjunto de propiedades. Parafraseando, esta metodología se trata de lograr una "cobertura del plan de prueba" del 100 % según lo verificado por los resultados del análisis formal exhaustivo, ¡donde nada es más "completo" que una prueba matemática!]

Paso 2: defina las restricciones de entrada y las comprobaciones que se ejecutarán en el DUT

Para complementar las propiedades de especificación de cada instrucción, el siguiente paso es definir las restricciones de entrada y las comprobaciones de salida adicionales. Nuevamente, se emplea SVA operativo, donde el usuario ahora especifica un "plan completo" para definir tanto las entradas legales como las señales ilegales que el DUT debe ignorar. Según el ejemplo que se muestra en la figura 2, hay tres secciones: suposiciones de determinación, requisitos de determinación y gráfico de propiedades.

procesador de integridad; determinacion_supuestos: // ENTRADAS determinadas(imem_datos_i); determinado(dmem_valid_i); si (dmem_valid_i) determinado (dmem_data_i) endif; determinación_requisitos: // SALIDAS determinado(imem_read_o), if (imem_read_o) determinado(imem_addr_o) endif; determinado (dmem_enable_o); si (dmem_enable_o) determinado(dmem_rd_wr_o), determinado(dmem_addr_o) endif; // ESTADOS ARQUITECTÓNICOS determinados(PC); determinado (RF); property_graph: todas_las_instrucciones := instrucción_no_a, instrucción_agregar_a, instrucción_sub_a, [...] todas_las_instrucciones -> todas_las_instrucciones; integridad final; 

Fig. 2: Ejemplo de un plan de completitud con supuestos y requisitos de determinación condicional.

Elaborar:

• "determinación_supuestos" es simplemente un nombre elegante para las restricciones de valor de entrada
• "determination_requirements" es una definición de las señales que deben verificarse (tanto las señales de salida del procesador como los estados arquitectónicos)
• La sección "property_graph" es simplemente un enlace de este archivo a todas las propiedades creadas en el Paso 1

Recapitulando dónde nos encontramos en este punto: en el Paso 1 creó lo que efectivamente es un modelo de ciclo preciso del dispositivo bajo prueba que debe demostrarse como verdadero en todo momento y con todas las entradas; en el Paso 2, configura las restricciones y cualquier comportamiento especial a tener en cuenta. ¡Agréguelos y, de hecho, tendrá un banco de pruebas formal que está listo para ejecutarse!

Paso 3: ejecutar el análisis

El objetivo de todas las herramientas formales es probar exhaustivamente que todas las propiedades son verdaderas para todo el tiempo y todas las entradas. En el caso de la verificación del procesador RISC-V, la herramienta funciona para demostrar que cualquier secuencia de entrada arbitrariamente larga puede coincidir con una secuencia única del SVA operativo especificado que predice los valores de las salidas y los estados arquitectónicos.

Y esto es exactamente lo que sucede. Si se detecta alguna diferencia en el comportamiento entre la especificación y el DUT, la herramienta formal entrega una forma de onda de "contraejemplo" que muestra exactamente la serie de señales de entrada y datos que pueden crear una violación de la especificación. Como se mencionó anteriormente, tales fallas se pueden encontrar en el interior de la lógica RTL de la instrucción o en la "lógica de traspaso" que conecta la siguiente rama/instrucción legal.

De cualquier manera, cuando se solucionan estos problemas y la herramienta prueba todas las propiedades, los resultados son realmente "completos", es decir, puede estar matemáticamente seguro de que no hay errores de codificación RTL: el análisis formal ha demostrado literalmente la ausencia de errores. !

Resultados

En primer lugar, como se señaló anteriormente, a lo largo de los años, muchos desarrolladores de procesadores se han beneficiado de este flujo [2], [3], [4].

Al poner a prueba esta metodología con RISC-V, mis colegas realizaron un estudio de caso utilizando el popular núcleo de código abierto Rocket Chip. Específicamente, se examinó la configuración RV64IMAFDC – sv39 vm. Este es un núcleo de procesador de 64 bits con un sistema de memoria virtual de 39 bits [5] y extensiones, como instrucciones comprimidas y atómicas [6]. Esta implementación RISC-V ISA de código abierto utiliza una canalización en orden de cinco etapas, de un solo problema, con finalización fuera de orden para instrucciones de latencia prolongada, como división o errores de caché. El núcleo también admite la predicción de bifurcaciones y la modificación del tiempo de ejecución del registro "misa", lo que le permite desactivar ciertas extensiones del conjunto de instrucciones.

Aunque esta instantánea del Rocket Chip había sido ampliamente verificada y grabada varias veces, se identificaron y se informaron a los desarrolladores de Rocket Core RTL cuatro comportamientos sospechosos previamente desconocidos. Estos problemas ([7], [8], [9] y [10]) se descubrieron únicamente a través de la aplicación sistemática del enfoque de verificación formal completo descrito en este artículo.

Profundizando en [10] específicamente: el descubrimiento de una instrucción CEASE no estándar (Opcode 0x30500073) en el RTL: claramente el equipo de Rocket Chip se retrasó en su documentación (y arreglaron esto casi inmediatamente después de presentar la solicitud de extracción de GitHub). El punto más importante es que esto demuestra que la lógica requerida para implementar una instrucción completa (docenas de líneas de código y muchas puertas de lógica sintetizada, colocada y enrutada) puede escapar a la detección mediante inspección visual, simulación RTL, simulación de nivel de puerta, todo proceso de implementación de back-end y prototipos de hardware en el laboratorio.

Pero, ¿qué pasa con el rendimiento de este flujo?

Primero, abordemos el significado más amplio de "rendimiento". Debido a la naturaleza novedosa del diseño de Rocket Chip, para este estudio de caso, nuestros profesionales de verificación formal tardaron aproximadamente 20 semanas de ingeniería en desarrollar todo el banco de pruebas y las restricciones. Sin embargo, las aplicaciones anteriores de este flujo en una IP comercial más estructurada generalmente han tomado una fracción de este tiempo. Naturalmente, todo el proceso de creación será mucho más rápido cuanto más estables y maduras sean las especificaciones, qué tan bien documentado y legible esté el código DUT RTL y cuánto acceso tenga a los ingenieros de diseño para preguntas y respuestas.

Una vez que se configuró el entorno, el tiempo de ejecución del reloj de pared fue de 2 horas, es decir, mucho menos de lo que cabría esperar razonablemente de la simulación RTL aleatoria restringida e incluso de la verificación asistida por hardware. Además, recuerde que los resultados de este análisis son válidos para todas las entradas y en todo momento; en una palabra, son exhaustivos [11].

Resumen

El enfoque completo de verificación del procesador de base formal que se presenta en este artículo utiliza una extensión de IEEE SVA, Operational SVA, para verificar formalmente que un RISC-V ISA está libre de brechas e inconsistencias. A diferencia de los bancos de pruebas de simulación aleatoria restringida, la emulación o la creación de prototipos físicos, el conjunto completo de propiedades y restricciones detecta exhaustivamente muchos tipos de errores RTL, así como la presencia de código no documentado o mal especificado y troyanos maliciosos.

Referencias

1 – Conferencia GOMACTech de 2019, Albuquerque, NM, 28 de marzo de 2019: Verificación formal completa de las direcciones IP del procesador RISC-V para circuitos integrados de confianza libres de troyanos, David Landoll, et.al.

2 – DVCon 2007: Verificación formal completa de TriCore2 y otros procesadores, Infineon Gmbh.

3 – 51 ^st Conferencia de automatización de diseño (DAC): verificación formal aplicada a la plataforma de diseño MCU de Renesas mediante las herramientas OneSpin

4 – DVCon Europe 2019: Verificación formal completa de una familia de DSP automotrices, Bosch Gmbh.

5 – Manual del conjunto de instrucciones de RISC-V, Volumen II: Arquitectura privilegiada, Versión del documento 1.10.

6 - https://github.com/freechipsproject/rocket-chip [consultado el 20 de diciembre de 2018]

7 – Resultado de la instrucción DIV no escrito en el archivo de registro
https://github.com/freechipsproject/rocket-chip/issues/1752

8 – Las instrucciones JAL y JALR almacenan una PC de devolución diferente
https://github.com/freechipsproject/rocket-chip/issues/1757

9 – Códigos de operación ilegales reproducidos y que causan efectos secundarios inesperados
https://github.com/freechipsproject/rocket-chip/issues/1861

10 – Instrucción no estándar CEASE (Opcode 0x30500073) Descubierto en RTL, https://github.com/freechipsproject/rocket-chip/issues/1868

11 – Blog de Verification Horizons, ¿Cómo se puede decir que la verificación formal es exhaustiva?, Joe Hupcey III
https://blogs.sw.siemens.com/verificationhorizons/2021/09/16/how-can-you-say-that-formal-verification-is-exhaustive/

Fuente: https://semiengineering.com/do-you-know-for-sure-your-risc-v-rtl-doesnt-contain-any-surprises/