# Syllabus For Preliminary Examination In CAD

##### Revised March 2011
Prelim Format
• Each student will be examined by the entire group of examiners. The exam will last about 1h; expect 3 questions of 20m each. The format is oral. As a component of the exam, you may be asked questions somewhat outside the syllabus or your domain of knowledge. It is understood that you may not know the answer; the intent is to see how you approach such problems.

Syllabus and Materials (effective Fall 2011)

1. Timing
• Fundamental algorithms for timing analysis of circuits and systems. Concepts include setup/hold time, slack, clock skew, critical paths, DAG timing models, static and incremental timing analysis, longest path algorithms, false paths, delay intervals, controlling values, static sensitization and co-sensitization, static timing analysis, linear and nonlinear optimization frameworks for timing. Re-timing: goals, graph abstractions, register insertion/deletion concepts for re-timing, re-timing formulation and solution techniques (Bellman-Ford, FEAS). Obtaining delays using continuous-time circuit and interconnect analysis. Applications to software and circuits.
2. Continuous-Time Modelling and Simulation
• Modelling continuous-time systems (circuits, simple mechanical systems, reaction rate equations) as differential-algebraic equations. Quiescent steady-state analysis; the Newton-Raphson algorithm. Solving sparse systems of linear equations: Gaussian Elimination and LU factorization. Numerical solution of differential equations: existence/uniqueness, Picard-Lindelof theorem, Lipschitz condition; ODE solution fundamentals; Forward Euler, Backward Euler, Trapezoidal methods; LMS methods; use of ODE techniques for DAEs; stability of LMS methods; accuracy, truncation error of LMS methods. Sinusoidal steady state analysis of linear time-invariant systems: DAE linearization, frequency-domain computation of sinusoidal steady state responses, connection with Laplace transforms. Stationary noise analysis of linear time invariant systems: propagation of stationary noise through LTI systems, transfer functions from DAEs, direct and adjoint computation of noise power spectral densities.
3. Boolean Reasoning and Synthesis
• Boolean functions and their interpretation as sets. On/off/don't care sets. Cubes and literals. Truth tables. CNF and DNF representations. Two-level minimization: Implicants, prime implicants; covers, prime, irredundant and minimum covers; Quine-McCluskey exact minimization; heuristic minimization via the Espresso algorithm. Multi-level logic optimization: Boolean networks; Simplification, Elimination, Decomposition, Extraction and Substitution operations on Boolean networks; Boolean and algebraic division; Boolean kernels and kernel-finding algorithms. Binary Decision Diagrams: co-factors, Shannon expansions, and their properties; binary decision trees; variable ordering; reduction rules and how they lead to reduced, ordered binary decision diagrams (ROBDDs); canonicity of ROBDDs; if-then-else operator on ROBDDs; ROBDD implementation concepts; multi-rooted BDDs; BDD size bounds; dynamic variable re-ordering by sifting. Technology mapping; strategies for design and implementation of parallel software.
4. Models of Computation
• Sequential circuits. Feedback in cyclic combinational circuits: well-formed and ill-formed models. Expressing feedback using fixed-point semantics and synchronous abstractions. Constructive semantics. The Knaster-Tarski (Tarski Fixed Point) theorem: partial ordering and posets; Scott order, "bottom", Hasse diagrams; total orders; least upper bounds (joins); monotonic (order-preserving) functions; fixed-point theorem and its proof. Bourdoncle's algorithm. Constructiveness over a range of different inputs: motivation for symbolic execution. Replacing Boolean and "bottom" symbols with functions of input values. Characteristic functions; operations on characteristic functions. Monotonicity of gate operations. Proof of convergence via the Knaster-Tarski theorem. Extension of symbolic execution to handle state machines. Constructive composition of state machines. Concepts of synchronous languages.
5. Scheduling
• Connected and disconnected dataflow models. Balance equations: production-consumption matrix, unique least-positive solution, consistent and inconsistent models. Solving the balance equations: fractional iteration vector, least integer solution via the LCM/GCD, Euclid's algorithm. Symbolic execution, periodic sequential schedules. Sequential scheduling for SDFs: least positive integer null space of the production/consumption matrix. Parallel scheduling. Unbounded compute resources. Modelling separate hardware for each actor; modelling synchronous circuits as dataflow; retiming as dataflow firings. Parallel scheduling with bounded resources. Acyclic precedence graphs; list scheduling; Hu Level Scheduling technique. Max-Plus algebra and dynamics.
• Lee/Messerschmitt: Static Scheduling of Synchronous Data Flow Programs for Digital Signal Processing," IEEE Trans. on Computers, Vol. C-36, No. 1, pp. 24-35, January, 1987.
• Baccelli, F., G. Cohen, G. J. Olster and J. P. Quadrat (1992). Synchronization and Linearity, An Algebra for Discrete Event Systems. New York, Wiley.
• Sih/Lee: "Declustering: A New Multiprocessor Scheduling Technique," IEEE Trans. on Parallel and Distributed Systems, vol. 4, no. 6, pp. 625-637, June 1993.
• Bhattacharyya, Murthy, Lee: Software Synthesis from Dataflow Graphs, Kluwer Academic Press, 1996.
• Geilen, M. and S. Stuijk. Worst-case Performance Analysis of Synchronous Dataflow Scenarios. CODES+ISSS, Scottsdale, Arizona, USA, October 2010.
6. Formal Verification and Constraint Solving
• The SAT problem and its applications. CNF representation for SAT. Worst-case and typical complexity. 2-SAT, 3-SAT and Horn-SAT. Resolution and the Davis-Putnam (DP) algorithm. Davis-Logemann-Loveland (DLL) algorithm. Conflict analysis and backtracking. Branching and decision heuristics. Chaff SAT solver heuristic. Boolean Constraint Propagation (BCP). 2-literal watching. Sequential equivalence checking: consensus (universal quantification) and smoothing (existential quantification) operators. Limitations of low-level circuit equivalence techniques for sequential circuits. Equivalence concepts for finite state machines. Composing FSMs for equivalence checking. Representing states and transitions as Boolean functions/sets; FSM encoding via BDDs. Reachability analysis. Sequential equivalence checking via reachability analysis and SAT. Execution trace of a state machine. Propositional logic on execution traces. Properties over a single time-line: Linear Temporal Logic (LTL). LTL operators: G, F, X, U. Safety and liveness. Monitor state machines for temporal logic formulae. Properties over all possible executions: Computation Tree Logic (CTL*, CTL). Path qualifiers: A, E. Backward Reachability Analysis. Verifying safety properties using forward and backward reachability analysis. CTL property verification via fixpoint computation. Use of BDDs: symbolic model checking. Bounded model checking and SAT-based model checking. Timed automata; basics of verification of infinite-state systems and SMT solving.