Department of Computer Science
CPSC 513: Introduction to Formal Verification and Analysis
Assignments:
Assignment 1: (Assigned September 20, Due September 29)
Fill in some missing code to get a working combinational
circuit comparison tool using BDDs.
Please finish before class time on September 29, 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 29, Due October 6)
Fill in some missing code to get a working combinational
circuit comparison tool using SAT.
Please finish before class time on October 6, 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 13, Due October 25)
Write a simple sorting program and then generate the
SMT expressions to verify that the output is sorted.
Detailed description of assignment.
Assignment 4: (Assigned October 25, Due November 3)
Use Murphi to model and verify a simple cache coherence protocol.
Link to description of assignment.
OPTIONAL Assignment: (Not Assigned, Not Due -- I will not mark this.)
Several people asked that I make the symbolic reachability assignment
available (a few weeks after everyone told me not to have the extra
assignment). If you are interested and have time, it's kind of fun
to see this work... (BTW, I haven't checked that all the links work
this year, since this isn't an assignment this year.)
Fill in some missing code to get a working (BDD-based symbolic)
reachability program for sequential circuits.
Link to description of assignment.