Symbolic Resource Allocation during Sketch Generation

[bkushigian]

Setup

In #129 I began chatting about basic outlines of sketch generation. The idea is that an architecture-agnostic sketch template is specialized to a concrete architecture-specific sketch by querying an architecture configuration to replace abstract primitive interfaces (e.g., a generic LUT4) with architecture-specific primitives (e.g., a Lattice ECP5 LUT4).

When we specialize (or should we say implement?) a primitive interface with an arch-specific primitive we might not know all the details of the replacing value. For instance, we don't know what the lut memory should be when we provide a Lattice LUT4. Rather than specify this during sketch generation we want to make these values symbolic and use a program hole.

The problem is, when sketches get large (say we have 64 lut memories), the search space can get way too big and synthesis times can blow up. One way around this is to use the same symbolic values over and over again. It is often (usually, in fact!) the case: if we are making a 64 bit binary and function each of the 64 bits will be identical (modulo some unused bits being different).

When we wrote templates explicitly we could specify how many symbolic values we wanted:

(let ([lutmems (choose (?? (bitvector 16)) (?? (bitvector 16)))])
    (for/list ([i 64]) (lut4 lutmems (list-ref inputs i)))

This also provides a layer of flexibility: for instance, multiplication programs have two layers, an 'ANDing' layer, and a 'summing' layer. The 'anding' layer ands a bunch of bits and then passes these to be summed up:

      1101
  x   0101
    ------
      1101        ; This layer the result of ANDing bits in the product
     00000
    110100
+   000000
  --------
   1000001    ; This output the result of ADDing the numbers from previous layer

At least in Lattice, bot the CCU2Cs used for summing in the second layer and the LUT4s used for ANDing in the first layer are backed by 16-bit bitvectors. Even though they have the same 'type' from a symbolic allocation standpoint, we the sketch writers know that they will be used differently and thus should be allocated differently: we don't want to use the same symbolic variables between layers.

The Problem with Sketch Generation

The Sketch Generation design decouples sketch structure and symbolic allocation, and this decoupling makes it harder to easily allocate symbolic resources depending on a program point. To be explicit I'll spell it out:

1. We are writing architecture-independent sketch templates, and these know nothing about things like LUT memories or other architecture-dependent things. Basically anything that's a PARAM in verilog is beyond the Sketch Generator's scope.
2. This means that symbolic resource allocation is occurring at architecture configuration time. But the architecture configuration should be independent of runtime stuff like symbolic resource allocation; this can change from run to run.

The Symbolic Resource Allocator

My solution is to have a third component which I'm calling the Symbolic Resource Allocator (SRA). The SRA should have the following properties:

1. SRA should have a reasonable default behavior
2. SRA's behavior should be flexible: more resources should easily be allocated if needed
3. SRA should support sketch templates marking different allocation requests as being different, much as the LUT memories and CCU2C memories were marked as different in the multiplication template above.
4. SRA should support customization of allocation

I propose something like the following:

(provide (rename-out [make-symbolic-allocator symbolic-allocator]))

(struct symbolic-allocator (allocator [hashed #:mutable]))

(define (make-symbolic-allocator #:allocation-size [allocation-size 1])
  (define allocator (lambda (sra bw #:hint [hint '()])
    (let* ([key (cons bw hint)]
           [hashed (symbolic-allocator-hashed sra)]
           [retrieved (assoc key hashed)])
      (match retrieved [(cons _ value) value]
                       [#f (let ([allocated (make-n-choose (bitvector bw))])
                             (set-symbolic-allocator-hashed!
                               sra (cons (cons key allocated) hashed)))])) ; end def of allocator
  (symbolic-allocator allocator '())

The basic idea is that hashed is a mutable association list mapping keys to previously allocated symbolic values, and allocator is a method/function that queries hashed for an already allocated symbolic resource, returning it if it exists and allocating/storing/returning the resource if it does not exist.

The allocator function will take the symbolic-allocator struct, the bitwidth it is to allocate, and optionally some form of hint (this can be anything):

(lambda (sra bw #:hint [hint '()]))

The bw and hint arguments will be used to form a key into the hashed assoc list stored in sra (via (cons bw hint)). By default only the bitwidth will be used to determine if a symbolic resource has been allocated yet (e.g., a bitvec16). But if the sketch designer would like to specify that different program points should have their own allocation they can pass different values to hint via (allocator sra 16 'AND-LUTS), (allocator sra 16 'SUM-CCU2Cs), etc.

The above design ticks off the first three of the four requirements I mentioned above:

1. The SRA has a reasonable default behavior: by default we allocate 1 possible symbolic variable for each needed bitwidth.
2. The SRA is flexible: we can easily increase the number of resources allocated when we create a new allocator
3. The SRA supports different program points being marked by the sketch generation: we support hints which allow different resources to be allocated for values of the same bitwidth.

I haven't tackled 4 yet, but in the worst case scenario we can provide raw access to the symbolic-allocator or a field to manually override the allocator function:

(define (make-symbolic-allocator #:allocation-size [allocation-size 1] #:allocator-fn [allocator-fn #f])
  (define allocator (if allocator-fn allocator-fn (lambda ...))) ...)

[bkushigian]

I've added an initial implementation to PR #133 (see source code here)

[gussmith23]

from my slack message:

I will dive deep into your notes this afternoon, but before I read them, I had this thought: what if the architecture config also specified the solvable state that a primitive uses, and one could query the config to get a new instance of that solvable state. so in the case of eg a lut4 on lattice (or any platform we support right now, actually) it would give back a symbolic bv16. then, the bitwise sketch generator could easily control how many symbolic variables are used, because it explicitly requests new ones each time. for example in the bitwise template generator, you would

1. query the architecture config for the symbolic state of a lut4
2. figure out how many luts you need based on bitwidth of the operation
3. for each lut, query the architecture config to construct a lut4, passing in the symbolic state constructed in step 1
   then, the template generator explicitly controls how much symbolic state there is floating around. if you want to have multiple options for lutmems, you could specify that as an arg to the templwte generator, and it could request multiple unique symbolic states in step 1

[gussmith23]

Specifically, the way this would work is: the entry for a given interface implementation in an architecture configuration would contain an additional field, which describes the symbolic state associated with the implementation. So, for a LUT4 on Lattice:

...
{
  'interface': 'LUT4',
  'module-name': 'LUT4',
  'ports' : {
    'I0' : 'I0',
    ...
  },
  'symbolic-state': {
    'lutmem': '(bitvector 16)',
  }
}

Then, in the sketch generator, we can query the architecture configuration to get a new, unique instance of the symbolic state:

(define symbolic-state (get-symbolic-state arch-config "LUT4"))

And then later, when we want to make sure different LUT4s get the same symbolic state, we can do:

(define lut-a (make-interface arch-config "LUT4" symbolic-state))
...
(define lut-b (make-interface arch-config "LUT4" symbolic-state))

(calling make-interface, or whatever it may be called, without symbolic state should just introduce a fresh lutmem!)