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

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