Ab­ge­schlos­se­ne Ab­schulss­a­r­bei­ten - De­tails

SAT-ba­sier­te Test­mus­ter­er­zeu­gung für Ver­zö­ge­rungs­sfeh­ler

Studierender: Moritz Schniedermann
Betreuer: Matthias Kampmann

In dieser Arbeit soll ein Algorithmus zur Testmustererzeugung (engl. Automatic Test Pattern Generation, ATPG) für Übergangsfehler in digitalen Schaltungen entwickelt werden. Dabei soll der Algorithmus auf der Theorie der Booleschen Erfüllbarkeit (engl. Satisfiability, SAT) basieren. In der Literatur gibt es einige effiziente SAT-basierte ATPG Werkzeuge.

Arbeitsschwerpunkte

  • Umwandeln einer Schaltung in eine KNF-Form für SAT-Solver (Tseitin-Transformation)
  • Analyse und Auswahl von verfügbaren SAT-Solvern (z.B. OpenSource Solver wie MiniSAT)
  • Erweiterung des Solvers um die Fähigkeit, Übergangsfehler zu erkennen
  • Evaluation des Algorithmus anhand von SImulationen und vergleich mit der Literatur

Anforderungen

  • Gute C++ Kenntnisse
  • Kenntnisse im Bereich des Tests hochintegrierter Schaltungen
  • Kenntnisse im Bereich Boolescher Theorie / Boolescher Erfüllbarkeit sind von Vorteil (aber keine Voraussetzung)

Literatur

  • S. Eggersglüß und R. Drechsler, "High Quality Test Pattern Generation and Boolean Satisfiability", Springer, New York, 2012