Enabling Symbolic Execution for Hardware TCP/IP Stack based on AMD Vitis HLS

Hardware TCP/IP stacks, which directly implement TCP/IP functionality in hardware, have gained increasing attention due to their ability to meet the performance requirements of rapidly growing network speeds while significantly reducing CPU overhead. However, comprehensively testing these hardware implementations remains challenging because of their prohibitively large test input spaces involving diverse packet contents and complex packet dynamics. Symbolic execution, a powerful program analysis technique, has successfully improved testing coverage in software TCP/IP stacks but has not yet been widely adopted for hardware TCP/IP stacks. This paper addresses this gap by enabling symbolic execution to systematically test hardware TCP/IP stacks based on AMD Vitis High-Level Synthesis (HLS). We identify key challenges in applying symbolic execution in this hardware context and propose methods to overcome them. Evaluations on a real-world open-source hardware TCP/IP stack demonstrate the effectiveness of our methods in achieving high test coverage and discovering previously undetected bugs.