Publication
LLM-guided Formal Verification Coupled with Mutation Testing
Muhammad Hassan; Sallar Ahmadi-Pour; Khushboo Qayyum; Chandan Kumar Jha; Rolf Drechsler
In: Design, Automation and Test in Europe Conference (DATE). Design, Automation & Test in Europe (DATE-2024), March 25-27, Valencia, Spain, 2024.
Abstract
The increasing complexity of modern hardware designs poses significant challenges for design verification, particularly defining and verifying properties and invariants manually. Recently, Large Language Models (LLMs) such has GPT-4 have been explored to generate these properties. However, assessing the quality of these LLM generated properties is still lacking. In this paper, we introduce a LLM-guided formal verification methodology combined with mutation testing for creating and
assessing invariants for Design Under Verification (DUV). Utilizing OpenAI’s GPT-4, we automate the generation of invariants and formal models from design specifications and Verilog behavioral models, respectively. We further enhance this approach with mutation testing to validate the quality of the invariants. We use a 27-channel interrupt controller (C432) from ISCAS-85 benchmarks as a complex case-study to showcase the methodology.