ECE 667 / 567
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 construction
- 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
- Computer algebra based verification (arithmetic circuits)