EECS 144/244
Fall 2015
Contents
Home
Overview
Logistics
Lectures
Homeworks
Reading
Resources
Projects
Fall 2015 edition
Fall 2014 edition
Fall 2013 edition
Spring 2013 edition
Fall 2011 edition
bCourses
Course Development
Wiki
SVN
|
EECS 144/244 Lectures Spring 2013
(click on topic title for slides in PDF)
| No. | Date |
Topic, Slides |
Reading | Milestones |
| 1a | 01/23/13 |
Introduction, Systems |
|
|
| 1b | 01/25/13 |
Design approaches |
Special issue of IEEE Solid-State Circuits Magazine |
|
| 2a | 01/30/13 |
Automata, state machines, circuits |
|
|
| 2b | 02/01/13 |
Transition systems, temporal logic |
A logic primer Propositional logic |
|
| 3a | 02/06/13 |
Reachability, enumerative methods |
A logic primer Predicate logic |
HW 1 out |
| 3b | 02/08/13 |
Symbolic reachability, bounded model-checking |
CACM Article on SAT,
Clarke, Grumberg, Long paper |
|
| 4a | 02/13/13 |
Synchronous composition |
Lublinerman et al 2008,
Lublinerman et al 2009
|
|
| 4b | 02/15/13 |
Cyclic combinational circuits |
Malik 1994,
Shiple, Berry, Touati 1996,
Edwards, Lee 2003
|
HW 1 due 02/18 |
| 5a | 02/20/13 |
Contracts, asynchronous composition, fairness |
|
HW 2 out |
| 5b | 02/22/13 |
Timing analysis of circuits; Retiming |
Chapter 5 of "Timing" by S. Sapatnekar,
Devadas et al 1993,
Leiserson Saxe 1981,
Leiserson Saxe 1991,
Shenoy 1997,
Chapter 15 of Lee and Seshia
|
|
| 6a | 02/27/13 |
Dataflow: SDF, Kahn process networks |
Lee & Messerschmitt, SDF,
Kahn 1974
|
|
| 6b | 03/01/13 |
Dataflow: timed SDF, throughput analysis |
Ghamarian et al 1996
|
|
| 7a | 03/06/13 |
Continuous systems: Introduction to ODEs |
Detailed proof of Picard's theorem |
|
| 7b | 03/08/13 |
Continuous systems: Numerical Integration of ODEs |
Chapter 2 of Continuous Simulation by F. Cellier
|
HW 2 due. HW 3 out |
| 8a | 03/13/13 |
Revision 1 |
|
|
| 8b | 03/15/13 |
Midterm 1 (in class) |
|
|
| 9a | 03/20/13 |
Continuous systems: Linear |
Feedback
Systems: An introduction for scientists and engineers,
Karl J. Astrom and R. Murray |
|
| 9b | 03/22/13 |
Continuous systems: Non-Linear, Newton Raphson, Signal
Temporal Logic |
Tool (ODE simulation, STL): Breach |
|
| 03/27/13 |
Spring recess, no class |
|
|
| 03/29/13 |
Spring recess, no class |
|
|
| 10a | 04/03/13 |
Hybrid systems |
Tool (Hybrid system modelling and simulation and
more Ptolemy II |
HW 4 is out. |
| 10b | 04/05/13 |
Hybrid systems |
Tool (hybrid systems verification): Spaceex |
|
| 11a | 04/10/13 |
Timed systems: discrete-event simulation |
Lee 1999,
Misra 1986
|
|
| 11b | 04/12/13 |
Timed systems: timed automata |
Alur Dill 1994
|
|
| 12a | 04/17/13 |
DAEs, Modelica |
|
HW 4 solution |
| 12b | 04/19/13 |
DAEs, Modelica |
|
HW 5 is out. |
| 13a | 04/24/13 |
Stochastic systems: Markov Chains and Markov Decision Processes |
Chapter 10 of Principles of Model Checking, by Baier, Katoen |
|
| 13b | 04/26/13 |
Stochastic systems: Continuous Time Markov Chains, Continuous
Stochastic Logic |
|
|
| 14a | 05/01/13 |
Revision 2 |
|
HW 6 is out. |
| 14b | 05/03/13 |
Midterm 2 (in class) |
|
|
| 05/15/13 |
Project presentations |
|
|
|
