Semantics of guarded assignments

[rachitnigam]

Calyx's guarded assignments work by the following logic: if one of the guards is true, forward the corresponding. If no guard is true, no value is forwarded. For example, for the following code:

r.in = a.out ? 32'd1;
r.in = b.out ? 32'd2;

The program should assign 1 to r.in if a.out is high, 2 if b.out is high and "nothing" if neither are true. Both conditions being true is a runtime error. However, the generated Verilog code for this looks like:

r.in = a.out ? 32'd1
     : b.out ? 32'd2
     : '0;

This means that when neither of the two guards are active, then we assign 0 to the port. This is technically fine because our semantics don't provide any guarantee on what value is assigned when no guard is active for the port.

Switching to X Simulation

Verilog provides the 'x value to represent "unknown values" which should not affect the outcome of the design. X values are also useful in detecting problems in the design; for example, at start of simulation, all state is initialized with x to ensure that the design explicitly sets it some initial value before using it. The other possible benefit of x-values is that synthesis toolchains can optimize the design more since it's allowed to use whatever value it needs when it sees an x.

Given how we've defined Calyx's semantics, it seems possible that we can replace the above Verilog with the following:

r.in = a.out ? 32'd1
     : b.out ? 32'd2
     : 'x;

Ideally, if our semantics is correct and our compiler correctly transforms the program correctly, this change would of course be transparent. foreshadowing

Interface Signals

One immediate problem with the aforementioned semantics is that not all signals are created equal. Interface signals, like go and done cannot simply receive an 'x when no driver is active. For example, in the program:

r.write_en = a.out ? 1'd1 : 'x;

The write_en signal of a register is responsible to commit a value into the register. However, in this program, 'x is truly allowed to be any value, including 1. This means that r.write_en can arbitrarily be high in any cycle which is definitely incorrect. To address this, we need to come up with some refinement to the semantics.

Possible options include distinguishing "data signals" from "interface signals" and ensure that the latter always have defined inputs.

Guards

Ports that appear in a guard have a similar problem---if any of them take the value x then the entire guard is an x value which can either be 0 or 1. This means that the guard can arbitrarily take the value 1 and trigger an assignment unexpectedly. #859 documents one case where this is problematic because we cannot check if a unique guarded assignment is active in a cycle.

It's not quite clear what to do with this because a fix requires that guards never evaluate to an 'x value. This is definitely a desirable property but not quite clear what we need to do to enforce it.

[rachitnigam]

One possible solution to the semantic quandary is that things are assigned the default 'x value unless they are specified to be a data port. For example, the in port of a register is marked a data port in the standard library and can therefore be assigned 'x during code generation but write_en is not and therefore gets the default 0.

This safe-by-default semantics is useful but it side steps the question of what the default semantics should be. Should guarded assignments in Calyx be read as "if none of these are active, assign 0" and the 'x is a pure optimization?

[sampsyo]

At a very high level, I agree that deciding on a complete set of rules for dealing with undefinedness are still important—and I think this boils down to roughly the same questions I tried to pose in #922. To summarize those bullet points:

1. Propagation: what happens in x = y when y is undefined?
2. What happens when a guard is undefined?
3. What to do about interface signals? For these, "using undefined is an error" is unsatisfying.

I think it is probably possible to resolve all of these, but it would be great to drive the discussion from the semantics themselves and view the compilation to Verilog 'x as a consequence rather than the inspiration/goal unto itself. A consequence alongside what we can feasibly "sanitize" in the interpreter and optimizations like the one in #1010, which we actually might want to allow!