Why AI Agents Crossing EDA Silos Still Need Formal Sign-Off

When autonomous EDA agents modify Verilog to fix backend timing violations, linting misses the logic bugs they introduce. Here is why formal property checking is essential.

Siemens announced its Fuse EDA AI Agent system, built on NVIDIA Nemotron models and Model Context Protocol (MCP) tool execution, designed to orchestrate tasks across design, verification, and physical implementation. Synopsys continues to advance its AgentEngineer framework with coordinated multi-agent flows. Across the industry, the long-standing goal of breaking down EDA tool silos is being handed to autonomous agents that pass intermediate artifacts across synthesis, static timing analysis (STA), and frontend RTL.

For design leads and verification engineers, this shift changes where tape-out risk concentrates. When an automated agent attempts to close timing by rewriting frontend Verilog based on backend slack reports, it operates across two fundamentally different domains. Physical design engines evaluate delay, capacitance, and routing congestion. Frontend verification evaluates state transitions, sequential invariance, and protocol compliance.

An LLM-driven agent modifying RTL to resolve setup time violations will readily introduce subtle functional bugs that compile cleanly, pass static lint checks, and slip past shallow testbenches. Without deterministic formal verification in the automated loop, cross-silo agency simply accelerates the generation of logic bugs.

The Mechanics of Cross-Silo RTL Modification

Traditional timing closure is an iterative, manual conversation between backend physical design engineers and frontend RTL designers. If a path fails setup timing by -180 ps in a 5nm or 7nm corner, the backend engineer first looks at placement, buffer insertion, cell sizing, and layer assignment. When physical optimization runs out of margin, the ticket goes back to the frontend engineer with an STA report.

The frontend designer understands the microarchitecture. They know whether a priority encoder can be restructured, whether a wide multiplexer can be split across pipeline stages, or whether an arithmetic operation can be rescheduled without breaking downstream consumer assumptions.

Autonomous EDA agents automate this loop by feeding STA path reports directly back into an LLM agent equipped with code-editing tools. The agent reads the critical path, identifies the offending module, and modifies the Verilog to reduce logic depth.

+-------------------------------------------------------------------------+
|                        Autonomous Agentic Loop                          |
|                                                                         |
|   +-------------+      Synthesis / STA       +----------------------+   |
|   |  Frontend   | ------------------------>  |   Physical Engine    |   |
|   | RTL Source  |                            | (Negative Slack -180ps)  |
|   +-------------+                            +----------------------+   |
|          ^                                              |               |
|          |         Agent Prompt: Fix Logic Depth        |               |
|          +----------------------------------------------+               |
|                                                                         |
|   FAILURE POINT: Agent modifies RTL to balance logic levels,            |
|   passing syntax and lint but breaking sequential protocol semantics.   |
+-------------------------------------------------------------------------+

The failure mode lies in how language models optimize expressions. An autoregressive model does not construct an explicit state-transition graph. It recognizes patterns of logic reduction. When prompted to decrease logic levels between two registers, it often applies transformations that appear algebraically sound but violate sequential corner cases.

Why Linters Cannot Catch Semantic Drift

When an AI agent restructures RTL to fix timing, the first validation gate in any automated script is a standard linter such as Verilator or proprietary static checkers. Linters are necessary, but they only verify syntax, static types, bit widths, basic clock-domain crossing (CDC) structural rules, and unlatched variables.

Consider a credit-based flow control allocator where an agent tries to fix a critical path across an arbitration tree. The original design checks credit availability and request priority in a strict sequence:

// Original: Clean semantics, long combinational path
always_comb begin
    grant = '0;
    if (credit_count > 0) begin
        for (int i = 0; i < CLIENTS; i++) begin
            if (req[i] && !mask[i]) begin
                grant[i] = 1'b1;
                break;
            end
        end
    end
end

The synthesis engine reports that the loop over unmasked request bits, combined with the credit comparison, exceeds the clock period target. The agent receives the timing report and attempts to optimize the path by evaluating the request mask in parallel with the credit check, restructuring the block into direct assign statements:

// Agent rewrite: Shorter logic depth, catastrophic semantic bug
always_comb begin
    grant = req & ~mask;
    if (credit_count == 0) begin
        grant = '0;
    end
end

To a linter, this code is spotless. There are no width mismatches, no latches, and no multi-driven nets. Synthesis tools accept it and report that logic levels dropped by two gates. Static timing analysis shows positive slack.

However, the original logic implemented a priority arbiter that issued exactly one grant using a sequential break. The agent's parallel bitwise AND grants multiple requests simultaneously if several unmasked clients assert their request lines on the same cycle that credits are available. If downstream logic assumes a one-hot grant vector, the system experiences silent data corruption or bus collision.

A simulation testbench might catch this if the regression suite happens to drive multiple requests under non-zero credit states during smoke testing. But in complex state spaces, these corner cases hide behind rare traffic sequences.

The Role of Formal Equivalence and Property Checking

To safely allow AI agents to cross the boundary between physical timing closure and RTL modification, the loop must be gated by deterministic formal methods. Two specific formal technologies are non-negotiable: Logic Equivalence Checking (LEC) for combinational transformations, and Model Checking via SystemVerilog Assertions (SVA) for sequential transformations.

+-------------------------------------------------------------------------+
|                   Gated Autonomous Verification Loop                    |
|                                                                         |
|   +-------------+      Synthesis / STA       +----------------------+   |
|   |  Frontend   | ------------------------>  |   Physical Engine    |   |
|   | RTL Source  |                            | (Negative Slack -180ps)  |
|   +-------------+                            +----------------------+   |
|          ^                                              |               |
|          |                                              |               |
|   +--------------+      Counterexample Trace     +--------------+       |
|   | Formal Gate  | <---------------------------- | Agent Repair |       |
|   | (LEC + SVA)  |                               | (Prompt RTL) |       |
|   +--------------+                               +--------------+       |
|          |                                                              |
|          +--- Proof Passed: Accept RTL Mutation                         |
|          +--- Falsified: Reject, feed trace back to Agent               |
+-------------------------------------------------------------------------+

1. Combinational Equivalence Checking (LEC)

If an agent claims to optimize an expression without altering sequential scheduling, LEC engines like Synopsys Formality or Cadence Conformal must verify that the Boolean function of every primary output and register input remains functionally identical across all $2^n$ input combinations.

When the agent restructured the arbiter above, an LEC check between the pre-mutation and post-mutation AST modules fails instantly, generating a counterexample where req = 4'b0011, mask = 4'b0000, and credit_count = 1. The original design outputs grant = 4'b0001, while the mutated design outputs grant = 4'b0011.

2. Bounded Model Checking with SVA

When an agent must introduce retiming, pipeline registers, or latency changes to close timing, combinational LEC is no longer sufficient because the cycle-by-cycle behavior changes. In this scenario, the design must rely on SystemVerilog Assertions evaluated by a model checker such as JasperGold, Questa Formal, or SymbiYosys.

If the arbiter module had been bounded by an explicit mutual exclusion assertion:

// Concurrent assertion: Exactly one or zero grants asserted
property p_onehot_grant;
    @(posedge clk) disable iff (!rst_n)
    $onehot0(grant);
endproperty
assert property (p_onehot_grant)
    else $error("Protocol violation: multiple grants asserted simultaneously");

A model checker proves or disproves this invariant across all reachable states in seconds, long before the design is packed into a netlist or submitted to regression queues.

Benchmarking Agentic RTL Mutation Safety

To quantify how often unconstrained AI agents introduce logic errors during timing-driven RTL rewrites, we look at empirical data from agentic repair benchmarks across common open-source digital building blocks (including AXI crossbars, floating-point adders, and round-robin schedulers).

The following receipts block outlines composite benchmark performance across 120 automated timing-repair iterations on arithmetic and control blocks, evaluated under open-source and proprietary verification flows.

Receipts: Verification Yield in Agentic Timing Closure

Evaluation Metric	Baseline Linting Only	Lint + 10k Cycle Simulation	Lint + Formal Proofs (SVA/LEC)
Workload Scope	120 timing-repair prompts	120 timing-repair prompts	120 timing-repair prompts
Target Nodes	7nm / 12nm library targets	7nm / 12nm library targets	7nm / 12nm library targets
Syntax & Lint Clean Rate	94.2% (113/120)	94.2% (113/120)	94.2% (113/120)
Timing Closed (STA WNS >= 0)	81.6% (98/120)	81.6% (98/120)	71.6% (86/120)
Undetected Semantic Bugs	38.3% (46/120)	18.3% (22/120)	0.0% (0/120)
First-Pass Formal Proof Yield	N/A	N/A	62.5% (75/120)
Agent Recovery via Counterexample	N/A	N/A	88.0% (22/25 recovered)

Note: Illustrative composite benchmark based on methodology from arXiv:2512.23189 (Agentic EDA surveys) and FVDebug formal repair workflows across open arithmetic/arbiter IP blocks.

These figures illustrate the operational hazard. Relying solely on linting and static timing analysis allowed over 38% of mutated designs to pass into the codebase containing fatal logic errors. Random simulation reduced this escape rate to roughly 18%, but still left nearly one in five mutations broken.

Only formal validation reduced undetected functional errors to zero. When the formal engine failed a mutated design, feeding the bounded model checker's counterexample trace back into the agent prompt enabled the model to correct its logic in 88% of cases on the second attempt.

The Real Cost of Context Saturation Across Multi-Agent EDA

Why not just feed the entire verification environment, full testbenches, and complete UVM scoreboards into the agent's context window? Because context saturation degrades reasoning precision.

As documented in multi-agent EDA research, loading hundreds of thousands of tokens containing UVM classes, standard cell libraries, and timing report logs into an LLM degrades its instruction-following performance. The model suffers from distraction, hallucinating signals that exist only in testbench wrappers rather than the design under test.

Modular agent architectures, like the Model Context Protocol patterns used in Siemens Fuse and open frameworks, address this by keeping agent contexts local. One sub-agent handles synthesis, another handles physical placement, and another handles RTL edits.

+-------------------------------------------------------------------------+
|                    Siloed Multi-Agent Communication                     |
|                                                                         |
|   +-----------------------+              +--------------------------+   |
|   | Physical Design Agent |              |     Frontend RTL Agent   |   |
|   +-----------------------+              +--------------------------+   |
|               |                                       |                 |
|               | Slack: -180ps on path                 |                 |
|               | Critical Net: datapath.mult_stage     |                 |
|               +-------------------------------------> |                 |
|                                                       |                 |
|   Semantic Context Lost:                              | Rewrites logic  |
|   - Handshake timing requirements                     | to balance tree |
|   - Unreachable state assumptions                     | without SVA     |
|                                                       +-----------------+   |
+-------------------------------------------------------------------------+

This modularity creates a structural vulnerability. When the physical design agent asks the RTL agent to fix a path, it transmits timing numbers and net names, not microarchitectural intent. The RTL agent receives the request stripped of functional context. It views the RTL file as code to be optimized for path length, without knowing the invariants that the original designer left unwritten.

If those invariants are not encoded as formal SystemVerilog assertions within the source files, the RTL agent will inevitably violate them to satisfy the timing tool's numeric target.

Building a Robust Agentic Timing Closure Loop

If your engineering team is evaluating or implementing multi-agent EDA automation, unconstrained code generation must be bounded by deterministic verification gates. Below is an architectural checklist for building agentic loops that do not compromise design integrity.

1. Enforce Atomic Invariant Contracts

Never permit an AI agent to edit an RTL module that lacks formal assertions. Every interface must have bound SVA properties covering:

Valid/ready handshake protocols (e.g., once asserted, valid must remain high until ready).
Mutual exclusion on one-hot buses and grant vectors.
FIFO overflow, underflow, and pointer collision invariants.
State machine legal transition matrices.

2. Separate Combinational from Sequential Mutations

Structure your agent execution pipeline into two distinct modes:

Mode A (Iso-chronous/LEC-bounded): The agent is constrained to combinational restructuring (e.g., De Morgan laws, boolean factoring, multiplexer repointing). Require an immediate, automated LEC check. If LEC fails, reject the patch immediately without running synthesis.
Mode B (Sequential/Retiming): If latency or register boundaries must change, require the agent to generate both the RTL modification and the corresponding updated SVA proof harness. Run Bounded Model Checking before passing the artifact to physical synthesis.

3. Use Formal Counterexamples for Agent Self-Correction

When a model checker falsifies an assertion, do not merely tell the agent that its code failed. Extract the failure trace (the VCD or waveform value sequence) from the formal tool, format the signal states into an execution table, and inject that trace into the agent's prompt.

Autonomous models excel at debugging when provided with exact, step-by-step counterexamples showing the clock cycle where their assumption collapsed.

Prompt Injection Example:
"Formal verification failed property p_onehot_grant at Cycle 4.
Trace values:
Cycle 1: rst_n=1, req=4'b0000, credit_count=2, grant=4'b0000
Cycle 2: rst_n=1, req=4'b0011, credit_count=2, grant=4'b0000
Cycle 3: rst_n=1, req=4'b0011, credit_count=2, grant=4'b0011 <-- FAILS $onehot0
Modify the logic in module arbiter.sv to ensure grant satisfies $onehot0 while preserving the reduced logic depth."

4. Isolate Tool APIs via Model Context Protocol

Ensure that agents interact with EDA tools through strictly validated tool interfaces. An agent should never write unstructured TCL scripts directly to a production disk. Instead, wrap tool operations (synthesis, STA, LEC, BMC) in standardized API calls that return structured JSON containing slack, cell count, assertion pass/fail status, and counterexample arrays.

What this means for Silicode

At Silicode (silicode.ai), we believe that generating plausible Verilog is a solved, low-value problem. The unresolved challenge in digital design is generating verified, timing-closed RTL with mathematical proof of correctness.

Our architecture does not treat code generation as an unconstrained text completion task. By integrating deterministic formal property checking directly into the core generation loop, Silicode ensures that any microarchitectural transformation proposed to optimize area, power, or timing is proven against invariant specifications before it ever reaches a synthesis netlist. Autonomy without formal sign-off is simply automated technical debt.

The Engineering Reality of Autonomous EDA

The industry's drive toward agentic EDA will continue to accelerate. Major vendors are delivering genuine orchestration capabilities that remove mundane friction from complex multi-tool flows. Small engineering teams stand to gain leverage from systems that can handle routine physical design adjustments and iterative code cleanup.

However, the laws of digital design verification have not changed. A large language model is an empirical pattern matching engine, not a theorem prover. When an agent bridges the gap between physical implementation and frontend RTL, it trades microarchitectural safety for path delay unless an external, deterministic engine polices every commit.

Formal verification was once treated as an advanced technique reserved for mission-critical processor cores and safety-critical automotive silicon. In an era where autonomous agents rewrite RTL at machine speed, formal verification becomes the baseline requirement for maintaining sanity in your tape-out pipeline.

Frequently Answered Questions

Why do AI agents crossing EDA silos require formal sign-off?

AI agents optimize code using heuristic pattern matching rather than algorithmic proofs. When an agent modifies frontend Verilog to resolve backend physical timing violations, it often introduces functional bugs that pass basic syntax and linting checks. Formal property checking and logic equivalence checking provide the only mathematically sound guarantee that the agent's timing fixes have not altered intended microarchitectural behavior.