LLM assisted assertion-based verification

Abstract

Con la amplia adopción de la Inteligencia Artificial (IA) en el mundo de la programación, a través de la aparición de los Grandes Modelos de Lenguaje (LLM), el proceso de verificación es más crucial que nunca, tanto en software como en hardware. A medida que los LLMs comienzan a automatizar la creación y modificación de diseños hardware, asegurarse de que estos cambios no rompan la funcionalidad ya existente es crucial para desarrollar confianza en estos procesos dirigidos por IA. Presentamos una nueva herramienta que aprovecha los LLMs para generar y analizar SystemVerilog Assertions (SVA) para módulos Register Transfer Level (RTL). La herramienta no solo automatiza la generación de assertions, sino que también introduce una metodología de instantánea: capturando la funcionalidad actual de un diseño como un conjunto de propiedades formales, que pueden ser usadas para verif icar cambios futuros, independientemente de si son hechos por humanos o IA. Esta metodología incluye detección de propiedades duplicadas, expansión del conjunto de propiedades y reparación iterativa de propiedades que fallan utilizando LLM y métodos automáticos a través de la evaluación formal vía la herramienta estándar de FPV en la industria, JasperFPV, de Cadence Design Systems. La propuesta ha estado evaluada usando diferentes LLMs y módulos RTL para determinar el rendimiento general de la herramienta y de cada una de sus fases.

Con la amplia adopción de la Inteligencia Artificial (IA) en el mundo de la programación, a través de la aparición de los Grandes Modelos de Lenguaje (LLM), el proceso de verificación es más crucial que nunca, tanto en software como en hardware. A medida que los LLMs comienzan a automatizar la creación y modificación de diseños hardware, asegurarse de que estos cambios no rompan la funcionalidad ya existente es crucial para desarrollar confianza en estos procesos dirigidos por IA. Presentamos una nueva herramienta que aprovecha los LLMs para generar y analizar SystemVerilog Assertions (SVA) para módulos Register Transfer Level (RTL). La herramienta no solo automatiza la generación de assertions, sino que también introduce una metodología de instantánea: capturando la funcionalidad actual de un diseño como un conjunto de propiedades formales, que pueden ser usadas para verif icar cambios futuros, independientemente de si son hechos por humanos o IA. Esta metodología incluye detección de propiedades duplicadas, expansión del conjunto de propiedades y reparación iterativa de propiedades que fallan utilizando LLM y métodos automáticos a través de la evaluación formal vía la herramienta estándar de FPV en la industria, JasperFPV, de Cadence Design Systems. La propuesta ha estado evaluada usando diferentes LLMs y módulos RTL para determinar el rendimiento general de la herramienta y de cada una de sus fases.

Con la amplia adopción de la Inteligencia Artificial (IA) en el mundo de la programación, a través de la aparición de los Grandes Modelos de Lenguaje (LLM), el proceso de verificación es más crucial que nunca, tanto en software como en hardware. A medida que los LLMs comienzan a automatizar la creación y modificación de diseños hardware, asegurarse de que estos cambios no rompan la funcionalidad ya existente es crucial para desarrollar confianza en estos procesos dirigidos por IA. Presentamos una nueva herramienta que aprovecha los LLMs para generar y analizar SystemVerilog Assertions (SVA) para módulos Register Transfer Level (RTL). La herramienta no solo automatiza la generación de assertions, sino que también introduce una metodología de instantánea: capturando la funcionalidad actual de un diseño como un conjunto de propiedades formales, que pueden ser usadas para verif icar cambios futuros, independientemente de si son hechos por humanos o IA. Esta metodología incluye detección de propiedades duplicadas, expansión del conjunto de propiedades y reparación iterativa de propiedades que fallan utilizando LLM y métodos automáticos a través de la evaluación formal vía la herramienta estándar de FPV en la industria, JasperFPV, de Cadence Design Systems. La propuesta ha estado evaluada usando diferentes LLMs y módulos RTL para determinar el rendimiento general de la herramienta y de cada una de sus fases.