[LLHD] Allow verif ops in comb canonicalization

[towoe]

Hello again :)

I am not so confident about this commit, so I would appreciate some feedback if there is a problem which this change would introduce in situations I am not aware of.

The intention here is to allow SV assert input which is not causing llhd operations to remain in the IR.
So to be able to work with only core dialects when using circt-verilog.

Operation like verif.assert are not memory effect free. This prevents the llhd.combinational operation from being inlined. With this change the canonicalization is ignoring the memory effect of AssertLikeOps and the ops are moved.
The question is probably, what is the reason why no memory effect ops are allowed?

Thanks!

[fabianschuiki]

I think this makes sense! The reason llhd.combinational is so conservative about inlining is that the semantics of having side-effecting ops like $display in the op are a bit strange: Since the combinational op gets executed whenever any of the SSA values it uses change, you can cook up a weird process that prints something whenever a signal changes:

hw.module @Foo(in %a: i42) {
  llhd.combinational {
    comb.add %a, %a
    display "Hello"
  }
}

Whenever %a changes, this prints "Hello". However, inlining this into the module would change the semantics, which is why we disallow it:

hw.module @Foo(in %a: i42) {
  comb.add %a, %a
  display "Hello"
}

In this case, when %a changes only the add gets recomputed, but the display does not have %a as an operand so does not gets executed. Inlining changes semantics.

We could argue that an assert can be outline even though it has side effects, since it has the condition it checks as an operand so inlining it would only cause it to be executed fewer times (not executed when any of the operands of sibling ops change), but it would still execute at least whenever the condition changes, which is the only thing that triggers the assert.

[fabianschuiki]

You can combine the isas into one 🙂 (probably needs reformatting):

Suggested change

	if (isa<circt::verif::AssertOp>(inner) ||
	isa<circt::verif::AssumeOp>(inner) ||
	isa<circt::verif::CoverOp>(inner))
	if (isa<circt::verif::AssertOp, circt::verif::AssumeOp, circt::verif::CoverOp>(inner))

[towoe]

Thanks, seems like I forgot this from the last time :)

[towoe]

Thank you so much @fabianschuiki for the explanation, much appreciated!
I added a short comment for the exception, hopefully correctly covering the reason you gave.