ECE 598 SV

Formal Hardware/SoC Verification

Reading

Reading for Friday (September 5th):
-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. pdf
This is the original paper on model-checking. 
 
Additional readings:
 
Surveys:
 
-Edmund M. Clarke and Robert P. Kurshan, "Computer-Aided Verification", IEEE
Spectrum, June 1996, pp. 61-67. pdf
This article is old, but it is general and describes the field. Good overview of the work that's happening in industry 
 
-Aarti Gupta, "Formal Hardware Verification Methods: A Survey", Formal
Methods in System Design, Vol. 1, pp. 151-238, 1992. pdf
This is a good general survey article for you to read at your leisure. It talks about techniques that will be covered in the class, so you can come back to it later. Again,
it is dated. 
 
-Carl Seger, “An Introduction to Formal Hardware Verification”, Technical
Report: TR-92-13, 1992. ps
This is an industrial perspective on the use and need for formal verification. It does not deal with SAT base, BDD based techniques or abstractions, so it is incomplete but is worth a read. 
 
- “Formal Verification in Hardware Design: A Survey” pdf
 
Three fundamental papers in software verification:
 
-C. A. R. Hoare, “An Axiomatic Basis for Computer Programming”,
Communications of the ACM, October 1969, pp. 576-583. pdf
This is a classic paper on the basic ideas of software verification, some of which we spoke in class. 
 
-R. W. Floyd, "Assigning Meanings to Programs", Proceedings of Symposia in
Applied Mathematics, Vol. 19, 1967, pp. 19-32. pdf
This is the original. I can't find the text on-line, but I know Grainger has one, and can procure one for you if you want to read it. 
 
-Edsger W. Dijkstra, “Guarded Commands, Nondeterminancy, and the Formal
Derivation of Programs,” Communications of the ACM, 18(8), August 1975, pp.
453-457. pdf
A classic in software verification. You can read weakest precondition from here if you like, but we will be dealing with non-determinism later in the class. 
 
LTL Model Checking:
 
- “Reasoning About Infinite Computations” pdf
 
- “An Automata-Theoretic Approach to Automatic Program Verification” pdf
 
- “The model checker SPIN” pdf
 
- SPIN, Model Checker
 
- SPIN Workshop
 
CTL Model Checking:

- “Design and synthesis of synchronization skeletons using branching time temporal logic” pdf

- “Characterizing correctness properties of parallel programs using fixpoints” pdf

Symbolic Model Checking:

- Getting started with SMV (Tutorial)

- Cadence SMV download