Metrics for Formal Property Checking Against Undesired Circuit Behavior in Embedded Systems

Abstract

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.