VERIFICATION OF RTL Design Using Formal Technique

Abstract

As SOC designs have become more complex, traditional verification methods are increasingly difficult and expensive to implement effectively. To tackle this challenge, current research is exploring the integration of formal verification with changes in design methodology. Early formalization of abstract models has shown potential in identifying design flaws sooner, which can reduce the cost of fixing bugs. Recognizing that different verification challenges require tailored approaches is crucial for effectively applying formal verification in the early design stages. By using various models and tools, different perspectives on the design can be explored, helping to capture the design’s essence in a way that allows quick validation and modification. Identifying corner-case issues early in the design process can significantly reduce the costs of re-designing later on. While traditional formal verification, which begins from the very start of the design, is useful for initial verification, it often falls short when it comes to uncovering complex bugs that result from rare or intricate interactions between events. In this thesis, introduce a methodology that utilizes functional simulation traces to guide formal verification. Instead of starting the formal verification process from the beginning, we focus on "interesting spots" in the simulation that are likely to reveal complex bugs. By using formal engine health to prioritize these critical areas, we can make the bug-hunting process more efficient and targeted. This approach not only improves the chances of detecting complex bugs but also helps reduce the cost of fixing them.