EE 510 FV CLASS SYLLABUS FOR SPRING 2000
INTRODUCTION TO FORMAL VERIFICATION AND DESIGN OF DIGITAL SYSTEMS.


Meetings:

OCATE. Tuesdays and Thursdays 6:40-8:20 p.m.

Teacher:

Marek A. Perkowski, Professor of Electrical Engineering.

Prerequisities:

graduate standing in Electrical Engineering.

OFFICIAL SYLLABUS:


Official Syllabus of this class.

MAIN TEXT BOOK:

  • Marek Perkowski, "Design of Testable and Verifiable Sequential Circuits",
    textbook in preparation,
    will be available from professor, on the chapter-by-chapter basis.
  • PROLOG Primers and Manuals. PSU on-line.
  • G. Hachtel, and F. Somenzi, ``Logic Synthesis and Verification Algorithms,'' Kluwer, 1996.
    Here are the lectures of Hachtel and Somenzi:
    Chapters related to this class in their book are:
    Chapter 7: Models of Sequential Circuits.
    FSM Minimization.
    FSM Traversal.
    FST and Reachability.
    FSM Equivalence Checking.
    Symbolic FSM Traversal.
    Chapter 9. Finite Automata and Regular Languages.

    ADDITIONAL TEXTBOOKS AND RESOURCES:

  • XILINX Student Edition, 1/e, Prentice Hall Engineering, December, 1997.
    For people who take projects based on design using FPGAs.

    How to order exam copy.

    Xilinx University Program
    This textbook is only about Xilinx tools usage.
    People who want to learn Altera tools, please ask me about the manuals.
    Other materials, especially on verification, will be available from the professor.
  • A. Ghosh, S. Devadas, and A.R. Newton, "Sequential Logic Testing and Verification",
    go to this link to find their transparencies in postscript format.
    This book describes methods other than based on automatic theorem proving.
  • Hardware Verification by Jurgen Staunstrup, version 0.4, January 19, 1995.
  • Tutorial on Design Verification with Synchronized Transitions
  • G. Birtwistle, and P.A. Subrahmanyam,
    ``Current Trends in Hardware Verification and Automated Theorem Proving,''
    Springer Verlag, available from the professor, only for volunteers.
  • J. Staunstrup, (Ed),
    ``Formal Methods for VLSI Design,''
    North Holland, available from the professor, only for volunteers.
  • M.Yoeli (ed.) , Formal Verification of Hardware Design,
    Tutorial, IEEE Computer Society Press, 1990.
  • T. Melham, Higher Order Logic and Hardware Verification,
    Cambridge Tracts in Theoretical Computer Science 31
    (Cambridge University Press, 1993). Difficult.
  • Higher Order Logic and Hardware Verification, T. F. Melham
  • An online book by Graham Birtwistle et al
  • Nancy G. Leveson and Clark S. Turner. An Investigation of the Therac-25 Accidents. IEEE Computer, 26(7):18-41, July 1993.
  • Robert L. Hummel. Cyrix 6x86 Bug Puts Brakes on NT 4.0. Byte Magazine, 21(11):30,32, November 1996.
  • Other Digital Design Books from Prentice Hall.
  • Marek Perkowski, "Fast Prototyping of Logic Machines with DEC-PERLE-1 Board," textbook in preparation.
    Available from professor.
    Only for people who will work on Cube Calculus Machine Project.
  • Our resources on Test, Verification, Validation, Manufacturable Design.
    Auxiliary information and links, useful for projects, but not a must.
  • Other materials about commercial tools available from professor and his WWW Page.
    available from professor.
  • Commercial tools information available on WWW Pages; primers, manuals, etc., see packages for EE Department.
    available from professor.