librarylibs/Uart/src/Uart.xtl
Uart: a serial port (UART: 8 data bits, no parity, 1 stop bit) as X_eTaL step functions: a transmitter, a receiver, and the two looped back Import it with an alias of your choice: "ua:" u_se< "Uart". Put libs/Uart/src on XETAL_PATH ("just path"); the reference is libs/Uart/docs. Names with l: are exported; the others are private to this file.
A line idles at 1. A byte is sent as a frame of ten bits, each held for d clocks: a start bit (0), the eight data bits, least significant first, and a stop bit (1). d, the clocks per bit, is the clock rate over the baud rate: 234 for a 27 MHz Tang Nano at 115200 baud, 3 in the tests. It is the first argument of every step, bound once: u:t_x := ua:t_x 3, then s0 'u:t_x ck:r_un commands (Clocked's harness). Each step is pure, one clock's input in, the next state out.
The transmitter
ˡTxIdle : Int
Its state, four registers: busy (0 or 1), clocks left in this bit, bits left in the frame, the frame (bit 0 on the line).
ᵘᵃ⁼u̲se< "Uart"
ᵘᵃTxIdle 0 0 0 0
ˡTxIdle ← 0 0 0 0
ˡt̲x : Int -> Int -> Int -> Int
d t_x s c: the transmitter after one clock. A command c of 0 to 255 starts sending that byte when it is idle; -1 is no command (a command while busy is ignored).
ᵘᵃ⁼u̲se< "Uart"
ᵘt̲x ← ᵘᵃt̲x 3
ᵘᵃTxIdle ᵘt̲x 65 1 2 10 642
ˡt̲x ← { d s c → b ← f̲irst s n ← 2 s̲elect s k ← 3 s̲elect s f ← 4 s̲elect s (b = 0) ∧ c ≥ 0 ? 1 c̲at (d − 1) c̲at 10 c̲at 512 + 2 × c m̲od 256 b = 0 ? 0 0 0 0 n > 0 ? 1 c̲at (n − 1) c̲at k c̲at f k = 1 ? 0 0 0 0 1 c̲at (d − 1) c̲at (k − 1) c̲at f d̲iv 2 }
ˡl̲ine : Int -> Int
l_ine s: the transmitter's line: 1 when idle, else the frame's bit 0.
ᵘᵃ⁼u̲se< "Uart"
ᵘᵃl̲ine 1 2 10 642 0
ˡl̲ine ← { s → (1 − f̲irst s) + (f̲irst s) × (4 s̲elect s) m̲od 2 }
The receiver
ˡRxIdle : Int
Its state, six registers: phase (0 idle, 1 receiving, 2 waiting for the stop bit), clocks to the next sample, bits left, the bits so far, the last byte received, and valid (1 for the one clock after a byte arrives).
ᵘᵃ⁼u̲se< "Uart"
ᵘᵃRxIdle 0 0 0 0 0 0
ˡRxIdle ← 0 0 0 0 0 0
ˡr̲x : Int -> Int -> Int -> Int
d r_x s l: the receiver after one clock of the line l. A fall to 0 while idle is a start bit; each data bit is sampled in its middle (d + d/2 clocks after the fall, then every d clocks), least significant first.
ᵘᵃ⁼u̲se< "Uart"
ᵘr̲x ← ᵘᵃr̲x 3
ᵘᵃRxIdle ᵘr̲x 0 1 3 8 0 0 0
ˡr̲x ← { d s l → p ← f̲irst s n ← 2 s̲elect s k ← 3 s̲elect s sh ← 4 s̲elect s da ← 5 s̲elect s (p = 0) ∧ l = 0 ? 1 c̲at (d + (d d̲iv 2) − 1) c̲at 8 c̲at 0 c̲at da c̲at 0 p = 0 ? 0 0 0 0 c̲at da c̲at 0 p = 2 ? (2 × 1 − l) c̲at 0 0 0 c̲at da c̲at 0 n > 0 ? 1 c̲at (n − 1) c̲at k c̲at sh c̲at da c̲at 0 s2 ← (sh d̲iv 2) + 128 × l k = 1 ? 2 0 0 0 c̲at s2 c̲at 1 1 c̲at (d − 1) c̲at (k − 1) c̲at s2 c̲at da c̲at 0 }
ˡr̲eceived : a -> a
ˡr̲eceived ← { s → 5 s̲elect s }
ˡv̲alid? : (Num a, Truthy b) => a -> b
v_alid? s: whether the last byte arrived on the last clock.
ᵘᵃ⁼u̲se< "Uart"
ᵘᵃv̲alid? 0 0 0 0 72 1 1
ˡv̲alid? ← { s → 1 = 6 s̲elect s }
Looped back
ˡLoopIdle : Int
The transmitter's line wired to the receiver, and a log of the first four bytes received with their count: fifteen registers, the transmitter's four, the receiver's six, the log's four, the count.
ᵘᵃ⁼u̲se< "Uart"
ᵘᵃLoopIdle 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
ˡLoopIdle ← 15 r̲eshape 0
ˡl̲oopback : Int -> Int -> Int -> Int
d l_oopback s c: one clock: the receiver samples the line as the transmitter drives it now, then both step, and a byte that arrives goes into the log at the count.
ᵘᵃ⁼u̲se< "Uart"
ᶜᵏ⁼u̲se< "Clocked"
ᵘl̲oop ← ᵘᵃl̲oopback 3
ᵘᵃl̲og ᵘᵃLoopIdle 'ᵘl̲oop ᶜᵏr̲un 3 ᵘᵃc̲ommands 65 65
ˡl̲oopback ← { d s c → tx ← 4 t̲ake s rx ← 6 t̲ake 4 d̲rop s lg ← 4 t̲ake 10 d̲rop s ct ← 15 s̲elect s rx2 ← (d ˡr̲x rx)_ ˡl̲ine tx v ← 6 s̲elect rx2 lg2 ← lg + v × ((o̲ffsets 4) = ct) × (5 s̲elect rx2) − lg ((d ˡt̲x tx)_ c) c̲at rx2 c̲at lg2 c̲at ct + v }
ˡl̲ines : Int -> Int
l_ines t: the transmitter's line for every row of a trace (of the transmitter, or of the looped-back pair: both start with its four registers).
ᵘᵃ⁼u̲se< "Uart"
ᵘᵃl̲ines 2 4 r̲eshape 0 0 0 0 1 0 10 640 1 0
ˡl̲ines ← { t → b ← 1 s̲elect₂ t (1 − b) + b × (4 s̲elect₂ t) m̲od 2 }
ˡl̲og : Int -> Int
l_og s: the bytes received so far, from a looped-back state.
ᵘᵃ⁼u̲se< "Uart"
ᵘᵃl̲og 0 0 0 0 0 0 0 0 0 0 72 105 0 0 2 72 105
ˡl̲og ← { s → (4 m̲in 15 s̲elect s) t̲ake 4 t̲ake 10 d̲rop s }
ˡc̲ommands : (Num a, Truthy a) => Int -> a -> a
The commands that send bytes (0 to 255), each when the transmitter is free: d c_ommands bytes gives one command per clock, the byte at the start of each frame of 10 d + 1 clocks, -1 elsewhere, with d more clocks at the end for the last stop bit.
ᵘᵃ⁼u̲se< "Uart"
2 ᵘᵃc̲ommands 65 65 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
ˡc̲ommands ← { d bytes → per ← 1 + 10 × d at ← per × o̲ffsets t̲ally bytes all ← ((per × t̲ally bytes) + d) r̲eshape -1 all + ((o̲ffsets t̲ally all) '= t̲able at) '+ '× i̲nner bytes + 1 }