VC Formal Special Interest Group

Large Language Models (LLMs) have gained worldwide attention for their potential impact if deployed properly. LLMs are designed to comprehend natural language(s) and generate responses using underlying neural network techniques. These models are tuned for data curation, retrieval augmented generation (RAG), customization and accelerating performance. This talk will discuss how such LLMs can impact formal verification (FV). We’ll explore various applications, starting with benchmarking where we are today and outlining where we want to be. We’ll investigate the deployment of LLMs in various avenues that would aid in formal verification, including co-pilots, test-planning, code generation, and accelerating FV. The goal is to use AI to solve some of the primary challenges including reducing manual effort and time required for FV, as well as improving results. 

In this presentation, we will discuss the formal verification methodology used for RISC-V verification at Untether AI. First, we’ll briefly go over Untether AI’s “at-memory compute” architecture, the overall verification methodology, RISC-V verification objectives achievable through formal verification, and the challenges faced.​

Next, we’ll dive into the details of the methodology, i.e. the testbench architecture, ISA checks, performance covers, Etc. We will also discuss the tool setup and coding styles that can be used to leverage tool features such as RMA for convergence.​

Lastly, we’ll showcase some of the bugs exposed through this methodology and why it has become an important part of RISC-V verification at Untether AI. 

Dot-product computation engines are crucial for any AI/ML hardware accelerators. The complexity of the datapath increases in multi-term and floating-point dot-product engines because of the additional logic required for rounding, normalization, and alignment of significands according to the maximum exponent. To perform exhaustive verification of these dot-product compute engines, tools like Synopsys VC Formal DPV are employed, which executes the C/C++ versus RTL transactional equivalency checks. The complexity of the datapath in multi-term and floating-point dot-product engines, especially in sophisticated AI/ML chips, combined with varying dataflow graph (DFG) structures in the corresponding C/C++ and RTL models, often challenges the formal tool's ability to converge. This presentation outlines various strategies (such as assume-guarantee, lemma partitioning, DFG optimization, maximizing equivalence points, case splitting, and the use of optimized solvers) used to achieve formal convergence across different floating-point types. Additionally, we introduce helper lemmas following the development of adder tree expressions to align the RTL and C-model adder tree structures. The findings show that a formal run for a 16-input FP32-based dot-product engine can achieve complete convergence within 30 minutes.

Join us for a reception after the sessions to network with colleagues and presenters.