CSE773 Design Verification, Spring 2003
Formal Methods for Specification and Verification of Digital Systems
Syllabus
- Catalog Description:
- Theory, practice and tools for using higher order logic as a means for describing, designing and verifying computer systems.
- Prerequisite:
- CSE607, CSE561
- General Information
- Place & Time
- Tu,Th 1:00 to 2:20, 2-120 CST
- Instructor
-
- Edward Stabler
- 2-133 CST
- email
stabler@ecs.syr.edu
- Anonymous Email :
Click Here
- Office Hours:
- Stabler
- Tue. 8-noon, 2-122 CST
- Thur.8-noon, 2-122 CST
- Morris
-
- Prof. Lockwood Morris will be assisting in this course.
He is a scholar in the field of functional languages and
theorem-proving.
- Evaluation:
I am hoping the enrollment will be about 15-20 students.
Students will keep a 'course book' continuously that will describe
what they are working on, what they have completed,
plans for next steps, etc. I expect to review these course
books with each student, one to one, each week. It is possible
I will require final presentation in which students will describe
their work to other students in the class. I do not expect to
give examinations but there will be simple quizzes that will count
towards the final grade.
- Web Site
http://web.ecs.syr.edu/~stabler/773s03
- Course Directory: There is a readable directory for the class. We expect
to use it for material that will be helpful. /home/ecefac/cse773
- Resources
- Introductory Notes
This course is devoted to studying methods for analyzing digital designs.
The course involves using mathematical methods for specifying design goals
and formal analysis of proposed design to prove that the design meets
the specification.
The sentence above is an odd one.
People who are not familiar with digital system
design practice probably assume that designers analyze their designs to
make sure specifications are met. But the practice of digital system design is
not like that. Specifications are seldom given in a clear and unambiguous
way, using a language with unambiguous semantics. The proposed designs are
checked for correctness by simulation. In some cases the number of
simulation runs
is very large but for all but the most elementary designs the verification
cannot be complete. In addition, it is essential that all large designs
be 'layered', divided into related design levels ranging from the actual
physical layout of switches and pads, to the abstract level where algorithms
for floating point addition are implemented. Another major drawback to
checking design correctness by simulation is checking results. In all
practical cases
checking for correctness by human viewing and checking is not feasible.
What is needed is a 'standard' so the simulation results can be checked
against those
provided by the standard.
But of course checking by simulation works very well in some respects. Big
design errors are almost always detected and very good design environments based on a core simulation engine are available.
All design seems to be characterized by the idea of putting simple components
together to meet a design goal. The creative process of the designer involves
understanding component behavior, and the required behavior of the design, and
then cleverly combining components to provide that behavior. It is common that
designers may overlook design errors which arise when th design is used in a way
not intended or expected by the designer, but capable of occurrence in situ.
Designers are asked to submit to a 'design review' in which the designer proudly presents his/her design while a group of designers listen and look for
ways the design might fail or be improved.
My dream is that eventually CAD
support tools will include a computer-based design review service.
The designer would explain why the components are connected in a particular
way to achieve a design goal, and the computer will check this reasoning.
It will check for:
- Completeness.
- Does the design meet the design goals for all
the required external environments?
- Contradictory specifications.
- It is easy to make this mistake
since specifications are often not procedural, but describe a beginning and
ending relatiosnhip.
- Redundancy
- Are all the components needed, used? Is there a simpler
equivalent?
We are far from having computer support for checking reasoning on designs
of substantial complexity. In the course of your professional careers you can
expect a continuing effort to provide more effective computer support for checking
design correctness. It is a very important topic. Companies like Intel and IBM admit that the engineering man-hours devoted to 'checking' now exceeds the man-hours
devoted to 'designing'. It is as if we are looking at an ancient map of the
world, with some parts shown in great detail and accuracy, while there are other large spaces labeled 'Terra Incognita' or something similar. In your lifetime
these areas will be investigated and developed. Surely there can be no doubt
that eventually it will be possible for computers to become reasonable partners in reasoning about designs.
There are a number of computer-based checking
methods The main computer-based tool to be used in this course is a system
called HOL (Higher Order Logic). At the first level HOL provides a 'proof
checker'. It checks a sequence of logical steps for logical correctness.
The designer, or the design checker, provides the logical argument to be checked. HOL keeps track, making sure that there are no errors in the proof.
The nature of our proofs problem will often be 'I claim this configuration of gates will exhibit a required overall behavior'.
HOL also provides a very large collection of theorems that have been
proven correct by others. Since HOL is an open system the proofs of all the
library theorems is available.
HOL provides a large collection of 'tactics'. Our proofs tend to be constructed "backwards" in the following sense. We wish to prove something, a goal,
and we search for a step to help us prove the goal. That is backwards.
Logical demonstrations like: "Socrates is a man, All men are mortal, therefore
Socrates is mortal" reason "forwards" from facts to conclusions.
But we will usually go the other direction and HOL provides a large number
of Tactics to support backward reasoning. An example is CONJ_TAC which says
that in order to prove a goal "A and B", it is sufficient to split the
goal in two, prove A, prove B.
I used the word 'large' several times above. It is unfortuantely true that
our work will require quite a lot of 'familiarization' work as students
explore the libraries of theorems and the tactics offered to assist them in
their proof efforts.
Students in CSE773 will learn
- to write precise descriptions of specifications, of components, and of designs or networks of components. The verification task starts with three things, the specification, the components and the network. All three will be described carefully. This requires some skill development.
- effective methods for proving that designs meet their
specifications.
- to structure a design environment, creating definitions
and theorems that will assist a particular verification problem, and
be useful over a range of verification tasks.
- To use hierarchies of abstractions to describe designs and specifications
and to connect the levels explicitly, definingforammly the relationships
between levels.
- to use HOL, a logical proof environment.
The tools we will use check the designer's
reasoning. This requires a clear statement of the specification, of component
behavior and of the line of reasoning justifying the belief the design
meets the design goal.
It can be tedious. Since this kind of verification is not included
in early courses in digital design, new ways of thinking and reasoning are
needed. But the process is intriguing in the same sense that a good puzzle
or mystery is intriguing. And, a very deep level of understanding is usually
developed in the process of constructing the line of reasoning verifying
correctness of a design.
The course will consider designs on increasing interest as the semester
proceeds. In the early weeks only very simple tasks are assigned since the main
goal is to develop skill in using the logic checking environment, HOL.
However it important to note that the formal design verification methods
are useful at many levels of abstraction, so the simple proofs and
definitions created early in the course will be used later.
For example, once we have designed and verified an adder using simple gates,
it will never be necessary to refer again to the gate level design when using
the adder as a component. If we wish to use an adder as a component, we do
not need to know the gate structure of the adder. we need only use the
specification of the adder. After designing a particular arrangement
of adders we would argue, "Given that adders work as specified,
then the following arrangement of adders constitutes a multiplier".
Then we would prove it so.