ECE 697B - 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

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

• Satisfiability Problem (SAT)
  • Formulation, applications
  • CNF based vs BDD based
  • Word-level and multi-valued SAT

• Logic Minimization of Combinational Circuits
  • Two-level, basics (Quine/Mc. Clusky)
  • Multi-level minimization: Ashenhurst/Curtis decomposition, algebraic (SIS), BDD-based (BDS)
  • Timing optimization
  • Technology Mapping

• Logic Optimization of Sequential Circuits
  • Synchronous optimization
  • Retiming

• Verification - simulation based
  • Functional test generation
  • Boolean vs word-level SAT

• Formal verification
  • Models, theory
  • FSM reachability analysis
  • Equivalence checking: combinational, sequential
  • Model and property checking