EE 510 FV CLASS SCHEDULE, SPRING 1999

INTRODUCTION TO FORMAL VERIFICATION AND DESIGN OF DIGITAL SYSTEM.


Meetings:

OCATE. Tuesdays and Thursdays 6:40 - 8:20 pm. CR 4.

Teacher:

Marek A. Perkowski, Professor of Electrical Engineering.

BACK TO MAIN PAGE OF Professor Marek Perkowski.

Short Description:



The class is an introduction to formal verification, formal synthesis correct from
construction and transformational high-level design methods.
It covers predicate calculus, temporal logic, higher order logic, resolution theorem
proving, language Prolog, model checking, decision diagrams, and several modern
integrated approaches to formal verification and design.
PREREQ: Familiarity with basic combinational/sequential design.


BACK TO MAIN PAGE of Professor Marek Perkowski


TUESDAY, MARCH 30

  • What is this class about.
    The goal of the class is to learn how to verify your design
    and next how to use CAD tools for automatic design free from errors.
    Verification will be done in Prolog.
    Next the design will be transformed to VHDL, schematic capture or Summit tools.
    Next the design will be synthesized using Xilinx or Altera tools. (option, for some projects only).
    The groups of students will be created.
  • Introduction to Automatic Theorem Proving and Prolog language.
  • Predicate Calculus versus Boolean Logic, quantifiers (Chapter 12 from my book).

    THURSDAY, APRIL 1

  • Automatic Theorem Proving.
    Clauses, Horn Clauses, Substitution, Resolution, Unification.
  • Examples of reasoning: forward, backward.
  • Prolog language.
    Simple question answering, logic puzzles, family databases.

    TUESDAY, APRIL 6

  • Presentation and discussion of projects.
  • Brief presentation of the DEC PERLE board and the discussion of mapping to it.
  • List processing and automatic theorem proving in Prolog.

    THURSDAY, APRIL 8

  • Examples of Test Generation and Verification in Prolog.
  • Formal Synthesis correct from specification: Regular Expressions in Prolog.
  • Fundamentals of verification.
  • Verification of a multiplier.

    TUESDAY, APRIL 13

  • Various approaches to formal verification.
  • Sequent calculus: Petri Nets, Flowcharts, natural language described machines.
  • Sequent calculus: Mealy and Moore Machines, Data Path circuits.

    THURSDAY, APRIL 15

  • Student Presentations.
  • Designs correct from specifications. Transformational design methods.

    TUESDAY, APRIL 20

  • CAD tools for logic specification, simulation and synthesis.
  • Introduction to EPLDs and FPGAs.
  • Xilinx chips.
  • Altera chips.

    THURSDAY, APRIL 22

  • CAD tools for logic verification.
  • FPGA computing.

    TUESDAY, APRIL 27

  • Formal verification algorithms based on theorem proving in higher order logic.

    THURSDAY, APRIL 29

  • Formal verification in HOL, introduction.
  • Principle of perfect induction.

    TUESDAY, MAY 4

  • Lecture: Formal verification in HOL, verifying Comparator, Counter, Shifter and Serial
  • to Parallel converter.

    THURSDAY, MAY 6

  • Lecture: formal verification based on automatic theorem proving.
  • HOL: Verifying microprograms. Verifying multiplier.

    TUESDAY, MAY 11

  • Lecture: formal verification based on automatic theorem proving.
  • Using FOL for adder and microprograms.

    THURSDAY, MAY 13

  • Lecture: formal verification based on automatic theorem proving.
  • Using Boyer-Moore to prove correctness of circuit generators.

    TUESDAY, MAY 18

  • Examples of formal verification on simple examples.

    THURSDAY, MAY 20

  • I am absent, attending ISMVL'99.
  • Please meet in class and discuss your projects.
  • Student Presentations (videotaped?).

    TUESDAY, MAY 25.

  • Using Boyer-Moore to proove correctness of circuit generators.
  • Using Relational System.
  • Examples of formal verification performed by students on simple examples.

    THURSDAY, MAY 27

  • Repetition and projects discussions. New approaches and systems for formal verification/design.
  • Student Presentations (videotaped?).

    MONDAY, JUNE 1.

  • Lecture: formal verification based on functions.
  • Lecture: formal verification based on state machines.
  • Presentation and discussion of projects.

    THURSDAY, JUNE 3.

  • Classical and Modern Decision Diagrams.
  • Model Checking.

    TUESDAY, JUNE 8.

  • Model Checking (cont).

    THURSDAY, JUNE 10.

  • Final presentations and discussions of class projects.

    SUNDAY, JUNE 13.

    Last day of accepting class reports.