A Comprehensive Study on the Application of LLM for Hardware Property Generation

Automated generation of hardware design properties has long been an active area of research, yielding a wide variety of techniques using a combination of lightweight analysis of design source code and data-driven dynamic analysis targeting design functionality and security. However, all these works suffer from numerous shortcomings, such as they (i) do not scale for industrial-scale designs, (ii) often require massive amounts of trace data to generate properties, (iii) generate too many design properties, often redundant, without any explanation on their usability for verification tasks, (iv) fail to generalize the properties beyond what is seen in the trace, and (v) encompass an extremely small subset of SystemVerilog grammar, limiting the expressibility and richness of the generated design properties. Recently, the massive success of Large-Language Models (LLMs), e.g., GPT, LLaMA, Gemini, in diverse applications has led researchers to investigate the application of LLMs for hardware property generation. However, almost all recent works on property generation using LLMs suffer from various shortcomings, such as they (i) require considerable human efforts and a deep understanding of the target hardware designs to devise hand-crafted specialized prompts to generate and refine properties, (ii) do not generalize the assertions, and (iii) do not consider execution traces, risking to potentially miss subtle incorrect design behaviors or security vulnerabilities that are not obvious in the design source code. In this thesis, we dive deep and investigate the usefulness of LLMs for hardware property generation. First, we propose AssertionBench, a benchmark consisting of a curated set of hardware designs in Verilog and their respective formally verified assertions. We use AssertionBench to comprehensively evaluate four state-of-the-art commercial and open-source LLMs for assertion generation. Our investigation found that all four LLMs generate a considerable amount of syntactically and semantically incorrect assertions, making them inadequate for practical adoption in industrial practice. We next develop AssertionLLM, a specialized LLM for hardware property generation derived by fine-tuning open-source LLaMa3 LLM to address this deficiency. Finally, we will conclude this thesis by outlining our insights and future works for the development of specialized LLMs for a broad spectrum of hardware design and verification tasks.