Hardware Description and Verification
You are not required to buy any textbook for this course. We will make
course materials available online, and mark them as [online]
below. Read these documents!
As general reference for the course, you can
use the Handbook on EDA for IC System Design, Verification, and
Testing (ed. Scheffer, Lavagno, Martin).This is
available as an e-Book
the Chalmers library
Chalmers e-book collection (available from computers at Chalmers,
or by using your library card number).
Search on CRCnetBASE. How much of this you need
to look at depends on your background.
However, we also mention some other textbooks below in case you wish
to consider buying them. See also the links
page for further sources of information.
- Peter J. Ashenden:
Designer's Guide to VHDL.
- This is the VHDL book, and it the most commonly used VHDL
book in industry. Note all the useful supplementary material on the
web page, including a Quick Start lecture on VHDL.
Suggested reading: Chapter 1-7, 8 (sect 1-4
briefly, 5 important), 11.1, 12, 20.1 (only for reference), 21.3,
App A (briefly), App B-C (for reference).
Stefan Sjöholm, Lennart Lindh: VHDL för konstruktion.
This is an alternative for those who speak Swedish.
This book focuses on VHDL for synthesis, which we will not use in
this course. Still, it describes VHDL well, and is a good (and
cheaper) alternative to the previous book. Note that the
book VHDL - en introduktion by the same authors doesn't
cover everything needed in this course.
Suggested reading: chapter 1-5, 6 (except sect
6), 8 (sect 0, 1), 9 (sect 0-9), 12, 13 (sect 0), 14 (sect 1, 3,
- Jiri Gaisler: Notes on a Structured VHDL Design Method [online]
- Cindy Eisner and Dana Fisman:
A Practical Introduction to PSL.
- This seems to be the book about the property
specification language that we will use. I bought it on Amazon.co.uk,
but it was expensive. You should be able to access the book through the
Chalmers library if you are on the Chalmers network.
- Alan J. Hu: Formal Hardware
Verification with BDDs: An Introduction [online]
- Carl-Johan Seger, An
Introduction to Formal Hardware Verification [online], UBC CS TR-92-13, 1992.
Here are some resources for those who have not seen Haskell before, and
for those who have seen it but are rusty:
- Learn you a Haskell, a light, funny read and a good place to start.
- An interactive, online Haskell tutorial
- Programming in Haskell by Graham Hutton This is an excellent introductory textbook. It is also accompanied by slides and by vidoes.
- Real World Haskell for more information about practical appiications of Haskell.
Thanks to Anton Ekblad for good tips.
Second part (may be revised)
Koen Claessen and Mary Sheeran:
Lava Tutorial [online] (PDF).
- (For printing, you might want to use the shrunk version (PDF), with
2 pages put on one page.)
- A Gentle Introduction to
- To be read if Lava expressions make you puzzled. More
info on Haskell can be found at
M. Sheeran, S. Singh and G. Stålmarck: Checking Safety Properties using Induction and a SAT-solver [online], FMCAD 2000.
K. Claessen, N. Een, M. Sheeran and N. Sörensson: SAT-solving in practice [online], WODES08.
This is a recently written tutorial paper (draft) that very briefly
covers SAT-solving, bounded model checking and temporal induction, as
well as giving lots of relevant references.