Bei der Herstellung von Schaltkreisen wird ein Großteil der Zeit im Produktionszyklus zur Verifikation der Schaltkreisentwürfe und der resultierenden Prototypen verwendet. Das sogenannte "Property Checking" dient dabei zur Validierung von gewünschten und erwarteten Eigenschaften des Schaltkreises.

Heutige Techniken überprüfen diese Eigenschaften auf der Gatter-Ebene des Schaltkreises, bei der bereits alle logischen und arithmetischen Operationen in elektronische Gatter umgesetzt wurden. Diese Gatternetzliste wird in ein Zulässigkeitsproblem über Boole'schen Variablen transformiert (SAT), welches dann mit herkömmlichen SAT-Algorithmen gelöst wird. Die SAT-Techniken stoßen aber bei manchen Schaltkreis-Klassen an Komplexitätsgrenzen -- insbesondere bei komplexen arithmetischen Operationen wie z.B. der Multiplikation.

Das Ziel dieses Projektes ist die Anwendung von "Property Checking" auf einer höheren Ebene (der "Register-Transfer-Ebene"), um die spezielle Struktur der verschiedenen Operationen besser ausnutzen zu können. Anstelle von SAT-Techniken soll ein Mix aus Constraint Programming und Integer Programming verwendet werden, um die für SAT-Löser schwierigen Schaltkreis-Klassen bearbeiten zu können.

• Infineon Technologies AG (Raik Brinkmann, Wolfram Büttner, Yakov Novikov)
• Universität Kaiserslautern -- Lehrstuhl für Entwurf informationstechnischer Systeme (Wolfgang Kunz, Dominik Stoffel, Markus Wedler)