Allow specification of custom default bit lengths

[rachitnigam]

@sampsyo said the following in #46:

It would be nice to make sure that the number fits into a 32-bit size. And even if not, it could be sensible to put the default integer type into a constant somewhere.

I realize this seems like a low-level detail, but this could actually be a deeper question: we might want to let people specify the default numeric type within a scope. Because numeric widths are so important for accelerator efficiency, people often want to decide the numeric type for an entire design or module at once. That should probably affect (most?) literals as well as the buffers they eventually flow into. Seems sort of tricky.

This can be implemented in two ways: (1) Parsing magic comments in fuse files that specify bit lengths, or (2) Making default bit length a CLI option.

[sampsyo]

Here are two wacky ideas (not sure they are bad, good, or indifferent).

magic type alias

The default numeric type could be specified via "special" type alias. Assume we had type aliases in our language (as I believe we did in OCaml land):

type intbuf = int[10 bank 2];
decl a: intbuf;
decl b: intbuf;

We could have a "special" type named num that controls the "default" type for numbers. The imaginary "preamble" could be:

type num = bit<32>;

or something, which would result in the behavior we currently have. But an any scope—module, function, etc.—the programmer could shadow the existing num type with their own definition:

function f() {
  type num = bit<16>;
  let x = 4;
}
function g() {
  let y = 4;
}

Here, x would have type bit<16> but y would have type bit<32>.

just enough width

One way to explain the current system is that it "promotes" static integer types to proper, dynamic integer types when they're assigned to a variable—and that the type system chooses bit<32> for that dynamic integer type. The type system could instead choose the bit width that is just big enough to hold the static value, i.e., $floor(log n) + 1$ for any static integer $n$. Then it could rely separately on implicit conversions to zero-extend the values when necessary.

For example:

let x = 5;  // type: bit<3>
let y = 1000;  // type: bit<10>
let z1: bit<32> = y;  // OK (zero-extend)
let z2: bit<5> = y;  // error: unsafe narrowing of integer type

[rachitnigam]

The second one is quite easy to do. Is there a reason to prefer the first option over the second?

[sampsyo]

I think the latter makes the most sense? It seems nice and clean, and I can’t really think of any real problems with it. Let’s go for it!

[sa2257]

Hi, I think variable bit lengths are great!

I have some concerns over automatically inferring the sizes though. These concerns are about enforcing bit width specification and making the automatic inference the default.

First up, I agree with the concern @rachitnigam has on why is 32 bit the accepted default. I think a reasonable first take could say bit width default can be byte aligned. But maybe 32 is taken because its a commonly accepted default range.

I believe the idea from #46 is to reduce bit width to improve efficiency? I'm finding it a little hard to understand why automatic inference would help.

1. I think the automatic inference is applied to local variables. This is counter to my understanding of a local variable.

• I think a local variable in Seashell is usually a wire (depending on the context a register). And wires are intended to be capable of handling a range of values, i.e. let x = a[i]*b[i] or for(let i = 0..10). This makes it useful to either infer its size from its range (which is difficult, @rachitnigam said it's impossible) or use a default size and optimize at a later stage by shedding additional bit ranges.

2. Why are they useful?

• I don't see the benefit of tying the bit width of local variables to an initialization value. Maybe this will be beneficial when we define constants. I might be missing a specific example which will clear this up.

3. Arrays vs. local variables

• I'm also not following why we are not treating array bit widths and local variable bit widths similarly. The distinction between these are whether these are in the memory or not. So if Arrays support int and float, local variables should follow that.

• Suggestion
  Maybe it'll be useful to allow declaration of int bit width size at the function declaration. (Personally I prefer before the function declaration (the magic type alias), which will allow us to alter bit widths of interfaces too.)

decl: int <bit32>
def foo () {
}

Also we should certainly use the automatic inference mechanism for constants. I feel it's a perfect match there.

Some additional notes,
Maybe these declarations can be stripped out and add to the Vivado header file? This might allow us to actually test variable bit lengths in hardware.

[sa2257]

More semantics questions,

1. How do operators use automatically inferred variables

• Do operators assume zero padding or only allow same bit width local variables?
  do operators assume zero padding

let x = 1
let y = 2
let z = x + y

2. What bit width would z get? 1 or 2?

let x = 1
let y = 1
let z = x + y

3. What happens when array values transfer into local variables?

let z = a[0] +  b[0]

4. How to carry negative and positive values?
   assume a[0]=-5

let x = a[0]
let y = <bit64> 2
let z = x + y

Will x get padded with 1s?

[rachitnigam]

This makes it useful to either infer its size from its range (which is difficult, @rachitnigam said it's impossible).

To clarify, I think @sa2257 means looking at every use of a variable x and inferring the lowest bit width that satisfies all uses.

Something to keep in mind: bit width directly effect type checking and subtyping in the language which makes it hard to treat bit width optimizations transparently.

One can imagine an explicit version of the language with no subtyping where everything is explicitly cast or moved into larger bit size registers when needed for a computation with misaligned bit widths. This language might address @sa2257 concerns.

Inference is just trying to alleviate the overhead of annotations, but it always needs to be sound and conservative with respect to the explicit language. That is to say, it should never allow a program that is not hardware realizable.

@sa2257 can you write a full program for your suggestion? I’m not sure I fully understand how function level type inference should be working in that.

[rachitnigam]

Equivalent programs with explicit types
1.

let x: bit<1> = 1
let y: bit<2> = 2
let temp_x: bit<2> = 2 // zero padding x
let z: bit<2> = temp_x + y;

2. This is one of the unintuitive cases:

let x, y: bit<1> = 1;
let z: bit<1> = x + y // overflow!

decl a: bit<BW1>[1]
decl b: bit<BW2>[1]
let z: bit<max(BW1, BW2)> = a[0] + b[0]

4. Will fail since negative numbers are not correctly supported! Will fix.

[sampsyo]

The short answer to “why infer the type of a variable to be ‘just big enough’ to hold the initial constant value?” is “we need some way to guess the appropriate type.” That is, unless we’re going to require explicit type annotations on all variables that hold integers, or do one of the more exotic proposals discussed here, we need to determine the type of x in let x = 42 somehow, and using the initial value doesn’t seem any worse than other ways to guess (and IMO is definitely better than a fixed 32-bit default).

A global unification-based type inference strategy (i.e., one where we look at all the uses of a variable and try to guess a width that would fit all of them) would be convenient and a classic PL approach to the problem. But global type inference is trickier to realize than it seems! So even if we eventually decide to try it, I think we need a simpler strategy for now.

About a few of the specific questions from @sa2257 above:

• For addition expressions (i.e., a + b where a has type bit<N> and b has type bit<M>), inference actually does not come into it! This is a question about how we type-check + expressions given the types of the operands. It seems clear that zero-extending the narrower number is the right thing to do (and what our implementation currently does). At the risk of opening another can of worms… we can decide whether we want the addition to overflow by default or always "resize" to avoid overflow—and require an explicit cast as "permission" to overflow. For the former, which runs the risk of unintentional overflow, the result would be the join of the two argument types (i.e., max(N, M)). That's what our current implementation does. For the latter, which avoids overflow but might be more annoying to actually use, the result type would have one more bit in the case that the operands are equal (i.e., N + 1 if N=M).
• As @rachitnigam said, we don't currently have signed integers, so bit<N> cannot hold negative numbers. We should probably explore a signed type as distinct from our current unsigned type…
• In let z = a[0] + b[0], the type of z just gets the type of the result of this addition. There's no fancy inference to be done here. (Unless we go with the global inference approach, of course.)

A near-term change we could make—which really just sidesteps the problem—would be to remove any fancy special-casing and require explicit types on any variable you actually want to change. So let x = 5 would give x the type TStaticInt(3), preventing all mutations to x. If you ever want to change x, you'd have to write let x: bit = 5for someN`. This would be kind of annoying to use but would motivate us to find a good solution using polymorphism or type aliases!

[rachitnigam]

@sa2257 What's the consensus on this? Are you satisfied with saying something like "inference in Fuse is conservative, i.e., it will always infer the smallest bit width of a constant is inferred. If you would like a constant to be stored with a larger bit width, use explicit types for let" in the docs?

[sa2257]

I think I'm still not on the same page with you on bit width inference.

My specific concern is why are local variables treated this way. I noted above

I don't see the benefit of tying the bit width of local variables to an initialization value. Maybe this will be beneficial when we define constants. I might be missing a specific example which will clear this up.

and it seems @rachitnigam you are referring to constants?

it will always infer the smallest bit width of a constant is inferred. If you would like a constant to be stored with a larger bit width, use explicit types for let" in the docs?

Maybe what I'm missing is the implied notion that this is intended for constants?

taking a modified int version of gemm

// m1 is <bit32>
// m2 is <bit32>

let K = 42; // this is a constant, inferred bit width is useful

for (let i = 0..32) unroll 1 {
        for (let j = 0..32) unroll 1 {
            let sum = 0; // this is not a constant, this is a wire. inferred bit width is a burden

            for( let k = 0..32) unroll 32 {
                let mult = m1[i][k] * m2[k][j] + K; // mult wire type is determined from the operation
            } combine {
                sum += mult; // this is the useful inference point for sum wire. (+ register)
            };
            
            prod[i][j]  := sum;
        }
}

My concern is why sum would get just 1 bit and mult would evidently have 33 bits. These are not constants and inferring bit width at let seems counter intuitive to me.

I agree K inferred to have 6 bits is great.

Personally, I would rather have local variables defined bit widths explicitly, as in Verilog, than be inferred, as local variables are supposed to carry different values during operation.

We can differentiate between constants and local variables.

@sa2257 can you write a full program for your suggestion? I’m not sure I fully understand how function level type inference should be working in that.

What I naively have in mind are the magic types,

define int: <bit16>
// m1 is int
// m2 is int

let const K = 42; // this is a constant, infer bit width

for (let i = 0..32) unroll 1 {
        for (let j = 0..32) unroll 1 {
            let sum = 0; // this is not a constant, use default unless otherwise specified

            for( let k = 0..32) unroll 32 {
                let mult = m1[i][k] * m2[k][j] + K; // mult is default unless otherwise specified
            } combine {
                sum += mult;
            };
            
            prod[i][j]  := sum;
        }
}

Or we can explicitly specify bit widths for variables. This is Verilog like. But designers are fully aware of them, eg. whether an overflow will occur.

// m1 is <bit32>
// m2 is <bit32>

let sum : <bit32>
let mult : <bit32> 

let K = 42; // this is a constant, infer bit width

for (let i = 0..32) unroll 1 {
        for (let j = 0..32) unroll 1 {

            for( let k = 0..32) unroll 32 {
                mult = m1[i][k] * m2[k][j] + K;
            } combine {
                sum += mult;
            };
            
            prod[i][j]  := sum;
        }
}

[rachitnigam]

Or we can explicitly specify bit widths for variables. This is Verilog like. But designers are fully aware of them

Yup, I agree. You can do this with or without the PR. The first program you wrote doesn't fully make sense from the type checker's perspective. To the type checker, both let K = 0 and let sum = 0 are just definitions and the same inference procedure is applied.

Anyways, since you can always specify the types, I think your concerns are covered. Let's merge #102 for now and talk more about it as issues come up.

[sa2257]

Things that are unclear to me,

1. In the gemm example above
   What is mult going to be? There's no default. Do we include policies based on operators?

This is a question about how we type-check + expressions given the types of the operands. It seems clear that zero-extending the narrower number is the right thing to do (and what our implementation currently does).

So I think the answer is yes, we decide based on the operator?

I was ignorant of this, my understanding was (assuming bit width not specified) we truncate to fit to the default size int (in our current implementation ). If we decide bit width of mult based on the operation, then doesn't our translated HLS C (which would define mult to be int) mismatch?

2. In the gemm example above
   K probably needs to be casted. So designer needs to be aware of what the multiplication would do (if it decides the bit width of mult based on operator)? This seems more tedious than even Verilog. Assuming pre-specified different bit widths, mult = m1 * m2 + K would work, because only the operators need to be aware of the bit widths.

[sa2257]

Anyways, since you can always specify the types, I think your concerns are covered. Let's merge #102 for now and talk more about it as issues come up.

Yes, but K and sum both can be written to.

In my version, I'm imagining the inferred types as constants. I.e. we can't write to them.

[rachitnigam]

What is mult going to be?

bit<32>

then doesn't our translated HLS C (which would define mult to be int) mismatch?

No, the emitted code will say ap_int<32> mult = ...

K probably needs to be casted

That depends on the implementation of ap_int headers. If they allow the semantics we have (i.e., adding bit<32> and bit<6>), we're good. If not, we can simply emit the cast ourselves from the compiler.

Assuming pre-specified different bit widths, mult = m1 * m2 + K would work, because only the operators need to be aware of the bit widths.

Unclear what you meant by this.

In my version, I'm imagining the inferred types as constants. I.e. we can't write to them.

Ah, I missed the const annotation. Regardless, I am hesitant to offer different inference procedures for let and let const. A simple principle of language design is keeping uniform semantics for things that look similar. Adding subtleties like this makes it harder to write programs.

For an example of why this is considered bad design, look at the semantics of final in Java: https://www.geeksforgeeks.org/final-keyword-java/

---

Maybe one thing that would alleviate your concerns would be adding explicit casting in the language. If you want to disable all inference, you can simply use casts and explicit lets to do so.

[sa2257]

Unclear what you meant by this.

In my version, I'm imagining the inferred types as constants. I.e. we can't write to them.

constants are things you can store a value to use within a program. You can't write to this store within the program.
local variables are things you can use to transfer values from one place to another. So reading a local variable is, using wire as input; writing to a local variable is putting values on to a wire.

Ah, I missed the const annotation. Regardless, I am hesitant to offer different inference procedures for let and let const. A simple principle of language design is keeping uniform semantics for things that look similar. Adding subtleties like this makes it harder to write programs.

That's just an example. We can call let- wire and let const- const

What is mult going to be?

bit<32>

Isn't it 64, if we don't consider mult to be default size 32?

then doesn't our translated HLS C (which would define mult to be int) mismatch?

No, the emitted code will say ap_int<32> mult = ...

I mean in the current translation. I agree we can handle it.

K probably needs to be casted

That depends on the implementation of ap_int headers. If they allow the semantics we have (i.e., adding bit<32> and bit<6>), we're good. If not, we can simply emit the cast ourselves from the compiler.

So we don't throw an error if the bit widths don't match? Okay.

Assuming pre-specified different bit widths, mult = m1 * m2 + K would work, because only the operators need to be aware of the bit widths.

[rachitnigam]

Hm, I am finding it hard to distill what needs to happen in the langauge.

@sa2257 can you create a proposal titled “Sized Numbers” and explain what you would like the language to do in every case where numbers are used. Assume nothing about numbers in the language as they are. Just describe what your desired behavior would be along with example programs.

Instead of me explaining each case, maybe it’ll help if I can probe your reasoning about numbers.

[sampsyo]

Perhaps one useful (albeit pessimistic) perspective here is that there is no perfect answer without some significant changes. We need to do something for assignments like let x = 5, and to summarize the options:

0. Pick a fixed default like 32 bits or use a compiler flag (I would really like to not do this).
1. We could disallow this altogether (emit an error when assigning a constant into a number).
2. Use a "just big enough" integer type (the current behavior; has the downside that @sa2257 has pointed out that the initial value may be way too small and therefore counterintuitively not be what the programmer wants).
3. Use a constant type (i.e., x has type static(5)). This would essentially force the programmer to use an explicit bit width whenever doing something like let x = 5, like the option 1, but could be a little friendlier because at least constants will work fine with no additional changes.

This list does not include what I called "significant changes" above, which would include global constraint-based type inference and the "magic type alias" approach. Given that, I think all of these simple options are unsatisfying in some way—meaning that there's no moral imperative to choose one over any other. The right path in that case is probably to just go for one arbitrarily-selected option and revisit as we gain experience with real-world usage.

[rachitnigam]

Discussion on bitwidth inference in the Chisel paper. See section 10.4.

[rachitnigam]

HardCamel requires wires to have the same bitwidth.

[rachitnigam]

Closing this since #111 and explicit annotation on let allows programmers to just write down all inferred bitwidths by the subtyping.

We can open more issues about subtyping as they come up. In the limit, we might eventually remove subtyping if it confusing enough.