Exploring Formal in Datapath Verification

Vaishnavi Dinesh Thorve ()

Beskrivning

One of the major contributors to the increasing complexity of integrated circuits, is the datapath logic, responsible for data transformations and manipulations. As performance demands increase, the complexity of these datapath logic increases, making the functional verification both tedious and expensive. A single undetected bug in this logic can compromise the system integrity, highlighting the need for efficient verification technique. This thesis explores the role of formal verification in datapath logic by assessing its advantages and limitations. It further evaluates the tool-specific strengths for Cadence JasperGold C2RTL, and Synopsys VC formal DPV, and analyses design scenarios that best leverage them. The thesis adapts the vendor-specific formal verification flow to two representative designs- a matrix multiplier, and a complex number multiplier, tailoring it to adapt MATLAB generated C/C++ reference model, and temporal mapping customizations. To address state space explosion, targeted abstraction techniques and proof convergence strategies, such as anchoring assertions and arbitrary slice setup are introduced. Experimental results demonstrated that formal verification efficiently detects subtle corner case errors, scales effectively to higher operand widths, and remains robust across diverse datapath structures. The findings indicate that, with appropriate customizations, formal verification can deliver exhaustive, high-assurance validation for complex datapath logic within practical timelines.