T4B: Formal verification in system-on-chip design: Scientific foundations and practical methodology

Summary form only given. The role of formal techniques in SoC design has constantly increased over the last two decades. Yet, in today\´s practice, the extent to which formal techniques are involved in actual design flows varies widely between different industrial settings. In some scenarios, formal techniques are conceded a rather minor role and are viewed as nice-to-have additions to conventional simulation, for example as a tool for “hunting bugs” in corner cases. In other scenarios, more and more responsibility is shifted from simulation to formal techniques. Verification methodologies have emerged that involve formal property checking comprehensively, and in a systematic way. In this tutorial, we review the scientific foundations of modem formal verification tools. A particular focus will be on demonstrating how basic algorithmic issues and the choice of computational models influence industrial verification methodologies. We report on experiences from large-scale industry projects. A systematic property checking methodology is presented as it has evolved in some parts of the industry. System-level design flows pose new challenges for formal methods. A formal methodology will be outlined that can contribute to closing the "semantic gap" between the system level and the RTL. Based on formal techniques a perspective is developed how to extend traditional design flows by system-level models, not only for prototyping purposes at the system level but also for reducing design and verification costs at the RTL.