Exploring Formal in Datapath Verification

Abstract

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 ef
ficient 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.

Popular Abstract

Modern electronics, from smartphones to satellites, rely on incredibly small but
complex digital circuits. As the demand for smarter, and faster technologies increases, these circuits become even more complex and they pack within them
selves several mathematical operations. The downside? The more calculations
they perform, the more chances there are for something to go wrong. Traditionally, engineers check these designs by feeding in different inputs and observing the
corresponding outputs, often using very large verification setups. However, with
increasing complexity the inputs themselves have become wider. These lead to
millions of possible combinations that must be checked and executing all these,
along with building the environment is a slow and tedious process.
This is where formal verification comes into picture. It uses mathematical reasoning to automatically check the design for all possible inputs, instead of
manually providing each input. For designs that perform mathematical operations,
the approach is simple; compare the output of the design with the output of a
software model that implements the same function. If the two always match, the
design is proven correct. All that is required are two models and a script to connect them, with the formal tool that handles the input generation and verification.
This makes it incredibly good at catching tricky bugs with less effort. The catch?
Extremely large designs can overwhelm the process. While the challenge is known,
the ability of formal tools to handle such complex models remains untested. This
thesis addresses the gap by exploring methods to reduce the complexity of the
design such that formal verification can focus on the validation of relevant logic.
It customizes the datapath verification flow to specific design under test, to attain faster proofs, and verification environment setup all without losing the accuracy.
Further it examines the capabilities of formal verification, to adapt to different
designs using two tools; Cadence JasperGold and Synopsys VC Formal. The
study evaluates the strengths of each tool and identify design scenarios for which
they are best suited.

• author: Thorve, Vaishnavi Dinesh
• supervisor: Victor Åberg
• organization: Department of Electrical and Information Technology
• course: EITM02 20251
• year: 2025
• type: H2 - Master's Degree (Two Years)
• subject: Technology and Engineering
• report number: LU/LTH-EIT 2025-1096
• language: English
• id: 9213247
• date added to LUP: 2025-10-01 15:14:59
• date last changed: 2025-10-01 15:14:59