Herramienta facilita verificación de código RISC-V

Un desarrollador ha presentado una nueva herramienta llamada "Knuckledragger" para simplificar la verificación de código ensamblador RISC-V. La herramienta aborda la complejidad inherente a la verificación de ensamblador, un proceso propenso a errores y con herramientas limitadas, especialmente en el contexto emergente de la generación de código ensamblador a partir de modelos de lenguaje grandes (LLMs). Knuckledragger permite a los usuarios definir una versión de alto nivel del programa, facilitando la depuración y el razonamiento sobre el código. La herramienta funciona transformando la ejecución simbólica de bajo nivel en un modelo de alto nivel más comprensible, lo que permite una verificación más eficiente a través de la bisimulación. Se ha demostrado su utilidad en la detección de errores, como un fallo en un programa de copia de memoria (memcopy) que no manejaba correctamente un tamaño de copia cero. El código fuente está disponible en GitHub, y un video de demostración está disponible en YouTube, mostrando cómo la herramienta puede simplificar el proceso de verificación y ayudar a identificar errores sutiles en el código ensamblador.