Faster Formal Verification Closure For Datapaths In AI Designs

In recent years, many longstanding assumptions about formal verification have been rendered obsolete by ever-improving technology. Applications such as connectivity checking have shown that formal can work on large system-on-chip (SoC) designs, not just small blocks. Standard SystemVerilog Assertions (SVA) have eliminated the need to learn an abstruse mathematical language for each new formal tool. Perhaps most surprising to early formal users focusing only on control logic is the development of methods to verify complex datapaths. Floating-point arithmetic, digital signal processing (DSP) and even convolutional neural networks (CNNs) are being verified formally today.

The timing for this innovation could not be better. Many of the applications now driving the semiconductor industry are math-heavy, especially those incorporating artificial intelligence (AI) techniques such as deep learning. Everyone’s favorite example seems to be self-driving cars. Their intense requirements for image recognition, machine learning and sensor integration mean that the chips in autonomous vehicles are complex, with computational datapaths that are challenging to verify. Only formal methods can perform exhaustive verification and provide the necessary level of confidence.

Synopsys has developed a novel approach for datapath verification that relies on equivalence checking between the register transfer level (RTL) design and a C/C++ model of the design’s functionality. Many chip projects have such a model as part of a virtual platform to support early software development and test. There are also numerous open-source libraries that implement common arithmetic functions, such as the Berkeley SoftFloat package for the IEEE 754 floating-point standard. The C/C++ model is generally at a higher abstraction level than the RTL implementation, matching end-to-end functionality but not the timing or other details of the hardware.

Traditional equivalence checking cannot handle a comparison of such RTL and C/C++ models. Combinational/Boolean equivalence checkers rely on the models having matched state elements (registers/flip-flops/memories) and are commonly used to compare the RTL input and netlist output of a logic synthesis tool. Sequential equivalence checkers allow for state differences between the models and check that equal inputs produce equal outputs on every clock cycle. Since the C/C++ model is not cycle-accurate and may be completely untimed, transaction equivalence checking is required. This technique checks the results of equal inputs only at the end of a transaction, such as a multi-cycle arithmetic operation.

Figure 1: Different forms of equivalence checking

The Synopsys VC Formal Datapath Validation (DPV) App is a transaction equivalence checker with the power to verify complex datapaths. It is used on DSP engines, floating-point units (FPUs), graphics processing units (GPUs), CNNs and other elements used in AI applications. It supports all common arithmetic operations, including iterative calculations such as division and square root. It uses the Synopsys HECTOR best-in-class technology, a well-established solution for equivalence checking challenges. The DPV App contains custom optimizations and engines tuned for its primary task of comparing the results of transactions.

As an example of usage, consider a multiplier. Its operation can be modelled trivially in C code, for example with a function call such as “result = multiply(a, b)” in the abstract model. However, the implementation might require hundreds of lines of RTL code to capture the specific algorithm used. The RTL calculation could require multiple cycles to complete, whereas the C/C++ result is untimed and available immediately. Transaction equivalence checking ignores these details and checks that the results agree only when both are ready. If any cases of disagreement are found, the DPV App provides detailed information and an intuitive graphical user interface (GUI) in the Synopsys Verdi SoC debug platform to track down the cause of the differences. Once a full proof is reported, the design and verification teams know for certain that the two models produce the same transaction results under all circumstances.

Figure 2: Datapath Validation (DPV) App flow

Unlike other forms of equivalence checking, the DPV App does not require any correspondence between state elements in the two models being compared. However, if it is possible to match some of the state, this improves performance by making the comparison less difficult. Capacity and performance are affected by the length of the transactions. There is no fixed upper limit, but the length of all transactions must be bounded so that the results can be compared. The DPV App is specifically designed for use on datapaths, although it can handle designs containing both datapath and control functionality. The size of the design also affects performance; the technology is best used as a block-level verification solution.

The DPV App can be used to compare two C/C++ models or two RTL models, in addition to comparing one of each. This proves the consistency of independently developed models, for example ensuring that the IEEE 754 content in a custom C/C++ model matches a reference implementation such as SoftFloat. At the RTL stage, successive design refinements can be verified exhaustively even when the modified design changes the lengths of some transactions.

Figure 3: Multiple uses for the DPV App

The DPV App has been used successfully on many different types of datapaths. Within Synopsys, the DesignWare team uses the app to verify complex IP products, including FPUs, embedded vision processors and CNN engines. The GPU and CPU team at Samsung SARC and Advanced Computing Lab reported that VC Formal’s HECTOR technology reduced their simulation efforts and helped catch more than 30 RTL bugs in their datapath-centric designs. In addition, a leading fabless graphics company found no post-silicon bugs after deploying the DPV App in their verification flow. This contrasted sharply with a pre-deployment design in which more than ten datapath bugs were found in silicon. These examples demonstrate the tremendous value that transaction equivalence checking provides.

Datapaths require exhaustive verification for use in autonomous vehicles, medical electronics and other critical applications. The Synopsys VC Formal DPV App combines powerful formal solvers with a user-friendly GUI to provide a novel and proven solution. More information, including a demonstration, is available in a webinar.