How formal verification saves time in digital IP design
David Vincenzoni
EDN (November 10, 2015)
It is well known that the task of verification looms large in the design of digital IP, as well as the design of SoCs. The target is to reach 100% for both RTL code and functional coverage, minimizing the time spent obtaining it. The most widely used methodology is based on Universal Verification Methodology (UVM) random constrained tests (either System Verilog or e language) that permit the construction of complex tests in a relatively short time while stressing the RTL code and keeping track of functional coverage. Some verification engineers also use formal methodology for verifying a dedicated part of the block such as standard interfaces, which completes the verification of the IP.
This article will describe a different approach for digital IP verification based on formal methodology, exhaustively verifying the functionalities through the definition of properties. The formal approach has the advantage of avoiding development of test benches. This new flow has been used during the design of a digital IP and has proven to significantly shrink verification time.
To read the full article, click here
Related Semiconductor IP
- HBM4 PHY IP
- Ultra-Low-Power LPDDR3/LPDDR2/DDR3L Combo Subsystem
- HBM4 Controller IP
- IPSEC AES-256-GCM (Standalone IPsec)
- Parameterizable compact BCH codec
Related Articles
- Formal-based methodology cuts digital design IP verification time
- How to manage changing IP in an evolving SoC design
- Time Interleaving of Analog to Digital Converters: Calibration Techniques, Limitations & what to look in Time Interleaved ADC IP prior to licensing
- Design patterns in SystemVerilog OOP for UVM verification
Latest Articles
- A 14ns-Latency 9Gb/s 0.44mm² 62pJ/b Short-Blocklength LDPC Decoder ASIC in 22FDX
- Pipeline Stage Resolved Timing Characterization of FPGA and ASIC Implementations of a RISC V Processor
- Lyra: A Hardware-Accelerated RISC-V Verification Framework with Generative Model-Based Processor Fuzzing
- Leveraging FPGAs for Homomorphic Matrix-Vector Multiplication in Oblivious Message Retrieval
- Extending and Accelerating Inner Product Masking with Fault Detection via Instruction Set Extension