Domain-Adapted LLMs for VLSI Design and Verification: A Case Study on Formal Verification

Abstract

Large language models (LLMs) present unprecedented opportunities in task automation for industrial chip design and verification that can yield significant improvements in engineering productivity. Instead of deploying off-the-shelf LLMs, we present our methodology for adapting a language model to the domain of VLSI design, and we show that our domain-adapted model, ChipNeMo, achieves improved performance against models of similar size on benchmarks concerning chip design and electronic design automation (EDA). We finally present a case study on the prospective of applying LLMs to hardware formal verification. Our results indicate that the largest and most capable models, such as GPT-4, are able to generate syntactically correct SVA implementations, yet there exists room for improvement in ensuring precise reflection of user intent given as high-level natural language descriptions of formal properties.