A hardware Trojan (HT) is a malicious modification of the design done by a rogue employee or a malicious foundry to leak secret information, create a backdoor for attackers, alter functionality, degrade performance and even halt the system. In Black-hat high-level synthesis (HLS) (Pilato et al., 2019), the authors have introduced a possibility of HTs insertion in the register transfer level (RTL) design by the HLS tool itself. Specifically, degradation attack (DA), battery exhaustion (BE) attack, and downgrade attack (DG) have been proposed in that work. In this study, we show how all three HTs inserted by Pilato et al. (2019) can be detected using a C-to-RTL equivalence checking framework. We have assumed that both the input C code and the Trojan-infected RTL code are available for our analysis. Specifically, our framework extracts an RTL-level finite-state machine with datapaths (RTL-FSMDs) from the HLS-generated RTL. During finite-state machine with datapath (FSMD) construction, a BE attack can be identified. Our proposed method then compares the FSMD of the input C code with the RTL-FSMD to identify the DA and the DG. The experimental results confirm the detection of HTs of the black-hat HLS tool.

High-level synthesis (HLS) is a well-established framework used to translate high-level algorithmic behaviors into hardware designs. Despite the enduring research efforts, a major prevailing bottleneck of HLS is the large gap between the design and verification processes. Presently, register transfer level (RTL) simulation is the primary platform used for HLS design verification. Although most of the state-of-the-art RTL simulators provide an abstracted user-friendly platform for verification, they are undesirably slow and sometimes incomprehensible to non-field-programmable gate array experts to debug. The alternative software simulators (C simulation) introduced by commercial HLS tools render faster simulation, but are not cycle accurate and are not capable to estimate design performance. In this article, we introduce an automatic cycle-accurate simulation tool, FastSim, that manipulates certain unique features of HLS design to extract a concise, well-indented, and debug-friendly C behavior from the synthesized RTL. Our simulation tool ensures RTL correctness, provides cycle accuracy, accurate performance estimation, and renders on an average around 300 times faster simulation compared to RTL simulators and comparable performance to that of software C simulators.