Notation for unrolling / handling register arrays

[maxkurze1]

Why Unrolling

Some parts of hardware circuits are very repetitive, e.g. register files with multiple identical registers or SIMD calculation units. In Coq we are able to express these patterns by dependent Inductive constructors or dependent functions, but there is currently no Koika syntax to shift this dependence to Koika.

Consequently, I would like to introduce a new Notation / a couple of Notations to enable Koika code to depend on Coq values (some FiniteType) which are then unrolled into all possible states. Or alternatively, Coq lists which are simply unrolled into their values.

Examples

For the two examples I've built so far, the following turned out pratical:

Generation of match branches

In my opinion, the match version makes the unrolling very explicit, as it literally generates a big match statement that switches over all possible values.

match addr unroll (list_seq_index reg_count) as idx with
  | #(Bits.of_nat (log2 reg_count) (index_to_nat idx)) => read0(regs idx)
  return default: |64`d0|
end

For this syntax, it might be very interesting to evaluate if it makes sense to improve the normal Koika match statement and make it more powerful. For example, we could enable matching multiple values simultaneously like:

match a,b with
  | a_pattern, b_pattern => ...
  | _ , _ => ...
  return default: ...
end

Or maybe also add the ability to combine match branches, like in Coq:

match a with
  | pat1 | pat2 => ...
  | pat3 => ...
  return default: ...
end

My hope is that the unrolling can maybe fit into this somehow.

Standalone unroll construct

Another Notation that I thought of was a new unroll expression that is somewhat similar to
OpenMP's parallel construct.

Something like:

unroll [1;2;3;4] as n reduction [(a,b) => a ++ b] in (
  (* get single value *)
  let a' := a[ #(Bits.of_nat 6 (n * 16)) :+ 16] in 
  let b' := b[ #(Bits.of_nat 6 (n * 16)) :+ 16] in 

  (* compute result *)
  a' + b'
)

This Notation fulfills a somewhat different purpose as it can be used to generate arbitrary Koika code. However, the especially powerful feature of this statement is its reduction function, as it can be used to combine the partial results in different ways.

One could even mimic the match statement by reducing into a big if-elseif statement like this:

unroll (list_seq_index reg_count) as idx reduction [(a,b) => if addr == idx then a else b] in (
  ... content of match ....
)

Admittedly, the reduction is still missing a start value, but you get the idea. The unrolling statement is simply more powerful.

Unrolling for Koika values

One could go event further and maybe think about unrolling over Koika bit vectors like SIMD -> take the vector apart into N parts -> compute some function on each -> put them back together with some form of reduction.

Such operations could definetly be integrated into the unrolling statment.

Your Help

Since I am still very unsure about all of this, I would really appreciate your feedback and also other ideas on how we could add unrolling to Koika.