Reading Schedule

My goal is to cover a smaller number of papers in greater depth than the typical graduate course. Rump's paper on interval arithmetic is very well-written, lovely mathematics with a practical slant, and so much material (162 pages!) we could spend an entire term on it. Likewise, Kundert's paper on RF simulation is a classic, and is easily worth several classes -- it's an amazing combination of mathematical techniques with solving real problems.

This schedule is a draft. We'll definitely cover the Z3 paper on January 8. The rest I'll update as we go, trying to keep the list up-to-date enough that papers appear at least one or two weeks before we discuss them in class.

    January 8:

Leonardo Moura and Nikolaj Bjørner, "Z3: An Efficient SMT Solver", In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340, 2008, http://leodemoura.github.io/files/sbmf09.pdf.

    January 13:

Leonardo Moura and Nikolaj Bjørner, "Satisfiabilty Modulo Theories: An Appetizer", In Proceedings of 12th Brazilian Symposium on Formal Methods (SBMF 2009), pp. 23-36, 2009, http://leodemoura.github.io/files/sbmf09.pdf.

    January 15:

Jaeha Kim, Metha Jeeradit, Byongchan Lim, Mark A. Horowitz, "Leveraging Designer's Intent: a path toward simpler analog CAD tools", Proceedings of the Custom Integrated Circuits Conference (CICC'2009), Sep. 2009, pp. 613--620, dx.doi.org/10.1109/CICC.2009.5280741.

    January 20

Mark Greenstreet and Suwen Yang, "Verifying Start-up Conditions for a Ring Oscillator", Proceedings of the 18th Great Lakes Symposium on VLSI (GLSVLSI'2008), pp. 201-206, May 2008, doi.acm.org/10.1145/1366110.1366160.

    January 22 and beyond

We will continue following a path the develops both analysis methods and their applications to real problems. We could follow a "circuits first" approach, or a "math first" approach.

• Circuits first:
      Jan. 22: An Event-driven Simulation Methodology for Integrated Switching Power Supplies in SystemVerilog.
      Jan. 29 - Feb. 3: Introduction to RF simulation and its application.
      Feb. 5 - 12: CasADi: A Symbolic Package for Automatic Differentiation and Optimal Control.
      Feb. 10: Family Day, university closed.
      Feb. 17 - 19: Spring break.
      Feb. 24: SpaceEx: Scalable Verification of Hybrid Systems.
      Feb. 26 - Mar.10: interval arithmetic and decision procedure papers from the "math first" approach (below).
• Math first:
      Jan. 22: Solving non-linear arithmetic.
      Jan. 24: Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods.
      Jan. 29: dReal: An SMT Solver for Nonlinear Theories over the Reals
      Feb. 3 - 12: Verification methods: Rigorous results using interval arithmetic"
      Feb. 10: Family Day, university closed.
      Feb. 17 - 19: Spring break.
      Feb. 24: CasADi: A Symbolic Package for Automatic Differentiation and Optimal Control.
      Feb. 26 - Mar. 10: circuit analysis stuff from the "circuit first" approach.

Either way, I plan to spend the last month on more verification examples and some of the "application" papers below. I'd welcome making the last month a "workshop" where we spend half our time discussing papers and half our time with a show-and-tell of examples from our projects and our own research. The focus would be on identifying the problems, brainstorming for solutions, trying it out, and reporting back.

If nothing changes, our schedule could be:
    Mar. 12: Formal Verification of Phase-Locked Loops Using Reachability Analysis and Continuization.
    Mar. 17: Verifying Global Convergence for a Digital PLL.
    Mar. 19 - 24: A tutorial introduction to non-linear dynamics and chaos and their application to sigma–delta modulators.
    Mar. 26: MEMS Inertial Sensors: A Tutorial Overview.
    Mar. 31: TBD
    Apr. 2: Computer Systems Based on Silicon Photonic Interconnects.
    Apr. 7: TBD

It's very unlikely that nothing will change. I expect to add a few "tutorial" lectures to cover topics such as numerical integration, FFTs, MOSFET models, connecting linear algebra with circuit analysis, etc. On the other hand, this should provide a pretty good approximation of the topics that we will cover.