Using verification coverage with formal analysis
Vinaya Singh, Joseph Hupcey III, Cadence Design Systems Inc.
EEtimes (4/13/2011 9:13 AM EDT)
Introduction
Verification engineers are increasingly using coverage metrics such as code coverage and functional coverage to guide the verification process to completion. These metrics, however, were developed specifically for simulation. Many contemporary verification flows also include formal analysis tools that provide exhaustive block-level proofs based on properties or assertions. The level of coverage provided by these tools needs to be evaluated, too – but it’s necessary to understand how formal “coverage” differs from simulation coverage, and how formal coverage results can reinforce, or in some cases even replace, coverage created by simulation engines.
In metric-driven verification flows, an executable verification plan tracks simulation coverage metrics on an ongoing basis, using the metrics to evaluate the completion of the verification process. As a result, engineers can quickly see whether a block is completely verified, or if further tests are needed. Steps of the process include developing the verification plan, constructing tests, executing tests, and measuring and analyzing coverage metrics.
To read the full article, click here
Related Semiconductor IP
- AXI to UCIe FDI Interface IP
- 45SPCLO UCIe-Class 1-32Gbps Low Power Receiver IP (NRZ)
- 45SPCLO UCIe-Class 1-32Gbps Low Power Transmitter IP (NRZ)
- Peripheral Sensor Interface (PSI5) Host Controller
- Link Acceleration Unit
Related Articles
- Bridging Design Verification Gaps with Formal Verification
- Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation
- Agentic AI-based Coverage Closure for Formal Verification
- SoC Test and Verification -> Coverage analysis essential in ATE
Latest Articles
- Croc: Training the Next Generation Chip Designers on Domain-Specific End-to-End Open Source Silicon
- Design and Development of a Neuromorphic Silicon Suite: PVT Sensing, Stochastic LIF Inference, On-Chip STDP Learning, and Crossbar Programming
- LLM4RTL: Tool-Assisted LLM for RTL Generation
- Towards Delta Aware Training: Efficient DNN Weight Storage for Resource-Constrained FPGAs
- CHERI-D: Secure and efficient inline object ID for CHERI temporal memory safety