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.

• Infineon Technologies AG (Raik Brinkmann, Wolfram Büttner, Yakov Novikov)
• University of Kaiserslautern -- Electronic Design Automation Group (Wolfgang Kunz, Dominik Stoffel, Markus Wedler)