|
Lecture May 25 09:30 |
Verification accounts for 60 to 80 % of the design costs in System-on-Chip design flows. It is widely agreed that the “verification crisis”, often discussed in industry and academia, can be overcome only by a true paradigm shift towards fundamentally new design and verification methodologies. Already for quite some time, formal verification has been promised to be a major pillar in bridging the verification gap. Yet, in conventional design flows formal techniques are often conceded a minor role. They are viewed as nice-to-have additions to conventional simulation, for example as a tool for “hunting bugs” 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 lecture will provide a basic understanding of formal verification technology and of the challenges that are faced in practical verification methodologies.
The lecture reviews the scientific foundations of modern formal verification tools. Basic algorithmic concepts of formal verification tools are explained and related to notions of automatic test pattern generation where possible. It will be demonstrated how basic algorithmic issues and the choice of computational models influence industrial verification methodologies. A systematic property checking methodology is presented as it has evolved in some parts of the industry. Furthermore, we 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 fairly mature it is well-known that there are tremendous obstacles when moving the focus from modules to the entire system. On the system level, today’s verification tools run into severe capacity problems. These do not only result from the sheer size of the system but also from the different nature of the verification tasks. In this lecture, we will analyze and discuss these challenges, relating to well-known abstraction approaches. A scenario will be presented how formal architectural models can be created that pave the way to a new SoC design methodology which integrates formal verification in a more natural way, thus significantly reducing its costs.
- Prerequisites & suggested preliminary readings
Basic understanding of digital design, fundamentals of discrete mathematics, BS or MS in Electrical Engineering, Computer Engineering or Computer Science.
- Learning outcomes
You will gain a basic understanding of the technology underlying today’s formal verification tools in terms of both, computational models and algorithms. You will also acquire a conceptual understanding of a practical SoC verification methodology using property checking. Important trends in this field and their scientific challenges will exposed to you so that you get an idea of possible research directions that you might want to pursue yourself.
- Syllabus
- Basic proof engines:
- Binary Decision Diagrams
- Boolean satisfiability (SAT) solving
- Model Checking
- Computation Tree Logic (CTL)
- Kripke model
- fixed point characterization of CTL operators
- symbolic traversal of finite state machines (FSM)
- Bounded FSM Model
- Bounded Model Checking
- Interval Model Checking
- Induction
- Methodology
- The bounded versus the unbounded paradigm
- Invariants: theoretical concept and practical methodology
- Abstraction in property checking
- Integrating property checking into SoC design flow
- Basic proof engines: