librarylibs/Clocked/src/Clocked.xtl
The harness: one input per clock
ˡr̲un : Any a => (a -> b -> a) -> a -> b -> a
s0 'step r_un xs: the state after every input (an item, or a row of a matrix, per clock).
ᶜᵏ⁼u̲se< "Clocked"
0 'ᶜᵏa̲ccumulate ᶜᵏr̲un 1 2 3 4 10
ˡr̲un ← { f̲ s xs → (n, last) ← (t̲ally xs) '{ (i, t) → (i + 1, t f̲ i s̲elect xs) } p̲ower (1, s) last }
ˡt̲race : (a -> b -> a) -> a -> b -> a
s0 'step t_race xs: every state from s0 on, one per row (a vector for a scalar state): what the registers hold after reset and after each clock.
ᶜᵏ⁼u̲se< "Clocked"
(0 0 0) 'ᶜᵏs̲hift ᶜᵏt̲race 1 1 0 0 0 0 0 0 1 0 1 1 1 1 0
ˡt̲race ← { f̲ s xs → first ← (1 c̲at s̲hape s) r̲eshape s (n, last, rows) ← (t̲ally xs) '{ (i, t, m) → t1 ← t f̲ i s̲elect xs◆ (i + 1, t1, m c̲at t1) } p̲ower (1, s, first) rows }
Counters and accumulators
ˡt̲ick : Int -> Int -> Int
s t_ick e: an 8-bit counter that counts when its enable e is 1.
ᶜᵏ⁼u̲se< "Clocked"
127 ᶜᵏt̲ick 1 -128
ˡt̲ick ← { s e → 8 ᶠˣw̲rap s + e }
ˡa̲ccumulate : Int -> Int -> Int
s a_ccumulate x: an 8-bit accumulator (an adder and a register).
ᶜᵏ⁼u̲se< "Clocked"
100 ᶜᵏa̲ccumulate 100 -56
ˡa̲ccumulate ← { s x → 8 ᶠˣw̲rap s + x }
Shift register
ˡs̲hift : a -> a -> a
s s_hift b: the bits move one place toward the front and b comes in at the end (a serial-in, parallel-out shift register: wiring and flip-flops, no logic).
ᶜᵏ⁼u̲se< "Clocked"
(0 0 0 1) ᶜᵏs̲hift 1 0 0 1 1
ˡs̲hift ← { s b → (1 d̲rop s) c̲at b }
A sequence detector: a state machine from a table
ˡNext101 : Int
Next101: the next state of a detector of the bits 1 0 1 (overlapping), a table indexed by state and bit: item 1 + s + 4 * b. States: 0 nothing yet, 1 seen 1, 2 seen 1 0, 3 seen 1 0 1 (found). In hardware the table is a ROM or a few gates.
ᶜᵏ⁼u̲se< "Clocked"
ᶜᵏNext101 0 2 0 2 1 1 3 1
ˡNext101 ← 0 2 0 2 1 1 3 1
ˡf̲ound? : (Num a, Truthy b) => a -> b
f_ound? s: whether the state says 1 0 1 was just seen (the Moore output).
ᶜᵏ⁼u̲se< "Clocked"
ᶜᵏf̲ound? 0 1 2 3 0 0 0 1
ˡf̲ound? ← { s → s = 3 }
A RAM
ˡw̲rite : Int -> Int -> Int
m w_rite c: a memory of 8-bit words after one clock of a write port: the command c is write-enable, address (from 0) and data; when write-enable is 1 the word at the address becomes the data, every other word is kept (each word a register with a mux in front).
ᶜᵏ⁼u̲se< "Clocked"
(4 r̲eshape 0) ᶜᵏw̲rite 1 2 9 0 0 9 0
ˡw̲rite ← { m c → we ← f̲irst c hit ← (o̲ffsets t̲ally m) = 2 s̲elect c 8 ᶠˣw̲rap m + we × hit × (3 s̲elect c) − m }