Robustness Verification For Neural Networks In High Level Synthesis

This repository includes a method for the robustness verification of neural networks in high-level synthesis using alpha-beta Crown methods and RTL equivalence techniques.

Requirments

1. Fully Built ScaleHLS (https://github.com/hanchenye/scalehls)
2. Fully Built OpenHLS (https://github.com/makslevental/openhls/tree/main/examples)
3. Vitis HLS (https://www.xilinx.com/support/download.html)
4. Vivado (https://www.xilinx.com/support/download.html)
5. Torch MLIR (https://github.com/llvm/torch-mlir)

Repo Structure

• Vitis HLS

  • linear.cpp: C++ ScaleHLS generated code from the example model defined in linear_test.py.
  • linear.h: Corresponding header file to linear.cpp.
  • linear_tshls.cpp Testbench that instantiates the top-level function in linear.cpp and passes in input vector X.
  • forward_csim.log: Output of testbench run from linear_tshls.cpp

• Vivado

  • linear.v: RTL OpenHLS generated code from the example model defined in linear.v file
  • test_linear.v Testbench that instantiates the module defined in linear.v and passes in input vector X.
  • simulate.log Output of testbench run from test_linear.v.
  • Rest of .v files The rest of the files are verilog files generated by OpenHLS that need to be imported into Vivado along with linear.v.

• Python

  • linear_test.py: Python file that defines the linear neural network model.
  • linear_bench.py: Python file that passes in an input vector X to the PyTorch model defined in linear_test.py. Imports the simulation logs from OpenHLS and Vitis HLS and compares their outputs to the output of the PyTorch model.

Running The Project

1. Define A PyTorch model in linear_test.py (You can change the name of the file).
2. Uncomment the torch.mlir code at the bottom and convert it into its C++ HLS representation using ScaleHLS.
3. Open Vitis_HLS and import the cpp file generated by ScaleHLS. (In the example this would be linear.cpp).
4. Create a header file for the cpp file that also includes a testbench that instantiates the top level function in the cpp file (In the example this would be linear.h and linear_tshls.cpp).
5. Run C simulation or C/RTL simulation if possible and generate the output simulation log. This output log should then be moved into the same folder as the repo (In the example it is forward_csim.log).
6. Convert the neural network defined in linear_test.py into RTL by using OpenHLS (In this example the RTL generated would be linear.v and its corresponding .v files).
7. Import the contents of the RTL into Vivado and make a testbench that instantiates the top level module and sets the inputs to vector X and the weights to the weights set in linear_test.py (In this example the testbench would be test_linear.v)
8. Run Simulation of the testbench. Import the simulation.log file (found in the output of the xsim folder in the project directory) and move it into the same folder as the repo.
9. In a terminal, run the testbench file linear_bench.py to check if it passes the verification test. This testbench file can be changed according to the neural network model that is used.

Link To Thesis: https://acrobat.adobe.com/id/urn:aaid:sc:us:b9f26a67-90fc-401c-8b79-504672fccf0c