AssertGPT: LLMs-empowered Assertion-based Verification of Programmable Networks

Assertion-based verification is essential for ensuring that the operational behavior of programmable networks aligns with their intended design specifications. However, reliance on manual assertion generation prolongs verification cycles and introduces deployment barriers due to its labor intensity, limiting scalability in practical implementations. While Large Language Models (LLMs) have demonstrated transformative potential in automating engineering tasks with their excellent natural language understanding, their application to assertion-based network verification remains underexplored. In this study, we propose leveraging LLMs for assertion-based verification of programmable networks. We introduce AssertGPT, an LLMdriven automated assertion generation framework designed to streamline the verification workflow. Firstly, we construct a highquality dataset in the field of assertion-based network verification, and further develop a domain-specific LLM tailored for automated assertion generation in network verification scenarios by synergizing custom instruction refinement with the Retrieval Augmented Generation (RAG) technique. To mitigate hallucinations, we develop a multi-stage assertion checker with a dynamic feedback loop, enabling iterative refinement of AssertGPT’s performance through continuous assertion regeneration guided by syntactic and semantic verification outcomes. An evaluation of diverse network verification requirements and multiple assertion languages (e.g., those in AssertP4, DBVal) underscores AssertGPT’s efficacy in automated assertion generation for assertionbased network verification.