Nested `if` conditions that share combinational groups

[polybeandip]

This issue is a summary of this slack thread.

Suppose I made the following combinational group:

comb group check {
    lt_1.left = reg_1.out;
    lt_1.right = reg_2.out;

    lt_2.left = reg_3.out;
    lt_2.right = reg_4.out;

    and.left = lt_1.out
    and.right = lt_2.out
}

Then, could I do something like this in my control?

if lt_1.out with check {
    if and.out with check {...}
}

More concretely, here's a small program that tries to do this:

import "primitives/core.futil";
import "primitives/memories/comb.futil";

component main(@go go: 1) -> (@done done: 1) {
  cells {
    @external mem = comb_mem_d1(32, 1, 1);
    lt_1 = std_lt(32);
    lt_2 = std_lt(32);
    conj = std_and(1);
  }

  wires {
    comb group check {
        lt_1.left = 32'd10;
        lt_1.right = 32'd11;

        lt_2.left = 32'd15;
        lt_2.right = 32'd16;

        conj.left = lt_1.out;
        conj.right = lt_2.out;
    }

    group write {
      mem.addr0 = 1'd0;
      mem.write_en = 1'd1;
      mem.write_data = 32'd500;
      write[done] = mem.done;
    }
  }

  control {
    if lt_1.out with check {
      if conj.out with check {write;}
    }
  }
}

If we ran this, we'd be met with the error

Assignments from 'check' are actived here

from Calyx's well-formed pass.

This might be expected since, as per the docs, our code is maybe in violation of well-formedness:

Well-formedness: The combinational group is considered to be running during the entire execution of the control program and therefore should not have conflicting assignments with either true_c or false_c.

Perhaps this suggests that tweaking our control to say

if lt_1.out with check {
  if conj.out {write;}
}

(deleting with check from the inner if) should make our program work since well-formedness says the combinational group is running through the entire execution of the control program. However, if we ran this modified program, we'd see the error

If statement has no comb group and its condition port conj.out is unstable

Is there a good way to do this kind of construction in Calyx?

[sampsyo]

Thanks for the detailed writeup! I'm afraid that a near-term solution is not clear to me right now (except that the stability heck in well-formedness may yet again be too eager), but I think it's useful to talk over what's going wrong here and why this might indicate a limitation in the IL.

First, maybe this is obvious, but the problem with the original code is that it appears to have two simultaneous activations of the check comb group. From the Calyx compiler's perspective, this is indistinguishable from simultaneous activations of two different groups that both happen to separately assign to lt_1.left, which we can all agree would be a problem. So it rejects the program on these grounds.

One fairly narrow decision we could make here is that two nested withs of the same comb group should be considered the same as one big activation of the comb group. So there could be special-case reasoning that says that it's OK to do with check twice in nested statements, even when it would not be legal to do with check1 and with check2 where these are identical copies of the same list of assignments. This actually feels a little dubious to me, despite an initial attraction… it would complicate the compiler's ability to decide when to activate the check group. Even though the wellformedness rules say that it might be active for the whole execution, in practice the compiler wants to activate it only at specific points. And joining multiple such points with an "or" might complicate the compiler's life? I'm not entirely sure, but it doesn't seem quite as simple as it might on first glance.

Next, I'll bring in everyone's favorite bogeyman: generalized with. There is a world in which we allow syntax like this:

with check {
  if lt_1.out {
    if conj.out {
      ...
    }
  }
}

That is, if you want to reuse the same comb group in multiple constructs, no problem: just wrap those two constructs in a with scope to activate it for as long as you need. This at least makes the sharing explicit. IMO this seems to express the intent pretty cleanly and has a straightforward compilation story, i.e., we delimit exactly which FSM states where we want the comb group to be active.

Generalized with is a somewhat controversial idea, but this might add a tiny bit of weight on the side of the positive case for it?

[anshumanmohan]

Shall we close this issue as a wontfix?