In the following, we outline the contributions of this thesis on each of the objectives identified above. An overview of the contributions of the Thesis is depicted in Fig. 1.8.
Vivado HLS
Construct FSMD
RTL to C reverse Engineering Frame work
Detected Faster simulation
(FastSim)
Equivalent
RTL-C
C VerilogRTL
Verification (DEEQ)
Register to variable mapping (REVAMP)
HTs detection (BLAST) RTL-C
Construct FSMD
RTL-FSMD
May not be
Equivalent Successful Not Successful
Not Detected C-FSMD
Pass Fail
Applications
Figure 1.8: Contributions of the Thesis
Introduction
1.4.1 FastSim: A Fast Simulation Framework for High-Level Syn- thesis
This work is primarily motivated by the fact that C-simulation is much faster compared to RTL-simulation. A fast simulation frameworkFastSim is developed in this work that manip- ulates certain unique features of HLS design to extract a concise, well-indented, and debug friendly C behaviour from the synthesized RTL by the HLS tool. Specifically, we present a completely automated, fast, and cycle accurate simulation-based verification framework for HLS generated RTLs. The framework ensures the end-to-end correctness of HLS. It is also equipped to give accurate design performance estimation. In our approach, the Verilog RTL is first converted into an abstract syntax tree (AST) format using the PyVerilog [9]. The AST is then pre-processed, i.e, the C incompatible constructs of Verilog like bit-select and part-select are replaced with equivalent compatible representations. Next, we identify the register transfer operations in the datapath concerning the control signals at each control step of the controller FSM to generate an equivalent finite-state machine with datapaths (FSMD) code. To generate the equivalent C code, the intermediate FSMD and the variables, controller state, RT operations, etc. are mapped into appropriate data types, and the equiv- alent C code called RTL-C is generated. Finally, the input C source code and the RTL-C code are co-simulated using C compilers like GCC or using C-simulation of HLS tools with test cases to verify the functional correctness of the generated RTL. The correctness and cycle accuracy of our tool has been proved. We then compare the simulation time of our tool with the RTL simulator, software C simulator, and the Verilator. Experimental results demonstrate that FastSim is on average around 300 times faster simulation compared to RTL simulators and comparable performance to that of software C simulators.
1.4.2 DEEQ: Data-driven End-to-End Equivalence Checking of High-Level Synthesis
This work contributes a C to the RTL equivalence checking method to prove the correctness of the HLS generated RTL with respect to its original C code. In our method, we have utilized the C-like behaviour, called RTL-C extracted from the RTL in our first work. Our method identifies all traces of both behaviours C and RTL-C, we identify the compatible traces (i.e., traces which have the same outputs) within behaviour and merged them into one. This will improve performance by reducing many-to-many equivalences of traces into
Contributions
one-to-one trace equivalence. The method then finds the corresponding traces between two behaviours using a data-driven approach. Finally, a satisfiability problem is formulated to prove the equivalence of corresponding traces of both behaviours. The proposed method does not take any internal information from the HLS tool. Primarily novelty of our method:
(i) use of RTL-C to make C to RTL-C equivalence checking feasible (ii) use data-driven approach to find the correspondence of traces between two behaviours (iii) finding and merging compatible traces to reduce complexity. Experimental results show that our pro- posed method can prove the end-to-end equivalence for a commercial HLS tool for several benchmark examples.
1.4.3 REVAMP: Reverse Engineering Register to Variable Map- ping in High-Level Synthesis
The primary motivation of this work is to extract the register to variable mapping in HLS for efficient correlation between input C/C++ and the corresponding HLS generated RTL.
Specifically, we have developed two register to variable reverse engineering frameworks: one based on the invariant generator Daikon [4] and the other one using Satisfiability Modulo Theory (SMT) solver based tool Z3. In the Daikon based framework, the goal is achieved in three steps. In the first step, we obtain the scheduled C code (SD-C) and high-level behaviour (RTL-C) from the scheduling information generated by the HLS tool and the output RTL, respectively. In the second step, we use the invariant generator tool Daikon to find invariants at each state in a program. Since Daikon finds invariants in a program, we combine state-wise SD-C and RTL-C. From the outputs of Daikon, we extract the invariants in which there is an equality relation between a variable of SD-C and a register of RTL-C.
Finally, with this mapping information, we can rewrite the RTL-C in terms of variables and finally generates an equivalent C-code from the RTL. In SMT based approach, both input C and the output RTL-C are modeled as FSMDs. Next, both FSMDs are converted into SSA form. A Satisfiability Modulo Theory (SMT) problem is then formulated to obtain the register to variable mapping. Finally, the RTL-FSMD is rewritten with this mapping information to obtain an equivalent C code from the RTL. Our frameworks can be utilized by the algorithm developers to use HLS tools efficiently. It also can be used for efficient debugging of non-equivalent scenario that arises in FastSim. The framework is implemented and tested on a commercial HLS tool for several benchmark designs.
Introduction
1.4.4 BLAST: Belling the Black-Hat High-Level Synthesis Tool
We propose a formal detection framework for HLS tool inserted hardware Trojans. In this work, we show how battery exhaustion, degradation, and downgrade attacks can be detected using our C to RTL equivalence checking framework. We have utilized two of the previous works RTL to C reverse engineering method and the equivalence checking framework in this work to develop the HT detection framework. We have assumed that both the input C code and the Trojan infected RTL code are available for our analysis. Specifically, our method extracts an RTL finite-state machine with datapaths (FSMD) from the HLS generated RTL.
During FSMD construction, a battery exhaustion attack can be identified. Our proposed method then compares the FSMD of the input C code with the FSMD of the RTL to identify the degradation attack and the downgrade attack. The experimental results confirm the detection of HTs of the black hat HLS tool [106].