Advanced Formal Techniques along the Design Flow

Prof. Dr. Rolf Drechsler

Universität Bremen

 

Traditionally, the tool flow for the realization of digital circuits was purely design-centered, 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 talk gives an overview of the development of solve engines and automatic decision procedures over the past two decades. It is shown how the core techniques work and what the main 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.