librarylibs/Datapath/src/Datapath.xtl
Elementwise: one unit per element
ˡv̲add : Int -> Int -> Int -> Int
w v_add x y: the sum, item by item, wrapped to w bits (eight 16-bit numbers: eight 16-bit adders).
ᵈᵖ⁼u̲se< "Datapath"
ᵘv̲add ← ᵈᵖv̲add 16
30000 ᵘv̲add 30000 -30000 -5536 0
ˡv̲add ← { w x y → w ᶠˣw̲rap x + y }
ˡs̲axpy : Int -> Int -> Int -> Int -> Int
w s_axpy a x y: a times x plus y, wrapped at each unit (a multiplier and an adder per element); bind w and a: u:s_axpy := 16 dp:s_axpy 3.
ᵈᵖ⁼u̲se< "Datapath"
ᵘs̲axpy ← 16 ᵈᵖs̲axpy 3
1 2 3 4 ᵘs̲axpy 100 200 300 400 103 206 309 412
ˡs̲axpy ← { w a x y → w ᶠˣw̲rap y + w ᶠˣw̲rap a × x }
ˡr̲elu : Num a => a -> a
r_elu x: x where positive, 0 elsewhere (a comparator and a mux).
ᵈᵖ⁼u̲se< "Datapath"
ᵈᵖr̲elu 1 -2 3 -4 1 0 3 0
ˡr̲elu ← { x → x m̲ax 0 }
Masks and select: a mux
ˡt̲hreshold : (Num a, Truthy a) => a -> a -> a
t t_hreshold x: x where x > t, 0 elsewhere: the mask x > t is the
mux's select line.
ᵈᵖ⁼u̲se< "Datapath"
2 ᵈᵖt̲hreshold 1 2 3 4 0 0 3 4
ˡt̲hreshold ← { t x → x × x > t }
ˡk̲eep : Num a => a -> a -> a
m k_eep x: x where the mask m is 1, 0 elsewhere.
ᵈᵖ⁼u̲se< "Datapath"
(1 0 1 0) ᵈᵖk̲eep 5 6 7 8 5 0 7 0
ˡk̲eep ← { m x → x × m }
Reductions: a tree of adders
ˡs̲um : Int -> Int -> Int
w s_um x: the sum of a vector as a balanced tree of w-bit adders: the first half added to the second half, item by item, then that vector likewise, down to one number (a loop over the log2 n levels of the tree; an odd length is padded with a 0). Wrapping at every adder gives the same bits as wrapping the exact sum once (checked in tests/checks.xtl).
ᵈᵖ⁼u̲se< "Datapath"
16 ᵈᵖs̲um 20000 20000 20000 20000 14464
ˡs̲um ← { w x → levels ← '+ r̲/ (2 ^ o̲ffsets 63) < t̲ally x f̲irst levels '{ v → w ʰh̲alve v } p̲ower x }
ʰh̲alve : Int -> Int -> Int
One level of the tree: the first half added to the second (after a 0 pads an odd length).
ʰh̲alve ← { w v → e ← v c̲at ((t̲ally v) m̲od 2) r̲eshape 0 h ← (t̲ally e) d̲iv 2 w ᶠˣw̲rap (h t̲ake e) + h d̲rop e }
ˡl̲argest : Num a => a -> a
l_argest x: the largest item (a tree of comparators and muxes).
ᵈᵖ⁼u̲se< "Datapath"
ᵈᵖl̲argest 3 9 2 9
ˡl̲argest ← { x → 'm̲ax r̲/ x }
ˡd̲ot : Int -> Int -> Int -> Int
w d_ot x y: the inner product, a multiplier per element then the tree.
ᵈᵖ⁼u̲se< "Datapath"
ᵘd̲ot ← ᵈᵖd̲ot 16
1 2 3 ᵘd̲ot 4 5 6 32
ˡd̲ot ← { w x y → w ˡs̲um w ᶠˣw̲rap x × y }
The acceptance pipeline
ˡp̲ipeline : Int -> Int -> Int -> Int
w p_ipeline x k: multiply, add, select, reduce in one expression, the sum of the positive items of x + x * k, every unit w bits: the first end-to-end test research7 asks for (arithmetic, map, zip, comparison, selection, reduction).
ᵈᵖ⁼u̲se< "Datapath"
ᵘp̲ipeline ← ᵈᵖp̲ipeline 16
1 2 3 4 ᵘp̲ipeline 1 -2 1 -2 8
ˡp̲ipeline ← { w x k → w ˡs̲um ˡr̲elu w ᶠˣw̲rap x + w ᶠˣw̲rap x × k }