Skip to content

Commit f62af1b

Browse files
lmbollenlmbollen
committed
Add Df based utilities
1 parent a607255 commit f62af1b

3 files changed

Lines changed: 346 additions & 4 deletions

File tree

‎bittide-extra/bittide-extra.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -173,6 +173,7 @@ library
173173
Data.List.Extra
174174
Numeric.Extra
175175
Project.Handle
176+
Protocols.Df.Extra
176177
Protocols.Extra
177178
Protocols.Spi
178179
Protocols.Wishbone.Extra

‎bittide-extra/src/Protocols/Df/Extra.hs‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,17 @@
55
module Protocols.Df.Extra where
66

77
import Clash.Prelude
8+
import Data.Maybe
9+
import Data.String.Interpolate (i)
810
import Protocols
11+
import Protocols.Df (forceResetSanity)
12+
13+
import qualified Clash.Explicit.Prelude as E
14+
import qualified Clash.Explicit.Signal.Delayed as ED
15+
import qualified Clash.Explicit.Signal.Delayed.Extra as ED
16+
import qualified Clash.Signal.Delayed as D
17+
import qualified Debug.Trace as Debug
18+
import qualified Protocols.Df as Df
919

1020
andAck :: forall dom a. Signal dom Bool -> Circuit (Df dom a) (Df dom a)
1121
andAck extraAcks = Circuit go0
@@ -61,3 +71,96 @@ skid = Circuit go
6171

6272
ackWhen :: Signal dom Bool -> Circuit (Df dom a) ()
6373
ackWhen canDrop = Circuit $ \_ -> (Ack <$> canDrop, ())
74+
75+
{- | Creates a `Df` wrapper around a block RAM primitive that supports byte enables for
76+
its write channel. Writes are always acked immediately, reads receive backpressure
77+
based on the outgoing `Df` channel.
78+
-}
79+
fromBlockramWithMask ::
80+
(HiddenClockResetEnable dom, Num addr, NFDataX addr, KnownNat words) =>
81+
( Enable dom ->
82+
Signal dom addr ->
83+
Signal dom (Maybe (addr, BitVector (words * 8))) ->
84+
Signal dom (BitVector words) ->
85+
Signal dom (BitVector (words * 8))
86+
) ->
87+
Circuit
88+
( Df dom addr
89+
, Df dom (addr, BitVector words, BitVector (words * 8))
90+
)
91+
(Df dom (BitVector (words * 8)))
92+
fromBlockramWithMask primitive = circuit $ \(r, w) -> do
93+
Fwd (D.fromSignal -> writeOp) <- Df.toMaybe <| forceResetSanity -< w
94+
let
95+
write = fmap (\(addr, _, dat) -> (addr, dat)) <$> writeOp
96+
mask = maybe 0 (\(_, mask', _) -> mask') <$> writeOp
97+
primitiveD ena readD = ED.fromBlockramWithMask (primitive ena) readD write mask
98+
fromDSignal hasClock hasReset hasEnable primitiveD <| forceResetSanity -< r
99+
100+
{- | Creates a `Df` wrapper around a block RAM primitive. Writes are always acked
101+
immediately, reads receive backpressure based on the outgoing `Df` channel.
102+
-}
103+
fromBlockram ::
104+
(HiddenClockResetEnable dom, Num addr, NFDataX addr, NFDataX a) =>
105+
(Enable dom -> Signal dom addr -> Signal dom (Maybe (addr, a)) -> Signal dom a) ->
106+
Circuit (Df dom addr, Df dom (addr, a)) (Df dom a)
107+
fromBlockram primitive = circuit $ \(r, w) -> do
108+
Fwd (D.fromSignal -> write) <- Df.toMaybe <| forceResetSanity -< w
109+
let primitiveD ena readD = ED.fromBlockram (primitive ena) readD write
110+
fromDSignal hasClock hasReset hasEnable primitiveD <| forceResetSanity -< r
111+
112+
-- | Converts a delay annotated circuit with enable port into a `Df` circuit.
113+
fromDSignal ::
114+
forall dom a b n.
115+
( KnownDomain dom
116+
, NFDataX a
117+
, NFDataX b
118+
, KnownNat n
119+
) =>
120+
Clock dom ->
121+
Reset dom ->
122+
Enable dom ->
123+
(Enable dom -> D.DSignal dom 0 a -> D.DSignal dom n b) ->
124+
Circuit (Df dom a) (Df dom b)
125+
fromDSignal clk rst ena0 f = withReset rst Df.forceResetSanity |> Circuit go
126+
where
127+
go (dataLeft, ackRight) = (fmap Ack ackLeft, D.toSignal dataRight)
128+
where
129+
ackLeft = fmap not (D.toSignal dataRightValid) .||. fmap (\(Ack ack) -> ack) ackRight
130+
dataLeftValid = fmap isJust dataLeft
131+
dataRightValid = ED.delayI False ena1 clk $ D.fromSignal dataLeftValid
132+
dataRight = liftA2 (\v d -> if v then Just d else Nothing) dataRightValid data_
133+
ena1 = E.andEnable ena0 ackLeft
134+
data_ = f ena1 (D.fromSignal (fromJustX <$> dataLeft))
135+
136+
-- | Generates an infinite stream of values by repeatedly applying a function.
137+
iterate ::
138+
forall dom a.
139+
(HiddenClockResetEnable dom, NFDataX a) =>
140+
(a -> a) ->
141+
a ->
142+
Circuit () (Df dom a)
143+
iterate f s0 = Circuit (((),) . mealy go s0 . snd)
144+
where
145+
go now (Ack respAck) = (next, Just now)
146+
where
147+
stalled = not respAck
148+
next
149+
| stalled = now
150+
| otherwise = f now
151+
152+
{- | `Df` version of `traceShowId`, introduces no state or logic of any form. Only prints when
153+
there is data available on the input side. Prints available data, clock cycle count in the
154+
relevant domain, and the corresponding Ack.
155+
-}
156+
trace ::
157+
(KnownDomain dom, ShowX a, NFDataX a) =>
158+
String ->
159+
Circuit (Df dom a) (Df dom a)
160+
trace msg =
161+
Circuit
162+
(unbundle . withClockResetEnable clockGen resetGen enableGen mealy go (0 :: Int) . bundle)
163+
where
164+
go cnt (m2s, s2m) = (cnt + 1, (s2m, fmap f m2s))
165+
where
166+
f m = Debug.trace [i| Df.Trace #{msg} | #{cnt}: #{showX m}, #{showX s2m}|] m

‎bittide-extra/tests/unittests/Tests/Protocols/Df/Extra.hs‎

Lines changed: 242 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,40 @@
11
-- SPDX-FileCopyrightText: 2026 Google LLC
22
--
33
-- SPDX-License-Identifier: Apache-2.0
4+
{-# LANGUAGE OverloadedStrings #-}
5+
46
module Tests.Protocols.Df.Extra where
57

68
import Clash.Prelude
79

8-
import Hedgehog (Gen, Property, Range)
10+
import Clash.Hedgehog.Sized.BitVector
11+
import Clash.Hedgehog.Sized.Unsigned
12+
import Clash.Hedgehog.Sized.Vector
13+
import Data.Maybe
14+
import Data.String.Interpolate (i)
15+
import Hedgehog (Gen, Property, Range, assert, cover, footnote, forAll, (===))
916
import Protocols
10-
import Protocols.Hedgehog (defExpectOptions, idWithModelSingleDomain)
17+
import Protocols.Df.Extra (skid)
18+
import Protocols.Hedgehog (
19+
ExpectOptions (..),
20+
defExpectOptions,
21+
idWithModelSingleDomain,
22+
idWithModelSingleDomainT,
23+
propWithModelSingleDomain,
24+
)
25+
import Protocols.Internal (circuitMonitor)
1126
import Test.Tasty (TestTree)
1227
import Test.Tasty.Hedgehog (testProperty)
1328
import Test.Tasty.TH (testGroupGenerator)
1429

15-
import Protocols.Df.Extra (skid)
16-
1730
import qualified Clash.Prelude as C
31+
import qualified Data.List as L
32+
import qualified Hedgehog as H
1833
import qualified Hedgehog.Gen as Gen
1934
import qualified Hedgehog.Range as Range
35+
import qualified Protocols.Df as Df
36+
import qualified Protocols.Df.Extra as Df
37+
import qualified Prelude as P
2038

2139
smallInt :: Range Int
2240
smallInt = Range.linear 0 10
@@ -51,5 +69,225 @@ prop_skid =
5169
(C.exposeClockResetEnable id)
5270
(C.exposeClockResetEnable skidDropReady)
5371

72+
-- | Merges two BitVectors according to a mask.
73+
mergeWithMask ::
74+
forall bv m.
75+
(KnownNat m, KnownNat bv) =>
76+
BitVector (bv * m) ->
77+
BitVector (bv * m) ->
78+
BitVector m ->
79+
BitVector (bv * m)
80+
mergeWithMask (unpack -> old) (unpack -> new) (unpack -> mask) =
81+
pack (mux @(Vec m) @(BitVector bv) mask new old)
82+
83+
-- | Simply try reading the initial contents of a blockram
84+
prop_fromBlockram :: Property
85+
prop_fromBlockram =
86+
idWithModelSingleDomain @System
87+
defExpectOptions
88+
(genData (genUnsigned Range.linearBounded))
89+
(\_ _ _ -> model)
90+
top
91+
where
92+
mem = iterate d16 succ 0 :: Vec 16 Int
93+
94+
dut :: forall dom. (HiddenClockResetEnable dom) => Circuit (Df dom (Unsigned 4)) (Df dom Int)
95+
dut = circuit $ \rd -> do
96+
wr <- Df.empty
97+
Df.fromBlockram (\ena -> withEnable ena (blockRam mem)) -< (rd, wr)
98+
99+
top clk rst ena0 = withClockResetEnable @System clk rst ena0 dut
100+
model = fmap (mem !!)
101+
102+
-- | First write a new configuration to the blockram, then read it back
103+
prop_fromBlockramWrites :: Property
104+
prop_fromBlockramWrites = H.property $ do
105+
oldMem <- forAll $ genVec @16 $ Gen.integral Range.linearBounded
106+
newMem <- forAll $ genVec @16 $ Gen.integral Range.linearBounded
107+
let
108+
writes = L.zip [0 ..] (toList newMem)
109+
model = fmap (newMem !!)
110+
111+
dut :: forall dom. (HiddenClockResetEnable dom) => Circuit (Df dom (Unsigned 4)) (Df dom Int)
112+
dut = circuit $ \rd0 -> do
113+
wr <- Df.drive def (fmap Just writes)
114+
rd1 <- Df.stall def{resetCycles = 0} StallWithNack [100] -< rd0
115+
Df.fromBlockram (\ena -> withEnable ena (blockRam oldMem)) -< (rd1, wr)
116+
117+
top clk rst ena0 = withClockResetEnable @System clk rst ena0 dut
118+
119+
idWithModelSingleDomainT @System
120+
defExpectOptions
121+
(genData (genUnsigned Range.linearBounded))
122+
(\_ _ _ -> model)
123+
top
124+
125+
-- | Write a configuration to the blockram with byte enables, then read it back
126+
prop_fromBlockramWithMaskWrites :: Property
127+
prop_fromBlockramWithMaskWrites = H.property $ do
128+
oldMem <- forAll $ genVec @8 genDefinedBitVector
129+
newValues <- forAll $ genVec genDefinedBitVector
130+
masks <- forAll $ genVec genDefinedBitVector
131+
132+
let
133+
newMem = zipWith3 mergeWithMask oldMem newValues masks
134+
135+
-- First write old memory with full masks, then write new values with given masks
136+
writes =
137+
L.zip3 [0 ..] (L.repeat maxBound) (toList oldMem)
138+
<> L.zip3 [0 ..] (toList masks) (toList newValues)
139+
model = fmap (newMem !!)
140+
141+
dut ::
142+
forall dom. (HiddenClockResetEnable dom) => Circuit (Df dom (Unsigned 3)) (Df dom (BitVector 32))
143+
dut = circuit $ \rd0 -> do
144+
wr <- Df.drive def{resetCycles = 0} (fmap Just writes)
145+
rd1 <- Df.stall def{resetCycles = 0} StallWithNack [50] -< rd0
146+
Df.fromBlockramWithMask (exposeEnable $ blockRamByteAddressableU d8) -< (rd1, wr)
147+
148+
top clk rst ena0 = withClockResetEnable @System clk rst ena0 dut
149+
150+
idWithModelSingleDomainT @System
151+
defExpectOptions{eoStopAfterEmpty = Just 100}
152+
(genData (genUnsigned Range.linearBounded))
153+
(\_ _ _ -> model)
154+
top
155+
156+
prop_fromDSignal :: Property
157+
prop_fromDSignal =
158+
idWithModelSingleDomain @System
159+
defExpectOptions
160+
(genData genSmallInt)
161+
(\_ _ _ -> id)
162+
dut
163+
where
164+
reference clk ena = withClock clk $ withEnable ena $ delayN d10 (0 :: Int)
165+
dut clk rst ena = Df.fromDSignal clk rst ena (reference clk)
166+
167+
{- | Verify that the circuit always produces less backpressure than it receives
168+
This should check that the circuit can run at without more stalls than strictly necessary
169+
-}
170+
prop_fromDSignalBackpressure :: Property
171+
prop_fromDSignalBackpressure = H.property $ do
172+
inputData <- forAll $ Gen.list (Range.linear 0 20) $ Gen.maybe $ pure ()
173+
stalls <- forAll (Gen.list (Range.linear 0 10) (Gen.integral (Range.linear 0 10)))
174+
let
175+
reference clk ena = withClock @System clk $ withEnable ena $ delayN d5 ()
176+
dut clk rst ena = Df.fromDSignal clk rst ena (reference clk)
177+
top clk rst ena = circuit $ do
178+
(drive1, driveMonitor) <- circuitMonitor <| driveC def inputData
179+
(sample1, sampleMonitor) <- circuitMonitor <| dut clk rst ena -< drive1
180+
withReset rst Df.consume <| Df.stall def{resetCycles = 0} StallCycle stalls -< sample1
181+
idC -< (driveMonitor, sampleMonitor)
182+
183+
isStalled (fwd, (Ack bwd)) = isJust fwd && not bwd
184+
isTransfer (fwd, (Ack bwd)) = isJust fwd && bwd
185+
isIdle (fwd, _) = isNothing fwd
186+
187+
getStalls = L.scanl (\acc inps -> if isStalled inps then succ acc else acc) (0 :: Int)
188+
getTransfers = L.foldl (\acc inps -> if isTransfer inps then succ acc else acc) (0 :: Int)
189+
getIdles = L.foldl (\acc inps -> if isIdle inps then succ acc else acc) (0 :: Int)
190+
(driveSignals, sampleSignals) = sampleC def{timeoutAfter = 200} (top clockGen resetGen enableGen)
191+
driveStalls = getStalls driveSignals
192+
sampleStalls = getStalls sampleSignals
193+
194+
assert (getTransfers driveSignals == L.length (catMaybes inputData))
195+
assert (getTransfers sampleSignals == L.length (catMaybes inputData))
196+
cover 1 "Idle cycles in driver" (getIdles driveSignals > 0)
197+
cover 1 "Idle cycles in sampler" (getIdles sampleSignals > 0)
198+
199+
footnote
200+
$ [i|Drive stalls: #{show (runLengthEncode driveStalls)} \nSample stalls: #{show (runLengthEncode sampleStalls)}|]
201+
assert $ and $ L.zipWith (<=) driveStalls sampleStalls
202+
203+
-- | Utility function to run-length encode a list
204+
runLengthEncode :: (Eq a) => [a] -> [(a, Int)]
205+
runLengthEncode = go Nothing
206+
where
207+
go (Just (a, n)) (x : xs)
208+
| a == x = go (Just (a, n + 1)) xs
209+
| otherwise = (a, n) : go (Just (x, 1)) xs
210+
go Nothing (x : xs) = go (Just (x, 1)) xs
211+
go (Just s) [] = [s]
212+
go Nothing [] = []
213+
214+
prop_iterate :: Property
215+
prop_iterate =
216+
propWithModelSingleDomain
217+
defExpectOptions{eoResetCycles = 10}
218+
gen
219+
(\_ _ _ -> model)
220+
dut
221+
prop
222+
where
223+
f = (+ 1) :: Int -> Int
224+
model = const $ L.take 100 (P.iterate f 0)
225+
226+
-- After 100 cycles stall comes out of reset and stalls communication to
227+
-- terminate the simulation.
228+
dut =
229+
exposeClockResetEnable
230+
(Df.stall def{resetCycles = 100} StallCycle [1000] <| Df.iterate f 0 :: Circuit () (Df System Int))
231+
gen = pure ()
232+
prop expected actual = do
233+
let len = L.length actual
234+
footnote [i|Expected length: Actual length: #{show len}|]
235+
assert (len > 10)
236+
L.take len expected === actual
237+
238+
-- Start of shamelessly copied code from bittide
239+
240+
{- | Version of 'blockRamByteAddressable' with undefined initial contents. It is similar
241+
to 'blockRam' with the addition that it takes a byte select signal that controls
242+
which nBytes at the write address are updated.
243+
-}
244+
blockRamByteAddressableU ::
245+
forall dom memDepth n m addr.
246+
( HiddenClockResetEnable dom
247+
, Enum addr
248+
, NFDataX addr
249+
, KnownNat memDepth
250+
, 1 <= memDepth
251+
, KnownNat n
252+
, KnownNat m
253+
) =>
254+
-- | Memory depth
255+
SNat memDepth ->
256+
-- | Read address.
257+
Signal dom addr ->
258+
-- | Write operation.
259+
Signal dom (Maybe (addr, BitVector (n * m))) ->
260+
-- | Byte enables that determine which nBytes get replaced.
261+
Signal dom (BitVector n) ->
262+
-- | Data at read address (1 cycle delay).
263+
Signal dom (BitVector (n * m))
264+
blockRamByteAddressableU SNat readAddr newEntry byteSelect =
265+
pack <$> readBytes
266+
where
267+
writeBytes = unbundle $ splitWriteInBytes <$> newEntry <*> byteSelect
268+
readBytes = bundle $ ram readAddr <$> writeBytes
269+
ram = blockRamU NoClearOnReset (SNat @memDepth)
270+
271+
{- | Takes singular write operation (Maybe (Index maxIndex, writeData)) and splits it up
272+
according to a supplied byteselect bitvector into a vector of byte sized write operations
273+
(Maybe (Index maxIndex, Byte)).
274+
-}
275+
splitWriteInBytes ::
276+
forall addr m n.
277+
(KnownNat n, KnownNat m) =>
278+
-- | Incoming write operation.
279+
Maybe (addr, BitVector (n * m)) ->
280+
-- | Incoming byte enables.
281+
BitVector m ->
282+
-- | Per byte write operation.
283+
Vec m (Maybe (addr, BitVector n))
284+
splitWriteInBytes (Just (addr, writeData)) byteSelect =
285+
(\m d -> if m then Just d else Nothing)
286+
<$> unpack byteSelect
287+
<*> fmap (addr,) (unpack writeData)
288+
splitWriteInBytes Nothing _ = repeat Nothing
289+
290+
-- End of shamelessly copied code from bittide
291+
54292
tests :: TestTree
55293
tests = $(testGroupGenerator)

0 commit comments

Comments
 (0)