Top 10 Tips for Success with Formal Analysis - Part 1
Thomas Anderson, Verification Product Management Group Director, Cadence
EETimes (12/12/2011 10:00 AM EST)
Formal analysis, also known as property checking, has made significant progress in the last ten years in terms of ease of use, speed, capacity, and assertion-language standardization. Formal analysis has demonstrated clear value as an important component in the functional verification of both intellectual property (IP) and system-on-chip (SoC) designs. It complements RTL “lint” checking, simulation, simulation acceleration, in-circuit emulation (ICE), equivalence checking, and other verification techniques that are more widely adopted.
The use of formal analysis is not yet as widely adopted as its advocates once predicted it would be. In part, this is because many potential users have unrealistic expectations or try to deploy formal analysis in ways that do not play to its strengths. However, thousands of users on hundreds of IP and SoC projects have used formal analysis successfully, so it is clearly possible to apply the technology in appropriate ways to improve design quality and accelerate verification schedules. Knowing when, where, and how to apply formal analysis is the key.
To read the full article, click here
Related Semiconductor IP
- eUSB2V2.0 Controller + PHY IP
- I/O Library with LVDS in SkyWater 90nm
- 50G PON LDPC Encoder/Decoder
- UALink Controller
- RISC-V Debug & Trace IP
Related Articles
- Top 10 Tips for Success with Formal Analysis - Part 2
- Top 10 Tips for Success with Formal Analysis - Part 3
- Top 10 Tips for efficient Perl Scripting for Chip Designers
- Getting the most out of formal analysis
Latest Articles
- ChipBench: A Next-Step Benchmark for Evaluating LLM Performance in AI-Aided Chip Design
- COVERT: Trojan Detection in COTS Hardware via Statistical Activation of Microarchitectural Events
- A Reconfigurable Framework for AI-FPGA Agent Integration and Acceleration
- Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation
- FlexLLM: Composable HLS Library for Flexible Hybrid LLM Accelerator Design