Assignments:

Assignment 1: (Assigned September 17, Due September 26)

Fill in some missing code to get a working combinational circuit comparison tool using BDDs. Please finish before class time on September 26, so we can talk about the assignment in class. Also, start early! The assignment should be very easy, once you get the hang of things, but the initial learning curve to get the code running can be steep!

Assignment 2: (Assigned September 26, Due October 3)

Fill in some missing code to get a working combinational circuit comparison tool using SAT. Please finish before class time on October 3, so we can talk about the assignment in class. Also, start early! As before, the assignment should be very easy, once you get the hang of things.

Assignment 3: (Assigned October 3, Due October 10Extended by Popular Demand to October 15)

Assignment 4: (Assigned October 15, Due October 24)

Assignments 5a and 5b: (Assigned Oct 24, Due Oct 31)

Pick one or the other. Or do both if you want. (But I'd rather you spend more time thinking about project ideas.) 5a is better if you think you'll be implementing something with BDDs for your project. 5b is better if you think you'll be using a model checking tool to verify something.

• Assignment 5a: Fill in some missing code to get a working (BDD-based symbolic) reachability program for sequential circuits. Link to description of assignment.
• Assignment 5b: Add some specs and fairness constraints to verify (or find errors in) a simple mutual exclusion protocol. Link to description of assignment.