MATHEON-D17: Chip Design Verification
Chip-Design-Verifikation durch Constraint-Integer-Programmierung
Beschreibung
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 Boolschen 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. Ein weiteres Ziel des Projektes ist die Weiterentwicklung unserer Software zum Lösen von Constraint-Integer-Programmen und Linearen Programmen. Diese wird bereits in einigen Projekten innerhalb und außerhalb des Matheon und des ZIB verwendet. | |
| Weitere Informationen finden sich in der ausführlichen Projektbeschreibung. |
Ansprechpartner
| Stefan Heinz |
Mitarbeiter
| Tobias Achterberg Martin Grötschel Stefan Heinz Thorsten Koch |
Partner
|
Finanzierung
| DFG Forschungszentrum Matheon "Mathematik für Schlüsseltechnologien: Modellierung, Simulation und Optimierung realer Prozesse." |
Dauer
| 06/2006 - 04/2009 |