VC Formal Datapath Validation

With Integrated HECTOR Technology

CPU, GPU and AI designs are datapath heavy with unique design characteristics and require advanced verification techniques and methodology. These designs have mathematical functions like addition, subtraction, multiplier, square root and floating point units (FPU). Specialized AI-enabled processors excel at machine learning tasks and employ large arrays of arithmetic processing units including matrix multiplication and fused multiply-add structures. Verifying these mathematical functions using traditional methods is inefficient, time consuming and impractical.

The VC Formal Property Verification (FPV) App is designed to verify control paths (example arbiters, FIFOs, FSMs, bus bridges, etc.). The VC Formal Datapath Validation (DPV) App with integrated HECTOR™ technology contains custom optimizations and engines for datapath verification (ALU, FPU, DSP etc.).

Key Features:

  • Uses C/C++ model as reference and checks for transactional equivalence against RTL implementation
  • Supports SoftFloat and DesignWare reference models
  • Provides exhaustive proofs and the fastest way to find architectural and implementation bugs
  • Leverages VCS® for unified compile and Verdi® for unified debug
VC Formal Datapath Validation
VC Formal DPV

Additional Resources:

SemiEngineering Tech Talk - Functional Datapath Verification
Drill down into how to achieve confidence in datapath designs by applying formal solvers and methods to data transformation areas of a design rather than the control path areas.