VC Formal SIG 2024 - Proceedings

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.

Formal property verification (FPV) results may contain inconclusive assertions and covers, which can harm verification completeness and confidence levels. In this presentation, we will explore a convergence improvement method using an out-of-order, read-only cache as an example. 

Abstraction, including reduced parameter, blackboxing, and symbolic variables, is the major methodology to help FPV converge. The cache FPV testbench benefitted from the convergence effort and greatly improved the result. 

In the high-stakes world of design verification, we have traditionally relied on the thrilling realm of constrained random simulations. But as the complexity of our chips grew, we found ourselves chasing bugs in a never-ending game of hide-and-seek. For some of our challenging problems, we leveraged the power of formal verification – a strategic approach that trades in the dice rolls for mathematical precision. 

In this presentation, we'll take you on a journey through the formal verification apps that we've used as our trusty sidekicks: FPV, SEQ, DPV, and FRV. We'll share how these formal techniques have helped us optimize the "bugs found vs. time spent" ratio, allowing us to tackle even the most daunting verification challenges. 

But the real showstopper is our deep dive into DPV, where we'll demonstrate how we used this formidable tool to verify a FP16 implementation in under 8 weeks – a feat that would have had our simulation-based counterparts scratching their heads. 

So, buckle up and get ready to witness the transformation of our design verification process, from the wild west of randomness to the disciplined world of formal rigor. We can't wait to share it with you.

This presentation will explore the integration of Synopsys VC Formal and Generative AI, highlighting its potential to automate the creation of formal verification testbenches and democratize the use of formal verification. We will discuss current capabilities, such as generating System Verilog Assertions (SVA) and integrating with VC Formal flow, as well as limitations like the accuracy of SVA generation. Finally, we will delve into the future vision of this technology, emphasizing continuous improvements and feedback loops to enhance AI-generated formal verification testbenches.