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

Konferenz: ANALOG 2016 - 15. ITG/GMM-Fachtagung
12.09.2016 - 14.09.2016 in Bremen, Germany

Tagungsband: ITG-Fb. 266: Analog 2016

Seiten: 6Sprache: EnglischTyp: PDF

Persönliche VDE-Mitglieder erhalten auf diesen Artikel 10% Rabatt

Autoren:
Rathmair, Michael; Schupfer, Florian (Technical University Wien, Institute of Computer Technology, Gusshausstr. 27-29/384, 1040 Vienna, Austria)

Inhalt:
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.