Formal Analysis of MSMA Pipeline for Hardware Trojan Detection

Faiq Khalid Lodhi , Syed Rafay Hasan , Osman Hasan and Falah Awwad


Globalization trends in integrated circuit (IC) design using deep submicron (DSM) technologies are leading to increased vulnerability of IC against malicious intrusions. These malicious intrusions are referred to hardware Trojans. One way to address this threat is to utilize unique electrical signatures of ICs, and any deviation from this signature helps in detecting the potential attack paths. Recently we proposed hybrid macro synchronous micro asynchronous (MSMA) pipeline technique while utilizing, non-conventional, asynchronous circuits to generate timing signature. However, traditionally generating these timing signatures with environmental uncertainties require extensive simulations. It is known to the engineering community that computer simulations have its limitations due to the associated heavy computational requirements. In this project, as a more accurate alternative, we propose a framework to detect the vulnerable paths in the MSMA pipeline for hardware Trojan detection using formal verification methods. In particular, the paper presents a formal model of the MSMA pipeline and its verification results for both functional and timing properties.


Low Power Soft Error Tolerant Macro Synchronous Micro Asynchronous (MSMA) Pipeline


Test vector insertion to obtain timing signature in MSMA


Formal Analysis


Potential Attack Path when Asynchronous Registers are intruded


FSM of Hardware Trojan Detetion in MSMA



Function and Timing Analysis


  1. F. K. Lodhi, O. Hasan, S. R. Hasan and F. Awwad,”Formal Analysis of Macro Synchronous Micro Asychronous Pipeline for Hardware Trojan Detection, ” in Nordic Circuits and Systems Conference (NORCAS 2015): NORCHIP & International Symposium on System-on-Chip (SoC), Oct. 2015, pp.1-4.