[HWToBTOR2] Deduce resets from (Fir)RegOps

[TaoBi22]

Currently, the HWToBTOR2 lowering assumes all regs will only be reset by one hw.module argument called %reset, and produces incorrect BTOR2 if this isn't the case. This PR changes the pass so that register constructs in the output are instead reset by the value corresponding to the reset operand (if present) of the corresponding MLIR op.

[TaoBi22]

@dobios doesn't look like I can request a review from you since you're not in the LLVM org but if you could make sure this looks ok it would be much appreciated!

[uenoku]

I think getOpLID(Value value) already covers block argument case?

Suggested change

	size_t resetLID = noLID;
	if (BlockArgument barg = dyn_cast<BlockArgument>(reset)) {
	// Extract the block argument index and use that to get the line number
	size_t argIdx = barg.getArgNumber();
	// Check that the extracted argument is in range before using it
	resetLID = inputLIDs[argIdx];
	} else {
	resetLID = getOpLID(reset);
	}
	size_t resetLID = getOpLID(reset);

[TaoBi22]

It does, but here it needs to be explicitly checked - AFAICT, this is because of some undesired behaviour in the pass currently where the SetOpLID call above inserts nullptr into the LID map if the register input is a blockarg, and getOpLID gets confused. This is pretty counterintuitive and probably worth fixing, so once this lands I'll probably do another PR to neaten this up (by explicitly incrementing the LID instead, and probably adding an assert that nullptr isn't the SetOpLID input) - in the meantime it should work fine with the explicit check.

[dobios]

The issue is more that SetOpLID is never called on block arguments, so getOpLID will return null if called on a block argument, which is why I have the explicit check there. What you're doing here seems to be doing exactly what my check does in getOpLID so I don't think that it's useful (as @uenoku mentioned). I still need to test this out to make sure it works as expected. I really don't know why I didn't just get the reset like this in the first place lol

[TaoBi22]

Very possible I've missed something, but I think setOpLID is called on a blockarg if the reg input is a blockarg in this function? I also thought that getOpLID would work on its own originally and tried that first, but it didn't seem to behave as it should so I added the explicit check - if I just use getOpLID, then:

module {
  hw.module @MultipleResets(in %clock : !seq.clock, in %reset0 : i1, in %reset1 : i1, in %in : i32) {
    %c0_i32 = hw.constant 0 : i32
    %reg0 = seq.compreg  %in, %clock reset %reset0, %c0_i32 : i32  
    %reg1 = seq.compreg  %in, %clock reset %reset1, %c0_i32 : i32  
    %0 = comb.and bin %reset0, %reset1 : i1
    %reg2 = seq.compreg  %in, %clock reset %0, %c0_i32 : i32  
    hw.output
  }
}

from the test added in this PR gets lowered to

1 sort bitvec 1
2 input 1 reset0
3 input 1 reset1
4 sort bitvec 32
5 input 4 in
6 state 4 reg0
7 state 4 reg1
8 state 4 reg2
9 constd 4 0
10 and 1 2 3
11 ite 4 2 9 5
12 next 4 6 11
13 ite 4 11 9 5
14 next 4 7 13
15 ite 4 10 9 5
16 next 4 8 15

which is incorrect, as the line 13 ite 4 11 9 5 takes 11 (the output of the previous reset ite) as the reset signal rather than 3, which is the desired reset signal. I think this is because if next is a blockarg, setOpLID is called on its defining op (nullptr) and so getOpLID finds the 'defining op' of all blockargs in the LID map and so doesn't realise they're blockargs (as getOpLID only checks if it's been given a blockarg once it fails to find the operation in opLIDMap) (but I may well have missed something so please correct me if this doesn't sound like the right explanation!).

[dobios]

Ah damn I see what you mean, it that case it might be worth doing it manually like you did. I'll go over this pass and clean things up a bit to make the behavior a bit more consistent.

[TaoBi22]

That would be great, thanks - I have some free cycles at the moment if I can be of any help with that! Are you happy to approve this PR in the meantime?

[dobios]

Thanks for fixing this! I've been meaning to do it for while but got lost in other work. Looks good to me, I'm not quite sure the explicit block argument check is necessary though given that getOpLID does exactly that.

[dobios]

The issue is more that SetOpLID is never called on block arguments, so getOpLID will return null if called on a block argument, which is why I have the explicit check there. What you're doing here seems to be doing exactly what my check does in getOpLID so I don't think that it's useful (as @uenoku mentioned). I still need to test this out to make sure it works as expected. I really don't know why I didn't just get the reset like this in the first place lol

[dobios]

This should be good enough for now imo, I have a few changes to this pass on my fork which will hopefully clean things up and make this cleaner to fix in the future. Thanks for the fix!