In den letzten Jahren wurden verstärkt Eigenschaftprüfer genutzt, um die Korrektheit von Chip-Designs zu testen. Diese überprüfen, ob alle möglichen Eingabemuster eine gewisse Eigenschaft erfüllen. Eine solche Eigenschaft ist in einer formalen Sprache, wie zum Beispile Verilog oder VHDL, beschrieben und stellt bestimmte Aspekte des Verhaltens eines Chips dar. Dieses Verfahren brachte einen großen Fortschritt gegenüber der Simulation. Es verifiziert jedoch ein Chip-Design nur punktuell, so dass die globale Korrektheit offen bleibt. Falls eine Eigenschaft fehlschlägt, ist man an der Anzahl von Eingabemustern interessiert, welche zu einem falschen Output führen.

Das Ziel diese Projektes ist es, mathematisch zu analysieren, ob es möglich ist, effizient die fehlschlagenden Eingabemuster zu zählen. Insbesondere ist zu untersuchen, ob die entwickelten Techniken aus dem Valse-XT Projekt erweitert werden können, um dieses Zählproblem in einer angemessenen Zeit zu lösen.

• OneSpin Solutions GmbH
• DFG Forschungszentrum Matheon “Mathematik für Schlüsseltechnologien”,
  Projekt B12: Symmetrien in der Ganzzahligen Programmierung
• DFG Forschungszentrum Matheon “Mathematik für Schlüsseltechnologien”,
  Projekt D17: Chip Design Verifikation