Rethinking RTL flows with AI-driven hybrid formal verification

Modern RTL verification flows generate more evidence than engineers can always review with equal priority. Simulation, assertions, coverage, and formal analysis each expose different classes of behavior, but a large design can produce hundreds or thousands of properties.

This article describes an AI-assisted workflow that uses machine learning to prioritize those properties while leaving proof and counterexample generation to the formal engine. The approach is intended to complement, not replace, established SystemVerilog, Universal Verification Methodology (UVM), simulation, and formal verification practices.

The problem: too many properties, too little verification time

Verification teams face a practical allocation problem. A complex subsystem may include control-state logic, FIFO interfaces, arbitration, multiple clock domains, configuration registers, error handling, and protocol checks. Each area can generate assertions, and each assertion can have a different verification cost and value. Some properties prove quickly. Others expose difficult corner cases or consume substantial solver resources.

Simulation remains essential because it exercises realistic scenarios, software interactions, coverage goals, and system-level behavior. Formal verification offers a different capability: it can prove or disprove a specified property over the modeled state space under explicit assumptions. Formal methods therefore complement simulation rather than simply compete with it.

The remaining question is operational: when a verification environment contains a large property set, which properties should receive attention first? Engineers normally answer this using design knowledge, coverage, previous failures, proof history, and experience. As designs grow, an automated way to organize that evidence becomes attractive.

AI as a prioritization layer

Machine learning has become an active research area in electronic design automation, including hardware design and verification. For formal verification, the most useful role may be narrower than asking AI to determine whether a design is correct. AI can instead act as a prioritization layer in front of the formal engine.

The model can assign a priority to each property using features such as RTL hierarchy, number of referenced signals, control and data dependencies, state-machine complexity, clock relationships, previous proof duration, coverage gaps, prior failures, and related assertions. The output is a recommendation about verification order, not a proof result.

A five-stage workflow

The workflow can be organized in five stages: RTL and property analysis, feature extraction, AI-based property ranking, formal execution, and feedback.

Figure 1 Here is a broad view of the five-stage AI-assisted formal verification workflow. Source: Author

1. RTL and property analysis: Collect the RTL, assertions, hierarchy, interfaces, assumptions, and available verification metadata.
2. Feature extraction: Convert verification information into features that describe structural complexity, dependencies, coverage, history, and proof behavior.
3. AI-based ranking: Use one or more machine-learning models to estimate which properties may provide useful verification information earlier.
4. Formal execution: Run selected properties in the formal engine, which produces the authoritative proof result or counterexample.
5. Feedback: Feed proof results, counterexamples, and verification history back into the prioritization process.

Why use more than one model?

A single machine-learning model may not capture every relationship in a verification dataset. A hybrid system can compare recommendations from multiple models and look for agreement. If several models independently place a property near the top of the queue, the system can treat that agreement as a scheduling signal.

This does not make the prediction a formal result. The distinction is important. Machine learning estimates where verification effort may be useful; formal verification establishes whether the selected property holds under the specified assumptions.

Figure 2 In this illustrative AI-assisted property prioritization, scores are conceptual and are not measured results from a specific project. Source: Author

Counterexamples can become verification feedback

A formal counterexample contains more information than a pass/fail label. It can expose a state transition, control path, boundary condition, protocol sequence, or assumption associated with failure. A verification workflow can use those observations to identify related properties that deserve attention.

For example, consider a hypothetical subsystem with a FIFO, arbitration logic, and two clock domains. Suppose a clock-domain property receives high priority because it involves multiple clocks, has limited simulation coverage, and is related to previous failures. If formal analysis produces a counterexample, the system can increase the priority of other properties that share the affected control or clock-domain path.

This is a feedback mechanism, not autonomous verification. The engineer still determines whether the property is correctly formulated, whether assumptions are valid, and whether the resulting evidence is sufficient.

Working with UVM and simulation

The AI layer does not require a new verification environment. Existing SystemVerilog and UVM infrastructure already produces useful information, including test results, functional coverage, assertion status, regression history, and debug information.

Figure 3 UVM and simulation data have been integrated with AI analysis, formal verification, and engineer review. Source: Author

Simulation can provide scenario coverage and failure information. UVM can provide structured testbench and regression data. The AI layer can organize these signals and recommend formal priorities. The formal engine can then produce proofs or counterexamples. This division lets each part of the flow retain its established role.

• Review low-confidence or strongly disagreeing model recommendations manually.
• Keep AI priority, formal status, and signoff status as separate fields.
• Record the features and model version that produced each recommendation.
• Make sure that critical properties are protected by explicit rules.

In a continuous-integration environment, the loop can run after an RTL change: identify affected properties, update their features, generate priorities, execute selected formal jobs, collect results, and store the new evidence. The next run can then use that history. The result is a practical feedback loop that fits around existing verification infrastructure instead of requiring a separate verification methodology.

The scheduler should also enforce engineering rules outside the model. A property marked as mandatory for signoff should remain in the verification plan even if the model assigns it a low priority. Likewise, the system can reserve resources for regression baselines while using AI to order the remaining work. This makes the AI layer a scheduling aid rather than an uncontrolled gatekeeper.

For example, a property record might contain the number of referenced signals, hierarchy depth, number of state elements involved, clock-domain count, previous proof time, previous failure frequency, coverage status, and whether the property belongs to a critical interface or reset sequence. These features are useful because engineers can inspect them and relate them to the underlying design rather than relying on an opaque score.

The approach can be introduced without replacing the existing verification tool chain. A lightweight orchestration script can collect RTL and assertion metadata, regression results, coverage summaries, formal proof history, and counterexample information. The collected information can be normalized into one record per property. Each record can then be passed to a trained model or a small ensemble of models that returns a priority recommendation.

Turning the concept into an engineering workflow

Below is an illustrative property prioritization example.

Table 1 In this illustrative prioritization example, the entries demonstrate the method and are not experimental measurements. Source: Author

The main benefit is not that AI makes formal verification mathematically stronger. The benefit is that it can help organize verification work. A team can use prioritization to focus compute time on properties associated with complex control, weak coverage, previous failures, or other signals that indicate potential value.

The same idea can help with regression management. If a new RTL revision changes a particular control path, the system can identify related properties and move them upward in the queue. If a property repeatedly consumes large amounts of solver time without producing useful evidence, engineers can inspect its formulation and decide whether to refine it, decompose it, or change its assumptions.

What AI should not decide

AI-based prioritization introduces a new failure mode if engineers treat a low score as permission to ignore a critical property. The system should therefore preserve explicit criticality rules. Safety-critical, security-sensitive, interface, reset, and other signoff properties may require execution regardless of their predicted rank.

The workflow should also remain explainable. Engineers should be able to see which features influenced a ranking and distinguish between a property that was not selected, a property that timed out, and a property that was formally proven. These states carry very different meanings.

From verification execution to verification management

As IC designs become larger, verification teams need more than additional tests. They need ways to organize the evidence produced by tests, assertions, coverage, formal analysis, and debug. AI can provide one layer of that organization.

The practical model is therefore a division of responsibility. Simulation explores scenarios. UVM structures the verification environment. AI analyzes evidence and recommends priorities. Formal verification supplies rigorous proofs and counterexamples. Engineers interpret the results and make signoff decisions.

AI-assisted formal verification is most useful when it remains an assistant to established verification methods. Using machine learning to prioritize properties can help teams direct limited compute and engineering resources toward potentially informative checks, while formal verification remains the authority for proof and counterexample generation.

The approach does not require replacing SystemVerilog, UVM, simulation, or existing formal tools. It adds a layer that connects the evidence those systems already produce. With appropriate safeguards, that layer can turn verification history and counterexamples into feedback for the next analysis cycle.

Praveen Kumar Vagala is a semiconductor design verification professional and independent researcher with extensive experience in the semiconductor industry.

Related Content

• Introduction to Formal Verification
• Is Formal Verification Artificial Intelligence?
• Formal verification: where to use it and why
• Specifications: The hidden bargain for formal verification
• Formal Verification Moves Firmly into the Design Environment

The post Rethinking RTL flows with AI-driven hybrid formal verification appeared first on EDN.