Symbolic execution based test-patterns generation algorithm for hardware Trojan detection

Hardware Trojan detection is a very difficult challenge. However, the combination of symbolic execution and metamorphic testing is useful for detecting hardware Trojans in Verilog code. In this paper, symbolic execution and metamorphic testing were combined to detect internal conditionally triggered hardware Trojans in the register-transfer level design. First, control flow graphs of Verilog code were generated. Next, parallel symbolic execution and satisfiability modulo theories solver generated test patterns. Finally, metamorphic testing detected the hardware Trojans. The work used Trust-Hub benchmarks in experiments.