Formal verification best practices to reach your targets
This blog is the first of a series where I will show how to use Formal Verification (FV) with a pragmatic, realistic, predictable, and efficient approach. The goal of this blog series is not to explain how FV works, but how to use best practices to achieve verification targets. Indeed, having efficient tools is one thing, bringing higher quality is another thing. I will tell a real life story where FV has been used within Codasip and provided excellent results.
If you have a basic understanding of FV principles (if you don’t I recommend reading this book), and experience in digital hardware design and verification, then this case study is for you.
A bit of context
Our tools and IPs
First things first. Let me give you some context. At Codasip we develop processor design solutions to enable Custom Compute. In other words, we develop an EDA tool called Codasip Studio and RISC-V processor IPs. With such an approach, we are able to provide an end-to-end methodology, supported by a tool, in order to customize these IPs.
Codasip Studio is our design automation toolset. It offers a library of generic modules which can be instantiated within IPs. One of these is a highly configurable cache to be connected to a processor, using an AHB or AXI interface.
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 Blogs
- Formal verification best practices: investigating a deadlock
- Formal verification best practices: towards end-to-end properties
- Formal verification best practices: checking data corruption
- Formal verification best practices: sign-off and wrap-up
Latest Blogs
- ReRAM in Automotive SoCs: When Every Nanosecond Counts
- AndeSentry – Andes’ Security Platform
- Formally verifying AVX2 rejection sampling for ML-KEM
- Integrating PQC into StrongSwan: ML-KEM integration for IPsec/IKEv2
- Breaking the Bandwidth Barrier: Enabling Celestial AI’s Photonic Fabric™ with Custom ESD IP on TSMC’s 5nm Platform