Expressivity evaluation: compile Filament types to straight-line protocols

[ngernest]

(Summary of this Slack discussion)

To evaluate the expressivity of our language, we can build a compiler from Filament type signatures that only mention one single event to straight-line protocols. Examples:

Note that we use DontCare assignments to indicate when a DUT input port is no longer available (i.e. the time has exceed its availability interval the Filament type for the port).

Implementation sketch:

• cd into the Filament repo and run cargo run <prog> --dump-interface, which extracts the main Filament module's type signature into a JSON object.
• In a separate package within the existing Protocols cargo workspace, parse the JSON and use the latency / delay information from the Filament type to determine how many step()s to insert and where to insert the fork(), following the images above. Also insert DUT port assignments / DontCare assignments accordingly.
• We will want to check that the generated Protocols program behaves the same as the original Filament program. I think we can do this by running the Protocols interpreter with the generated Protocols spec against the Verilog that the Filament program compiles to, and seeing if the Protocols interpreter succeeds. (This checks if the generated spec faithfully models the Filament program.)
• We can build up a test suite of Filament programs that compile to straight-line Protocols. For each source Filament program, we will want two Turnt snapshot tests:

1. One which checks that the generated straight-line protocol remains the same (given the same JSON representation of a Filament type)
2. One which checks that the Protocols interpreter accepts the generated protocol as a spec for the Verilog that the Filament compiles to

What remains to be done:
This model only works for Filament types that have one single event. We need to think about how to handle Filament types that mention two events (e.g. the following Filament type for a combinational adder, which mentions two events G and L):

comp Add<G: L-G, L: 1>(@[G, L] l: 32, @[G, L] r: 32) -> (@[G, L] o: 32) where L > G

This type signature means if the inputs are provided for multiple cycles, then outputs will be provided for the same amount of cycles.

Rachit mentioned that this should result in some Protocols program which behaves the same as a Filament module which triggers the @interface signal for G before L. In other words, the target Protocols program should find some way of ensuring that event G happens before L. Maybe this can be done by including some extra control pins in the compiled Protocols program which are modified at the right times? (e.g. one for G and one for L) Need to think a bit more about this.

Alternatively, perhaps we could express this range of timing behaviors if our language adopted the non-deterministic loop / fixed loop-iteration operators mentioned in #167.

Rachit also mentioned there is a test case in the Filament repo which contains 3 events -- might be good to look into that.

Assuming we find a work around to handle multiple events, we should be able to handle all Filament types (including ones in the follow-up language Lilac, since all Lilac types compile to base Filament via elaboration and are type-checked again).

[ngernest]

Rachit also mentioned there is a test case in the Filament repo which contains 3 events

Here's the Filament program with 3 events:

  // Merge two signals with disjoint lifetimes to generate a new signal available
  // for the union of their lifetimes
  // Implemented using a temporal mux that switches from signal `in1` to `in2`
  // on event L.
  // The signals `in1` and `in2` might exist for more their specified lifetime
  // in this function's signature but that is okay because inputs only require
  // signals to be active for at least as long as the requirement
  comp Merge<'G: 'E-('G), 'L: 'E-('L), 'E: 1>(
    go_G: interface['G],
    go_L: interface['L],
     in1: ['G, 'L] 32,
     in2: ['L, 'E] 32,
  ) -> (
     out: ['G, 'E] 32,
  ) where 'L > 'G, 'E > 'L, 'E > 'G;

Intuition for the three events:

• 'G is the cycle when input in1 becomes available
• 'L is the cycle when the merge component switches from in1 to in2
• 'E is the cycle in which the merged output ceases to be available

The Merge component takes two inputs in1, in2 with disjoint availability intervals (['G, 'L) and ['L, 'E)), and merges them into a single signal that is available for ['G, 'E). The ordering constraints 'E > 'L > 'G ensure that the intervals are well-formed.

The fact that there are separate interface ports for different events 'G and 'L in the Filament type leads me to think if we were to compile this to Protocols, we would also need separate DUT pins that correspond to them.

Idea for compiling multi-event Filament types to Protocols:

• Sort all events temporally based on the constraints in the where ... clause in the Filament type, with earlier events coming first
• For all events except the final event, produce a DUT input port that represents the event's interface port

This means the combinational adder

comp Add<G: L-G, L: 1>(@[G, L] l: 32, @[G, L] r: 32) -> (@[G, L] o: 32) where L > G

would only have one DUT input pin DUT.go_G, representing the interface port for Add's G event,
while the Merge example above would have two interface ports, namely go_G and go_L for the two "non-final" events 'G and 'L.