Jasper C2RTL App for Datapath Verification

12 Jul 2022 • 5 minute read

Datapath designs, common to the GPU, CPU, and AI domains, typically involve floating-point units (FPUs), integer and fixed-point arithmetic units, matrix multiplications, polynomials, and other complex arithmetic operations. Design architects create models of these blocks in C++ as these are faster to model and verify due to the higher level of abstraction. Ensuring that the RTL designs correctly implement the C++ algorithmic intent in every circumstance is difficult to achieve with conventional verification.

The Jasper C2RTL App is optimized for checking pipelined datapaths versus their C/C++ algorithmic specifications. It uses these C++ models as the golden reference for verifying the RTL implementation. It offers 100X performance improvements compared with general-purpose formal engines and allows direct comparisons of C++ and RTL code traces and root-cause analysis. Validating the functional equivalence of C++ (untimed) and the RTL implementation (timed and pipelined) is outlined here in this blog.

Motivation

RTL designers use the data path design algorithms written in C++ as reference (golden) models for their RTL implementation. So, it would be nice to have a formal tool to verify that the RTL implementation is functionally equivalent to the C++ reference models.

Requirements

The requirements to perform C versus RTL equivalence checking are:

C++ language compiler and standard library support for the same
Datapath-specific formal engines
Specialized debug for C vs. RTL equivalence checking
Verify control and datapath logic interactions
Advanced proof management

Solution

Jasper C2RTL app enables datapath design verification by verifying the Functional equivalence of handwritten RTL against a golden C++ reference model. It also has the capability of checking the equivalence between two C++ models. Its features are:

Best-in-class word-level and bit-level solvers along with datapath-specific abstractions
Side-by-side waveforms-based debug for C and RTL models with advanced debug features of Jasper Visualize (like quite-trace, freeze-and-extend, what-if analysis, etc.) working for C++ side as well.
Supports simultaneous verification of control and datapath. i.e. you don’t need to tie the control signals to their active values. Jasper C2RTL can gracefully handle stalls and wait conditions.
State of the art management of advanced proof decomposition techniques through the usage of Jasper Proof Structure

Capabilities

It can verify designs ranging from unit arithmetic operations and higher-level image processing operations/algorithms to cryptography RTL blocks.

Unit arithmetic operations

Integer arithmetic
Fixed Point arithmetic
Floating-point arithmetic

Higher-level image processing operation/algorithms
ACE/LAC
Matrix multipliers
FFTs/DFTs
Compression/Decompression
Portions of Video codecs

Encryption/Decryption Models

AES, DES, RSA, MD5, etc.

C2RTL App- Flow Diagram

The setup and flow are very similar to a standard model checking verification setup, and there would hardly be any ramp-up time for an engineer having formal experience.

Jasper C2RTL App Components

The major components of this App are:

C++ Frontend
Datapath Specific Solvers and Proof Engines
VisualizeTM Interactive Environment for debugging

Verification Set Up

The C model is untimed, so as soon as the input is present, the results are available immediately, i.e., on the same cycle while on the RTL, it could be pipelined, and it could take a few cycles to compute the result.

The verification setup in Jasper C2RTL is like a typical model checking setup and hence easy to ramp up and has the below features:

It starts from an actual reset state, so there are no false counterexamples to deal with
Checks all occurrences of operations for infinite timeline
Allows simultaneous verification of control and datapath logic as control signals are not required to be tied off. This allows having stalls/wait states as well
Supports System-Verilog Assertion (SVA) style constraints/assertions

JASPER C2RL Proof

We have a new state-of-the-art data path proof stack with powerful bit-level engines, SMT solvers, and industry-leading powerful engines built into the tool. It also contains datapath-specific optimizations and is capable of specialized bit-level multiplier handling such as:

Datapath-specific optimizations

Support for floating-point multiplication to minimize the manual case splits
Dedicated handling of large integer multipliers implemented using smaller multipliers and adders
Word-level arithmetic abstractions, term-rewriting, reduction of vectors

Specialized bit-level multiplier handling

Unique engine to verify the bit-level implementation of array multipliers, radix2, radix4 booth multipliers with variants like Baugh Wooley.

All the advanced features of the Jasper platform, such as ML-based proof orchestration, regressions and compute resource optimization via Provecache and Proof Profiling data (PPD), management of thousands of parallel proof jobs on server farms via proof grid manager, and Powerful Jasper interactive proof cockpit are available for C2RTL App. Further, in terms of managing advanced proof decomposition techniques, it has a proof structure option that supports several proof decomposition operations like assume-guarantee, case split stopats, partitioning[VM1] , etc., and provides a foolproof way of collating proof results from the decomposed problems.

Jasper C2RTL Debug

Hardware engineers typically debug more with waveforms, and it's challenging for hardware engineers to debug through C++ code using gdb debuggers. So, we are also trying to bring the RTL-like debug to the C++ domain in this App. All Jasper's advanced debug features in Visualize for RTL debug now seamlessly work for C/C++ code in this App. One can do driver/load tracing, what-if analysis, quite trace operation, freeze and extend and others directly on the C++ code.

Floating point support

It also supports floating-point radices IEEE 754 representations such as:

16-bit half precision
32-bit single precision
64-bit double-precision

Apart from this, the custom floating-point representation can also be taken care of by passing the definition as a Jason file to the tool. Then, all these representations would be available in the waveform debugger to convert between the bit-level and equivalent decimal value for that floating-point representation.

Summary

Jasper C2RTL is the formal App targeting the datapath design verification domain. The best-in-class C++ compiler allows verifying RTL blocks whose reference C++ models had been impossible to compile by similar technologies. Differentiated datapath engines and proof management techniques bring a significant left-shift in the CPU/GPU and AI domain verification productivity.

Subscriptions