Formal Verification Techniques to Check Functional Equivalence between High-Level C Models and RTL Implementations using Jasper C2RTL

The pervasiveness of digital systems in almost all commercial and industrial sectors has led to increased productivity and reduced time-to-market. Moreover, due to the complexity of modern Very Large Scale Integration (VLSI) designs, various verification techniques have been developed to cope with undetected functional failures. As a complement to traditional dynamic simulations, Formal Verification (FV) offers the possibility to mathematically check the functional correctness of the Device Under Verification (DUV) in a drastically shortened time, along with exhaustive coverage of the design state space. Formal Equivalence Verification (FEV) consists in comparing two models, known as specification and implementation, to check whether they are functionally equivalent or not. Although traditionally a similar verification methodology has been employed for RTL-versus-RTL and RTL-versus-netlist scenarios, thanks to the recent improvements in formal engines solving capabilities, nowadays one can perform C-versus-RTL equivalence. This thesis work aims to describe the state-of-the-art of Cadence® Jasper™ C2RTL App employed in the block-level verification of purely combinatorial and sequential digital circuits, possibly implementing iterative mechanisms. More specifically, given identical input values, the formal tool can be asked whether the high-level C model and the Hardware Description Language (HDL) implementation produce the same output values, regardless of their internal structures. Using FEV, automatically generated assertions can replace the task of writing properties, which is typical of Formal Property Verification (FPV): indeed, it may result in an error-prone activity, as some parts of the design state space may be not covered and properties may not be intuitive to write. Essentially, the added value of FEV technique consists in exhaustively verifying that the RTL design does not exhibit any non-equivalent behavior with respect to the C model, already at the early stages of the design cycle, without the need of writing either complex testbench or dozens of properties to verify. Starting from golden references written in C, possibly converted from MATLAB® abstract mathematical models developed at system-level, it has been possible to check the functional correctness of both datapath and control logic of different RTL designs. The analyzed case studies are: Floating-Point Unit (FPU) using the bfloat16 format, single-precision Floating-Point Multiplier-Accumulator (FP MAC), Tone Generator, and Automatic Gain Control (AGC). Although UVM dynamic simulations had taken months to verify these blocks, the use of C2RTL made it possible to prove the correctness of the designs within a few weeks, detecting all missed bugs hidden in subtle corner cases. Furthermore, advanced formal verification techniques have been employed to let the formal tool converge faster, such as insertion of cut points, overconstraint of internal nodes and proof structure construct in conjunction with assume-guarantee paradigm.