windley@cheetah.cs.uidaho.edu (Phil Windley/20000000) (11/28/90)
I'm going to be teaching a course on using formal methods in VLSI design this winter. The course will focus on the use of the HOL verification system in hardware verification. The course will be video taped and available through the University of Idaho Video Outreach program. The videos are available on VHS and 3/4" U-matic formats. You can take the course for credit (transferable graduate credit). The tapes will also be available for rental or purchase. If you take the course for credit, you will be required to make normal progress throughout the semester (this is not a self-paced course). For more information on the Video Outreach Program (or to talk to me about the class) call 800.824.2889 (outside Idaho). Here is a syllabus of the course: Formal Methods in VLSI Design CS 404/504 (Special Topics), 3 credits Spring, 1991 Phil Windley (208.885.6501) Formal methods have the potential for significantly reducing the number of design faults in VLSI and at the same time reduce the cost of that design. They are especially important in safety--critical and security--critical applications. Formal methods require skill in specification and entail reasoning about formal logic. Content: This class will introduce the use of logic in specifying and verifying significant hardware devices. The class will cover the following topics: o Higher--order logic. o How logic can be mechanized in a computer system. o The representation of hardware behavior and structure in logic. o The use of verification tools in manipulating logical expressions. o Techniques for making the specification and verification of large hardware devices practical. Prerequisites: There are no formal prerequisites, but you should be familiar with propositional logic and the concepts of basic computer architecture. You will also need to have a computer system capable of running HOL available. Contact Phil Windley for more information. Text: We will make use of recent papers describing research in this area along with reference manuals for the verification system that we use. Requirements: There will be no exams, but you must complete a term project to receive credit for the course. There are many projects to choose from and I expect that some of the class projects will result in publishable results. -- Phil Windley | windley@cheetah.cs.uidaho.edu Department of Computer Science | windley@cs.uidaho.edu University of Idaho | Fax: 208.885.6645 Moscow, ID 83843 | Phone: 208.885.6501