READING LIST FOR THE COURSE

This is a list of papers that do a deeper dive into some of the topics we will cover in class. While some of the papers are optional for summary writing, they are all highly relevant, so recommended for reading and getting appropriate context. Here is a general template for writing your summaries.

You can access these from IEEE and ACM websites if logged into UIUC machines. You can also log into the UIUC Library website with your Illinois netID and paste the title of the paper under "Article" or "Journal" depending on whether it is a conference or journal paper. You can use the get fulltext option, r access it through IEEE/ACM websites from links provided there.


Topic	Paper		Comments
EQUIVALENCE CHECKING	1. Daniel Brand, "Verification of Large Synthesized Designs", International Conference on Computer-Aided Design, pp. 534-537, 1993.	Reqd	This is probably the most cited paper, presenting a fully worked out version of the cutpoint idea. This paper is historically important. Without these ideas, we might have still been custom crafting little gatel level designs!
	2. C. Leonard Berman and Louise H. Trevillyan, "Functional Comparison of Logic Designs for VLSI Circuits", International Conference on Computer-Aided Design, pp. 456-459, 1989.		This is the original introduction of the cutpoint idea. This paper is also old and has historical importance for how we were able to scale this technlogy this far.
	3. Andreas Kuehlmann and Florian Krohm, "Equivalence Checking Using Cuts and Heaps", 34th Design Automation Conference, pp. 263-268, 1997.	Reqd	This papers covers most of the tricks used in modern tools. This paper might be easier to read after we cover the BDDs topic.
	4. Jerry R. Burch, Vigyan Singhal: "Robust latch mapping for combinational equivalence checking", ICCAD 1998: pp. 563-569.		Gives a technique for mapping of latches, as opposed to previous 3 that talk about showing equality once mapping is done. This is an optional read but will be very helpful t understand how the cutpooint matching is done.
Binary Decision Diagrams	1. Randal E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams", ACM Computing Surveys, Vol. 24, No. 3 (September 1992), pp. 293-318. (Preprint published as CMU CS Tech Report CMU-CS-92-160.)	Required	One of the most seminal papers in hardware verification and computer science. Sections 1, 2, 3 are relevant, but the entire paper is excellent.
	2. Randal Bryant, "On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Applications to Integer Multiplication", IEEE Transactions on Computers, Vol. 40, No. 2, February 1991	Optional	A general technique for proving BDDs big for certain functions (and getting better intuition about what makes BDDs big). You may find this interesting if you like theory and/or are interested in understanding what makes BDDs blow up.
SATisfiability solving	Joao Marques-Silva, Ines Lynce, and Sharad Malik, "Conflict-Driven Clause Learning for SAT Solvers", Chapter 4 in the Handbook of Satisfiability, Armin Biere, Marijhn Heule, Hans van Maaren, and Toby Walsch, Eds., IOS Press, 2008.	Required	More updated survey paper with different types of SAT heuristics
	Lintao Zhang and Sharad Malik, "The Quest for Efficient Boolean Satisfiability Solvers", Invited Paper, Proceedings of 14th Conference on Computer Aided Verification (CAV2002), Copenhagen, Denmark, July 2002, Springer Lecture Notes in Computer Science Volume 2404, pp. 17-36. (Also in Proceedings of 8th International Conference on Computer Aided Deduction (CADE 2002)	Required	Classic survey paper on SAT techniques from 2002. Things have moved much further along by 2021. But this gives an understanding of the key aspects of the problem and early solutions.
Temporal logic and model checking	Edmund M. Clarke, E. Allen Emerson, Joseph Sifakis, "Turing Lecture: Model Checking: Algorithmic Verification and Debugging", Communications of the ACM, Vol. 52, No. 11 (November 2009), pp. 74-84.	Required	This is the Turing award lecture on model checking. Good discussion on temporal logic by Allen Emerson (my co-advisor in grad school!).
Symbolic model checking	J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, "Symbolic Model Checking: 10^{20} States and Beyond", Information and Computation, Vol. 98, No. 2, June 1992.	Required	This is symbolic model checking, which treats states as sets of states and represents them with BDDs.
Bounded model checking	A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, "Symbolic Model Checking without BDDs," Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), LNCS Vol. 1579	Required	This is the first paper on BMC, the most practically used form of model checking.