TSS Polymorphic

Polymorphism

Let's try to validate the following assignments where mult is a multiplier, mod is a modulus unit, and r is a register:

wires {
  mult.go = 1;
  mult.left = 10;
  mult.right = r.out;

  mod.go = mult.done;
  mod.left = mult.out;
  mod.right = 20;
}

The example attempts immediately use the value generated by the multiplier (mult.out) in the computation of the mod. For this to work, the drive requirement for mod.left must be less than the amount of time mult.out is driven for.

For example, if mult.out is driven for one cycle but mod.left is required for two cycles, this program will be invalid.

First, here is the interface for mult (mod has the same interface):

component mult<G, @static(L)>(@hold(G, G+L) go,
                              @hold(G, G+1) left,
                              @hold(G, G+1) right) ->
                             (@hold(G+L, G+L+1) done,
                              @hold(G+L, G+L+1) out);

There are three components in this interface:

1. G: A callee parameter that states which cycle mult starts its execution in. In type systems land, G is universally quantified.
2. L: The latency of the mult unit. In type systems land, L is existentially quantified.
3. @hold(G, G+1): The drive requirement (resp. guarantee) for inputs (resp. outputs). States that the signal is driven between cycles G and G+1.

Checking the Program

To check the program, we'll generate constraints for each assignment.

mult.go = 1

Starts the execution of the dataflow pipeline. This generates an instantiation constraint:

m0 = mult[G = 0]

The constraint states that this use of the hardware instance mult starts at cycle 0. In general, each hardware instance can have multiple uses.

Next, it generates a constraint from the drive requirement of the go signal:

[m0.G, m0.G + m0.L] = [0, 0 + ∞]

The right hand side, [0, 0 + ∞] specifies the drive guarantee of the constant 1 which is available starting the first cycle till the end of the execution.

The constraint is a strict equality—the go signal must not be driven after the done signal is set to high. In this example, the constraint cannot be satisfied since the signal 1 will continue driving the module forever. This is a bug in our design!

mult.left = 10

This generates drive constraint:

[m0.G, m0.G + 1] ⊆ [0, 0 + ∞]

The constraint in this case is containment—the left signal must be driven at least as long as the requirement states. Driving it more than required is not an error.

mult.right = r.out

Same constraint as previous assignment because the out signal on registers is driven forever.

This might lead to some complexity in the future when writes to registers happen during the dataflow execution.

mod.go = mult.done

This assignment uses the done signal from the multiplier to start the execution of the mod unit. Again, this will generate both an instantiation constraint and a drive constraint:

m1 = mod[G = m0.G + m0.L]

Since the mod unit uses the signal from the m0 use of the mult unit, it is instantiated using constraints from that use.

The drive constraint is:

[m1.G, m1.G + m1.L] = [m0.G + m0.L, m0.G + m0.L + 1]

The right hand side is derived from the drive guarantee of the mult.done signal which is live for one cycle after the execution of the unit. Again, the constraint demands strict equality and again the right hand side fails. Yet another bug vanquished by the type system.

mod.left = mult.out

The assignment generates a drive constraint:

[m1.G, m1.G + 1] ⊆ [m0.G + m0.L, m0.G + m0.L + 1]

This constraint is valid since m1.G = m0.G + m0.L. The type system has proved that the chained use of mult.out is correct!

mod.right = 20

The final assignment demonstrates why the weaker, containment requirement is useful for input signals:

[m1.G, m1.G + 1] ⊆ [0, 0 + ∞]

The constant signal 20 is always driven which means that mod.right can safely read from it.