[comb] Missing ~(~foo) canonicalization when foo is defined in another region

[rwy7]

We are currently missing a ~(~foo) fold opportunity. The folder for comb.xor exists, but is blocked when an operand is defined in another block than the xor op itself.

See: #6235

I found this while looking at assumptions, which often are disabled when the reset signal is high. To accomplish this, the enable-line for an assumption is often ~reset. For example:

FIRRTL version 4.0.0

circuit Top:
  layer Verification, bind:
    layer Assert, bind:
  public module Top:
    input clock : Clock
    input reset : UInt<1>
    input test : UInt<1>
    node reset2 = asUInt(reset)
    node enable = eq(reset2, UInt<1>(0h0))
    intrinsic(circt_chisel_assert<format = "MYASSERT", label = "MYLABEL">, clock, test, enable)

If we compile this with --add-companion-assume, this becomes:

firrtl.module @Top(in %clock: !firrtl.clock, in %reset: !firrtl.uint<1>, in %test: !firrtl.uint<1>) attributes {convention = #firrtl<convention scalarized>} {
  %enable = firrtl.not %reset {name = "enable"} : (!firrtl.uint<1>) -> !firrtl.uint<1>
  firrtl.assert %clock, %test, %enable, "MYASSERT" : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1>  {eventControl = 0 : i32, isConcurrent = true, name = "MYLABEL"}
  firrtl.assume %clock, %test, %enable, "" : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1>  {eventControl = 0 : i32, guards = ["USE_PROPERTY_AS_CONSTRAINT"], isConcurrent = true, name = "MYLABEL"}
}

When we lower a FIRRTL assumption to SV, we merge the enable and predicate signals to a single formula: !enable | pred. Then our predicate in SV becomes ~(~reset) | test:

hw.module @Top(in %clock : i1, in %reset : i1, in %test : i1) {
  %true = hw.constant true
  %0 = comb.xor bin %reset, %true {sv.namehint = "enable"} : i1
  %1 = comb.or bin %reset, %test : i1
  sv.assert.concurrent posedge %clock, %1 label "assert__MYLABEL" message "MYASSERT"
  sv.ifdef  @USE_PROPERTY_AS_CONSTRAINT {
    %2 = comb.xor bin %0, %true : i1
    %3 = comb.or bin %2, %test : i1
    sv.assume.concurrent posedge %clock, %3 label "assume__MYLABEL"
  }
  hw.output
}

This never gets simplified, so our final output is:

// Generated by CIRCT unknown git version
module Top(
  input clock,
        reset,
        test
);

  assert__MYLABEL:
    assert property (@(posedge clock) reset | test) else $error("MYASSERT");
  `ifdef USE_PROPERTY_AS_CONSTRAINT
    assume__MYLABEL: assume property (@(posedge clock) ~(~reset) | test);
  `endif // USE_PROPERTY_AS_CONSTRAINT
endmodule

If folders in comb could fold across the sv.ifdef region, that would simplify the final verilog to "assume (reset | test)"

[uenoku]

FYI #6523 has the same root cause