Disjoint Write Analysis

[rachitnigam]

(Moved from #12)

The disjoint write analysis provides the second guarantee of the Filament type checker: that resource usage never conflicts. A naive way to enforce this is to require that writes to ports of the same instance are all disjoint. For example:

component MultTwice(@[G, G+1] left: 32, @[G, G+1] right: 32) -> (@[G+2, G+3] out: 32) {
  M := new Mult; // 1-cycle latency Mult
  m0 := M<G>(left, right);
  m1 := M<G+1>(m0.out, m0.right);
}

We can try to generate the following disjointness conditions where L give the liveness of a port:

L(left) /\ L(m.out) = ϕ
L(right) /\ L(m.out) = ϕ

In general, for a component with n input ports and k uses, we'd generate n constraints of size k. However, I want to demonstrate that we can get away by checking that the assignments to the abstract event variables do not conflict with each other.

The @interface Ports

The @exact modality allows us to reason about when signals will have zero and non-zero values. For example:

@[G, G+5] + @exact[G, G+1] go: 1

This states that we can reason about the value of go b/w [G, G+5] and rely on the fact that it will only be non-zero during [G, G+1].

An @interface definition like the following:

@interface<G, 2> go: 1

Is just sugar for:

@[G, G+2] + @exact[G, G+1]

Using this "required zero" semantics, @interface ports allow us to enforce requirements on repeated usage: a signal may not pulse more often than allowed by its interface requirement.

Correct Interface Ports

When compiling a high-level Filament program, the compiler infers interface ports that correspond to each event in the component.

Well-formedness of @interface: If a signal is used b/w [G+i, G+i+n], the interface signal should have a delay of at least n.

In other words, if a design is using the signal for n cycles, it is certainly not safe to trigger the design more than once every n cycles.

Correct Interface Usage Implies Disjoint Use

Going back to our original example, if the design uses an input signal between [G+i, G+i+n], then we know that the interface signal will require a delay of at least n.

m0 := M<G>    // <- first assignment to interface
m1 := M<G+1>  // <- second assignment to interface

If we can ensure that G and G+1 are n apart, then we know that all signals associated with them will also be disjoint.

In other words, the disjointness of @interface ports is a sufficient constraint for disjointness of all other ports that make use of the related event.