Error for comparions that are always true/false

[yn224]

Problem

When I wanted to loop only 4 times using 2-bit number representation for loop counts and 2-bit le operator, I ran into a problem where after checking that the count is 2'b11, it overflows to 2'b00 on the next iteration, causing the loop to run forever and simulation to run until the maximum number of clock cycle is reached. Below is a simple example illustrating such problem. Here, I am attempting to simply update the value in dest with the value stored in register r0 that gets incremented by 1 in each iteration of the loop. When producing the outputs, the maximum number of clock cycles were configured to 500.

import "primitives/std.lib";
component main() -> () {
  cells {
    @external(1) dest = std_mem_d1(32, 1, 1);
    r0 = std_reg(32);
    const11 = std_const(32, 1);
    add = std_add(32);

    // Problem
    // i0 = std_reg(2);
    // le = std_le(2);
    // add_cnt = std_add(2);
    // const0 = std_const(2, 0);
    // const1 = std_const(2, 3);
    // const2 = std_const(2, 1);

    // Resolved by,
    i0 = std_reg(3);
    le = std_le(3);
    add_cnt = std_add(3);
    const0 = std_const(3, 0);
    const1 = std_const(3, 3);
    const2 = std_const(3, 1);
  }
  wires {
    group init {
      r0.write_en = 1'd1;
      r0.in = 32'd0;
      i0.write_en = 1'b1;
      i0.in = const0.out;
      init[done] = r0.done & i0.done ? 1'd1;
    }
    group cond {
      le.left = i0.out;
      le.right = const1.out;
      cond[done] = 1'd1;
    }
    group upd {
      dest.write_en = 1'd1;
      dest.addr0 = 1'd0;
      dest.write_data = r0.out;
      upd[done] = dest.done ? 1'd1;
    }
    group incr {
      add.left = r0.out;
      add.right = const11.out;
      r0.write_en = 1'd1;
      r0.in = add.out;
      add_cnt.left = i0.out;
      add_cnt.right = const2.out;
      i0.write_en = 1'd1;
      i0.in = add_cnt.out;
      incr[done] = r0.done & i0.done ? 1'd1;
    }
  }
  control {
    seq {
      init;
      while le.out with cond {
        seq {
          upd;
          incr;  
        }
      }
    }
  }
}

Output

Using the 2-bit configurations for primitive components, the output looks like such:

{
  "cycles": 500,
  "memories": {
    "dest": [
      81
    ]
  }
}

By increasing the width to 3 to take overflow issues into account, the output becomes more reasonable:

{
  "cycles": 35,
  "memories": {
    "dest": [
      3
    ]
  }
}

Thoughts

It seems that the current implementation of different primitives ignores overflow bits?

[cgyurgyik]

So if I understand correctly, you're overflowing from 2b11 to 2b00 when doing something like 2b11 + 2b01. The current std_add primitive: https://github.com/cucapra/calyx/blob/9b76900d7f0e25df2aa09e55b5e868a02409b2ba/primitives/core.sv#L220-L228

just uses a System Verilog +, which seems to account for overflow simply by wrapping around for unsigned integers. There is currently no overflow bit.

[sgpthomas]

You are correct that primitives ignore overflow bits which makes it impossible to implement loops with the "correct" bitwidth. It shouldn't be too hard to add an overflow output port on relevant primitives and then you could check that to implement these types of loops.

[sampsyo]

Yep, I think @cgyurgyik diagnosed it right! To put it even more simply, the predicate i0.out <= 2'b11 is always true because i0.out is a 2-bit signal, and all n-bit unsigned integers are always less than or equal to (2^n)-1.

Makes me wish for an interpreter that has an "overflow detection" mode!

[sgpthomas]

we should add a paper cut pass for this type of error

[yn224]

What exactly is a paper cut pass?

[cgyurgyik]

A paper cut pass detects common mistakes found when writing a Calyx program. The current pass can be found here.

For example, https://github.com/cucapra/calyx/blob/9b76900d7f0e25df2aa09e55b5e868a02409b2ba/calyx/src/passes/papercut.rs#L19-L21

whenever you write to a std_reg, you need to drive the write_en(able) signal. This paper cut pass catches this case, and gives a descriptive compilation error. This makes the user's life easier, since it is a small bug that is not immediately obvious.

// This will throw a paper cut error.
group write_to_x {
  x.in = 32'd42;
  // x.write_en = 1'd1;   <-- Commented out.
  write_to_x[done] = x.done;
}

Edit: Here's an example program with the corresponding error message.

Perhaps something similar can be incorporated for simpler cases of overflow as described in your example program.

[rachitnigam]

In general, this kind of reasoning would require understanding all of the possible values a register can take (or an overapproximation of that) at any given program point. Might be worth looking into integer range analysis in LLVM or the like.

[cgyurgyik]

Another perhaps simpler solution might be to detect overflow at the SV module level?

[rachitnigam]

How would it be simpler?

[cgyurgyik]

When simulating,

1. detect under/overflow
2. throw some kind of error

[rachitnigam]

That sounds reasonable. TODO item to this issue:

• look into whether Verilator supports overflow checking
• Change simulation generated to error on overflows by default.

[rachitnigam]

@EclecticGriffin do you think that the interpreter would catch this problem? If so, we should probably close this issue and say the interpreter is the way to detect these problems.

[sampsyo]

Maybe I've missed the broader point here, but it seems like the original problem points to some pretty low-hanging fruit for a static checker (i.e., something for the paper-cut pass): in the specific (common) case where you're doing a std_le or std_ge comparison between a constant and a non-constant, but the non-constant has a bit width implying that the comparison is a "foregone conclusion," a warning might be nice.

(A dynamic (interpreter) check for something like this would be a little weird because the dynamic setting makes it a little harder to check when one input to the comparator is a constant.)

[EclecticGriffin]

Yeah I'm echoing Adrian's point, this is probably better left to a static analysis. While we could try to include a detection feature for this in the interpreter, it would either be unsound (just observing that a branch was always taken or never taken) or just a recreation of a static analysis for every such instance which is likely to be costly and no better than making it a papercut pass

[rachitnigam]

Ah, I misremembered the problem; I thought interpreter's overflow detection is sufficient to catch this problem because the loop index will keep overflowing.

[rachitnigam]

I don't know when or how this issue will be addressed. Cider does emit a warning on repeated overflow so I'm considering this "solved", at least in the dynamic case.