Hardware Trojan Detection using ATPG and Model Checking

The threat of hardware Trojans' existence in integrated circuits has become a major concern in System-on-Chip (SoC) design industry as well as in military/defense organizations. There is an increased emphasis on finding effective ways to detect and activate hardware Trojans in current research efforts. However, state-of-the-art approaches suffer from the lack of completeness and scalability. Moreover, most of the existing methods cannot generate efficient tests to activate the potential hidden Trojan. In this paper, we propose an effective test generation approach which is capable of activating malicious functionality hidden in large sequential designs. Automatic test pattern generation (ATPG) works well on full-scan designs, whereas model checking is suitable for logic blocks without scan chain. Due to overhead considerations, partial-scan chain insertion is the standard practice today. Unfortunately, neither ATPG nor model checking is suitable for partial-scan designs. Our proposed hardware Trojan detection technique utilizes the combination of ATPG and model checking approaches. We use model checking on a subset of non-scan elements and ATPG on scan elements to avoid common pitfalls of running the original design using any one of these techniques. Experimental results demonstrate the effectiveness of tests generated by our proposed approach to detect Trojans on Trust-hub benchmarks.