[Semantics] Undefined values, `'x`, and missing `ref` cells

[EclecticGriffin]

Once again time to discuss undefinedness and its semantic implications. This is sort of a grab bag issue for a couple of things that have come up during some of the recent Cider 2 work. There is motivating code for a lot of this, so the issue might be a little long, but to summarize the top-level questions go something like this:

1. Is the undef value used during convergence equivalent to 'x? If not, what are the semantics of the latter?
2. What happens when trying to read a ref-cell outside an invoke or during an invoke in which it is not supplied?
3. What are the semantics (or lack thereof) for writing an undef/x value to registers/memory or reading an undef/x value in a guard/condition?
4. How do @control annotations fit into our semantic model? It would not be correct to replace undef with 0 in all cases which returns us to question 1.

Example 1 - Missing Ref Cells

Here's a silly piece of example code I wrote while testing ref cells.

component my_add(left: 32, right: 32) -> (out: 32) {
    cells {
        ref result = std_reg(32);
        ref add = std_add(32);
    }
    wires {
        group do_add {
            add.left = left;
            add.right = right;
            result.in = add.out;
            result.write_en = 1'd1;
            do_add[done] = result.done;
        }

        out = result.out;
    }

    control {
        do_add;
    }
}

component main() -> () {
    cells {
        left_reg = std_reg(32);
        right_reg = std_reg(32);
        my_add = my_add();
        result = std_reg(32);
        inner_add = std_add(32);
        inner_result = std_reg(32);
    }

    wires {
        group init_left {
            left_reg.in = 32'd5;
            left_reg.write_en = 1'd1;
            init_left[done] = left_reg.done;
        }

        group init_right {
            right_reg.in = 32'd10;
            right_reg.write_en = 1'd1;
            init_right[done] = right_reg.done;
        }

        group store_result {
            result.in = my_add.out;
            result.write_en = 1'd1;
            store_result[done] = result.done;
        }
    }

    control {
        seq {
            init_left;
            init_right;
            invoke my_add[result=inner_result, add=inner_add](left=left_reg.out, right=right_reg.out)();
            store_result;
        }
    }
}

In the current version of Cider 2 this program will immediately error since my_add uses result.out in a continuous assignment and result, being a ref cell, is only defined during the later invoke and not otherwise. Should this be a hard error? Should the value read from result.out be undef?

This raises the additional question: Should ref cells be allowed in continuous assignments?

Example 2 - Writing undef to registers

the tests/correctness/pipelined-mac.futil program was tripping an undefined write error:

Error: Attempted to write an undefined value to register or memory named "main.mac.data_valid_reg"

This program invokes a mac written in calyx which has the following signature

 component pipelined_mac(
  data_valid: 1,
  a: 32,
  b: 32,
  c: 32
) -> (
  out: 32,
  output_valid: 1
)

and has a the following group

  group write_data_valid {
      data_valid_reg.write_en = 1'd1;
      data_valid_reg.in = data_valid;
      write_data_valid[done] = data_valid_reg.done;
    }

This group is the first thing executed by the control of the mac, so it always runs.

control {
    seq {
      write_data_valid;

The main component invokes mac three times.

seq {
    ...
      invoke mac(data_valid = 1'd1, a = read_a.out, b = read_b.out)();
    ...
          invoke mac(
            data_valid = 1'd1,
            a = read_a.out,
            b = read_b.out,
            c = mac.out
          )();
   ...
      // Pipeline flushing: when idx0 == 10.
      // Perform the final accumulate
      invoke mac(c = mac.out)();
   ...
    }

The first two are well-behaved, but this last one isn't since it never supplies a value to data_valid which causes the write to main.mac.data_valid_reg to be undefined, triggering the error. In this case, it is pretty clear that the component was assuming data_valid was zero when not driven Changing the last invoke to:

      invoke mac(c = mac.out, data_valid = 1'd0)();

resolves the problem and generates the expected results for the test

Example 3 - TCAM

The lpm.futil correctness test for TCAM looks like:

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

component main() -> () {
  cells {
    tcam = TCAM_IPv4();
    @external(1) index = comb_mem_d1(5, 1, 1);
  }

  wires {
    group save_index<"static"=1> {
      index.write_en = 1'd1;
      index.addr0 = 1'd0;
      index.write_data = tcam.index;
      save_index[done] = index.done;
    }
  }

  control {
    seq {
      // 1100xxxxxxxxxxxxxxxxxxxxxxxxxxxx
      invoke tcam(write_en=1'd1, write_index=5'd0, in=32'b11000000000000000000000000000000, prefix_len=6'd4)();
      // 110001xxxxxxxxxxxxxxxxxxxxxxxxxx
      invoke tcam(write_en=1'd1, write_index=5'd1, in=32'b11000100000000000000000000000000, prefix_len=6'd6)();
      // 11000xxxxxxxxxxxxxxxxxxxxxxxxxxx
      invoke tcam(write_en=1'd1, write_index=5'd2, in=32'b11000000000000000000000000000000, prefix_len=6'd5)();

      // Search.
      invoke tcam(search_en=1'd1, in=32'b11000000000000000000000000000000)();
      save_index;
    }
  }
}

Note that the invokes are only supplying one of write_en and search_en. The TCAM definition contains the following two groups:

    group write_write_en_reg {
      write_en_reg.write_en = 1'd1; 
      write_en_reg.in = write_en; 
      write_write_en_reg[done] = write_en_reg.done; 
    }
    group write_search_en_reg {
      search_en_reg.write_en = 1'd1; 
      search_en_reg.in = search_en; 
      write_search_en_reg[done] = search_en_reg.done; 
    }

which are unconditionally executed first thing in the program

control {
    write_write_en_reg; 
    write_search_en_reg;
    ...

Subsequently creating the same error condition as in example 2. And as with that example these registers are used to direct the control flow of the component.

[sampsyo]

This is a great writeup; thank you!

I just wanted to stake out one "philosophical" argument about this:

Is the undef value used during convergence equivalent to 'x?

Assuming that 'x means Verilog's 'x, my opinion is that the Calyx project should not attempt to adopt any Verilog semantics around undefinedness. Verilog's treatment of 'x is super complicated, probably for good reasons, and we should not create any constraints of the form "the Calyx semantics should easily map onto Verilog's semantics." Of course, Verilog-as-a-target may introduce certain constraints on what is practical! But to whatever extent we can, we should design the undefinedness semantics we want, and only later figure out how to realize those semantics when generating code.

[sampsyo]

And, to jot down initial gut reactions without thinking about them too hard:

1. Should the value read from unbound ref cells be undef? -> Sure? Using undef here is kinda analogous to using undef when ports are undriven, in the sense that a ref cell is like a "super-port" that binds several ports at once. Maybe?
2. Should it be an error to write undef to registers? -> Yes until we can think of what we might do otherwise. In particular, our current meaning of undef is "not assigned a value yet in this cycle." It's unclear what this means for a flip-flop.
3. Unstated, but how to implement @control? -> "Default to 0," in the sense that, after the convergence loop has finished, any @control ports that are still undef become 0 instead as a post-processing pass.

I reserve the right to be entirely wrong about all three of these!