SuperSAGA: A Supervisor-Subordinate Agentic workflow for the Generation of Assertions

We present SuperSAGA, an agentic semi-automated formal verification framework that assists in generating, debugging, and refining SystemVerilog Assertions (SVA) from natural language specifications. Rather than relying on full manual workflows, SuperSAGA combines Large Language Models (LLMs) with Retrieval-Augmented Generation (RAG) to guide assertion development based on human-reviewed verification plans using an agentic workflow. The framework translates specifications into syntactically correct assertions, integrates feedback from formal verification tools, and supports iterative refinement using an orchestration of supervisor and subordinate agents. Evaluation on OpenTitan IP modules shows improved quantitative coverage over state of the art and reduced manual effort, demonstrating the potential of guided automation in simplifying the assertion generation process for hardware designers.