MATHEON-D17: Chip Design Verification
Chip Design Verification with Constraint Integer Programming
Description
In the design process of integrated circuits and other electronic hardware, a huge amount of time and resources is spent on the verification of the design and the final prototype. A process called "property checking" is used to validate certain expected inherent properties of a chip design. Today's techniques validate these properties on the gate level by transforming the property checking problem into a satisfiability problem and using state-of-the-art SAT solvers. However, these techniques stumble across complexity troubles for certain classes of chip designs. The goal of this project is to apply property checking at a higher level (the "register transfer level") to be able to exploit the structure of the chip design in a more reasonable way. Instead of SAT techniques, a mixture of Constraint Programming and Integer Programming is used to tackle the design classes that are too complex for the currently used gate level approach. A second goal of the project is to further develop our Constraint Integer Programming and Linear Programming software, which is already used by a number of other projects in and outside Matheon and ZIB. | |
| Further information is available in the detailed project description. |
Contact
| Stefan Heinz |
Members
| Tobias Achterberg Martin Grötschel Stefan Heinz Thorsten Koch |
Partners
|
Funding
| DFG Research Center Matheon "Mathematics for key technologies: Modelling, simulation, and optimization of real-word processes." |
Duration
| 06/2006 - 04/2009 |