[HW] `hw-flatten-modules` can't find an module that exists

[dobios]

It seems that the hw-flatten-modules pass behaves weirdly when it's in a file that contains verif.formal and hw.module operations.

e.g., I modified integration_test/circt-test/contracts.mlir to make all modules other than @BoothMul private; if I then run circt-opt --lower-contracts --hw-flatten-modules integration_test/circt-test/contracts.mlir, I get the following error:

contracts.mlir:205:16: error: Cannot find module definition 'HalfAdder'
  %s_1, %c_2 = hw.instance "h2" @HalfAdder(a: %p2_1: i1, b: %p3_0: i1) -> (s: i1, co: i1)
               ^
contracts.mlir:205:16: note: see current operation: %21:2 = "hw.instance"(%12, %13) <{argNames = ["a", "b"], instanceName = "h2", moduleName = @HalfAdder, parameters = [], resultNames = ["s", "co"]}> : (i1, i1) -> (i1, i1)

even though @HalfAdder is defined in the same file (in the output of circt-opt) as:

[...]
hw.module private @HalfAdder(in %a: i1, in %b: i1, out s: i1, out co: i1) {
  %0 = comb.xor %a, %b : i1
  %1 = comb.and %a, %b : i1
  hw.output %0, %1 : i1, i1
}
[...]

Any ideas what might be causing this? (I'm assuming @fabianschuiki might be able to figure it out, as I think hw-flatten-modules is originally his code?)

Thanks!

[fabianschuiki]

Oh nice find! Could this be the pass not realizing that there is an instance inside of a contract, and thinking that the target module is unused? The pass should probably use MLIR's SymbolUserMap to find unused modules, which would look into contracts to see if there are any references to the module.