ECE 667 - Synthesis and Verification of Digital Systems

Course Outline

• Introduction
  • Design flow, design styles
  • Design models

• High Level Synthesis
  • Scheduling, allocation and resource bining
  • High level transformations; optimization metrics

• Representation of Boolean and Arithmetic Functions
  • Boolean formulas, DAG networks, AIG graphs
  • BDDs and other decision diagrams
  • Word-level diagrams: BMDs, TEDs

• Logic Minimization of Combinational Circuits
  • Two-level optimization, basics
  • Multi-level minimization
    • functional decomposition
    • algebraic-based methods
    • BDD-based methods
  • Timing optimization
  • Technology Mapping (ASIC, FPGAs)

• Logic Optimization of Sequential Circuits
  • Synchronous optimization
  • Retiming

• Satisfiability Problem (SAT, SMT)
  • Formulation, applications
  • CNF based vs BDD based SAT
  • Satisfiability modulo theorems (SMT)

• Formal verification and design validation
  • Models, theory
  • FSM reachability analysis
  • Equivalence checking (combinational, sequential)
  • Model and property checking