Blog
Notes from
the workbench.
On verification, provenance, and the proof behind every IP we ship. Specific, technical, occasional.
- 2026.07.06 verification
Free-form drift and its cure: what a renamed interrupt port taught us
A contract said irq_o_irq. The RTL implemented irq_o. The formal harness inherited the contract's name, wired a dangling wire to the DUT, and passed - vacuously. How generated verification catches drift, and where it does not.
Read → - 2026.07.06 verification
The evaluator's checklist, explained
Five questions that separate a real verification claim from a rubber stamp, each one mapped to a file you can actually open in a proof bundle.
Read → - 2026.07.04 verification
The bug formal verification never saw: anatomy of a composition escape
A crossbar arbiter was formally proven clean. The crossbar built from it still shipped a protocol bug into simulation. What the exclusion list was hiding, and the property that found it.
Read → - 2026.06.19 verification
How to split an AXI burst at a 4 KB boundary (and prove you did it right)
A graduate-level walkthrough of one small but treacherous AXI building block: the burst splitter. The naive version passes every simulation and quietly runs at one-sixteenth of the throughput you designed for. We show the failure, explain exactly why it happens, build the correct version line by line, weigh two architectures, and prove the result with formal - including a corruption bug no simulation would ever find.
Read → - 2026.06.14 verification
What a formal "PASS" has to earn
Vacuous proofs, beat-counting that never checks the data, and assertions too weak to fail. How we structure formal verification so a green result means something - and how we grade the grader with mutation testing.
Read → - 2026.06.11 provenance
Lineage, or it didn't happen
Every artifact in a proof bundle traces to the input that produced it. What that chain looks like, and why integrators should demand one.
Read → - 2026.06.10 verification
A passing testbench proves nothing - until it can fail
Inside the Regex Accelerator UVM campaign: 66 tests, a hard protocol gate, three suspected RTL bugs that were not, and why the zero matters.
Read → - 2026.06.08 fabric
Anatomy of a Fabric run
What actually happens between a product brief and a 39-block verified IP repository - stage by stage, gate by gate.
Read → - 2026.06.02 fpga
Patterns are data, not gates
Why the Regex Accelerator keeps its rules in runtime-programmable tables instead of compiling them into logic - and what that trade actually costs.
Read → - 2026.05.12 verification
Verification is the product
Generated RTL is cheap. The evidence that it is correct is what you are actually buying, and what we actually sell.
Read → - 2026.02.18 benchmarks
A benchmark without conditions is a rumor
Why every number we publish carries its operating conditions, and why standalone performance claims are worse than no claim at all.
Read →