CS 8001 Hardware Verification
Fall 2004

Instructor:

Pete Manolios
Office:
Office hours:
Email:
Phone:
CCB 217
By appointment
manolios@cc
404-894-9219

Class Information
Location:
Meeting times:
Web page:
Oscar info:
See notes below
See notes below
http://www.cc.gatech.edu/~manolios/courses/Hardware-Verification-Seminar/2004-Fall/
Seminar - 88543 - CS 8001 - HV

Tools

           
           
           
           

Announcements

Syllabus

Course Description

This seminar covers current research on modeling and formally verifying hardware. I will spend about half the semester introducing the topic. This will include:
  1. An introduction to the ACL2 theorem proving system, which we will use to model a simple DLX-like machine.
  2. A review of correctness criteria focusing on recent work on refinement.
  3. The use of ACL2 to prove the DLX machine correct.
  4. A discussion of decision procedures, including SAT-solvers and UCLID.
The rest of the semester will consist of student presentations. The course is only offered on a pass/fail basis. Students are expected to keep up with the readings and to give one presentation. On the first day of class, I will hand out a course packet consisting of the papers we will read.

Notes

I will be traveling for a good part of the semester, so only register for the class if you are willing to be flexible with scheduling. For example, we may meet twice a week for several weeks, then not meet at all for several other weeks, etc.

Questions?

If you have any questions, please come by and see me, call, or send email. My contact information appears above.

Schedule

Here is the expected schedule for the semester. Please read the assigned papers and materials before they are covered in class.

Class Number
Topics
Class 1
Th, Aug 19, 10-11
CCB 206
Motivation and goals.
Overview of class and ACL2.
Distribute readings.
Class 2
Mon, Aug 23, 11-12
CCB 206
Introduction to ACL2.
Readings:
  1. Tools
  2. A Gentle Introduction to ACL2 Programming
  3. Hyper-Card for ACL2 Programming
  4. Getting started. Getting Started with ACL2 Programming
Class 3
Tue, Aug 24, 1:30-2:30
CCB 206
Modeling and Reasoning about Processor Models in ACL2.
Readings:
  1. Mechanized Formal Reasoning about Programs and Computing Machines, Bob Boyer and J Moore, in R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1996. This paper explains a formalization style that has been extremely successful in enabling mechanized reasoning about programs and machines, illustrated in ACL2. This paper presents the so-called ``small machine'' model, an extremely simple processor whose state consists of the program counter, a RAM, an execute-only program space, a control stack and a flag. The paper explains how to prove theorems about such models.
  2. Panagiotis Manolios. Verification of Pipelined Machines in ACL2. In J Strother Moore and Matt Kaufmann, editors, ACL2 Workshop 2000. Only read the part that discusses the processor models.
Class 4
Tue, Sep 7, 11:10-12:00
CCB 206
Correctness of Pipelined Machines.
Readings:
  1. Burch and Dill. Automatic Verification of Pipelined Microprocessor Control. In Computer Aided Verification, CAV 1994. Springer-Verlag, 1994.
  2. Panagiotis Manolios. Correctness of Pipelined Machines. In W. A. Hunt, Jr. and S. D. Johnson, editors, Formal Methods in Computer-Aided Design, FMCAD 2000, volume 1954 of LNCS, pages 161-178. Springer-Verlag, 2000.
  3. Aagaard, Cook, Day, and Jones. A Framework for Microprocessor Correctness Statements. In T. Margaria and T. Melham, editors, Correct Hardware Design and Verification Methods, CHARME '01, volume 2144 of LNCS, pages 433-448. Springer-Verlag, 2001.
Class 5
Wed, Sep 29, 9:00-10:00
CCB 206
Proving Correctness of Pipelined Machines.
Readings:
  1. Panagiotis Manolios. A Compositional Theory of Refinement for Branching Time. CHARME 2003, the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, October 2003.
Class 6
Fri, Oct 1, 11:00-12:00
CCB 206
Proving Correctness of Pipelined Machines with ACL2.
Readings:
  1. Panagiotis Manolios. Verification of Pipelined Machines in ACL2. In J Strother Moore and Matt Kaufmann, editors, ACL2 Workshop 2000. Now read the whole paper.
Class 7
Tue, Oct 5, 11:10-12:00
CCB 206
SAT solvers.
Readings:
  1. M. W. Moskewicz and C. F. Madigan and Y. Zhao and L. Zhang and S. Malik. Chaff: Engineering an Efficient SAT Solver, Design Automation Conference (DAC'01), pages 530-535, 2001.
Class 8
Tue, Oct 12, 11:10-12:00
CCB 206
CLU Logic: Definition, Modeling, and Deciding.
Readings:
  1. Bryant, Lahiri, and Seshia. Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In E. Brinksma and K. G. Larsen, editors, Computer-Aided Verification--CAV 2002, volume 2404 of LNCS, pages 78-92. Springer-Verlag, 2002.
  2. Bryant, Lahiri, and Seshia. Deciding CLU Logic Formulas via Boolean and Pseudo-Boolean Encodings. In Proc. Intl. Workshop on Constraints in Formal Verification, September 2002.
Class 9
Tue, Oct 26, 11:10-12:00
CCB 206
Automating Refinement with UCLID and an outline of directions for future research.
Readings:
  1. Panagiotis Manolios and Sudarshan K. Srinivasan. Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements. DATE 2004, Design, Automation, and Test in Europe, 2004.
Class 10
Tue, Nov 2, 11:10-12:00
CCB 206
Ivan Raikov: Efficient Execution of Hardware Models.
Readings:
  1. High-speed, analyzable simulators (ACL2 Case Studies).
  2. Using a single-threaded object to speed a verified graph pathfinder. (Optional)
  3. Using MBE to speed a verified graph pathfinder. (Optional)
Class 11
Tue, Nov 9, 11:10-12:00
CCB 206
Preston Galle: Hardware-Accelerated Satisfiability Solvers.
Readings:
  1. Skliarova and de Brito Ferrrari. Reconfigurable Hardware SAT Solvers: A Survey of Systems. IEEE Transactions on Computers, Vol. 53, No. 11, 11/2004.
Class 12
Fri, Nov 12, 11:00-12:00
CCB 206
Shan Shan Huang: Converting Boolean formulas to CNF.
Readings:
  1. Paul Jackson and Daniel Sheridan Clause form convertions for Boolean Circuits.
Class 13
Tue, Nov 30, 11:10-12:00
CCB 206
Phu Le: Bit-Level Reasoning.
Readings:
  1. David M. Russinoff A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon Processor.
  2. Andraus and Sakallah Automatic Abstraction and Verification of Verilog Models.
Class 14
Fri, Dec 3, 11:00-12:00
CCB 206
Christopher Church: Symbolic Trajectory Evaluation.
Readings:
  1. Bryant, Beatty, and Seger. Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation.
  2. Ching-Tsun Chou. The Mathematical Foundation of Symbolic Trajectory Evaluation.

The rest of the semester will consist of student presentations and the default meeting time is Tuesday from 11:10 to 12:00. Here are some topics to choose from and for which I can suggest several papers, but feel free to suggest other topics that you find interesting. The presentations should cover 2-4 papers and students should decide what they are going to present by the beginning of class 7.

  1. Model checking approaches to hardware verification.
  2. STE (Symbolic Trajectory Evaluation) approaches.
  3. Encoding schemes.
  4. Exploiting positive equality.
  5. Modeling advanced features: OOO, Exceptions, superscalar processors, etc.
  6. Bit-level reasoning.
  7. Floating point verification.
  8. Assertion-based verification & Boolean equivalence checking.
  9. Efficiently executable formal models.

Last modified: Tue Nov 30 11:01:18 EST 2004