Why Spec-Driven SVA Generation Beats Prompting Raw Verilog

Recent research presented ahead of DAC 2025 and published across formal verification groups at Princeton and Cadence points to an uncomfortable truth for generative EDA startups: prompting an LLM to write raw Verilog solves the wrong problem. Synthesizable RTL generation feels fast in a demo, but verification still eats between 60 and 70 percent of front-end engineering hours on an ASIC or high-reliability FPGA project.

When a model generates an AXI4 crossbar, an arbiter, or a credit-based FIFO controller, it produces code that looks structurally sound. It passes basic linting. It compiles in Verilator. It even passes a few hand-rolled directed test vectors. Then, three thousand cycles into a randomized stress test with concurrent backpressure and back-to-back aborts, the state machine locks up. The engineering team spends four days debugging a waveform trace to find an unhandled corner case in an elastic buffer that an engineer could have written by hand in two hours.

Generating raw code without formal guarantees inflates downstream verification debt. The high-leverage application of language models and automated agents in front-end silicon design is not generating the implementation logic. It is parsing timing diagrams, register maps, and architectural specifications to generate formal SystemVerilog Assertions (SVA) and functional coverage models that hold the RTL accountable.

The Failure Mode of Direct RTL Generation

To understand why prompt-to-RTL workflows break down, consider how human designers write bugs. Bugs rarely stem from an inability to write a case statement or a synchronous always_ff block. Bugs occur because of cognitive gaps between the specification and the implementation. An engineer misunderstands a protocol rule, overlooks a multi-cycle grant latency, or misjudges how a FIFO empty flag behaves during a simultaneous read and write on opposite clock edges.

When an LLM generates both the RTL and the testbench from the same natural language prompt, it exhibits correlated hallucinations. If the model misinterprets the AXI4-Stream specification regarding whether TREADY can depend combinationaly on TVALID, it will generate RTL with that exact combinational loop. It will then generate a testbench driver that never asserts the sequence that exposes the hazard. The simulation passes with green checkmarks, giving the design lead false confidence.

True verification requires independent redundancy. The verification environment must be derived from the specification as a set of mathematical invariants, completely decoupled from the internal state registers chosen by the RTL author. This is where SystemVerilog Assertions excel.

Declarative SVA Versus Procedural Verification

Procedural testbenches written in Verilog or raw SystemVerilog tasks test paths sequentially. They drive inputs, wait a fixed number of clock ticks, and inspect outputs with $display or if/else checks. This approach suffers from two fatal weaknesses in complex protocols:

1. Temporal blindness: Procedural checkers struggle to catch illegal signal relationships that happen outside the exact timestamp of an assert check.
2. State explosion: Writing procedural tasks for every combination of bus stalls, out-of-order responses, and interleaved resets requires thousands of lines of verbose, fragile code.

SystemVerilog Assertions are declarative. They define temporal logic relationships that must hold across every active clock edge of the simulation or formal state-space exploration.

Take a standard request-grant bus protocol with a maximum latency constraint and an active-low reset. In declarative SVA, the invariant is expressed in a single concurrent property:

property p_req_to_gnt_latency;
  @(posedge clk) disable iff (!rst_n)
  req && !gnt |-> ##[1:4] gnt;
endproperty

assert_req_gnt_latency: assert property (p_req_to_gnt_latency)
  else $error("Protocol Violation: Grant not asserted within 4 cycles of Request.");

This assertion monitors the design on every single clock cycle. If req goes high while gnt is low, the assertion engine spawns an active thread checking that gnt appears between 1 and 4 cycles later. If the RTL fails to assert grant, or drops request illegally, the simulator flags the exact simulation time step and signal hierarchy immediately. In a formal property checking tool such as Cadence JasperGold, Siemens Questa Formal, or SymbiYosys, this property is not just tested over randomized seeds; the model checker mathematically proves whether an input trajectory exists that can violate the assertion.

Automating Properties from Register and Interface Specs

Writing production-grade SVA is notoriously tedious. Verification engineers must master complex temporal operators like consecutive repetition ([*n]), non-consecutive repetition ([=n]), goto repetition ([->n]), and sequence match operators (intersect, within, throughout). Because of this steep learning curve, small design teams often skip SVA entirely, relying on basic directed tests and leaving interface edge cases to chance.

Recent academic and industrial tooling demonstrates that structured specifications (such as register specifications, AXI bus interface definitions, and packet framing docs) provide the exact constraint boundaries that automated engines need to synthesize correct SVA.

Consider a memory-mapped control status register (CSR) block governing an encrypted DMA engine. The specification documents several strict hardware invariants:

• Register STATUS_BUSY (bit 0) must rise exactly one cycle after CTRL_START (bit 0) is written with 1'b1.
• Writing to CONFIG_KEY while STATUS_BUSY is high must generate an error response (pslverr = 1'b1) on the APB interface and leave the internal key shadow registers unmodified.
• An interrupt irq_done must pulse high for exactly one clock cycle when the DMA transfer completes, accompanied by STATUS_DONE (bit 1) latching high until explicitly cleared by a write-one-to-clear (W1C) transaction.

An automated spec-to-SVA pipeline reads these rules directly from the register map and interface contracts, generating a clean SVA checker module:

module dma_csr_sva_checker (
  input logic        clk,
  input logic        rst_n,
  input logic        apb_psel,
  input logic        apb_penable,
  input logic        apb_pwrite,
  input logic [31:0] apb_paddr,
  input logic [31:0] apb_pwdata,
  input logic        apb_pslverr,
  input logic        status_busy,
  input logic        irq_done
);

  // Invariant 1: Status busy follows start write
  property p_start_sets_busy;
    @(posedge clk) disable iff (!rst_n)
    (apb_psel && apb_penable && apb_pwrite && (apb_paddr == 32'h00) && apb_pwdata[0]) 
    |=> status_busy;
  endproperty
  a_start_sets_busy: assert property (p_start_sets_busy);

  // Invariant 2: Write to key while busy must trigger APB error response
  property p_key_write_during_busy_err;
    @(posedge clk) disable iff (!rst_n)
    (apb_psel && apb_penable && apb_pwrite && (apb_paddr >= 32'h10 && apb_paddr <= 32'h2C) && status_busy)
    |-> apb_pslverr;
  endproperty
  a_key_busy_err: assert property (p_key_write_during_busy_err);

  // Invariant 3: IRQ Done must be a single-cycle pulse
  property p_irq_pulse_width;
    @(posedge clk) disable iff (!rst_n)
    irq_done |=> !irq_done;
  endproperty
  a_irq_pulse: assert property (p_irq_pulse_width);

  // Coverage: Ensure key writes during idle are exercised
  cover_key_write_idle: cover property (
    @(posedge clk) disable iff (!rst_n)
    apb_psel && apb_penable && apb_pwrite && (apb_paddr == 32'h10) && !status_busy
  );

endmodule

Notice the architectural advantage of this module. It requires zero modifications to the designer's RTL. Using the SystemVerilog bind construct, the verification suite instantiates this property checker directly inside the target DUT at elaboration:

bind dma_top dma_csr_sva_checker u_dma_sva (
  .clk         (clk),
  .rst_n       (rst_n),
  .apb_psel    (psel),
  .apb_penable (penable),
  .apb_pwrite  (pwrite),
  .apb_paddr   (paddr),
  .apb_pwdata  (pwdata),
  .apb_pslverr (pslverr),
  .status_busy (csr_regs.status_busy),
  .irq_done    (interrupt_done)
);

If the RTL team refactors the DMA engine from a monolithic state machine to a pipelined datapath, the assertions remain untouched. If an automated code generator refactors internal wire names, the interface contract still catches protocol breaks on cycle one.

Verification Receipts: Prompt-RTL vs Spec-Driven SVA

To evaluate the difference between unstructured prompt-to-RTL generation and spec-driven assertion automation, we evaluate a representative front-end block: a multi-channel AXI4-Stream packet router with priority arbitration, credit-based backpressure, and runtime packet drop capabilities.

The benchmark compares three approaches:

1. Unstructured Prompt-to-RTL: Generating the Verilog implementation and a standard testbench directly from natural language specifications.
2. Manual SVA + Hand-Coded RTL: Standard senior engineering workflow using hand-coded Verilog and manually written assertions.
3. Spec-Driven SVA Pipeline: Automated property extraction from interface definitions bound to the RTL, audited through mutation injection.

The metrics below represent an illustrative composite based on published formal verification methodologies (LAAG-RV, Princeton DAC benchmarks, and Cadence Jasper formal test suites across typical bus fabric IP).

In the prompt-to-RTL flow, the generated code compiled quickly but hid nine functional bugs, including two critical bus deadlocks where ready-valid handshakes froze under simultaneous buffer exhaustion. Because the generated procedural testbench did not model concurrent backpressure cycles, the bugs escaped functional simulation entirely.

In contrast, the spec-driven SVA flow generated properties for every AXI4-Stream rule before the testbench even ran. When fed into a formal model checker, the formal solver found counter-example traces for the deadlocks within 300 seconds, producing an exact, cycle-accurate VCD waveform showing the bug's origin.

Auditing Assertion Quality with Mutation Testing

Automating assertions introduces a new question: how do you know the generated assertions are actually testing the design, rather than writing vacuous tautologies?

A vacuous assertion is one that passes trivially because its precondition is never met. For example:

property p_flawed_vacuous;
  @(posedge clk) (req && gnt && 1'b0) |-> ##1 ack;
endproperty

Because 1'b0 is never true, the implication operator |-> evaluates to true on every cycle. The simulator reports that the property passed, while zero verification occurred.

To safeguard against vacuity and incomplete property sets, verification pipelines must use mutation testing. The workflow automatically injects synthetic faults into the target RTL:

• Inverting conditional branches (if (state == IDLE) becomes if (state != IDLE))
• Stuck-at faults on control signals (forcing tready = 1'b0 or tready = 1'b1)
• Off-by-one counter adjustments (changing <= to < on pointer comparison logic)
• Masking handshake signals during active transfers

Each mutated RTL variant is executed against the generated SVA suite. If every assertion continues to pass when a bug is present, the mutation survives, and the test suite has failed. An automated property pipeline only passes verification sign-off when its mutation kill rate exceeds 95 percent.

[Architectural Spec / Register Map]
               │
               ▼
   [Spec-to-SVA Generator]
               │
               ├──► [SVA Properties & Coverpoints] ──┐
               │                                     │
               ▼                                     ▼
       [Mutation Engine]                     [Formal Engine / Simulator]
               │                                     │
      (Injects RTL Faults)                           │
               │                                     │
               ▼                                     ▼
       [Mutated RTL DUT] ────────────────────► [Proof Check / Kill Audit]
                                                     │
                                                     ├──► All Mutants Killed (Sign-off)
                                                     └──► Surviving Mutant (Refine SVA)

Five Rules for Implementing Spec-Driven SVA Today

Engineering leads looking to reduce verification turnaround should adopt these practical constraints immediately:

1. Never prompt for RTL and checkers in the same session. Decouple your verification intent from implementation details. The team or agent writing the SVA must work strictly from interface and register specs, not from the Verilog source code.
2. Use the bind construct exclusively. Do not pollute production RTL source files with verification properties. Keeping assertions in standalone files bound by module type ensures your verification infrastructure can be audited independently.
3. Distinguish between assert, assume, and cover. Use assert to verify internal invariants and outputs. Use assume on inputs to bound formal state spaces (for example, assuming a reset remains asserted for at least three clock cycles). Use cover to prove that sequences of interest are reachable during simulation.
4. Run formal property verification before starting UVM simulations. A formal model checker running lightweight SVA catches handshake violations in seconds, eliminating days of debugging noisy randomized testbench logs.
5. Audit assertions with mutation testing. Never trust a test suite with 100 percent pass rates until you have verified that intentional bit-flips in the RTL reliably trigger assertion failures.

What this means for Silicode

At Silicode, we believe generating unverified Verilog is a solved, low-value problem. Real leverage comes from shipping verified, silicon-ready RTL backed by formal proof artifacts, automated SystemVerilog assertions, and verifiable testbenches. Silicode (silicode.ai) builds specification-driven pipelines that extract rigorous SVA properties and functional coverage directly from system architectures, ensuring small silicon teams tape out with mathematical confidence rather than hopeful prompts.

The Engineering Reality

Silicon does not forgive statistical hallucinations. In software, a runtime error caught by a customer can be patched with an over-the-air deployment in twenty minutes. In silicon, an undetected deadlock in an on-chip crossbar means a six-figure mask cost, a four-month fab turnaround, and a blown launch window.

Stop asking generative tools to write clever Verilog state machines. Start using automated tooling to extract strict, declarative properties from your hardware specifications. Let the compiler and the formal verification engine prove the logic before your RTL ever touches a synthesis tool.

Sources

• Cadence Verification Community on Large Language Models in Verification: https://community.cadence.com/cadence_blogs_8/b/fv/posts/why-llms-are-the-best-thing-to-happen-to-chip-design
• LAAG-RV: LLM Assisted Assertion Generation for RTL Design Verification: https://arxiv.org/html/2409.15281v1
• Princeton Parallel Group on Formal Verification of RTL Interactions: https://parallel.princeton.edu/papers/dac21_marcelo.pdf
• Semiconductor Engineering on LLM-Assisted Generation of Formal Verification Testbenches: https://semiengineering.com/llm-assisted-generation-of-formal-verification-testbenches-rtl-to-sva-princeton/
• Doulos SystemVerilog Assertions Technical Resource: https://www.doulos.com/knowhow/systemverilog/systemverilog-tutorials/systemverilog-assertions-tutorial/
• ChipVerify SystemVerilog Assertions Reference: https://chipverify.com/systemverilog/systemverilog-assertions