The overall workflow of our approach is shown in the Figure REF  and leverages symbolic execution [1]}, a software testing technique that can
potentially achieve high coverage of the system under analysis.
We have implemented our approach on top of the KLEE symbolic execution engine [2]}.
We follow the approach in [3]} and translate Verilog designs and their synthesized gate-level netlists into their C++ implementations using Verilator, which
is a simulator for hardware designs [4]}. So, we use the KLEE symbolic execution engine with don't care
transition and Trojan detection extensions on the C++ implementations generated by Verilator.
<FIGURE>