Description

Modern hardware systems, such as RISC-V processors and hardware accelerators, rely on functional simulators and formal verification models to ensure correct, reliable, and secure operation. Today, these models are mostly developed manually from design specifications, which is time-consuming and increasingly difficult as hardware architectures become more complex. This PhD proposes to explore how Large Language Models (LLMs) can be used to assist the automatic generation of functional and formal hardware models from design specifications. The work will focus on defining a methodology that produces consistent and executable models while increasing confidence in their correctness. To achieve this, the approach will combine LLM-based generation with feedback from simulation and formal verification tools, possibly using reinforcement learning to refine the generation process. The expected outcomes include a significant reduction in manual modeling effort, improved consistency between functional and formal models, and experimental validation on realistic hardware case studies, particularly RISC-V architectures and hardware accelerators.