[HWToBTOR2] Avoid invalid BTOR2 when regs have same name#9916
Conversation
|
Please consider using https://github.com/llvm/circt/blob/main/include/circt/Support/Namespace.h. |
Ah thank you! I thought I'd seen something like this but looked in MLIR rather than CIRCT. I'll update it to use this. |
dobios
left a comment
There was a problem hiding this comment.
Oh nice, I was looking for this exact Namespace thing for the compreg and shiftreg lowerings, it's fine to handle this here, but generally speaking I would prefer to handle this kind of stuff in upstream passes as much as possible to keep this emission pass as easy to maintain as possible
Agreed it would be nice to not run into upstream but since it's valid IR nonetheless I figured support here was probably worthwhile! |
Currently we emit invalid BTOR2 if two regs have the same name attribute, as the
states get assigned the same symbol in BTOR2 and the parser complains (I ran into this using the LowerSeqShiftReg pass, as lowering two shiftregs will producecompreg.ces with the same name). This just works around that by tracking the symbols we've already created and suffixing names that are already in use