TDA956, LP4, VT2010
Hardware Description and Verification
Sources of further information relevant to the course:
The Conference on Formal Methods in Computer Aided Design, 2006, advance program, including slides
From the above:
Baumgartner's talk on Integrating FV into Main-Stream Verification: The IBM Experience.
From a workshop associated with the above conference (on same programme page),
Jacobi's talk on Formal Verification in Industry - Current State and Future Directions
. (Jacobi is also from IBM)
The Conference on Formal Methods in Computer Aided Design, 2007, advance program, including slides
From the above:
A panel on Formal Verification: a Business Perspective
comp.lang.vhdl Usenet news group Frequently Asked Questions
Slides on VHDL by Magnus Björk:
(2×2 per page:
) (used in this course in previous years)
The Electronic Design Automation industry:
Great slides on the EDA ecosystem
and its future, by the CEO of Mentor (the third largest EDA company)
. See for example the 2007 Verification Tool Survey.
. Weekly article about different aspects of technology and business. Enlightening!
To convince you that you are not the only ones using PSL.
An Operational Semantics for Weak PSL
, Koen Claessen and Johan Mårtensson, FMCAD 2004.
PSL Quick Reference Guide
(from Jasper, link only works on Chalmers computers).
Property Specification Language Reference Manual
version 1.1, from
. A formal semantics can be found in appendix B.
Formal Methods (survey papers)
E.M Clarke & J.M Wing
Formal Methods: State of the Art and Future Directions
Prasad, Biere and Gupta
A Survey of Recent Advances in SAT-Based Formal Verification
BDDs and Model Checking:
Randy Bryant's journal article on BDDs
(a very famous paper that also is quite accessible)
A more comprehensive document on BDDs
by Fabio Somenzi, author of a widely used BDD package
on model checking by Ken McMillan. Parts 2,3 and 5 most relevant.
A famous journal paper on symbolic model checking by
Burch, Clarke, Dill , Hwang and McMillan
Henrik Reif Andersen,
An Introduction to Binary Decision Diagrams
, Course Notes for C4340 E96, Department of Computer Science, Technical University of Denmark.
Lecture notes about hardware verification
by Mike Gordon from Cambridge. Chapter 5 is about model checking.
The SMV model checker from CMU
About SMV from Cadence
Relevant Conferences and Workshops:
Designing Correct Circuits 2006
. Slides of many great talks are available under Advance Program.
. Slides of many great talks are available under Advance Program, again.
Hardware design and Functional Languages
2007 and 2009.
. Archive including technical papers.
, March 2010