Formal Verification of Systems-on-Chip - Industrial Experiences and Scientific Perspectives

Even after years of progress in the field of formal property checking many system designers in industry still consider simulation as their most powerful and versatile instrument when verifying complex systems-on-chip (SoCs). Often, formal techniques are only conceded a minor role. At best, they are viewed as nice-to-have and may be employed in addition to simulation, e.g. for "bug hunting\´\´ in corner cases. Fortunately, in some parts of industry, a paradigm shift can be observed. Verification methodologies have emerged that involve property checking comprehensively, and in a systematic way. This has led to major innovations in industrial design flows. There are more and more applications where formal property checking does not only complement but replace simulation. In this talk, experiences from large-scale industrial projects are reported documenting this emancipation process of property checking. A systematic methodology is presented as it has established in some industries. Furthermore, there will be an attempt to identify the bottlenecks of today\´s technology and to outline specific scientific challenges. While formal property checking for individual SoC modules can be considered quite mature it is well-known that there are tremendous obstacles when moving from modules to the entire system. These problems do not only result from the sheer size of the system but also from the different nature of the verification problems. The presented analysis will also relate to well-known abstraction approaches and to techniques for state space approximation. More specifically, as a first step towards formal chip-level verification, the talk will discuss techniques for verifying communication structures (interfaces) between the individual SoC modules. New ideas will be outlined how certain abstraction techniques can be tailored towards a specific verification methodology such that correctness proofs become tractable even for complex SoC interfaces.