COEN6551 - Literature References

Surveys.

W.K. Lam: Hardware Design Verification: Simulation and Formal Method-Based Approaches. Prentice Hall, 2005. (ISBN: 0131433474, 624 pages)

T. Kropf: Introduction to Formal Hardware Verification, Springer Verlag, 1999. (ISBN: 3540654453, 304 pages)

O. Hasan and S. Tahar, Formal Verification Methods, Encyclopedia of Information Science and Technology, pp. 7162-7170, IGI Global Pub., Germany, 2015. (10 pages)

C. Kern and M. Greenstreet, "Formal Verification in Hardware Design: A Survey", ACM Transactions on Design Automation of E. Systems, Vol. 4, April 1999, pp. 123-193. (71 pages)

Carl-Johan Seger, "An Introduction to Formal Verification", Technical Report 92-13, UBC, Department of Computer Science, Vancouver, B.C., Canada, June 1992. (27 pages)

Aarti Gupta, "Formal Hardware Verification Methods: A Survey", Formal Methods in System Design, Vol. 1, pp. 151-238, 1992. (92 pages)

M. Yoeli, "Formal Verification of Hardware Design", IEEE Computer Society Press, 1991. (41 pages)

E. Clarke and J. Wing, Formal Methods: State of the Art and Future Directions, CMU Computer Science Technical Report CMU-CS-96-178, August 1996. (22 pages)

R. P. Kurshan, "Formal Verification in a Commercial Setting", Proc. Design Automation Conference, Anaheim, California, June 9-13, 1997, pp 258-262. also in PDF format

D. Dill, "What's Between Simulation and Formal Verification?" from a presentation by Prof. Dill, Stanford University at DAC'98.

Various Contributors, "Survey of Formal Verification", IEEE Spectrum, June 1996, pp. 61-67.

M.C. McFarland, "Formal Verification of Sequential Hardware: A Tutorial", IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst, Vol 12, No 5, pp. 633-54, May 1993.

ROBDDs.

Alan J. Hu, Formal Hardware Verification with BDDs: An Introduction, IEEE Pacific Rim Conference on Communications, Computers, and Signal Processing (PACRIM), pp.677-682, 1997.

Randal Bryant, "Graph-Based Algorithms for Boolean Function Manipulation", IEEE Transactions on Computers, pp. 677-691, August 1986. (Note: figures are missing in the ps file!)

Randal Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams", CMU CS Tech Report CMU-CS-92-160, 1992.

Randal Bryant, "Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification", International Conference on Computer-Aided Design, pp. 236-243, 1995.

Verification of Combinational Circuits.

Jawahar Jain, Amit Narayan, Masahiro Fujita, and Alberto Sangiovanni-Vincentelli, "Formal Verification of Combinational Circuits", VLSI Design, 1997. This is a survey of verifying combinational circuits.

Verification of Sequential Circuits.

Olivier Coudert and Jean Christophe Madre, "A Unified Framework for the Formal Verification of Sequential Circuits", International Conference on Computer-Aided Design, pp. 126-129, 1990.

Herve Touati, Hamid Savoj, Bill Lin, Robert K. Brayton, and Alberto Sangiovanni-Vincentelli, "Implicit State Enumeration of Finite State Machines Using BDD's", International Conference on Computer-Aided Design, pp. 130-133, 1990. (Optional Reading)

Model Checking.

C. Baier, J.-P. Katoen: Principles of Model Checking, MIT Press, 2008 (ISBN: 0262026499, 975 pages)

E.M. Clarke, O. Grumberg, D. Peled: Model Checking, Mit Pres, 2000. (ISBN: 0262032708, 330 pages)

K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.

E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach", Symposium on Principles of Programming Languages, pp. 117-126, 1983. This is the original paper on 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. This is the journal version of the original paper on symbolic model checking Also published in Proc. International Workshop on Formal Methods in VLSI Design, Miami, January 1991.

J. R. Burch, E. M. Clarke, D. Long, K. L. McMillan, D. L. Dill, "Symbolic Model Checking for Sequential Circuit Verification", IEEE Transactions on CAD, 13(4), 1994.

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.

HOL Theorem Proving.

T.F. Melham and M.J.C. Gordon, Higher Order Logic and Hardware Verification, Cambridge Tracts in Theoretical Computer Science 31, Cambridge University Press, 1993. (ISBN: 052141718X, 165 pages)

G. Birtwistle, B. Graham, and S.-K. Chin, new_theory `HOL`;; An Introduction to Hardware Verification in Higher Order Logic (August 1994).

Multiway Decision Graphs.

F. Corella, Z. Zhou, X. Song, M. Langevin, and E. Cerny, "Multiway Decision Graphs for Automated Hardware Verification," Formal Methods in System Design, Kluwer Academic Publishers, vol. 10, pp. 7-46, February 1997.

E. Cerny, F. Corella, M. Langevin, X. Song, S. Tahar, and Z. Zhou, Automated Verification with Abstract State Machines Using Multiway Decision Graphs, In: T. Kropf (editor), Formal Hardware Verification: Methods and Systems in Comparison, Lecture Notes in Computer Science 1287, State-of-the-Art Survey, Springer Verlag, pp. 79-113, 1997.

Bedtime reading

Semiconductor Engineering Is Formal Ready To Displace Simulation?, May 21, 2014.

J.A. Hall, Seven Myths of Formal Methods. IEEE Software, 7(5):11-19, September 1990.

A follow-up article as also available:
J.P. Bowen and M.G. Hinchey, Seven More Myths of Formal Methods. IEEE Software, 12(4):34-41, July 1995.

For some guidance on the industrial use of formal methods, see:
J.P. Bowen and M.G. Hinchey, Ten Commandments of Formal Methods. IEEE Computer, 28(4):56-63, April 1995.