Architecture-aware General Templating

[bkushigian]

Lakeroad Templates

Lakeroad uses a solver to search for an PFGA program P that implements a bitvec program B. To do this Lakeroad uses program synthesis to synthesize a program L in the Lakeroad DSL, and then compiles this to P (in Verilog).

The space of all programs in the Lakeroad DSL is too large to search exhaustively. For efficiency's sake we chose to introduce templates: program shapes that the solver tries to fill in. This is one design choice, and maybe not the best design choice (e.g., maybe using grammars is better? This is an open question). However, the up side of using templates is that we can easily constrain the search space so that it doesn't blow up too big.

Ad Hoc Templates

Initially Lakeroad used what I will call ad hoc program templating: each architecture has a set of templates that we feed to the solver. When the current set of templates doesn't cover all program functionality we introduce a new template to cover that functionality. The same basic templates are used across different architectures, and there is very little code reuse.

General Templates

To fix this we started hacking on general templates. These are templates that have generic constructs like lr:lut and lr:mux. These have generic implementations in the interpreter, and the compiler is then tasked with lowering these to architecture specific Verilog.

This addresses the problem of code reuse but has the following problems:

1. We are not synthesizing over hardware-specific code, and this loses some of the guarantees that we'd like to have (e.g., "correct by construction")

2. We are tasking the compiler writer with potentially non-trivial code writing to translate generic constructs to verilog. LUTs should be easy, but how do we handle DSPs?

Some New Approaches

@gussmith23 and I have been chatting about how to handle the above issues, and @ztatlock has also weighed in. There are two variants of the same idea, which is essentially:

we should use an architecture configuration file to automatically translate generic templates/LR programs to architecture-specific LR programs

Idea 1: Template Schemas

This was my first idea. Basically, instead of writing general templates we write template schemas. These look almost identical, but with one crucial difference: rather than having the interpreter run on general LR constructs such as lr:lut we replace these general LR constructs w/ architecture-specific LR constructs prior to passing to the interpreter. Thus, when we go to synthesis we are synthesizing over architecture-specific primitives rather than general LR constructs.

Idea 2: Multiple Lowering Stages

@ztatlock argued (and I think @gussmith23 also argued last wednesday) that we could use multiple stages:

1. synthesize over a general LR template, getting a general LR program
2. replace each general part of the program from 1 w/ architecture specifics and pass to solver to verify (or re-synthesize).

[bkushigian]

After chatting w/ @gussmith23 and @yzh119 yesterday we've settled on a new architecture. We are going to implement Sketch Generation, which will be a modular component of our overall design. Roughly we have:

(Arch Config) ------+------------------------------------------------------------------+
                    |                                                                  |
                    v                                                                  v
         [ Sketch Generation ]  --> (Sketch) --> [ Solver ] --> (LR Program) -->  [ Compiler ] --> (JSON)
                    ^                                 ^
                    |                                 |
(BV Expr) ----------+---------------------------------+

The idea is that:

1. Arch Config: We use an architecture configuration (generated automatically or written by hand) and a BV Expr to perform Sketch Generation
2. Sketch Generation: this step will generate Program Sketches based on the number of inputs into BV Expr and the Arch Config (we will probably want to transform Arch Config into something like a Primitive Factory). These program sketches will be architecture specific: it will involve replacing general lakeroad constructs, such as a LR:LUT_4->1 with architecture-specific primitives. These will be
3. LR Program: Once a set of program sketches have been generated we will pass these to a solver in some order (maybe all of them) and collect output Lakeroad programs. These Lakeroad programs should structurally map to an FPGA in an 'obvious' way: put another way, when passed to the Compiler stage, compilation should be simple syntactic transformations. No clever on-the-fly implementation (e.g., we need a LUT6 but we only have LUT4s, so let's combine them)
4. Compiler: as mentioned above, this should be a very simple step. This will use the Arch Config data to translate platform-specific parts of a sketch to JSON/verilog. We can either include the full Arch Config as an input, or we can make 'rich' primitive structs that include compilation details (e.g., name of primitive, names of arguments, parameters, outputs, etc). It is maybe possible for compilation to be completely platform independent?

[bkushigian]

I'm tring to figure out how to define arch primitives. The first way was via:

(make-primitive "Lattice-ECP5"
                    "LUT4"
                    "lut"
                    (signature '((A 1) (B 1) (C 1) (D 1)) '(Z) '((INIT 16)))
                    inputs)

which produces a struct. The problem is that this has inputs bound to it on creation, which won't work in an architecture configuration (we are defining primitives here before we bind them to inputs). I'd like to be able to create an ecp5:lut4 instance that doesn't already have inputs bound. One way to do this is via lambda abstraction:

(define ecp5:l6mux21
  (lambda (inputs)
    (make-primitive "Lattice-ECP5"
                    "L6MUX21"
                    "mux"
                    (signature '((A 1) (B 1) (C 1) (D 1)) '((Z 1)) '())
                    inputs)))

This suffers from a problem that I can't inspect the value: if I want to know if a primitie is a LUT or a MUX I need to instantiate it and then check the type. E.g., the following function fails at runtime:

(define (make-arch-config architecture primitives)
  (let* ([luts (for/list ([prim primitives] #:when (eq? (primitive-type prim) "lut"))
                 prim)]
         [muxes (for/list ([prim primitives] #:when (eq? (primitive-type prim) "mux"))
                  prim)]
         [other (for/list ([prim primitives]
                           #:when (and (not (eq? (primitive-type prim) "lut"))
                                       (not (eq? (primitive-type prim) "mux"))))
                  prim)])
    (arch-config architecture luts muxes other)))

The #:when clauses are left over from when a primitive was a raw struct and we could query primitive-type.