False positive on pin swap

[maliberty]

On the attached test case eqy gives (run eqy_test.run.sh):

EQY 22:43:51 [eqy_test] partition: ERROR: conflicting matches for gold bit _052_: _052_ vs _050_

In the golden netlist:

  OA21x2_ASAP7_75t_R _302_ (
    .A1(_052_),
    .A2(_050_),
    .B(_049_),
    .Y(_119_)
  );

while in the test netlist the A1/A2 pins are swapped:

 OA21x2_ASAP7_75t_R _302_ (.A1(_050_),
    .A2(_052_),
    .B(_049_),
    .Y(_119_));
```
This is logically equivalent for the cell:
```
module OA21x2_ASAP7_75t_R (Y, A1, A2, B);
	output Y;
	input A1, A2, B;

	// Function
	wire int_fwire_0, int_fwire_1;

	and (int_fwire_0, A2, B);
	and (int_fwire_1, A1, B);
	or (Y, int_fwire_1, int_fwire_0);

	
endmodule
```

[bug.zip](https://github.com/user-attachments/files/23780970/bug.zip)

[maliberty]

bug.zip

[oharboe]

@nekronos FYI

[nakengelhardt]

This is another case of "eqy currently requires extensive handholding and knowledge of internals": there's two core assumptions that eqy makes about design structure that aren't true in this case.

• One is that (unless it's told otherwise by a nomatch directive) things that have the same name in the gold and the gate netlist are supposed to be equivalent.
• The other is that if the names match, the two designs have the same module hierarchy (but some levels of hierarchy may have been flattened away).

In this design it's presented with two instances of a user-defined module (OA21x2_ASAP7_75t_R) of the same name (_302_), so it matches up those ports structurally. That port name matching conflicts with the wire name matching, hence the error you see.

However all of the names in question are just the auto-generated _123_ names that write_verilog generates by enumerating unnamed design elements, and there's no reason to expect that they would get named in the same order for two different netlists. We need to hide them from eqy to avoid it matching on them. This can be done with rename -hide w:\_*_ c:\_*_ (changing all these names to private names again, as they were before write_verilog). We also need to make it not structurally match the ports to accommodate the commutative operators, which we can do by running flatten.

After this there's still one unrelated issue remaining that it doesn't know what to do with the empty blackbox modules which have no ports: ERROR: No matched IDs for module DECAPx10_ASAP7_75t_R
I'll have to look further into that, but for now this can be worked around by removing the (at this point unneeded) blackbox definitions with hierarchy -purge_lib.

This is what the final eqy file looks like after these modifications:

[gold]
read_verilog -sv 1_synth.v asap7sc7p5t_AO_RVT_TT_201020.v asap7sc7p5t_INVBUF_RVT_TT_201020.v asap7sc7p5t_OA_RVT_TT_201020.v asap7sc7p5t_SIMPLE_RVT_TT_201020.v dff.v empty.v

[gate]
read_verilog -sv gcd_floorplan.v asap7sc7p5t_AO_RVT_TT_201020.v asap7sc7p5t_INVBUF_RVT_TT_201020.v asap7sc7p5t_OA_RVT_TT_201020.v asap7sc7p5t_SIMPLE_RVT_TT_201020.v dff.v empty.v

[script]
prep -top gcd
memory_map
rename -hide w:\_*_ c:\_*_
flatten
hierarchy -purge_lib

[collect *]

[strategy sby]
use sby
depth 1
engine smtbmc bitwuzla

With that the design passes the check.

[maliberty]

Thanks! We can omit writing the decap cells at all so no worries about those. @oharboe please give it a try.

[maliberty]

Thanks. I tried to find the rename command in the docs but failed. Did I miss something?

In previous discussion there was reference to a [match *] section using gate-nomatch. How does that relate to rename?

[oharboe]

Like so The-OpenROAD-Project/bazel-orfs#420 ?