Logic Synthesis and Verification

DATES: June 22-23, June 27-30 and July 1.

Time: 11-13h

Room: Room S215 (floor -2), Building Omega, Campus Nord, UPC

OUTLINE

1.        Introduction to logic synthesis

2.        Basic theory and data-structures

a.        Sum of product and factored form representation

b.        Canonical representations, Binary Decision Diagrams (BDD)

3.        Two-level logic optimization

a.        Exact logic minimization (Quine) 

b.        Heuristic logic optimization (Espresso)

4.        Functional decomposition

a.        Asenhurst-Curtis method

5.        Multi-level logic synthesis (technology independent)

a.        Kernel-based algebraic decomposition (SIS)

b.        AIG-based optimization (ABC)

6.        Technology mapping

a.        Graph based, standard cell matching (ASICs)

b.        Cut-based (FPGAs)

7.        Formal verification, equivalence checking

a.        Satisfiability (SAT)

b.        Combinational equivalence checking

c.        Sequential equivalence checking (ABC)

d.        FSM traversal, reachability

BIOGRPAHY

Maciej Ciesielski received the M.S. in Electrical Engineering from Warsaw Technical University in 1974, and Ph.D. in Electrical Engineering from the University of Rochester in 1983. From 1983 to 1986 he was a Senior Member of Technical Staff at GTE Laboratories, Waltham, MA, where he worked on silicon compilation and layout synthesis projects. In 1987 he joined the Department of Electrical and Computer Engineering at the University of Massachusetts, Amherst, where he is currently Professor and Associate Department Head. He teaches and conducts research in the area of electronic design automation, and specifically in high-level and logic synthesis, formal verification and design validation of digital systems. He is recipient of Doctorate Honoris Causa from the Université de Bretagne Sud, Lorient, France, in 2008. He is a senior member of the IEEE. For more details please consult his web site: http://www.ecs.umass.edu/ece/labs/vlsicad/ciesielski.html

Attendance: the course is open to any student. Attendance must be confirmed by sending an email to Jordi Cortadella (www.lsi.upc.edu/~jordicf)