TSS Current

Current Design

Interfaces

component mult<G, @latency(L)>(@exact(G, G+L) go,
                               @within(G, G+1) left,
                               @within(G, G+1) right) ->
                              (@exact(G+L, G+L+1) done,
                               @exact(G+L, G+L+1) out)

1. G is universally quantified and refers to the cycle in which mult starts execution.
2. L is existentially quantified and refers to the latency of mult.
3. @exact requirements specify that the signal must be driven for exactly the specified interval.
4. @within requirements specify that the signal must be driven for at least the specified interval.

Assignments

in = g ? out;

If in has an @exact requirement, we have the constraint:

I = G \intersect O

where I, G, and O are the lifetimes of in, g, and out respectively.

Lifetime of Guards

Guards may use boolean operators:

1. g1 ^ g2 (XOR): The lifetime is G1 \union G2.
2. g1 & g2 (AND): The lifetime is G1 \intersect G2.
3. g1 & !g2 (AND with complement): The lifetime is G1 - G2.

We currently disallow g1 || g2 (OR) because reasoning about potentially overlapping abstract intervals seems hard.

Abstract Lifetimes

To allow compositional reasoning, each primitive guard expression is given an abstraction lifetime. For the following assignment:

x.in = f.out == 0 ^ f.out == 2;

The expression f.out == 0 has the lifetime f0 and f.out == 2 has the lifetime f2.

An abstract lifetime has a start cycle (s) and the end cycle (e): f0 = [f0.s, f0.e]

The hope with using abstract lifetimes is that other assignments in the program can generate sufficient restrictions on the lifetime to enable precise verification.

Instantiation Constraint

We'll often refer to assignments to the go port of a component as an instantiation constraint. This because we use go signal to decide how many invocations of a particular component occur.

For example, given this assignment:

mult.go = 1; // active at cycle 0

We generate the constraint:

m0 = mult[G = 0];

Here m0 is the invocation of the component mult at cycle 0. The go signal itself has an exact requirement which can specify as:

{0, \inf} = [m0.G, m0.G + m0.L]

Requirements and guarantees for ports on mult are specified in terms of all of the invocations of the mult:

mult.left = a.out;

If the lifetime of a is A, then we'll generate the constraint:

[m0.G, m0.G+1] \subset A

Multiple Uses

In general, components may be invoked multiple times:

mult.go = f.out == 1 ^ f.out == 2;

This generates multiple instantiation constraints:

m0 = mult[G = f1.s]
m1 = mult[G = f2.s]

Where f1 and f2 are the abstract lifetimes of f.out == 1 and f.out == 2 respectively. The constraint from the go signal is:

f1 \union f2 = [m0.G, m0.G + m0.L] \union [m1.G, m1.G + m1.L]

Similarly, the requirements from other ports mention all invocations:

mult.left = 1;

Generates the constraint:

([m0.G, m0.G+1] \union [m1.G, m0.G+1]) \subset [0, \inf]

In particular, these disjoint unions let us prove chaining outputs from an invocation into the input of subsequent invocations correct.