CpSc 513             Binary Decision Diagrams                  Jan. 9, 2013

  0.  Topics for today
      A.  Announcements
        1.  CpSc 513 is on piazza.com
	  a.  We'll use piazza for
	      i.  On-line discussion
	     ii.  Announcements
	    iii.  I might mirror all/much of the course web page on
	    	  the piazza site
	  b.  Getting started with piazza
	      i.  Go to http://www.piazza.com
	     ii.  Create an account if you don't already have one
	    iii.  It's UBC -> Computer Science -> CpSc 513
	     iv.  I'll enroll everyone from the UBC registrar's classlist,
		    but you can enroll yourself first.
        2.  Department DLS tomorrow
	      not formal, but relevant:
	        Quick, Simple, And Easy Solutions To Hard Software Problems,
		Martin Renard, MIT
	        Dempster 110, Jan. 10, 3:30-5pm
        3.  Homework 1 will be ready "soon" (definitely before tutorial)
	  a.  I'll post it to the course website
	  b.  I'll post an announcemtn on piazza
        4.  Tutorial:  BDDs in Jython
	      Friday, Jan. 11, 11:00am-12:30pm
      B.  Lecture Overview
        1.  Representing Boolean Functions with ROBDDs
	      (Reduced Ordered Binary Decision Diagrams)
        2.  Operations on ROBDDs
        3.  Representing other data types
        4.  Applications for Verification
        5.  Review/Preview

  I.  Representing Boolean Functions with ROBDDs
        (Reduced Ordered Binary Decision Diagrams)
    A.  From decision trees to ROBDDs
      0.  Running example: one-bit adder
        a.  compute sum and carry_out given 'a', 'b', and carry_in
	b.  sum = a ^ b ^ c_in  (where ^ denotes exclusive-OR)
	c.  carry_out = majority(a, b, carry_in)
		= (a & b) | (a & c) | (b & c)
      1.  Decision tree
      2.  From tree to DAG:
        a.  remove duplicate terminals
	b.  share identical subtrees.
      3.  Remove redundant tests
    B.  ROBDDs are canonical
      Proof: by induction
	1.  Base case: ROBDD with no variables
	2.  Induction step:
	      assume ROBDDs with k variables are canonical
	      show that ROBDDs with k+1 variables are canonical as well
    C.  Variable ordering matters
      1.  Example: Let x and y be n-bit vectors
      2.  x == y can be done represented by an ROBDD with O(n) nodes
	     if bits are interleaved.
	a  At each level, compare the bits
	b  Pass the conjunction along
      3.  x == y requires Omega(2^n) nodes if the bits of x preceed
	      the bits of y:
	   Need to distinguishe all possible values of x
	&  There are 2^n such values
	=> The ROBDD has Omega(2^n) branches going from the last bit of
	     x to the first bit of y
	   
 II.  Operations on ROBDDs
    A.  Shannon expansion
    B.  Apply
    C.  Restrict
    D.  Quantifiers
    E.  Function composition

III.  Representing other data types
    A.  Finite domains
    B.  Sets
    C.  Relations

 IV.  Applications for Verification
    A.  Equivalence checking
    B.  Symbolic simulation
    C.  Model checking

  V.  Review/Preview
    A.  Review
      1.  ROBDDs are an optimized decision tree
        a.  They are efficient for many problems in practice
        b.  But they aren't efficient for everything:
	     if they did, we'd have a proof that P = NP
      1.  ROBDDs are a canonical form
        a.  Easy to test if two boolean functions represented by the
	      ROBDDs with the same variable ordering are the same
	      function -- O(1) time
        b.  Easy to test if a function is a tautology -- O(1) time
	c.  Easy to test if a function is satisfieable -- O(1) time
      2.  ROBDDs provide a way to treat boolean functions as first
      	      class citizens.  Given ROBDDs for f and g, we can
	a.  Compute the ROBDD for ~f, f&g f|g, f^g, etc.
	b.  Compute ForAll x. f(x, y), Exists x. f(x, y)
	c.  Compute function composition f(g(x))
      3.  ROBDDs are useful for
	a.  equivalence checking
	b.  model-checking (i.e. fixpoint computations)
    B.  Further reading:
      1.  http://www.itu.dk/courses/AVA/E2005/bdd-eap.pdf
            A detailed tutorial, going into more detail than
	    we'll need for this course.  By Henrik Reif Andersen
      2.  http://dx.doi.org/10.1145/123186.123222
            Efficient Implementation of a BDD Package
	    Brace, Rudell, and Bryant
      3.  http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=73590&userType=&tag=1
      	    "On the complexity of VLSI implementations and graph
	      representations of boolean functions with application
	      to integer multiplication"
	    Bryant.
      4.  http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=480018
            "Binary decision diagrams and beyond: enabling technologies
	    for formal verification".  Bryant.
	    A survey paper discussing many extensions to the BDD idea
	    including dynamic (automatic) variable re-ordering, diagrams
	    with more than two terminal values (for represnting arithmetic
	    and other domains), etc.
    C.  Preview
      0.  Python/Jython + BDDs tutorial on Friday, Jan. 11
      1.  Reading for Jan. 14:
            "Equivalence Checking Using Cuts and Heaps", Kuehlmann.
	    This is a short, but dense paper.  I hope to get some
	    notes up on the web by the weekend.