| Resumen castellano: | La transición a la criptografía poscuántica requiere implementaciones de hardware cuya corrección funcional y conformidad con la interfaz puedan establecerse de manera eficiente. Este artículo presenta un proceso de verificación unificado para aceleradores criptográficos FPGA, utilizando como caso de estudio un acelerador de transformación numérica (NTT) para ML-KEM (FIPS 203). La estrategia asigna cuatro enfoques de verificación complementarios en función de sus respectivas fortalezas y jerarquía de diseño: verificación formal con Sby para los módulos aritméticos, verificación funcional con Cocotb y modelos de referencia compartidos en Python para los módulos de uso general y la integración; VUnit con OSVVM para verificar las interfaces AXI4-Stream y AXI4-Lite; y verificación «hardware-in-the-loop» (HIL) con el acelerador implementado en una plataforma de desarrollo Arty Z7-20 para probar el diseño en un entorno cercano al de producción.
Un Makefile y una configuración YAML centralizada (project_config.yml) proporcionan flujos de ejecución simplificados y perfiles «light» y «full» destinados a la integración de CI/CD. Seis tareas formales, 13 archivos de prueba de Cocotb y 2 bancos de pruebas de VUnit pusieron de manifiesto una limitación en el rango de entrada de la reducción modular, una señal de validación ignorada y una violación del protocolo TLAST de AXI4-Stream. La cobertura de código agregada de Cocotb/VUnit alcanzó el 92,75 % por unidad de diseño y el 80,71 % por instancia. Las etapas formal, Cocotb, VUnit+OSVVM y HIL duraron 22:14, 5:29, 2:50 y 8:06 (min:s), respectivamente; al distribuir Cocotb entre simuladores de código abierto y comerciales, el tiempo se redujo a 2:46. Los resultados muestran un proceso de verificación unificado que reduce el esfuerzo de verificación duplicado, al tiempo que simplifica las tareas de verificación y las complejidades de la coordinación de técnicas. |
|---|
| Resumen inglés: | The transition to post-quantum cryptography requires hardware implementations whose functional correctness and interface compliance can be established efficiently. This paper presents a unified verification pipeline for FPGA cryptographic accelerators, using a Number Theoretic Transform (NTT) accelerator for ML-KEM (FIPS 203) as a case study. The strategy assigns four complementary verification approaches according to their respective strengths and design hierarchy: formal verification with Sby for arithmetic modules, functional verification with Cocotb, and shared Python reference models for general-purpose modules and integration, VUnit with OSVVM for verifying the AXI4-Stream and AXI4-Lite interfaces and hardware-in-the-loop (HIL) verification with the accelerator implemented on an Arty Z7-20 development platform to test the design in an environment close to production. A Makefile and a centralized YAML configuration (project_config.yml) provide simplified execution flows and light/full profiles intended for CI/CD integration. Six formal tasks, 13 Cocotb test files and 2 VUnit testbenches exposed an input range limitation in the modular reduction, an ignored validation signal, and an AXI4-Stream TLAST protocol violation. Aggregated Cocotb/VUnit code coverage reached 92.75% per design unit and 80.71% per instance. Formal, Cocotb, VUnit+OSVVM, and HIL stages took 22:14, 5:29, 2:50 and 8:06 (min:s), respectively, distributing Cocotb across open-source and commercial simulators reduced its time to 2:46. The results show a unified verification pipeline that reduces duplicated verification effort while easing the verification tasks and technique orchestration complexities.
|
|---|
Resumen