Formal verification has been used successfully to verify today’s SoC designs. Traditional formal verification, which starts from time 0, is good for early design verification, but it is inefficient for hunting complex functional bugs. Based on our experience, complex bugs happen when there are multiple interactions of events happening under uncommon scenarios. Our methodology leverages functional simulation activity and starts formal verification from interesting “fishing spots” in the simulation traces. In this article, we are going to share the interesting fishing spots and explain how formal engine health is used to prioritize and guide the bug hunting process.
Formal verification has been used successfully by a lot of