Efficient Verification of Timing-Related Network Functions in High-Speed Hardware

To achieve a line rate in the high-speed environment of modern networks, there is a continuing effort to offload network functions from software to programmable hardware (HW). Although the offloading effort has led to greater performance, it brings difficulty in the verification of timing-related network functions (Time-NFs) as well. Time-NFs use numerical timing values to perform various network tasks. For example, congestion control algorithm BBR uses round-trip time to improve throughput. Errors in Time-NFs could cause packet loss and poor throughput. However, verifying Time-NFs in HW often involves many clock cycles that can result in an exponentially increasing number of test cases. Current verification methods either do not scale or sacrifice soundness for scalability.In this paper, we propose an invariant-based method to improve the verification efficiency without losing soundness. Our method is motivated by an observation that most Time-NFs follow a few fixed patterns to use timing information. Based on these patterns, we develop a set of easy-to-validate invariants to constrain the examination space. According to experiments on real Time-NFs, our method can speed up verification by 7 times on average without losing the verification soundness.