Hardware Trojans detection through automatic properties extraction and formal verification

To address the difficulties in obtaining golden reference models and the low accuracy when conducting pre-silicon hardware Trojans detection on a large-scale integrated circuit design, a formal detection method to quickly and accurately locate hardware Trojans is proposed in this paper. The hopping signals within each clock cycle are used as the object of analysis in integrated circuit functional traces, in which the candidate set of these signals is obtained by a traversal matching approach. The properties of the candidate set are excavated by utilizing the low flip signal feature to realize the automatic extraction of the hardware design functional properties. According to the counterexamples given by the verification results, the hardware Trojans related design can be quickly located through analysis and formal verification. The experimental results of some Trust-Hub AES benchmarks show that the proposed method can automatically extract the constant properties related to low-activity signals and successfully detect hardware Trojans. This study provides a fast and accurate solution of hardware Trojans detection on a large-scale integrated circuit design.