How should we structure resources that we synthesize? #63
Replies: 1 comment
-
I'm gonna sketch out my pipe dream here. This is a mock of an API that I'd love to have to make this stuff super duper easy to play with/experiment with. This isn't written very well (it's 1am and I should be in bed) so apologies! Suppose I wanted to try to synthesize function
Finally, suppose I wanted to enforce that each LUT's input must come from one of I'm imagining something like this (resources-and-routing
; Specify the resources we need. These take the form of a key-value mapping "resource-name -> resource"
; These names will make it easy to generate code later
#:resources (hasheq
'a (INPUT 8)
'b (INPUT 8)
'L0 (LUT5) ; Creates a structure with five inputs I1...I5 (I6 is driven to high) and outputs O5 and O6
'L1 (LUT5)
'L2 (LUT5)
'L3 (LUT5)
'C (CARRY4)
'out (OUTPUT 8))
; Specify routing constraints. Each constraint is a mapping from a structure to the possible sources to its inputs
#:routing (hasheq
; For instance, L0 can only have input bits from 'a or 'b
'L0 (list 'a 'b)
; Instead of specifying the rest of the LUTs indivually we can do a cross product thingy:
(list 'L1 'L2 'L3) (list 'a 'b)
; We want to be a bit more strict about CARRY4's inputs. We don't want arbitrary LUT outputs
; going to arbitrary CARRY inputs as these are already specified. Instead, we want:
; + 'L0's O5 to go to CARRY4's S0
; + 'L0's O6 to go to 'C's DI0
; + 'L1's O5 to go to CARRY4's S1
; + 'L1's O6 to go to 'C's DI1
; + ...etc
(. 'C 'S0) (. 'L0 'O5) ; (. A B) is special syntax I just made up to specify "Field B inside A"
(. 'C 'DI0) (. 'L0 'O6)
(. 'C 'S1) (. 'L1 'O5)
(. 'C 'DI1) (. 'L1 'O6)
; ... ETC
) In a perfect world there would be an architecture-independent function The basic idea is that I can specify my resources as well as routing constraints (maybe even specify arbitrary SMT constraints somehow?) and have it packaged together in some sort of struct or something. Then I can run the solver and it will store the model inside of this struct thing that I just output, and there would be a nice interface to be able to extract routing information from the model. Basically, I want EVERYTHING we would need to compile, including names/etc, inside of the returned struct. Also, things like
So basically adding a new architecture would just involve providing a bunch of these |
Beta Was this translation helpful? Give feedback.
-
ultrascale-tests.rkt
performs synthesis using the(helper f arity)
function. This takes two explicit arguments:f
: the function on bit vectors we want to synthesizearity
: the arity of the desired function (always 2 for now I think)?and returns a solution (either satisfiable w/ a model or unsatisfiable).
In addition to these two explicit arguments it references a large number of globally defined values:
logical-inputs
: a list of symbolic bvs:lut-memory-x
: symbolic bit vectors representing each LUT's internal memoryout
: the symbolic output of the function, created by applyinginterpret-ultrascale-plus-clb
to the above global variablesThe exact components (e.g., number of luts, muxes, etc) as well as their routing will need to change depending on which function we are trying to synthesize.
Also, there is no way to know a priori what the 'right' number/routing will be.
I think we want a way to decouple synthesis from this choice of layout/resources. The question is: what's the best way to do this?
This should be architecture-specific. I'm imagining a struct
(struct resources-and-routing (resources routing))
where
resources
tracks symbolic resources as well as some meta info (like type of resource, etc), androuting
provides routing information, like "The output of lut-a goes to input lut-c.A` or something. This routing info needs to be presented in two ways:ultrascale-logical-to-physical-inputs
) so that it can be applied during synthesisBeta Was this translation helpful? Give feedback.
All reactions