Equivalence check failure due to non-unique resizer nets

[povik]

Describe the bug

EQY can fail to prove equivalence if the resizer reuses the same net name. Net names are generated by the code below,

string Resizer::makeUniqueNetName()
{
  string node_name;
  Instance* top_inst = network_->topInstance();
  do {
    // sta::stringPrint can lead to string overflow and fatal
    node_name = fmt::format("net{}", unique_net_index_++);
  } while (network_->findNet(top_inst, node_name.c_str()));
  return node_name;
}

but due to unique_net_index_ being reset each time the openroad process is restarted, the same name can be used twice.

The exact sequence of events observed is:

• repair_design -buffer_gain inserts net28 driven by a buffer at floorplan time
• repair_timing at cts time removes the buffer from above, applies Net::mergeNet to net28, and picks net28 for the name of an unrelated net
• EQY is run, expects net28 before and after is functionally equivalent, fails to prove equivalence of the design

Expected Behavior

Resizer nets are assured unique over a flow spanning multiple openroad processes. The counter for net naming could be saved as part of the database

Environment

commit d20db5d

To Reproduce

No reproducer, sorry!

Relevant log output

Screenshots

No response

Additional Context

No response

[povik]

@andyfox-rushc left this comment on makeUniqueNetName

//
// Todo update this to apply over whole design
// There is  a latent bug here. Note that we could
// be inserting a new net somewhere deep in the hierarchy
// which might, possibly, have a net called (say) net10 it in
// which would clash with net10 in the top level. The fix
// is to have another makeUniqueNetName which takes in a scope
// prefix.
//

Maybe we can fix this bug too, but given that we need to avoid conflict with a user net named netN, hierarchy shenanigans might be unavoidable. I don't understand the hierarchy API enough to be sure.

[maliberty]

Does eqy assume that if the nets have the same name they must match?

[povik]

Yes

[maliberty]

That doesn't seem like a good idea. For sequentials it makes some sense as you need some anchor points. Beyond that you should be proving equivalence rather than relying on names.

[povik]

It depends on how we configure it, but it's the default assumption. The new equivalence checker from YosysHQ might be able to recover from some names not matching, but that's far out from being available.

FWIW I think the principle of not reusing the same name for non-matching nets is a powerful principle and one that's been helpful in Yosys development, and we try e.g. to make Yosys rename a net if it changes the net's function as a result of an optimization. If you don't think the same is desirable for OR we can close the ticket.

[povik]

The LEC failures should be fully addressed by The-OpenROAD-Project/OpenROAD-flow-scripts#2693

[maliberty]

In a single run OR would do the same. Does yosys have this property across runs?

I think it is nice for developers to avoid reusing names for traceability but it shouldn't be a requirement for LEC. I am ok with adding it to the db for nets & insts as it won't take much space.

[povik]

In a single run OR would do the same. Does yosys have this property across runs?

Yes, if you work on the same design over multiple runs the counter is saved as part of the .il file (it's the autoidx line at the top)