Harness symmetry in LUT input routing

[gussmith23]

• LUT choice: wiring bits a,b,c into LUT0 is the same as wiring them into LUT1.
  • This symmetry may not be valid if you depend on the carry chain!
• LUT input order: wiring bits a,b,c into a LUT is equivalent to wiring bits b,a,c into a LUT.
• maybe? Reused inputs: wiring the same bit into multiple LUTs is not necessary.
  • I have no clue whether this is true or not, and it would be really interesting to try and prove.
  • I assume there's probably a fairly trivial proof, i.e. what if we wanted to compute two different functions over the same bit.
• Logical input order: the function (logical input 0 + logical input 1) is the same as (logical input 1 + logical input 0) if we re-route the inputs.
  • I'm struggling to find a way to encode this one.

[gussmith23]

Zach made a very good point, that the space of possible input mappings is pretty symmetric. For example, mapping bit 0 of input a into lut0 input0 and mapping bit 0 of input b into lut0 input1 would be the same as swapping which inputs of lut0 they feed into. Similarly, routing them into lut1 instead of lut0 is also equivalent assuming the carry chain isn't used.

[gussmith23]

Starting with a concrete example. For two 8 bit inputs a and b on Xilinx ultrascale. Assume we use all 8 LUTs.

For each LUT, we have a pool of 8+8=16 logical bits to choose from. We can wire between 0 and 6 logical bits into each LUT, giving us (16 choose 0) + (16 choose 1) + ... + (16 choose 6) = 14773 different ways to wire inputs into a single LUT. This number to the 8th power is still VERY large (10^33).

[gussmith23]

Does it make sense to wire an input bit to multiple LUTs? Can we show that there are operations that need this? I think it would only be useful when used with the carry chain.

If we assume a bit is used at most once, then our space is a lot smaller. Each bit can be assigned to no LUT, or one of the 8 LUTs. 9 options^16 = 10^15. But that's overcounting, because each LUT can only take 6 inputs.

How hard is it to express this in Rosette? I'm struggling!

[gussmith23]

There's even more symmetry here that we're not capturing. Specifically, we can rearrange how the inputs come in.

One way to handle this would be to force an order on how we can draw bits from the logical inputs. So if we have variables 0,...,47, indicating which logical input a physical input is drawing from, we can enforce a rule that says that we have to draw from logical inputs in order. That is, variable 0 cannot pull from logical input 2 when variable 1 pulls from logical input 1; we would need them to be ordered.

I'm not convinced that actually works, but something like that may be what we need.

It would be useful to list out the types of symmetries we need to take advantage of.

[gussmith23]

Zach: we can rely more on CDCL to identify symmetries.

First, we try with a set of "human readable"/interpretable templates of ways to commonly order the inputs.

zach suggests 48x48 table, rows are logical bits, cols are physical bits, "1" means connected. each column has at most one bit set, there's an SMTlib construct for this that Rosette may expose.

Ben also has ideas about this, follow up with him.

[gussmith23]

Zach suggests ensuring that everything is in theory of bitvectors and using boolector. I converted things to use only theory of bitvectors (I mostly just needed to change how LUTs work) but it's still not terminating. I also don't know if my implementation was correct.