Design for Assurance: Employing Functional Verification Tools for Thwarting Hardware Trojan Threat in 3PIPs

Third-party intellectual property cores are essential building blocks of modern system-on-chip and integrated circuit designs. However, these design components usually come from vendors of different trust levels and may contain undocumented design functionality. Distinguishing such stealthy lightweight malicious design modification can be a challenging task due to the lack of a golden reference. In this work, we make a step towards design for assurance by developing a method for identifying and preventing hardware Trojans, employing functional verification tools and languages familiar to hardware designers. We dump synthesized design netlist mapped to a field programmable gate array technology library and perform switching as well as coverage analysis at the granularity of look-up-tables (LUTs) in order to identify specious signals and cells. We automatically extract and formally prove properties related to switching and coverage, which allows us to retrieve Trojan trigger condition. We further provide a solution to preventing Trojan from activation by reconfiguring the confirmed malicious LUTs. Experimental results have demonstrated that our method can detect and mitigate Trust-Hub as well as recently reported don't care Trojans.