Never miss a story from Verification. Subscribe for in-depth analysis and articles.
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.
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.
The requirements to perform C versus RTL equivalence checking are:
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:
It can verify designs ranging from unit arithmetic operations and higher-level image processing operations/algorithms to cryptography RTL blocks.
Unit arithmetic operations
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.
The major components of this App are:
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:
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:
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.
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.
It also supports floating-point radices IEEE 754 representations such as:
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.
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.