Ramblings about imperative description of state machines
Imperative state machines in Spade
State machines are not particularly fun to work with in Spade at the moment because you often end up manually writing the logic for delaying, waiting for events etc. A lot of the time, this process is done by manually going from an imperative description to a set of states and transition conditions. We even do exactly that in docs https://docs.spade-lang.org/ws2812-example/state_machine.html.
Several people have pointed out that async/await semantics from rust are essentially describing state machines soI want to add a fsm sub-language to spade to perform this description. Spade isn't an imperative language and shouldn't be, but given how often FSMs are just manually translated imperative programs I want to add a way to do that.
In line with the rest of the language, FSMs will be expressions which produce an output every clock cycle. This output is produced with a keyword, probably yield
. A simple FSM of a counter would broadly look like this
entity counter(clk: clock, rst: bool) {
let count = fsm(clk, rst) {
let mut x = 0;
loop {
yield x;
x = x+1;
}
};
}
The idea is that at each clock cycle, the imperative program is "executed" from one yield point to the next, updating internal variables as it goes along.
To clarify some things, here is a bigger example
// We no longer have the state of an FSM as an explicit `enum` but the output of the FSM is probably
// often helpful to have as one
struct UartOut {
tx: bool,
}
fsm uart_tx(clk: clock, rst: bool, to_transmit: Option<[bool; 8]>) -> UartOut {
loop {
// The whole idea of this FSM thing is to encode the big-picture state of an FSM as
// control flow instead of as an explicit enum. This first while loop encodes that
// we are in the waiting state before getting the order to transmit
while to_transmit.is_none() {
yield UartOut$(tx: true)
}
// The data we want to transmit next. We need to remember this for a while
// which we do by binding it to a `data` variable
let mut data = to_transmit.unwrap();
// For-loops are a convenient way to do delay
// Emit the start bit
for _ in 0..delay {
yield UartOut$(tx: false);
}
// Iterate over the array, emitting the right 0 or 1 signal
for bit in 0..8 {
for _ in 0..delay {
yield UartOut$(tx: data[bit])
}
}
// Stop bit
for _ in 0..delay {
yield UartOut$(tx: true)
}
}
}
Comparing to a standard spade implementation of UART, each yield
in the code
is an enum variant. Yields within for loops need to keep track of the for-loop
duration, and yields after a variable where that variable is used later must
keep track of the variable value. FOr example, the yield in the start-bit loop
doesn't use data
, but the following transmission loop does.
Nesting FSMs
FSMs need to compose and they need to do so in a way that makes sense in hardware. For example, a more concise way of writing the above would be. For now, ignoring outputs
fsm uart_tx(clk: clock, rst: bool, to_transmit: Option<[bool; 8]>) -> UartOut {
loop {
while to_transmit.is_none() {
yield UartOut$(tx: true)
}
// The data we want to transmit next. We need to remember this for a while
// which we do by binding it to a `data` variable
let mut data = to_transmit.unwrap();
// Instantiate a sub-fsm using await (or something)
await delay(clk, rst, bit_duration)
// Iterate over the array, emitting the right 0 or 1 signal
for bit in 0..8 {
await delay(clk, srt, bit_duration)
}
await delay(clk, rst, bit_duration)
}
}
The problem with this scheme is that we need one output per yield point because otherwise there are clock cycles where the output is undefined. One option would be to have some mechanism to specify what to yield next, for example
for bit in 0..8 {
yeeting data[bit];
await delay(clk, rst, bit_duration)
}
Another idea is to allow specifying the output of the parent FSM during the period the sub-fsm is active
for bit in 0..8 {
during delay(clk, rst, bit_duration): data[bit]
}
This is more useful when you want to do something depending on the sub-fsm duration. For example, the ws2812 output scheme which graphically looks like
-----+
0: |
+-------------
------------+
1: |
+------
could be generated using
for n in 0..24 {
let bit = bits[0]
during delay::<8, 300>(clk, rst): duration => {
let on_duration if bit {
200
} else {
100
};
duration > on_duration
}
bits >> 1
}
here, delay returns the number of clock cycles during which it has been delaying for.