Five Defects, Found From the RTL

One manifest, one command: five design defects in an FFT accelerator, each backed by a replayed counterexample or a proof. After the fixes, every property that failed is proved, and the property set catches each defect when it is put back.

October 29, 2026 • By Shivaram Mysore

A testbench checks the scenarios someone thought to write. But an RTL defect can depend on a sequence of events that never appears in a directed test: a configuration write during an active run, or a read and a write competing for the same SRAM address in one cycle.

Formal property checking approaches the problem differently. You state an invariant the design must maintain, and the prover searches for a violation across every input sequence the design accepts under the assumptions you state. A proof establishes the property within that model. A counterexample gives you a cycle-by-cycle trace showing how the rule fails.

We pointed vyges formal at the FFT accelerator in our Edge Sensor SoC. The campaign exposed five design defects. We replayed the counterexamples in simulation, fixed the RTL, and re-ran the properties against the corrected design. Mutation testing then checked whether the properties would catch selected versions of those defects if they returned.

How a campaign runs

vyges formal runs the whole check from a single manifest:

  manifest.toml ──► bind monitors ─► synthesize ─► lint ─► prove ─► replay ─► mutate ─► report
                    (your Verilog)                         every     every     every
                                                           claim     counter-  mutant
                                                                     example

• Monitors are plain Verilog. Each one is spliced into the module it watches and reads that module's signals by name. A monitor usually holds several properties and covers: this campaign's 24 properties and 8 covers live in four monitors, one each for the engine, the memory interface, the control block and the bus adapter.
• Proofs are unbounded. The prover uses property-directed reachability (PDR), which ends either with an inductive invariant — the property holds in every state reachable from reset, under the stated assumptions — or with a counterexample. A check that does neither within its time limit is reported as undecided, never as a pass. A result that holds only up to a depth is reported as bounded.
• Every counterexample is replayed in Verilator from the same reset state before it is reported, so a failure is a waveform you can open rather than a claim you have to trust.
• Covers keep the assumptions honest. Each cover is a behaviour that must stay reachable — a run completes, rescaling becomes active. A cover the assumptions accidentally rule out would make every proof vacuous, so covers are proved reachable alongside the properties.
• Mutants measure the property set. The engine plants specific defects in the RTL, re-proves, and reports which properties catch each one.
• The report names the RTL commit, the file hashes, every assumption and the tool versions. A finding you expected is recorded as a finding, never as a pass. The exit status is the verdict — 0 when every result is as expected, 2 when anything is not — so it drops straight into CI.

The first campaign: the FFT in the Edge Sensor SoC

We ran it on the FFT accelerator as it is integrated in the Edge Sensor SoC — a 1024-point build with 16-bit data and twiddles behind the SoC's TL-UL bus, covering reset behaviour, completion, memory addressing, scaling, bus protocol and interrupts.

Replay shows that a counterexample is real behaviour of the RTL. Whether that behaviour is a defect is a question for the specification, so each one was reviewed against the IP's intended register and engine behaviour. The nine failing properties and the unreachable cover trace back to five design defects:

The error path is the clearest case for formal. No simulation can show that a state is unreachable — it can only fail to reach it. The prover shows it for every input sequence, and the circular condition explains why.

These defects are exposed by control, state, addressing and protocol properties. The campaign did not need a reference FFT output for any input vector; SRAM read data is left unconstrained, and the prover reasons about the RTL under the assumptions recorded in the manifest.

From counterexample to fix

A counterexample is a ready-made directed test: short, concrete and already replayed. Each one became a test and an RTL fix in the FFT IP repository. The fixes latch the configuration at launch and check the length, so an illegal length now reports ERROR. They give the engine one memory access per cycle in a fixed butterfly sequence, clear in-flight writes on abort, count scaling per stage, and make INT_STATUS write-1-to-clear so it holds until software clears it. A bit-exact golden-model regression now runs on both the RTL and the synthesized netlist.

We then ran a second campaign on the fixed IP itself — the engine, register block and interrupt controller behind the IP's own APB port, with the SoC's SRAM banks modelled beside it:

The property set changed with the design, so the counts differ. Seven properties checked the SoC's TL-UL-to-APB bridge, which is not part of the IP; in the IP campaign the APB port is driven by the environment, so its protocol became an assumption rather than a property. Four variants that qualified a rule with an extra assumption — three excluding aborts, one assuming well-behaved software — are no longer needed, because the rule now holds without it. In their place, six new properties pin the fixed behaviour: the configuration is latched, DONE follows the reorder pass, data writes happen only during a run and never after an abort, the interrupt is set only when enabled, and the done status holds. Every rule that failed on the SoC commit is carried into the second campaign, and every one is now proved — the completion and addressing rules with no software assumptions at all, where the first campaign needed them.

The mutants show the properties guard the fixes. Four of the fourteen put one of the found defects back into the fixed RTL, one at a time: re-sampling the configuration, counting butterflies instead of stages, a self-clearing interrupt bit, and a one-cycle done status. Each is caught, by the property written for that rule and in some cases by several others. This does not mean the property set catches every possible defect. It measures how well the selected properties detect the selected injected defects — here, specifically, the ones that have already happened once.

Run it yourself

The whole campaign is public in fast-fourier-transform-ip-formal: the manifests, the monitors, both reports and every counterexample trace. Each report records the RTL commit, the hash of every source file, and the versions of the campaign engine, the prover and Yosys it was produced with; the runs used Yosys 0.65 and Verilator 5.040. vyges formal and its prover ship with the physical engines, version 0.1.49 or later:

curl --proto '=https' --tlsv1.2 -LsSf https://github.com/vyges-tools/cli/releases/latest/download/vyges-installer.sh | sh
# or: brew install vyges/tap/vyges
vyges install physical

With Yosys and Verilator on PATH, and PDK_ROOT pointing at a sky130 install (the manifest reads the sky130_fd_sc_hd typical-corner Liberty from it; --liberty FILE overrides it):

git clone https://github.com/vyges/vyges-edge-sensor-soc
git -C vyges-edge-sensor-soc checkout df18c6d4abc2c5731efadc95d43d08132cd4ead0
git clone https://github.com/vyges-ip-tests/fast-fourier-transform-ip-formal
cd fast-fourier-transform-ip-formal

vyges formal run manifest.toml --out formal-out       # prove, replay, mutate, report
vyges formal replay manifest.toml c6_int_status_held --out formal-out \
    --show u_fft_top.fft_control_inst.fft_done_pending  # open one counterexample

The fixed-IP campaign sits in fixed-ip/; it reads the FFT IP cloned beside it, at the commit its report records. In the first campaign, most claims hold under assumptions the manifest states: software does not re-raise START during a run, the programmed length is legal, and — for the variants that say so — a run is not aborted. In the second, the proved properties need no software assumptions; one relies on the APB master following the protocol. Each report lists the assumptions next to every result, so a reader always knows exactly what was proved.

Then write a manifest for your own block. Start with the rules your specification already states in words — this bit holds until cleared, every write lands in the buffer — and let the prover look for the sequence your tests did not think of.

Tell us what to build next

vyges formal is actively developed, and what it learns next is driven by the designs people bring to it. If your block needs a property style, a prover setting or a report format we do not have yet, ask for it from the command line:

vyges --feature-request     # request a feature
vyges --bug-report          # report a problem

Both open the issue form in our public community tracker in your browser, and print the link when there is no browser to open. Every engine takes the same two flags, so the way to ask is the same wherever you are in the flow. Tell us the engine, the command you ran and what you expected to see.

Try formal property checking: the FFT campaign · install the CLI, then vyges install physical · vyges formal and the other Loom engines