Formal analysis of macro synchronous micro asychronous pipeline for hardware Trojan detection

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 paper, 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.