Using Formal Verification Signoff for Digital IP
TimeMonday, July 11th5pm - 6pm PDT
LocationLevel 2 Exhibit Hall
Engineering Track Poster
DescriptionWe are used to signoff a digital block with dynamic test benches based UVM-SV/UVMe methodologies. These are built on complex object/aspect-oriented languages and allows to build constrained-random tests to stress RTL blocks for discovering bugs.
Formal Verification technology allows us to do exhaustive verification with reduced effort in comparison to applying the classic dynamic UVM approach.
In this paper we shall share our experience of using Formal signoff methodology to do verification signoff of two examples of digital IPs.
We will also showcase how we applied the same UVM methodology steps during executing the Formal sign-off methodology.
Our Formal Flow is based on:
- RTL Linting including the DFT checks
- Protocol verification with Assertion Based VIP (ABVIP)
- Register verification
- Clock Domain Crossing (for the IP with resynchronization schemes)
- SVA assertion proving for checking all the features
- Formal Scoreboard
- RTL coverage extraction
The Formal approach, applied to these IPs, allowed us to discover tricky bugs and shorten the verification effort. We use exclusively Formal for IP signoff when it is applicable, allowing to have a huge advantage versus the dynamic approach saving weeks of verification and discovering more bugs than any constrained-random test