fix: name every write_blif_body node after its own wire
write_blif_body named a root after the primary output it drives and only
fell back to a buffer when the root was already MARKED. That is correct for
a single diagram, but breaks as soon as two outputs share a node.
The first output emits its cone and names the root after itself, so no wire
named <prefix><index> is ever defined. A later output whose diagram reaches
that same node finds it marked, stops the traversal there and refers to it
as <prefix><index> - a net that does not exist. Yosys reads the result as an
undriven wire and the netlist is silently wrong; the miter then fails with a
counterexample rather than an error, which is what made it hard to place.
Emit every node under its own wire name instead and buffer the output onto
it unconditionally. The buffers cost nothing: the opt pass that follows the
conversion in every .ys template removes them. Constant outputs keep their
existing special case and now short-circuit with a continue.
Verified on the ISCAS85 suite through yosys sat -tempinduct -verify
against the golden netlist: 10 of 11 circuits prove equivalent at n = 8,
where c432 and c880 previously produced counterexamples. The unpartitioned
path is unchanged - c17 at n = 0 still comes out at 13 gates and passes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014JTKS4uaDDZejKn7pE8vjc