Department of Computer Science
CPSC 513: Integrated System Design
Assignments:
Assignment 0: (Assigned January 12, Due January 24)
Draw a good BDD for the Boolean function (written in C notation)
g ? (f?e:d) : (c?b:a), where a, b, c, d, e, f, and g are all Boolean
variables. (In other words, this is a circuit with 3 multiplexers
arranged with two feeding the third.)
Assignment 1: (Assigned January 19?, Due January 31)
Fill in some missing code to get a working BDD-based combinational
circuit comparison tool.
Link to detailed description of assignment.
Assignment 2: (Assigned January 26, Due February 7)
Consider the (family of) Boolean function f, with inputs a[n-1]..a[0],
b[n-1]..b[0], and m[1]..m[log n]. (In other words, it's a function that
depends on 2n+logn Boolean inputs.) The function is defined in terms
of subfunctions g: f=g[i], where i is the value of the m inputs in binary.
(In other words, the m inputs select which g[i] gives the value of f.)
The subfunction g[i] is defined as the OR_{j=0..n-1} (a_j AND b_{i+j mod n}).
(g[i] is the dot product of a and (b rotated by i bits).) Prove that
the BDD for f is exponential-sized for all variable orders.
Assignment 3: (Assigned February 2, Due February 14)
Use Murphi to model and verify a simple cache coherence protocol.
Link to description of assignment.
Choose one (or both) of Assignments 4a and 4b to do.
Assignment 4a: (Assigned February 16, Due February 28)
Fill in some missing code to get a working BDD-based reachable states
computation tool.
Link to detailed description of assignment.
Assignment 4b: (Assigned February 16, Due February 28)
SMV is a model checker that uses CTL with fairness as its specification
language.
I'm giving you an SMV model of an alleged solution to the mutual exclusion
problem. Your job is to write appropriate specs and fairness constraints
to demonstrate the problem.
Link to detailed description of assignment.