Hardware Description and Verification
Sources of further information relevant to the course:
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!
Formal Methods (survey papers)
BDDs and Model Checking:
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,
, 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.
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
Cryptol from Galois Inc.
The Original Lava paper
Sheeran on generating fast multipliers in Lava (FMCAD'04)
Relevant Conferences and Workshops: