Well-formedness of done signals

[rachitnigam]

I've been a little more deeply about what makes the done signal of a group and a component to be well-formed. Here are a few examples of done conditions that don't make sense.

Examples

1. Logical combination of multiple done conditions:

group[done] = reg0.done & reg1.done;

The likely intention of the program is to say that the group is done when both registers reg0 and reg1 have set their done signal high once. However, in reality, this says that the group is done in the cycle when reg0 and reg1 simultaneously set their done signals high.

To encode the intended behavior, we need some state:

r0_done.in = 1'd1;
r0_done.write_en = reg0.done;
r1_done.in = 1'd1;
r1_done.write_en = reg1.done;
group[done] = r0_done.out & r1_done.out; 

2. Combinational done conditions:

Here is a done condition I was recently thinking about:

component incr_by_10(...) -> (...) {
  ...
  sub.left = count.out;
  sub.right = in;
  eq.left = sub.out;
  eq.right = 10;
  done = eq.out;
}

This component says that its done when count - in == 10. However, the eq component is combinational which means that when the component is invoked, we'll have something like:

comp.go = !comp.done;

Which means that the assignment eq.left etc. will have a guard that depends on eq.out creating a combinational loop.

A Well-Formedness Definition

One possible definition for well-formedness is that only signals that have the @done annotation or @stable annotation can be assigned as the right hand side of a done condition and logical combinations thereof. Using this definition, we have:

1. Example is rejected because the out port of a logical & is neither @done nor @stable whereas out signal of registers is @stable which means the logical and is also @stable.
2. Again, eq.out is not @stable nor @done.

I'm not sure if this definition is actually the right one but it's a start.

[sampsyo]

I agree that both of these examples are clearly examples of mistakes based on our current interpretation of done signals.

To think about what might be a good condition to put on the code, I think it would be best to reason about the exact correspondence between the static conditions and the dynamic behavior that constitutes a "correct" use of done. That is, I think we have a notion of what a done signal is supposed to do dynamically—it may not be high on the same cycle as go (any cycle thereafter is OK); and it should go high only after the group has finished the "work" it needs to do. Using this, we can think about whether there are any static conditions that would be (a) necessary or (b) sufficient to enforce these.

I think the @stable assignment criterion is sufficient but not necessary for the first condition. (It seems hard to enforce anything about the second condition because every group has a different notion of what "doneness" means.) It makes me wonder about the precise propagation rules for @stable, however. Would !!0_done.out be considered stable, for instance?

[rachitnigam]

Yeah, this runs into a different but relevant question about what stability of circuit signals means. For the above example, !!0_done.out is also stable because the not operation is combinational and if its input is stable, it will be stable as well.

[sampsyo]

Yeah… just makes me wonder a little bit about what the general rule is, which I don't quite see yet.