From x!0 to a Waveform

i started this as a fun thing.

i wanted to learn compilers but from a hardware perspective, cause that felt like the part of compilers i would actually enjoy. so i went digging through CIRCT issues looking for something to pick up. no plan beyond that.

and then i did something that mattered way more than i thought at the time.

instead of just picking an issue and disappearing into it, i commented on a couple of them with how i thought i would solve it. partly to be useful, but mostly to check if my own thought process was even pointing in the right direction. cause when you are new to a codebase this big you genuinely cannot tell the difference between “i understand this” and “i have made up a very confident story about this”.

and they came back and said yeah, thats roughly right.

small thing for them. huge thing for me. my self confidence shot up so hard, cause it meant the model in my head was not garbage. and the second i knew the model was not garbage, i could suddenly see how to actually implement the thing.

so now the only problem left was writing the code.

learning the codebase

which is its own problem obviously. CIRCT is big.

i got through it with a mix of claude code and reading code manually (and yes i actually did read it, which i feel like i have to say out loud now, cause “i used an AI tool to understand a codebase” apparently means you skipped the understanding part). the tool was good for orientation. where does this live, what calls this, that kind of thing. saved me a lot of grepping. but the part where you actually get why a pass sits where it sits in the pipeline, that i had to sit down and read for.

once i had the path in my head i implemented it and it worked.

sometimes it worked halfway. and thats where fabian comes in, he was helpful the whole way through and his reviews carried me through a lot of the “this works but i can tell its not right” stage. that kind of review is worth so much more than a green checkmark tbh.

so i kept going. fixed a couple more issues.

one was a mem2reg bug (#9552). the pass was only capturing llhd.prb results across llhd.wait ops, which is fine until its not, cause anything else live across the wait just got dropped. fix was to stop special casing probes and let liveness analysis decide what survives, which is what it was there for anyway.

the other one was bigger, teaching Deseq to handle projected clocks (#9588). if your clock came in through a comb.extract or a hw.struct_extract (a bit pulled out of a bus, a field pulled out of a struct) the pass could not see through the projection and would not recognise the process as a register. so i added a ValueField helper that tracks a value plus which slice of it you mean, and then rewrote most of the analysis to think in those terms instead of raw Value. around 700 lines. first time i restructured someone elses pass instead of just patching it.

why not

somewhere in there gsoc came around and i thought, why not. lets just try.

i only attempted one project. counterexample generation for circt-bmc.

i was pretty comfortable with the sv lowering passes by then, and bmc lowering was new to me. but i already had the structure in my head, i knew how the dialects fit together and how stuff flowed through, so the new part was only the domain and not the codebase. that felt like enough to go on.

so i did some digging, wrote up a plan, and fabian and bea healy both thought it was reasonable. and boom, thats the actual green light. i started on the initial setup while i was still writing the proposal, cause honestly i was gonna do this with or without gsoc.

then it got accepted (surprised me) and it stopped being a side thing and became the whole summer.

the actual problem

here was the entire user experience of circt-bmc when i started:

Assertion can be violated!

thats it. a bounded model checker just proved your design is broken and the only thing it will tell you is that it happened.

and the annoying part is this is not missing information. when the solver comes back sat, z3 is sitting on a full satisfying model. every input, every register, every cycle, the exact sequence that walks your design off a cliff. it knows exactly how to break your circuit. it just refuses to say it in a language you speak:

x!0 -> #b01
x!1 -> #b10
x!2 -> #b00

everything you need is in there and none of it is readable. you have the murder weapon and no names.

the dumb first attempt

obvious move, and the one i made first. if z3 is generating garbage names, generate better ones myself.

so in VerifToSMT, where bmc lowering makes its smt.declare_fun ops, i gave them real prefixes (#9794). free inputs became input_0, uninitialised registers became reg_0. and suddenly --print-solver-output gave you something you could squint at.

this was not the real answer and i knew it while writing it. input_3 beats x!7 the way being lost with a compass beats being lost without one. but it proved a name set at lowering time actually survives all the way into solver output, and that turned out to be the useful bit.

chasing the real names

real names in CIRCT live in dbg.variable ops. thats the debug dialects whole job, carrying user facing names down through lowering so the backend can still tell you what the frontend called things.

problem was timing. by the time bmc ran, the module inputs and registers i cared about had no dbg.variable ops on them. the registers especially got eaten by externalize-registers before anyone thought to label them.

so the fix had to happen earlier, which meant a new pass, materialize-debug-anchors (#10287). it runs before register externalisation and plants dbg.variable ops on module inputs and registers, named and unnamed both, so the names exist before the thing that would have destroyed them gets to run.

then VerifToSMT had to actually read them (#10492) instead of using my made up scheme.

and that mostly worked, except for one really annoying detail.

bmc is a loop. it unrolls your design over k cycles and threads symbolic values from one cycle into the next. the names survived fine inside the lowered circuit body, but the bmc wrapper that made and threaded those values across the loop boundary never reattached them. so the names were correct exactly where you did not need them, and gone everywhere you did. took #10604 to sort out.

at this point the model dump was readable. count -> #b10. you could tell what broke.

you still could not tell when.

names are not a trace

this is the part i underestimated, and its the actual technical heart of the whole thing.

a readable model dump is a flat list of values. a counterexample is not flat. its a value, per signal, per cycle. its a waveform. the whole point of bounded model checking is that the bug is a sequence, the counter was at 1, then 2, then the assertion died. a flat name to value map cannot say that, cause after unrolling, count at cycle 0 and count at cycle 3 are two completely different smt constants that just happen to share a lineage.

so i needed three things that did not exist.

somewhere to put a trace, so a BMCTrace runtime class (#10537). plain c++, storage indexed by cycle and signal. the bit im happiest about is it does not depend on z3 at all. it stores opaque handles and takes z3s api entry points as plain function pointers, so the runtime lib needs neither z3 headers nor a specific z3 shared library at link time. fussy but thats what kept the whole thing jit friendly.

a way to mark which values belong in it, so a new op, verif.bmc.trace (#10747). it says nothing more than “this value, under this name, matters for a counterexample”. a marker, not a mechanism.

a way to get values back out of z3 at runtime, which was the fiddly one (#10876). every verif.bmc.trace on a bit vector lowers to a call into the jit runtime carrying the cycle, the signal name, the bit width, and an opaque handle to the z3 expression. circt-bmc registers that callback with orc jit, and as the compiled solver code runs it records into a thread local BMCTrace. this is also where i learnt to be strict about names, duplicate trace names now give you a real diagnostic pointing back at the original marker, cause silently merging two signals into one trace row is so much worse than just failing.

and then the payoff (#10932). when the check comes back sat, walk everything the runtime recorded, evaluate each handle against the satisfying model, print it.

counterexample for FormalTop:
cycle 0:
  count = 0x2
Assertion can be violated!

months of work for four lines of output. and boom, worth it.

the part i did not expect to be the point

somewhere in the middle of all this i realised i was learning more from the conversations than from the code.

a lot of this project was design discussion. going back and forth with fabian and bea and the rest of the circt folks about where a thing should live, what an op should actually mean, whether a pass belongs before or after another one. and those conversations kept turning things i thought were implementation questions into design questions.

verif.bmc.trace is the good example. my instinct was to make the op do something. the better answer was to make it a marker that means nothing on its own and let the lowering decide what to do with it, cause that keeps the op honest at every level it passes through. i did not get there alone.

and thats the thing i keep thinking about now, how deliberately compiler infra is designed. every “why is this done in such a weird way” i ran into turned out to have a reason, usually some case i had not thought about yet. pass ordering, dialect boundaries, what info is allowed to survive a lowering and what isnt. none of it is accidental.

i came in to write some code and ended up learning how people think about building systems that other people are gonna extend. thats worth more to me than the feature honestly.

feeding it real designs

later on the bottleneck stopped being “can it explain itself” and became “can you even get anything into it”.

circt-bmc wanted mlir. nobody writes mlir. people write systemverilog, and if the tool cannot read systemverilog then the counterexample printer i just spent months on is a demo, not a feature.

so theres a PrepareForBMC pass (#10974) that gets a design into the shape bmc expects, and a branch (not merged yet) that lets circt-bmc take a .sv file directly and run the whole frontend itself.

what im in the middle of right now

the text trace is fine for two signals over three cycles and completely useless for anything real. nobody is debugging a 40 signal, 20 cycle counterexample by reading a column of hex.

hardware people have had the right tool for this for like thirty years and its a waveform viewer. so the current work is spitting counterexamples out as VCD, so what you get back from a failed proof is a file you drop into gtkwave or surfer and just look at.

thats on codex/bmc-vcd-pipeline and mostly works. vcd comes out by default named after the checked module, --vcd-output overrides the path, --print-trace keeps the text output if you want both. not upstream yet.

what is left

• land the systemverilog input path
• land vcd output
• traced values that arent bit vectors (smt arrays mostly, which means memories) still get silently dropped. memories are exactly where the interesting bugs live so thats the obvious next thing
• PrepareForBMC handles the cases i needed. its gonna need to grow

work product

all merged into llvm/circt unless noted.

in flight, not merged: systemverilog input for circt-bmc (bmc-sv-input-pipeline), vcd counterexample output (codex/bmc-vcd-pipeline).

thanks to fabian and bea for the reviews, the design arguments, and for taking some random guy commenting on issues seriously enough to actually answer properly. thats the whole reason any of this happened.