Courses

EE 290A. Advanced Methods in Logic Synthesis and Equivalence Checking

Description

Combinational and sequential synthesis, and equivalence checking are closely related, and increasingly, the ties between the two are becoming tighter. The reason is that advances in one enable further research and advances in the other. In this course, we will illustrate how ideas from the verification community have led to a kind of ¿rewriting the book for logic synthesis¿, which is embodied in a synthesis and verification tool, called ABC being developed at Berkeley. The flow of ideas is also bidirectional, leading to our belief that research and development in one area should go hand-in-hand with the other. This is especially important for industry where traditionally, synthesis and verification is done by different groups, often at different sites.

The goals of these advanced methods are speed, scalability, verifiability, and superior results over classical methods. Recent focus has moved to the sequential domain where new results are leading to greater acceptance of sequential operations such as retiming, register correspondence, and use of approximate unreachable states. Examples illustrating this synergy and new developments include: ¿ unifying representation (sequential AIGs), ¿ cut/window-based techniques ensuring scalability, ¿ assume then prove paradigm through simulations and SAT, ¿ interpolation, ¿ recording and use of a history of synthesis transformations.