-
Notifications
You must be signed in to change notification settings - Fork 50
Type System for Signals
Design a type system for the signatures in Calyx that captures how long input and output signals need to be driven.
Type safety: Ports are only used when they are driven.
Interfaces define how components are used. For example, given this interface for a component that implements a simple counter:
component counter(start: 32, end: 32) -> (out: 32) { ... }
We can use it:
cells {
c = counter;
}
group run_counter {
c.start = 32'd0;
c.end = 32'd10;
x.in = c.out;
c.go = 1'd1;
use_counter[done] = c.done;
}
The default interface specifies the following:
- Input signals: Must be driven till the component is done.
- Output signals: Assume that they are not driven after component is done.
This means that it is not safe to read the value of an output port from
a component when the go
signal is not high.
group run_counter { ... }
group use_counter {
x.in = c.out; // observe current value of the counter
}
invoke
is Calyx's control operator for "function calls".
Instead of running a component from a group, you specify the connections in a
control operator:
control {
invoke c(
// input ports
start = 32'd0, end = 32'd10
)(
// output ports
out = x.in
);
}
Invoke's interface: Due to the limitation of Calyx's interfaces, by default,
no signals from a component are visible after an invoke
call.
However, in order to make invoke
useful, Calyx specifies an ad-hoc protocol:
Components can store output signals in registers and make them available
through continuous assignments:
component counter(...) -> (out: 32, out_stable: 32) {
cells {
...
// register to save the value of
// signal out.
save = std_reg(32);
}
wires {
...
out_stable = save.out;
}
}
In this manner, the values from components can be read out after an invoke
call:
control {
invoke c(...);
// reads c.out_stable
read_c_out_stable;
}
Importantly, this interface is unspecified in the Calyx specification. This means, given a Calyx program, the compiler cannot prove that these reads are safe—that they will produce valid values. It is entirely the job of frontends to co-ordinate this, or almost any other, interface correctly.
Type safety: Ports are only used when they are driven.
For every read from a port in a Calyx program, prove that it is being driven by something else. Because of the dataflow-y nature of assignments in hardware, we need to be careful in defining reads and drives.
A port is only read from when an assignment is active:
x.in = false ? a.out;
x.in = true ? b.out;
In this example, x.in
is always driven but only b.out
is being read
from.
Challenge 1: Unsurprisingly, the type system will be incomplete because the language of guards is turing complete (guards can read from any port). In its simplest form, the type system needs to ensure that any port that may be read is being driven.
I think most of the interesting work lies here
The first step towards a type system is the specification of interfaces. In a Calyx component, the signature defines the input and output ports:
component std_mult_pipe(left: 32, right: 32) -> (out: 32)
Enriching this with requirements and guarantees about signal drives allows us to check uses:
component std_mult_pipe(
@hold(1) left: 32, @hold(1) right: 32
) -> (@hold(1) out: 32)
The @hold
attributes describes how many cycles a signal needs to be driven
for inputs or how long this component drives an output signal.
The start and end for these signals is defined the interface signals:
inputs use time after go
is set to high, and outputs use time after done
becomes high.
Holds within.
Interfaces can also specify that certain signals are only visible for the
duration of the execution of the component.
The hold(*)
attribute specifies that the out signal is only safe to read
while the component is executing.
For example, the following component interfaces with an external memory by
sending address over the m1_addr
signal. This signal should not be read
after the component has finished executing.
component read_mem(m1_data) -> (@hold(*) m1_addr);
Similarly, input signals can be required to be driven for the full duration
of the execution (as long as done
is not high):
component counter(@hold(*) start, @hold(*) end) -> (@hold(1) out)
Holds after. Some signals in a component are directly connected to a register and can be safely read after the execution of the component.
The @hold(^)
attribute specifies that output signals are only visible while
the component is executing.
component counter(@hold(1) start, @hold(1) end) -> (@hold(^) out)
Capturing Calyx's default interface. Given these extension, we can capture Calyx's default interface as:
component foo(
@hold(*) go, @hold(*) i1, @hold(*) i2, ...
) -> (@hold(1) done, @hold(*) o1, @hold(*) o2, ...)
Notes and Questions
- What does
@hold(^)
mean for input signals? - What happens if an output signal is held for more than one cycle and the component is re-executed.
- Output signals specified from the start time?
- This only works for static components.
- The dynamic interface builds "static worlds" before and after
go
anddone
. - What about components that can conditionally change their behavior?
- Done-based output signals can handle this.
- Output signals specified from the start time?
Combinational components update output signals immediately when the input
signals are updated.
Furthermore, combinational components don't have any status signals (go
,
done
) since they'd always be high.
One possible way to capture a combination interface is:
component std_add(@hold(0) l, @hold(0) r) -> (@hold(0) out)
It is not clear what @hold(0)
means. What we really want to say here is
that out
is held for exactly as long as l
and r
are held for.
There are three possible solutions:
Parametric hold. We can define a parametric version of hold
that takes
a bound parameter. Each set of input and output signals that use that parameter
have a combinational path between them:
// borrow rust syntax for lifetimes
component std_add<'a>(@hold('a) l, @hold('a) r) -> (@hold('a) out)
This captures the intent that if l
and r
driven for 5 cycles,
out
is safe to read for 5 cycles.
This system also implies that non-combinational interfaces actually have the signature:
// borrow rust syntax for lifetimes
component std_mod<'g, 'd>(@hold('g + 0) l, @hold('g + 0) r) -> (@hold('d + 2) out)
where 'g
and 'd
correspond to the start time of the go
and done
signals
respectively.
Interval-based hold. Extend hold
with intervals that contain start and
end times. This allows us to capture the intent that combinational signals
are sub-cycle events:
component std_add(@hold(0, 0) l, @hold(0, 0) r) -> (@hold(0, 0) out)
Weirdly, this still fails to capture the duration for which l
and r
must be held.
Challenge 2: Meaningful representation for combinational signals.
Notes
- What if a component has a combinational path from input to output?
- PEs in systolic array can have combinational paths b/w inputs and outputs
component std_reg(
@hold(1) write_en, @hold(1)
) -> (@hold(^) out, @hold(1) done)
component std_mult_pipe(
@hold(*) go, @hold(1) left, @hold(1) right,
) -> (@hold(1) out, @hold(1) done)
std_mod_pipe
has the same interface.
Using parametric + interval interface:
component std_mult_pipe<'g, 'd>(
@hold('g, 'g + 'd) go, @hold('g + 1) left, @hold('g + 1) right,
) -> (@hold('d, 'd + 1) out, @hold('d, 'd + 1) done)
In the case of latency-sensitive components, 'd - 'g = latency
.
TODO: Define a subtyping relationship
TODO
Given a component with a "static"
annotation, we can probably calculate
an approximation of when each input signal is used.
Sketch:
- For each group, calculate which input signals are used.
- Calculate the last "time" when all groups are used using the control.
Possible problems:
- Polymorphic
hold
might make this challenging. However, group's encapsulation facilities might scope the problem.
-
@hold
only captures end times. Do we need start times?- Intervals might capture combinational paths
- Is the type system tied to Calyx or can we make it work for Verilog?
- When would an output ever be driven for two cycles? It seems you'd only want,
@hold(^)
,@hold(*)
, orhold(1)
for outputs?- Maybe accumulation pipelines where you tie an output signal to an input?
- Adrian asked: The
^
lifetime is confusing—it states that an output signal is always available but it seems like it should say that the output signal is available till the next use of the component.- For something like a register, the
out
signal is truly always available. Adrian's concern is about using a stale signal. However, the correctness condition doesn't say anything about staleness of data. It only guarantees that ports that are read don't output garbage. - Possible solutions: (1) Strengthen the guarantee somehow to include a notion of stale signals. (2) Ignore this problem.
- For something like a register, the
- Variable latency components
- Memories
- Floating point unit
- The lifetimes of components is separate from input signals