Invited Talks

Formal Methods and Physical Design: Match Made in Heaven or Fools' Paradise?
Carl Seger (Intel)
Symbolic methods based on BDDs and SAT solvers have revolutionized functional verification. For example, no modern microprocessor or ASIC design goes to tape-out without first having successfully passed Formal Equivalence Verification between the RTL model and the implementation. In addition, many algorithms for performing logic manipulations, like synthesis, have successfully made use of these basic tools of the formal verification community. However, outside of the logic domain, these powerful tools and techniques are much less well known. This talk will discuss some non-traditional uses of symbolic formal methods, gradually moving away from the logic domain and focusing on physical design. Although some new algorithms will be presented, the talk is more aimed at inspiring and challenging rather than providing complete answers. To illustrate the second half of the title, some examples where symbolic methods have failed to improve more traditional approaches will also be discussed.