Property Coverage Analysis Based Trustworthiness Verification for Potential Threats from EDA Tools
Yingxin Qiu, Huawei Li, Tiancheng Wang, Bo Liu, Yingke Gao, Xiaowei Li · 2016
Trustworthiness of a hardware design has caused great concerns, including the malicious modifications on the design made by Electrical Design Automation (EDA) tools of third-party. In this paper, a novel hardware Trojan (HT) detection method based on the property coverage analysis is proposed to verify the synthesized netlist. The proposed method is motivated by the observation that the malicious modification on the design would threaten the predesigned properties, either by invalidating the properties or by lowering their state coverage, which can be verified by model checking in principle. The proposed method has generality and can be applied to a variety of hardware Trojans. With HTs inserted in the netlists, the experimental results show the proposed method can detect the malicious Trojans effectively.