Hardware Description and Verification 2012: Useful Links

Useful Links

Sources of further information relevant to the course:

The Conference on Formal Methods in Computer Aided Design, 2010. Note that the papers are available, and also slides for many talks. The FMCAD.org site (see links on the left) contains links to previous versions of the conference. This is the premiere conference on formal hardware verification.
From FMCAD 2006: Baumgartner's talk on Integrating FV into Main-Stream Verification: The IBM Experience.
From a workshop associated with FMCAD 2006 Jacobi's talk on Formal Verification in Industry - Current State and Future Directions. (Jacobi is also from IBM)
From FMCAD 2007: A panel on Formal Verification: a Business Perspective
From FMCAD 2010: Viresh Paruthi (IBM): Large-scale Application of Formal Veriﬁcation: From Fiction to Fact
From IEEE Transactions on CAD, Sept. 2005: An industrially effective environment for formal hardware verification by C.-J.H. Seger et al This paper describes Intel's Forte system for the formal verification of datapath-dominated hardware.

VHDL:

Big tutorial
Slides on VHDL by Magnus Björk: VHDL 1 (part 1) (pdf), VHDL 1 (part 2) (pdf) VHDL 2 (pdf) (used in this course in previous years)
The above slides refer to Gaisler's two process method. These are Gaisler's notes on the topic.
vhdl.org. Doesn't seem to have been updated since 2006, but some of the links may be interesting.
The comp.lang.vhdl Usenet news group Frequently Asked Questions

The Electronic Design Automation industry:

Great slides on the EDA ecosystem and its future, by the CEO of Mentor (the third largest EDA company)
DeepChip. See for example the recent summary of the many varieties of assertions (including PSL) that are out there.
EDACafe. Weekly article about different aspects of technology and business. Enlightening!

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).
For reference: Property Specification Language Reference Manual version 1.1, from Accellera. A formal semantics can be found in appendix B.

Formal Methods (survey papers)

BDDs and Model Checking:

Randy Bryant's journal article on BDDs (a very famous paper that is quite accessible)
Bryant's original 1986 paper, with later commentary. Appeared origninally in IEEE Transactions on Computers, Vol. C-35, No. 8 (August, 1986), pp. 677-691
A more comprehensive document on BDDs by Fabio Somenzi, author of a widely used BDD package
A tutorial 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.

SAT-based verification

Hardware Description and Verification in Functional Languages

Work at Centaur by Hunt, Slobodova, Boyer et al on formal verification of the VIA Nano X86-64 Microprocessor
Seger, Jones, O'Leary, Melham et al: Intel's Forte System
Intel's IDV System, abstract from Memocode 2006
Hawk by Matthews, Launchbury, Cook et al, slides from CAV'99, see also Matthews' home page for papers
Cryptol from Galois Inc.
The Original Lava paper
Sheeran on generating fast multipliers in Lava (FMCAD'04)

Relevant Conferences and Workshops:

Designing Correct Circuits 2006
FMCAD 2006. Slides of many great talks are available under Advance Program.
FMCAD 2007. Slides of many great talks are available under Advance Program, again.
FMCAD 2008, FMCAD 2009.
Hardware design and Functional Languages 2007 and 2009.