feat: Accounting for Zero-Extensions

[osmanyasar05]

This PR introduces a new mechanism for accounting for zero extended operands. In addition to the width w of ArithCircuit, we introduce a new variable bits : Nat for ArithCircuit operands, denoting the live bits. Any bit that has a position higher than bits is known to be zeros.

This makes our synthesis flow suitable for the zero-extended operands that arise in multiplication. Since multiplying two n-bit values produces a 2n-bit result, the convention in CIRCT is to zero-extend the operands by concatenating 0s onto their high bits. Therefore we model zero-extension by keeping track of live bits as a separate property, as Comb dialect does not have a zeroExtend operation but uses the concatenation operation.

This implementation will be handy when connecting our framework to CIRCT. In our verified synthesis pass that we'll implement in CIRCT, we will use MLIR's known-bit analysis to determine the zeros and pass that knowledge to our framework through this newly introduced bits variable.

[cowardsa]

Not fundamentally opposed but this does make your implementation diverge from comb (and pretty much all other compilers) allowing for different width operands and results.

How would you represent sign-extension here?

I also didn't see how the multiplier implementation has changed to factor in the bitwidth? Namely when the partial products are being constructed?

[cowardsa]

Hmmm - this is a slightly unconventional choice - here you're implicitly assuming everything is zero-extended - how would we represent sign-extension?

[osmanyasar05]

yes, this was implemented only with zero extension in mind. how is signedness expressed in Comb? Afaiu, there is no concept of signedness in Comb.

I imagine we can carry signedness on the var constructor of ArithCircuit. As in:

inductive ArithCircuit : Nat → Type
  | var (varIndex : Nat) (sign : Bool) : ArithCircuit w

something along these lines. We should probably think more about this part.

[cowardsa]

Sext is a sequence of three operations (extract msb, replicate bits, concatenate) - so indeed its not convenient

[osmanyasar05]

Not fundamentally opposed but this does make your implementation diverge from comb (and pretty much all other compilers) allowing for different width operands and results.

How would you represent sign-extension here?

I also didn't see how the multiplier implementation has changed to factor in the bitwidth? Namely when the partial products are being constructed?

That part happens in bitheapOfVar function. Basically, we create a BitHeap with the new size, but do not add any bit variables to the zero extended positions (or we could add False bits as well, it's the same thing). And then business as usual. This results in not creating any partial products for the zero-extended positions.

[cowardsa]

I'm happy with this approach for now - I think its quite similar to how the BitHeap folks do it as well

[osmanyasar05]

cool, I'm merging this now.

I'm happy with this approach for now - I think its quite similar to how the BitHeap folks do it as well