Automated Field-Based Decomposition To Accelerate Model Checking Fpga-Based Tcp/Ip

There is a rising effort to move the full TCP/IP stack from the software to the hardware to improve the network performance and programmability further. The hardware-based TCP/IP stack must be utterly correct since TCP is the foundation of many critical applications. However, it is impractical to apply the conventional model checking methods or decomposition techniques to verify the correctness because there are numerous stateless and stateful functions involved in TCP/IP stack. Therefore, we propose an automated field-based decomposition method to make feasible the model checking of the hardware-based TCP/IP. Our method can significantly mitigate the state space explosion issue while maintaining the verification completeness. We choose FPGA, a popular programmable hardware, as our study object in the paper. Our method effectiveness is demonstrated by the verification of both stateful and stateless functions of the FPGA-based TCP/IP.