|
Lecture May 25 15:20 |
Traditionally, the tool flow for the realization of digital circuits was purely design-centred, i.e. ensuring the quality through testing and verification was essentially considered as a post-processing step. To this end, mainly approaches based on simulation have been applied in the past. But the growing complexity according to Moore’s law showed the need for more powerful solutions. In the mid-80s, formal techniques have been proposed as a proper alternative – first in the area of verification. In the meantime, elaborated methods exploiting formal methods increasingly find application in industrial practice. This success was possible due to the improvements of the underlying solve engines, but also due to a better understanding of how to effectively apply them. Motivated by these results, applications of formal techniques beyond verification have been studied.
The lecture gives an overview of the development of solve engines over the past two decades. It is shown how the core techniques work and what the core paradigms behind a successful automatic engine are. Not only Boolean techniques, like BDD and SAT, are presented, but also extensions to word-level descriptions for decision diagrams and solve engines exploiting additional theories.
Along the design flow, starting from verification and debugging down to testing, the application of formal techniques is studied in different scenarios. First, the pros and cons of simulation and formal techniques in the context of verification are discussed. It is shown how the completeness of the verification task in the context of formal properties can be proven. Afterwards, also the problem of determining the reason for a faulty behaviour is addressed. Finally, it is shown how the task of test generation can be formulated using formal techniques.
In all the different domains along the design flow, it is discussed which aspects have to be taken into account when designing algorithms based on formal techniques for industrial use. For example, how to encode circuits with multiple-valued signal assignments, the incorporation of problem specific knowledge and the design of hybrid techniques that allow applying semi-formal approaches is presented.
- Prerequisites
Basic understanding of digital design, fundamentals of discrete mathematics, BS or MS in Electrical Engineering, Computer Engineering or Computer Science.
- Learning outcomes
You will get an understanding of the evolution of formal proof techniques over the last years and what is the “magic” behind their computational power. Looking at applications from different domains along the design flow will provide an in-depth view on the way these techniques can be applied today. This can be seen as a starting point for applying formal techniques in “your domain”. State-of-the-art and directions for future work are described.
- Syllabus
- Proof Techniques
- Boolean
- Decision diagrams
- Satisfiability
- Word-level
- Extensions of decision diagrams
- SMT solvers
- Boolean
- Verification
- Simulation vs. formal
- Constrained random simulation
- Measuring coverage
- Debugging
- Finding faults
- Error assumptions
- Corrections
- Test
- Black box vs. white box
- Encoding
- Hybrid approaches
- Proof Techniques