Posts

Showing posts from April, 2026

Formal verification isn’t scary — you’re just using it wrong

  DESIGN VERIFICATION   ·   ARTICLE 05 OF 06 Formal verification isn’t scary — you’re just using it wrong Most teams treat formal like a fire extinguisher — only when there’s a fire, and usually too late. Here’s how to bake it into your flow from day one.   Formal verification has a reputation problem. Among DV engineers who haven’t used it, formal is the thing that requires a PhD, takes weeks to set up, and either proves your design is correct (unlikely) or times out after 24 hours (common). Among engineers who have used it badly — usually by throwing a formal tool at a large, unconstrained design and waiting for magic — the reputation is similar: powerful in theory, impractical in practice. Both characterizations are wrong in the same way. They describe formal applied incorrectly, to the wrong problems, without the setup work that makes it useful. Formal verification, used well, is one of the few techniques in the DV toolkit that can give you a math...

How I debug a failing regression at 2am: my actual process

  DESIGN VERIFICATION     ARTICLE 04 OF 06 How I debug a failing regression at 2am: my actual process The test name is tc_random_stress_42891. The error is ‘X propagation on bus_data[7]’. The deadline is tomorrow. Here’s what I actually do.   It’s past midnight. The regression that was supposed to be clean isn’t. You have a test name, a seed, a cryptic error message, and a log file that is, conservatively, the length of a short novel. The tape-out review is in nine hours. This is the part of verification nobody talks about in conference papers. The methodology slides show clean flows: stimulus, checking, coverage closure. They don’t show the 2am session where you’re staring at a waveform trying to figure out why a 32-bit bus decided to go X on bit 7 and only bit 7. What follows is my actual process. Not the idealized version. The one I use when I’m tired, under pressure, and the failure is not obvious. Step 0:  Resist the waveform Th...