FORMAL VERIFICATION CLASS, SPRING 2000
POSSIBLE PROJECTS
Everybody has to sign for one group. Each group is 3-5 people.
THE CHOICE OF:
PROJECT NUMBER 1.
TITLE:
Designing a complete Prolog System for Formal Verification, Hazard Analysis and High-Level Synthesis.
PEOPLE: Bob Hatt plus more?
This project will use Prolog to integrate previous Prolog programs for verification, simulation
and design, written previously by me, by students in this class and by other researchers.
We would like to make it a useful system with a better interface.
Ideally, we would like to be able to read and write subsets of VHDL and Espresso,
or make link to Alan Mishchenko's EDA tools.
All details to be discussed. Open to new ideas.
This project requires learning Prolog.
PROJECT NUMBER 2.
TITLE: Verification of Cache Protocols using Model Checking.
PEOPLE:
FIRST TASKS: Present project ideas in class. Follow papers written by Robert Safranek.
This project requires learning Model-Checking System.
PROJECT NUMBER 3.
TITLE: Using HOL to verify the CCM2.
PEOPLE:
FIRST TASKS: Present project ideas in class.
Perhaps verifying its subset will be sufficient.
This project requires learning HOL.
COMMENT:
CCM machine has been already designed, students will work on improvements and realization.
This machine uses a controller, iterative circuits and controlled cellular automata,
plus two banks of memory for fast execution of algorithms based on binary and multi-valued logic.
CCM Assembly language is used as high-level language of the CCM machine.
This CCM Assembly language is embedded in C/C++.
VHDL Model of CCM exists.
PROJECT NUMBER 4.
TITLE: Using Boyer-Moore system to verify a digital system of your choice.
PEOPLE:
FIRST TASKS: Present project ideas in class.
The system to be verified should have the control unit and the data path and be not trivial.
This project requires learning Boyer-Moore system.
PROJECT NUMBER 5.
TITLE:
Designing the Verifiable Simplified Cube Calculus Machine (SCCM) Using Altera Tools and Board.
PEOPLE:
This project requires learning Altera tools. Use Prolog or any other system for verification.
PROJECT NUMBER 6.
TITLE: Design of Constructive Induction Machine Using Xilinx DEC-PERLE-1 Board.
PEOPLE:
FIRST TASKS:
student : Presentation of IM architecture, Mapping to DEC-PERLE board.
student : Using Mentor tools for simulation.
student : Select and verify formally its subset.
student : Using Xilinx tools for design.
COMMENTS: :
This project requires learning Xilinx tools. Use Prolog or any other system for verification.
This machine has been already designed, students will work on improvements and realization.
This machine learns from examples by creating a multi-level circuit from
arbitrary gates using the principle of Occam's Razor.
Partial VHDL Models of this machine exist. You can use schematic capture tools also.
PROJECT NUMBER 7.
TITLE: Design of Satisfiability/Search Machine (SSM) Using Xilinx DEC-PERLE-1 Board.
PEOPLE:
FIRST TASKS:
student : Presentation of SSM architecture, Mapping to DEC-PERLE board.
student : Using Mentor tools for simulation.
student : Using Xilinx tools for schematic capture and design.
student : Select and verify its subset.
Read the previous work of Patryk Lech and Chong-Ho from previous class.
This project requires learning Xilinx tools. Use Prolog or any other system for verification.
Partial VHDL Models of this machine exist. You can use schematic capture tools also.
PROJECT NUMBER 8.
TITLE: Design of Sorter-Absorber Machine (SAM) Using Xilinx DEC-PERLE-1 Board.
PEOPLE:
FIRST TASKS:
student : Presentation of SAM architecture, Mapping to DEC-PERLE board.
student : Using Mentor tools for simulation (partially completed).
student : Select and verify its subset.
Narit and Pavel : Using Xilinx tools for schematic capture and design.
Read previous reports by Pavel Kashubin, Narit Ruargjiratain, and Pongthai Sokornsint.
COMMENTS: :
This project requires learning Xilinx tools. Use Prolog or any other system for verification.
This machine has been already designed, students will work on improvements and realization.
Sorter-absorber machine sorts cubes and removes those that are subsumed to other cubes.
VHDL Model of this machine exists.
look here for it.
PROJECT NUMBER 9: Hough Transform Processor.
This machine has been already designed, students will work on improvements and realization.
This Processor used arithmetic operators and much memory for real time recognition
of straight lines. It is a kind of specialized Neural Net realized in hardware.
It can be easily adopted to arbitrary analytic curves, for instance circles.
It has many medical and robotics applications.
VHDL Model of this machine exists.
PROJECT NUMBER 10: Satisfiability Machine, for DEC-PERLE-1.
This machine finds all solutions to Boolean Equations, and allows for very fast solution
of many practical problems in CAD, layout, logic synthesis, Pattern Recognition and other.
VHDL Model of this machine exists.
PROJECT NUMBER 11:
Problem of your choice of similiar type (should include one of the following:
complex controller, cellular automata, iterative circuits, pipelined circuits, or systolic circuits)
and of similar complexity.
A project proposed by you will be accepted if it satisfies the following requirements:
- it is not your company proprietary and can be published.
- it is not too easy and/or uninteresting/boring.
- it is not too difficult.
- it solves some problem that was not solved before and is a good illustration
of techniques explained in this class.
For each project, partial analysis of testability and verification will be performed.
Please send me email if you have any questions.
Grading Policy:
The grade will be based on projects and class presentations of students.
No exams.
There will be first four short projects/homeworks,
but ulimately every group will work on a larger project.
I will try to make the final project of each group to be related to their previous homeworks.
Each project can be a starting point to a Master Thesis.