[StaticLogicToCalyx] Incorrect bound count in dot product.

[cgyurgyik]

// Original dot product.

// RUN: circt-opt %s -lower-static-logic-to-calyx

func.func @main() {
  %c0_i32 = arith.constant 0 : i32
  %lhs = memref.alloc() : memref<4xi32>
  %rhs = memref.alloc() : memref<4xi32>
  %result = memref.alloc() : memref<1xi32>
  %c0 = arith.constant 0 : index
  %c1 = arith.constant 1 : index
  %c4 = arith.constant 4 : index
  %0 = staticlogic.pipeline.while II =  1 trip_count = 5 iter_args(%i = %c0, %acc = %c0_i32) : (index, i32) -> i32 {
    %1 = arith.cmpi ult, %i, %c4 : index
    staticlogic.pipeline.register %1 : i1
  } do {
    %left, %right, %incr = staticlogic.pipeline.stage start = 0  {
      %4 = memref.load %lhs[%i] : memref<4xi32>
      %5 = memref.load %rhs[%i] : memref<4xi32>
      %6 = arith.addi %i, %c1 : index
      staticlogic.pipeline.register %4, %5, %6 : i32, i32, index
    } : i32, i32, index
    %2 = staticlogic.pipeline.stage start = 1  {
      %4 = arith.muli %left, %right : i32
      staticlogic.pipeline.register %4 : i32
    } : i32
    %3 = staticlogic.pipeline.stage start = 4  {
      %4 = arith.addi %acc, %2 : i32
      staticlogic.pipeline.register %4 : i32
    } : i32
    staticlogic.pipeline.terminator iter_args(%incr, %3), results(%3) : (index, i32) -> i32
  }

  memref.store %0, %result[%c0] : memref<1xi32>
  return
}

//  ./bin/circt-opt <file-name.mlir>  -lower-static-logic-to-calyx | ./bin/circt-translate -export-calyx 

import "primitives/core.futil";
import "primitives/binary_operators.futil";
component main<"toplevel"=1>(@clk clk: 1, @reset reset: 1, @go go: 1) -> (@done done: 1) {
  cells {
    std_slice_2 = std_slice(32, 2);
    std_slice_1 = std_slice(32, 2);
    std_slice_0 = std_slice(32, 1);
    std_add_1 = std_add(32);
    std_mult_pipe_0 = std_mult_pipe(32);
    std_add_0 = std_add(32);
    std_lt_0 = std_lt(32);
    @external(1) mem_2 = std_mem_d1(32, 1, 1);
    @external(1) mem_1 = std_mem_d1(32, 4, 2);
    @external(1) mem_0 = std_mem_d1(32, 4, 2);
    stage_1_register_0_reg = std_reg(32);
    stage_0_register_1_reg = std_reg(32);
    stage_0_register_0_reg = std_reg(32);
    while_0_arg1_reg = std_reg(32);
    while_0_arg0_reg = std_reg(32);
  }
  wires {
    group assign_while_0_init_0 {
      while_0_arg0_reg.in = 32'd0;
      while_0_arg0_reg.write_en = 1'd1;
      assign_while_0_init_0[done] = while_0_arg0_reg.done;
    }
    group assign_while_0_init_1 {
      while_0_arg1_reg.in = 32'd0;
      while_0_arg1_reg.write_en = 1'd1;
      assign_while_0_init_1[done] = while_0_arg1_reg.done;
    }
    comb group bb0_0 {
      std_lt_0.left = while_0_arg0_reg.out;
      std_lt_0.right = 32'd4;
    }
    group bb0_1 {
      std_slice_2.in = while_0_arg0_reg.out;
      mem_0.addr0 = std_slice_2.out;
      stage_0_register_0_reg.in = mem_0.read_data;
      stage_0_register_0_reg.write_en = 1'd1;
      bb0_1[done] = stage_0_register_0_reg.done;
    }
    group bb0_2 {
      std_slice_1.in = while_0_arg0_reg.out;
      mem_1.addr0 = std_slice_1.out;
      stage_0_register_1_reg.in = mem_1.read_data;
      stage_0_register_1_reg.write_en = 1'd1;
      bb0_2[done] = stage_0_register_1_reg.done;
    }
    group bb0_3 {
      std_add_0.left = while_0_arg0_reg.out;
      std_add_0.right = 32'd1;
      while_0_arg0_reg.in = std_add_0.out;
      while_0_arg0_reg.write_en = 1'd1;
      bb0_3[done] = while_0_arg0_reg.done;
    }
    group bb0_4 {
      std_mult_pipe_0.left = stage_0_register_0_reg.out;
      std_mult_pipe_0.right = stage_0_register_1_reg.out;
      stage_1_register_0_reg.in = std_mult_pipe_0.out;
      stage_1_register_0_reg.write_en = std_mult_pipe_0.done;
      std_mult_pipe_0.go = 1'd1;
      bb0_4[done] = stage_1_register_0_reg.done;
    }
    group bb0_5 {
      std_add_1.left = while_0_arg1_reg.out;
      std_add_1.right = stage_1_register_0_reg.out;
      while_0_arg1_reg.in = std_add_1.out;
      while_0_arg1_reg.write_en = 1'd1;
      bb0_5[done] = while_0_arg1_reg.done;
    }
    group bb0_6 {
      std_slice_0.in = 32'd0;
      mem_2.addr0 = std_slice_0.out;
      mem_2.write_data = while_0_arg1_reg.out;
      mem_2.write_en = 1'd1;
      bb0_6[done] = mem_2.done;
    }
  }
  control {
    seq {
      seq {
        par {
          assign_while_0_init_0;
          assign_while_0_init_1;
        }
        par {
          bb0_1;
          bb0_2;
          bb0_3;
        }
        par {
          bb0_1;
          bb0_2;
          bb0_3;
          bb0_4;
        }
        @bound(5) while std_lt_0.out with bb0_0 {
          par {
            bb0_1;
            bb0_2;
            bb0_3;
            bb0_4;
            bb0_5;
          }
        }
        par {
          bb0_4;
          bb0_5;
        }
        par {
          bb0_5;
        }
        bb0_6;
      }
    }
  }
}

{
    "mem_0": {
      "data": [
        1, 2, 3, 4
      ],
      "format": {
        "numeric_type": "bitnum",
        "is_signed": true,
        "width": 32
      }
    },
    "mem_1": {
      "data": [
        1, 2, 3, 4
      ],
      "format": {
        "numeric_type": "bitnum",
        "is_signed": true,
        "width": 32
      }
    },
    "mem_2": {
      "data": [
        0
      ],
      "format": {
        "numeric_type": "bitnum",
        "is_signed": true,
        "width": 32
      }
    }
}

// fud e mlir.futil --to debugger -s verilog.data mlir.data -q

 > watch bb0_3
 > continue
Hit breakpoint: main::bb0_3
 > continue
Hit breakpoint: main::bb0_3
 > continue
Hit breakpoint: main::bb0_3
 > continue
Jun 09 03:41:04.457 WARN While loop has violated its bounds. The annotation suggests that the body should execute 5 times, but it exited after 2 iterations. 
     147 |        @bound(5) while std_lt_0.out with bb0_0 {
, source: main

Looking at the generated Calyx IR, this does appear to be true. I'm going to guess it is related to this:

  %0 = staticlogic.pipeline.while II =  1 trip_count = 5 iter_args(%i = %c0, %acc = %c0_i32) : (index, i32) -> i32 {
    %1 = arith.cmpi ult, %i, %c4 : index
    ...

The trip count is 5, but the while loop comparison ends after 4 intervals.

[cgyurgyik]

Fixing bound = 2,

fud e mlir.futil --to dat --through icarus-verilog -s verilog.data mlir.data
{
  "cycles": 39,
  "memories": {
    "mem_0": [
      1,
      2,
      3,
      4
    ],
    "mem_1": [
      1,
      2,
      3,
      4
    ],
    "mem_2": [
      45
    ]
  }
}

I think that should be 1 + 4 + 9 + 16 = 30. Ah probably a because of the "pipeline"?

[mikeurbach]

Thanks for the deep dive!

I think this makes sense as a shortcoming: AffineToStaticLogic stamps out the bound from the affine loop's trip count directly, and I don't think anything changes it. Specifically, I don't think the StaticLogicToCalyx pass touches it, even though it peels off loop iterations into prologue and epilogue. At first blush, it seems like the bound attribute should be reduced by one for every "stage" that got peeled. Although I think for this example, we'd peel two prologue and two epilogue, leaving bound=1 🤔

@bound(3) while std_lt_0.out with bb0_0 {

Interesting that the bound=3 here... I wonder where that changed? Maybe infer-static-timing in the native compiler re-computed it?

I think that should be

What is "that"? The cycle count or the result? I seem to recall the expected result is 30.

[cgyurgyik]

AffineToStaticLogic stamps out the bound from the affine loop's trip count directly, and I don't think anything changes it. Specifically, I don't think the StaticLogicToCalyx pass touches it, even though it peels off loop iterations into prologue and epilogue. At first blush, it seems like the bound attribute should be reduced by one for every "stage" that got peeled. Although I think for this example, we'd peel two prologue and two epilogue, leaving bound=1

This might just be a human error then. This was hand-written, and pulled from the dot-product in the tests.

Interesting that the bound=3 here...

That should be 5. I was working with a lot of variations, and this is a copy-paste error. No bound updating occurs.

What is "that"?

The result. You're saying the correct result should be 30? Did you try to run your dot product test on Calyx native? My code example above is a variation of that (smaller memory sizes, external memories).

[cgyurgyik]

Although I think for this example, we'd peel two prologue and two epilogue, leaving bound=1 🤔

The bound is directly associated with bb0_3, which updates the index. This is run twice before hand, and the < condition is 4. This means we have a total of 2 iterations within the while loop.

[mikeurbach]

This might just be a human error then.

Well, I think StaticLogicToCalyx may still be wrong here (by not decrementing the loop bound as it peels iterations to prime the pipeline). I can check on that.

You're saying the correct result should be 30? Did you try to run your dot product test on Calyx native? My code example above is a variation of that (smaller memory sizes, external memories).

Sorry, I was testing with totally different inputs, and I think they also happened to add up to 30 in my test. But yes, I did run that dot product through the native Calyx compiler (and interpreter) and got the expected results. I didn't post the waveforms, but it was working a few months back: #1800 (comment).

It seems like the interpreter has since gotten more strict about bounds checks?

The bound is directly associated with bb0_3, which updates the index. This is run twice before hand, and the < condition is 4. This means we have a total of 2 iterations within the while loop.

I see, thanks that makes sense.

[cgyurgyik]

It seems like the interpreter has since gotten more strict about bounds checks?

It verifies that if a program uses a bound(N) attribute, exactly N iterations are executed now.