Generating Formal Property-Based Specifications for Hardware Designs from Informal Documents using Large Language Models

Abstract

This work aims to explore the possibility of using large language models (LLMs) to generate formal property-based specifications for hardware designs, from informal protocol documentation. Formal property verification (FPV) offers an exhaustive approach to ensure design correctness but requires significant expertise and effort. This work explores the potential of leveraging large language models (LLMs) to generate formal property-based specifications, specifically SystemVerilog Assertions (SVA), from informal documentation. We focus on deriving natural language (NL) properties from hardware waveforms using LLMs like GPT-4o, o3-mini, and o1. Initial experiments highlight both the promise and challenges of this approach, including issues of waveform misinterpretation and inaccuracies in generated properties. To address these limitations, the improved methodology incorporates SAT-based generation and LLM-filtering to improve the accuracy and comprehensiveness of the generated properties. A satisfiability (SAT) solver approach is proposed to systematically generate and validate NL properties. A LLM based approach is used, in conjunction, to filter out the essential properties using textual documentation. This research lays the groundwork for automating the generation of formal specifications from informal documentation, to enhance the accessibility and efficiency of FPV for hardware verification. Future work will refine these methodologies and validate their effectiveness in generating correct and meaningful assertions.