Formal property verification: A tale of two methods
David Vincenzoni, STMicroelectronics
EDN (January 15, 2018)
The Formal Property Verification (FPV) methodology often gets used in the last step of verification flow, after much time spent building a complex random constrained UVM (Universal Verification Methodology) environment where some corner cases are still not covered.
Other times, FPV is used when a silicon bug is found that was not raised during the dynamic verification phase.
In a wisely applied verification flow, FPV should be used in the first phase, as soon as the RTL (Register Transfer Logic) code is available.
Here we look at two examples of verification flow:
- A digital block verified through a UVM test bench
- Then, first verified using FPV flow.
To read the full article, click here
Related Semiconductor IP
- HBM4 PHY IP
- Ultra-Low-Power LPDDR3/LPDDR2/DDR3L Combo Subsystem
- MIPI D-PHY and FPD-Link (LVDS) Combinational Transmitter for TSMC 22nm ULP
- HBM4 Controller IP
- IPSEC AES-256-GCM (Standalone IPsec)
Related Articles
- Don't over-constrain in formal property verification (FPV) flows
- Formal, simulation, and AMBA verification IP combine to verify configurable powerline networking SoC
- How formal verification saves time in digital IP design
- Formal Verification Has It Covered!
Latest Articles
- ElfCore: A 28nm Neural Processor Enabling Dynamic Structured Sparse Training and Online Self-Supervised Learning with Activity-Dependent Weight Update
- 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