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.

In recent times, Bounded Model Checking (BMC) engines have gained wide prominence in formal verification. Different BMC engines exist, differing in their optimization, representations and solving mechanisms used to represent and navigate the underlying state transition of the given design to be verified. The objective of this article is to examine if combinations of BMC engines can help to combine their strengths. We propose an approach that can create a sequencing of BMC engines that can reach better depth in formal verification, as opposed to executing them alone for a specified time. Our approach uses machine learning, specifically, the Multi-Armed Bandit paradigm of reinforcement learning, to predict the best-performing BMC engine for a given unrolling depth of the underlying circuit design. We evaluate our approach on a set of benchmark designs from the Hardware Model Checking Competition (HWMCC) benchmarks and show that it outperforms the state-of-the-art BMC engines in terms of the depth reached or time taken to deduce a property violation. The synthesized BMC engine sequences reach better depths than HWMCC results and the state-of-the-art technique, super_deep, for more than 80% of the cases. It also outperforms single engine runs for more than 92% of the cases where a property violation is not found within a given time duration. For designs where property violations are found within the given time duration, the synthesized sequences found the property violation in a lesser time than HWMCC for all the designs and outperformed both super_deep and single engine runs for more than 87% of the designs.

We present two novel sound and complete netlist transformations, which substantially improve verification scalability while enabling very efficient trace reconstruction. First, we present a 2QBF variant of input reparameterization, capable of eliminating inputs without introducing new logic and without complete range computation. While weaker in reduction potential, it yields up to 4 orders of magnitude speedup to trace reconstruction when used as a fast-and-lossy preprocess to traditional reparameterization. Second, we present a novel scalable approach to leverage sequential unateness to merge selective inputs, in cases greatly reducing netlist size and verification complexity. Extensive benchmarking demonstrates the utility of these techniques. Connectivity verification particularly benefits from these reductions, up to 99.8%.

Verification is a critical task in the development of correct computing systems. Simulation remains the predominantly used technique to identify design flaws, due to its scalability. However, simulation intrinsically suffers from low functional coverage, hence often fails to identify all design flaws. Formal verification (FV) is a promising approach to overcome the coverage limitations of simulation, due to its exhaustiveness - which enables it to identify intricate design flaws too complex to practically find using simulation. However, automated FV techniques have scalability drawbacks that limit the size of design components that can be formally verified. One of the key strengths of FV techniques is their use of symbolic reasoning, to efficiently explore a huge number of individual scenarios that would be intractable using simulation. When used in an incomplete manner, the scalability challenges of these algorithms are lessened, enabling efficient and relatively scalable semi-formal bug hunting. Nonetheless, to yield a robust industrial-strength solution, the individual components of such a system - many being heuristic - must be highly tuned, and integrated and orchestrated in an intricate manner. In this paper, we overview the various components useful in a scalable semi-formal search framework, introducing several novel powerful techniques and providing experimental data to illustrate the strengths, weaknesses, and complementary nature of the various techniques.