What 320 Lanes Taught Us About 4
When you can't fit what you want, remove the thing that seems like it's helping.
Blog¶
The Proof That Caught a Wire
When native_decide returns false, the bug is real.
Intervals Collapse to Points
What happens to formal verification when the hardware is deterministic.
The Snow That Wasn't Bandwidth
When the obvious diagnosis is wrong, the real bug is always simpler.
120x in an Afternoon
Three multiplicative improvements that each looked trivial on their own.
Neither Theory Alone
An SMT solver with one theory is a SAT solver with opinions. Add a second theory and you need a protocol for disagreement.
One Oracle, Four Products
A SAT solver answers one question: is this set of clauses satisfiable? Four crates — the solver itself, a bounded model checker, an SMT solver, and a property-directed reachability engine — are built on that question, each posing it differently.
The Spec That Ate Its Registers
How a 62-register diagnostic braindump fed itself to an architecture and came out as 9 peripherals.
Debugging by Flashlight
When your diagnostic output shares a data path with the thing that's broken, you're debugging in the dark.
Zero New Opcodes
The entire warp scheduler fits in CSR space — no new decode logic, no new pipeline paths, no new encoding pressure.