Coding Guidelines for Datapath Verification

It has been an article of faith that you can’t use formal tools to validate datapath logic (math components). Formal is for control logic, not datapath, we now realize. We understood the reason – wide inputs (32-bit, 64-bit or more) fed through a multiplier deliver eye-watering state space sizes. State space explosions also happen ultimately in control logic, however there a bounded check is often sufficient to meet a coverage need. But what does coverage mean for a multiplier proof? Checking a subset of the state space isn’t good enough. The check must be exhaustive, demanding a formal-based approach. An equivalence check between RTL and a C/C++ reference model is how the VC Formal DPV app meets this objective. Of course, there are some usage guidelines for these checks. Synopsys recently released a webinar on C/C++ coding styles for datapath verification with DPV.

First understand the method

Equivalence checking here doesn’t work the same way as for RTL/gate equivalence. The C (or could be C++, I’ll just use C in what follows) is untimed and may have no obvious correspondence points with RTL other than inputs and outputs. Therefore the DPV team work with something they call transaction equivalence. Given equivalent inputs the C and RTL models will generate equivalent outputs, ignoring timing.

DPV is based on HECTOR technology first developed in the Synopsys Advanced Technology Group 20 years ago and first deployed in 2008. Over the years, DPV has evolved into a high value app in VC Formal.

Which provides a lot more freedom in software style than you would expect, if you thought this method would require SystemC. (Though it does also support SystemC datatypes.) Formal methods in software are subject to some of the same constraints for RTL, though synthesizability (in the RTL sense) is not one of them.

A few sample guidelines

A number of the guidelines are not absolute restrictions. You can view them as helpful to accelerate validation. Others, such as setting upper bounds for loops, are probably essential to ensure proofs finish in reasonable time. Here are a few examples:

• In C modeling, simulation, debug and the execution function are often intermixed. You should separate these for equivalence checking. DPV defines a macro to aid in conditionally ignoring all that peripheral stuff, or you can just refactor to present the checker with an unmixed function.
• Unsurprisingly you need to provide guidance on loop bounds. This is not as restrictive as you might think. You can still use while-loops or for-loops with variable upper bounds but with a mechanism to otherwise bound the loop, e.g. an exit on the loop test parameter exceeding a fixed value. DPV even supports a pragma to specify a bound.
• There are a few other recommendations, such as writing templates with easily recognized constant sized variables, also avoiding non-portable accesses e.g. byte-wise access through char* since behavior will be different on big-endian versus little endian machines.

Want to know more?

VC Formal DPV has already been widely adopted among blue-chip semiconductor, systems and AI companies so the technology is well-proven. If you’d like to learn more about how to write efficient C/C++ code for DPV, register for the webinar.

Also read:

Very Short Reach (VSR) Connectivity for Optical Modules

Bigger, Faster and Better AI: Synopsys NPUs

The Path Towards Automation of Analog Design