[Zurück]

M. Rathmair, F. Schupfer:
"Metrics for Formal Property Checking Against Undesired Circuit Behavior in Embedded Systems";
Vortrag: ANALOG 2016, Bremen; 12.09.2016 - 14.09.2016; in: "ITG-Fachbericht ANALOG 2016", VDE VERLAG GMBH; Berlin; Offenbach, Bismarckstraße 33, 10625 Berlin, (2016), ISBN: 978-3-8007-4265-3; S. 64 - 69.

Moderne Embedded-Systeme, bestehend aus analogen und digitalen Schaltungsstrukturen, beruhen auf der Verifika-
tion von spezifizierten Systemfunktionalitäten. "Property checking" als formale Verifikationsmethodik kann das richtige
Verhalten von Schaltungsteilen mathematisch beweisen. Aufgrund von Skalierbarkeitsproblemnen, kann nur eine
beschränkte Auswahl von Eigenschaften, sowie Modelle mit entsprechend reduzierter Komplexität geprüft werden.
In dieser Arbeit werden Systeme gegen unerwünschte Funktionalitäten geprüft. Diese können absichtlich (Debug-
Artefakte), unbeabsichtigt (Hardwaretrojaner) oder durch neue Kombinationen von wiederverwendeten Modulen im
Design vorhanden sein. Wir definieren Metriken (abstrakte Kosten), die für eine effektive Planung von Verifikation-
sprozessen verwendet werden können. Überprüfte Eigenschaften werden bezüglich ihrer Verifikationslaufzeit bewertet
und in einer Wissensbasis abgespeichert. Diese Wissensbasis wird kontinuierlich mit Daten von vorhergehenden Projek-
ten gefüllt und erlaubt so für neue Designs eine Abschätzung des Verifikationsaufwandes. Unter gegebenen Verikations-
budget können so die zu prüfenden Eigenschaften systematisch ausgewählt und automatischen checker tools übergeben
werden.

Modern embedded systems, including analog and digital circuits, strongly rely on the verification of the intended system
functionality. Property checking, as a formal verification methodology may prove the correct behavior of design subparts.
Due to scalability issues, a dedicated selection of characteristics to be checked and constrictive model complexity is
required for keeping the verification effort reasonable. In this work we propose checking for undesired functionalities,
whether they are intentionally (debug artifact), unintentionally (hardware Trojan) or due to reuse of functional modules
present in the design. We define measures (abstracted costs) which may be used for effective verification planning.
Characteristics are rated on a common knowledge base, revisioned over past design projects in combination with statistical
runtime estimation. A resulting subset of cost efficient properties is finally handed over to an automatic checking tool.

Circuit Formal Verification

http://publik.tuwien.ac.at/files/publik_252676.pdf