From ebebe6145364627b5d64173a9583355f8265030f Mon Sep 17 00:00:00 2001 From: t-wallet Date: Fri, 19 Jul 2024 10:54:49 +0200 Subject: [PATCH 1/5] change Fwd of Df to Maybe instead of Data and fix linter warnings --- .../src/Protocols/Avalon/Stream.hs | 17 +- clash-protocols/src/Protocols/Axi4/Stream.hs | 15 +- clash-protocols/src/Protocols/Df.hs | 258 +++++++----------- clash-protocols/src/Protocols/DfConv.hs | 29 +- .../tests/Tests/Protocols/Avalon.hs | 9 +- clash-protocols/tests/Tests/Protocols/Axi4.hs | 19 +- clash-protocols/tests/Tests/Protocols/Df.hs | 9 +- .../tests/Tests/Protocols/DfConv.hs | 7 +- 8 files changed, 143 insertions(+), 220 deletions(-) diff --git a/clash-protocols/src/Protocols/Avalon/Stream.hs b/clash-protocols/src/Protocols/Avalon/Stream.hs index 660a8189..b55cc177 100644 --- a/clash-protocols/src/Protocols/Avalon/Stream.hs +++ b/clash-protocols/src/Protocols/Avalon/Stream.hs @@ -172,13 +172,13 @@ instance toDfCircuit proxy = DfConv.toDfCircuitHelper proxy s0 blankOtp stateFn where - s0 = C.repeat @((ReadyLatency conf) + 1) False + s0 = C.repeat @(ReadyLatency conf + 1) False blankOtp = Nothing stateFn (AvalonStreamS2M thisAck) _ otpItem = do modify (thisAck +>>) ackQueue <- get pure - ( if (Maybe.isJust otpItem && C.last ackQueue) then otpItem else Nothing + ( if Maybe.isJust otpItem && C.last ackQueue then otpItem else Nothing , Nothing , C.last ackQueue ) @@ -211,8 +211,8 @@ instance simToSigFwd _ = fromList_lazy simToSigBwd _ = fromList_lazy - sigToSimFwd _ s = sample_lazy s - sigToSimBwd _ s = sample_lazy s + sigToSimFwd _ = sample_lazy + sigToSimBwd _ = sample_lazy stallC conf (head -> (stallAck, stalls)) = withClockResetEnable clockGen resetGen enableGen @@ -238,8 +238,7 @@ instance $ DfConv.drive Proxy conf vals sampleC conf ckt = withClockResetEnable clockGen resetGen enableGen - $ DfConv.sample Proxy conf - $ ckt + $ DfConv.sample Proxy conf ckt instance ( ReadyLatency conf ~ 0 @@ -253,10 +252,8 @@ instance ) => Test (AvalonStream dom conf dataType) where - expectN Proxy options sampled = - expectN (Proxy @(Df.Df dom _)) options - $ Df.maybeToData - <$> sampled + expectToLengths Proxy = pure . P.length + expectN Proxy = expectN (Proxy @(Df.Df dom _)) instance IdleCircuit (AvalonStream dom conf dataType) where idleFwd _ = pure Nothing diff --git a/clash-protocols/src/Protocols/Axi4/Stream.hs b/clash-protocols/src/Protocols/Axi4/Stream.hs index 2204121d..5ae6f366 100644 --- a/clash-protocols/src/Protocols/Axi4/Stream.hs +++ b/clash-protocols/src/Protocols/Axi4/Stream.hs @@ -151,8 +151,8 @@ instance simToSigFwd _ = fromList_lazy simToSigBwd _ = fromList_lazy - sigToSimFwd _ s = sample_lazy s - sigToSimBwd _ s = sample_lazy s + sigToSimFwd _ = sample_lazy + sigToSimBwd _ = sample_lazy stallC conf (C.head -> (stallAck, stalls)) = withClockResetEnable clockGen resetGen enableGen $ @@ -173,9 +173,8 @@ instance withClockResetEnable clockGen resetGen enableGen $ DfConv.drive Proxy conf vals sampleC conf ckt = - withClockResetEnable clockGen resetGen enableGen $ - DfConv.sample Proxy conf $ - ckt + withClockResetEnable clockGen resetGen enableGen + $ DfConv.sample Proxy conf ckt instance ( KnownAxi4StreamConfig conf @@ -188,10 +187,8 @@ instance ) => Test (Axi4Stream dom conf userType) where - expectN Proxy options sampled = - expectN (Proxy @(Df.Df dom _)) options $ - Df.maybeToData - <$> sampled + expectToLengths Proxy = pure . P.length + expectN Proxy = expectN (Proxy @(Df.Df dom _)) instance IdleCircuit (Axi4Stream dom conf userType) where idleFwd Proxy = C.pure Nothing diff --git a/clash-protocols/src/Protocols/Df.hs b/clash-protocols/src/Protocols/Df.hs index a051ccc9..b2b17896 100644 --- a/clash-protocols/src/Protocols/Df.hs +++ b/clash-protocols/src/Protocols/Df.hs @@ -19,7 +19,6 @@ carries data, no metadata. For documentation see: module Protocols.Df ( -- * Types Df, - Data (..), -- * Operations on Df protocol empty, @@ -82,13 +81,7 @@ module Protocols.Df ( -- * Internals forceResetSanity, - dataToMaybe, - maybeToData, - hasData, - noData, - fromData, - toData, - dataDefault, + toMaybe, ) where -- base @@ -96,8 +89,6 @@ module Protocols.Df ( import Control.Applicative (Applicative(liftA2)) #endif import Control.Applicative (Alternative ((<|>))) -import Control.DeepSeq (NFData) -import GHC.Generics (Generic) import GHC.Stack (HasCallStack) import Prelude hiding ( const, @@ -151,7 +142,7 @@ data Df (dom :: C.Domain) (a :: Type) instance Protocol (Df dom a) where -- \| Forward part of simple dataflow: @Signal dom (Data meta a)@ - type Fwd (Df dom a) = Signal dom (Data a) + type Fwd (Df dom a) = Signal dom (Maybe a) -- \| Backward part of simple dataflow: @Signal dom Bool@ type Bwd (Df dom a) = Signal dom Ack @@ -159,66 +150,14 @@ instance Protocol (Df dom a) where instance Backpressure (Df dom a) where boolsToBwd _ = C.fromList_lazy . Coerce.coerce -{- | Data sent over forward channel of 'Df'. Note that this data type is strict -on its data field. --} -data Data a - = -- | Send no data - NoData - | -- | Send /a/ - Data !a - deriving (Functor, Generic, C.NFDataX, C.ShowX, Eq, NFData, Show, C.Bundle) - -instance Applicative Data where - pure = Data - - liftA2 f (Data a) (Data b) = Data (f a b) - liftA2 _ _ _ = NoData - -instance Alternative Data where - empty = NoData - - Data a <|> _ = Data a - _ <|> b = b - -instance Monad Data where - (>>=) :: Data a -> (a -> Data b) -> Data b - NoData >>= _f = NoData - Data a >>= f = f a - instance IdleCircuit (Df dom a) where - idleFwd _ = C.pure NoData + idleFwd _ = C.pure Nothing idleBwd _ = C.pure (Ack False) --- | Convert 'Data' to 'Maybe'. Produces 'Just' on 'Data', 'Nothing' on 'NoData'. -dataToMaybe :: Data a -> Maybe a -dataToMaybe NoData = Nothing -dataToMaybe (Data a) = Just a - --- | Convert 'Maybe' to 'Data'. Produces 'Data' on 'Just', 'NoData' on 'Nothing'. -maybeToData :: Maybe a -> Data a -maybeToData Nothing = NoData -maybeToData (Just a) = Data a - --- | True if `Data` contains a value. -hasData :: Data a -> Bool -hasData NoData = False -hasData (Data _) = True - --- | True if `Data` contains no value. -noData :: Data a -> Bool -noData NoData = True -noData (Data _) = False - --- | Extract value from `Data`, Bottom on `NoData`. -fromData :: (HasCallStack, C.NFDataX a) => Data a -> a -fromData NoData = C.deepErrorX "fromData: NoData" -fromData (Data a) = a - --- | Construct a `Data` if bool is True, `NoData` otherwise. -toData :: Bool -> a -> Data a -toData False _ = NoData -toData True a = Data a +-- | Construct a `Just` if bool is True, `Nothing` otherwise. +toMaybe :: Bool -> a -> Maybe a +toMaybe False _ = Nothing +toMaybe True a = Just a {- | If the t'Data' is v'NoData', it returns the given value; otherwise, @@ -229,25 +168,25 @@ dataDefault a NoData = a dataDefault _ (Data a) = a instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom a) where - type SimulateFwdType (Df dom a) = [Data a] + type SimulateFwdType (Df dom a) = [Maybe a] type SimulateBwdType (Df dom a) = [Ack] type SimulateChannels (Df dom a) = 1 simToSigFwd _ = C.fromList_lazy simToSigBwd _ = C.fromList_lazy - sigToSimFwd _ s = C.sample_lazy s - sigToSimBwd _ s = C.sample_lazy s + sigToSimFwd _ = C.sample_lazy + sigToSimBwd _ = C.sample_lazy stallC conf (C.head -> (stallAck, stalls)) = stall conf stallAck stalls instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Drivable (Df dom a) where type ExpectType (Df dom a) = [a] - toSimulateType Proxy = P.map Data - fromSimulateType Proxy = Maybe.mapMaybe dataToMaybe + toSimulateType Proxy = P.map Just + fromSimulateType Proxy = Maybe.catMaybes - driveC conf vals = drive conf (dataToMaybe <$> vals) - sampleC conf ckt = maybeToData <$> sample conf ckt + driveC = drive + sampleC = sample {- | Force a /nack/ on the backward channel and /no data/ on the forward channel if reset is asserted. @@ -329,11 +268,11 @@ compander :: Circuit (Df dom i) (Df dom o) compander s0 f = forceResetSanity |> Circuit (C.unbundle . go . C.bundle) where - go :: Signal dom (Data i, Ack) -> Signal dom (Ack, Data o) + go :: Signal dom (Maybe i, Ack) -> Signal dom (Ack, Maybe o) go = C.mealy f' s0 - f' :: s -> (Data i, Ack) -> (s, (Ack, Data o)) - f' s (NoData, _) = (s, (Ack False, NoData)) - f' s (Data i, Ack ack) = (s'', (Ack ackBack, maybe NoData Data o)) + f' :: s -> (Maybe i, Ack) -> (s, (Ack, Maybe o)) + f' s (Nothing, _) = (s, (Ack False, Nothing)) + f' s (Just i, Ack ack) = (s'', (Ack ackBack, o)) where (s', o, doneWithInput) = f s i -- We only care about the downstream ack if we're sending them something @@ -399,7 +338,7 @@ const b = ( P.const ( Ack <$> C.unsafeToActiveLow C.hasReset - , P.pure (Data b) + , P.pure (Just b) ) ) @@ -409,7 +348,7 @@ empty = Circuit (P.const ((), P.pure NoData)) -- | Drive a constant value composed of /a/. pure :: a -> Circuit () (Df dom a) -pure a = Circuit (P.const ((), P.pure (Data a))) +pure a = Circuit (P.const ((), P.pure (Just a))) -- | Always acknowledge and ignore values. consume :: (C.HiddenReset dom) => Circuit (Df dom a) () @@ -436,9 +375,9 @@ Example: catMaybes :: Circuit (Df dom (Maybe a)) (Df dom a) catMaybes = Circuit (C.unbundle . fmap go . C.bundle) where - go (NoData, _) = (Ack False, NoData) - go (Data Nothing, _) = (Ack True, NoData) - go (Data (Just a), ack) = (ack, Data a) + go (Nothing, _) = (Ack False, Nothing) + go (Just Nothing, _) = (Ack True, Nothing) + go (Just (Just a), ack) = (ack, Just a) -- | Like 'Data.Maybe.mapMaybe', but over payload (/a/) of a Df stream. mapMaybe :: (a -> Maybe b) -> Circuit (Df dom a) (Df dom b) @@ -458,10 +397,10 @@ filter f = filterS (C.pure f) filterS :: forall dom a. Signal dom (a -> Bool) -> Circuit (Df dom a) (Df dom a) filterS fS = Circuit (C.unbundle . liftA2 go fS . C.bundle) where - go _ (NoData, _) = (Ack False, NoData) - go f (Data d, ack) - | f d = (ack, Data d) - | otherwise = (Ack True, NoData) + go _ (Nothing, _) = (Ack False, Nothing) + go f (Just d, ack) + | f d = (ack, Just d) + | otherwise = (Ack True, Nothing) -- | Like 'Data.Either.Combinators.mapLeft', but over payload of a 'Df' stream. mapLeft :: (a -> b) -> Circuit (Df dom (Either a c)) (Df dom (Either b c)) @@ -513,8 +452,8 @@ zipWithS :: zipWithS fS = Circuit (B.first C.unbundle . C.unbundle . liftA2 go fS . C.bundle . B.first C.bundle) where - go f ((Data a, Data b), ack) = ((ack, ack), Data (f a b)) - go _ _ = ((Ack False, Ack False), NoData) + go f ((Just a, Just b), ack) = ((ack, ack), Just (f a b)) + go _ _ = ((Ack False, Ack False), Nothing) -- | Like 'P.zip', but over two 'Df' streams. zip :: forall a b dom. Circuit (Df dom a, Df dom b) (Df dom (a, b)) @@ -538,10 +477,10 @@ partitionS :: partitionS fS = Circuit (B.second C.unbundle . C.unbundle . liftA2 go fS . C.bundle . B.second C.bundle) where - go f (Data a, (ackT, ackF)) - | f a = (ackT, (Data a, NoData)) - | otherwise = (ackF, (NoData, Data a)) - go _ _ = (Ack False, (NoData, NoData)) + go f (Just a, (ackT, ackF)) + | f a = (ackT, (Just a, Nothing)) + | otherwise = (ackF, (Nothing, Just a)) + go _ _ = (Ack False, (Nothing, Nothing)) {- | Route a 'Df' stream to another corresponding to the index @@ -560,12 +499,12 @@ route = Circuit (B.second C.unbundle . C.unbundle . fmap go . C.bundle . B.second C.bundle) where -- go :: (Data (C.Index n, a), C.Vec n (Ack a)) -> (Ack (C.Index n, a), C.Vec n (Data a)) - go (Data (i, a), acks) = + go (Just (i, a), acks) = ( acks C.!! i - , C.replace i (Data a) (C.repeat NoData) + , C.replace i (Just a) (C.repeat Nothing) ) go _ = - (Ack False, C.repeat NoData) + (Ack False, C.repeat Nothing) {- | Select data from the channel indicated by the 'Df' stream carrying @Index n@. @@ -613,13 +552,13 @@ selectN = go c0 ((dats, datI), Ack iAck) -- Select zero samples: don't send any data to RHS, acknowledge index stream -- but no data stream. - | Data (_, 0) <- datI = - (c0, ((nacks, Ack True), NoData)) + | Just (_, 0) <- datI = + (c0, ((nacks, Ack True), Nothing)) -- Acknowledge data if RHS acknowledges ours. Acknowledge index stream if -- we're done. - | Data (streamI, nSelect) <- datI + | Just (streamI, nSelect) <- datI , let dat = dats C.!! streamI - , Data d <- dat = + , Just d <- dat = let c1 = if iAck then succ c0 else c0 oAckIndex = c1 == C.extend nSelect @@ -629,12 +568,12 @@ selectN = ( c2 , ( (datAcks, Ack oAckIndex) - , Data d + , Just d ) ) -- No index from LHS, nothing to do | otherwise = - (c0, ((nacks, Ack False), NoData)) + (c0, ((nacks, Ack False), Nothing)) where nacks = C.repeat (Ack False) @@ -680,16 +619,16 @@ selectUntilS fS = nacks = C.repeat (Ack False) go f ((dats, dat), Ack ack) - | Data i <- dat - , Data d <- dats C.!! i = + | Just i <- dat + , Just d <- dats C.!! i = ( ( C.replace i (Ack ack) nacks , Ack (f d && ack) ) - , Data d + , Just d ) | otherwise = - ((nacks, Ack False), NoData) + ((nacks, Ack False), Nothing) {- | Copy data of a single 'Df' stream to multiple. LHS will only receive an acknowledgement when all RHS receivers have acknowledged data. @@ -708,13 +647,13 @@ fanout = forceResetSanity |> goC f acked (dat, acks) = case dat of - NoData -> (acked, (Ack False, C.repeat NoData)) - Data _ -> + Nothing -> (acked, (Ack False, C.repeat Nothing)) + Just _ -> -- Data on input let -- Send data to "clients" that have not acked yet valids_ = C.map not acked - dats = C.map (bool NoData dat) valids_ + dats = C.map (bool Nothing dat) valids_ -- Store new acks, send ack if all "clients" have acked acked1 = C.zipWith (||) acked (C.map (\(Ack a) -> a) acks) @@ -755,10 +694,10 @@ bundleVec :: bundleVec = Circuit (B.first C.unbundle . C.unbundle . fmap go . C.bundle . B.first C.bundle) where - go (iDats0, iAck) = (C.repeat oAck, maybeToData dat) + go (iDats0, iAck) = (C.repeat oAck, dat) where oAck = maybe (Ack False) (P.const iAck) dat - dat = traverse dataToMaybe iDats0 + dat = sequenceA iDats0 -- | Split up a 'Df' stream of a vector into multiple independent 'Df' streams. unbundleVec :: @@ -771,20 +710,19 @@ unbundleVec = initState :: C.Vec n Bool initState = C.repeat False - go _ (NoData, _) = (initState, (Ack False, C.repeat NoData)) - go acked (Data payloadVec, acks) = + go _ (Nothing, _) = (initState, (Ack False, C.repeat Nothing)) + go acked (Just payloadVec, acks) = let -- Send data to "clients" that have not acked yet valids_ = C.map not acked - dats0 = C.zipWith (\d -> bool Nothing (Just d)) payloadVec valids_ - dats1 = C.map maybeToData dats0 + dats = C.zipWith (bool Nothing . Just) payloadVec valids_ -- Store new acks, send ack if all "clients" have acked acked1 = C.zipWith (||) acked (C.map (\(Ack a) -> a) acks) ack = C.fold @(n C.- 1) (&&) acked1 in ( if ack then initState else acked1 - , (Ack ack, dats1) + , (Ack ack, dats) ) {- | Distribute data across multiple components on the RHS. Useful if you want @@ -802,15 +740,14 @@ roundrobin = . B.second C.bundle ) where - go i0 (NoData, _) = (i0, (Ack False, C.repeat NoData)) - go i0 (Data dat, acks) = + go i0 (Nothing, _) = (i0, (Ack False, C.repeat Nothing)) + go i0 (Just dat, acks) = let - datOut0 = C.replace i0 (Just dat) (C.repeat Nothing) - datOut1 = C.map maybeToData datOut0 + datOut = C.replace i0 (Just dat) (C.repeat Nothing) i1 = if ack then C.satSucc C.SatWrap i0 else i0 Ack ack = acks C.!! i0 in - (i1, (Ack ack, datOut1)) + (i1, (Ack ack, datOut)) -- | Collect modes for dataflow arbiters. data CollectMode @@ -838,45 +775,45 @@ roundrobinCollect NoSkip = Circuit (B.first C.unbundle . C.mealyB go minBound . B.first C.bundle) where go (i :: C.Index n) (dats, Ack ack) = - case (dats C.!! i) of - Data d -> + case dats C.!! i of + Just d -> ( if ack then C.satSucc C.SatWrap i else i , ( C.replace i (Ack ack) (C.repeat (Ack False)) - , Data d + , Just d ) ) - NoData -> - (i, (C.repeat (Ack False), NoData)) + Nothing -> + (i, (C.repeat (Ack False), Nothing)) roundrobinCollect Skip = Circuit (B.first C.unbundle . C.mealyB go minBound . B.first C.bundle) where go (i :: C.Index n) (dats, Ack ack) = - case (dats C.!! i) of - Data d -> + case dats C.!! i of + Just d -> ( if ack then C.satSucc C.SatWrap i else i , ( C.replace i (Ack ack) (C.repeat (Ack False)) - , Data d + , Just d ) ) - NoData -> - (C.satSucc C.SatWrap i, (C.repeat (Ack False), NoData)) + Nothing -> + (C.satSucc C.SatWrap i, (C.repeat (Ack False), Nothing)) roundrobinCollect Parallel = Circuit (B.first C.unbundle . C.mealyB go NoData . B.first C.bundle) where go im (fwds, bwd@(Ack ack)) = (nextIm, (bwds, fwd)) where nextSrc = C.fold @(n C.- 1) (<|>) (C.zipWith (<$) C.indicesI fwds) - i = dataDefault (dataDefault maxBound nextSrc) im + i = fromMaybe (fromMaybe maxBound nextSrc) im bwds = C.replace i bwd (C.repeat (Ack False)) fwd = fwds C.!! i nextIm = - if noData fwd || not ack - then nextSrc - else im + if isJust fwd && ack + then im + else nextSrc -- | Place register on /forward/ part of a circuit. This adds combinational delay on the /backward/ path. registerFwd :: @@ -884,11 +821,11 @@ registerFwd :: (C.NFDataX a, C.HiddenClockResetEnable dom) => Circuit (Df dom a) (Df dom a) registerFwd = - forceResetSanity |> Circuit (C.mealyB go NoData) + forceResetSanity |> Circuit (C.mealyB go Nothing) where go s0 (iDat, Ack iAck) = (s1, (Ack oAck, s0)) where - oAck = Maybe.isNothing (dataToMaybe s0) || iAck + oAck = Maybe.isNothing s0 || iAck s1 = if oAck then iDat else s0 -- | Place register on /backward/ part of a circuit. This adds combinational delay on the /forward/ path. @@ -902,10 +839,10 @@ registerBwd = go (iDat, iAck) = (Ack <$> oAck, oDat) where oAck = C.regEn True valid (Coerce.coerce <$> iAck) - valid = (hasData <$> iDat) C..||. (fmap not oAck) - iDatX0 = fromData <$> iDat + valid = (Maybe.isJust <$> iDat) C..||. fmap not oAck + iDatX0 = C.fromJustX <$> iDat iDatX1 = C.regEn (C.errorX "registerBwd") oAck iDatX0 - oDat = toData <$> valid <*> (C.mux oAck iDatX0 iDatX1) + oDat = toMaybe <$> valid <*> C.mux oAck iDatX0 iDatX1 -- Fourmolu only allows CPP conditions on complete top-level definitions. This -- function is not exported. @@ -965,11 +902,11 @@ fifo fifoDepth = Circuit $ C.hideReset circuitFunction ) -- when reset is on, set state to initial state and output blank outputs - machineAsFunction _ (_, True, _, _) = (s0, (0, Nothing, Ack False, NoData)) + machineAsFunction _ (_, True, _, _) = (s0, (0, Nothing, Ack False, Nothing)) machineAsFunction (rAddr0, wAddr0, amtLeft0) (brRead0, False, pushData, Ack popped) = let -- potentially push an item onto blockram - maybePush = if amtLeft0 > 0 then dataToMaybe pushData else Nothing + maybePush = if amtLeft0 > 0 then pushData else Nothing brWrite = (wAddr0,) <$> maybePush -- adjust write address and amount left -- (output state machine doesn't see amountLeft') @@ -987,7 +924,7 @@ fifo fifoDepth = Circuit $ C.hideReset circuitFunction brReadAddr = rAddr1 -- return our new state and outputs otpAck = Maybe.isJust maybePush - otpDat = if amtLeft2 < maxBound then Data brRead1 else NoData + otpDat = if amtLeft2 < maxBound then Just brRead1 else Nothing in ((rAddr1, wAddr1, amtLeft3), (brReadAddr, brWrite, Ack otpAck, otpDat)) @@ -1020,13 +957,13 @@ drive SimulationConfig{resetCycles} s0 = where go _ resetN ~(ack : acks) | resetN > 0 = - NoData : (ack `C.seqX` go s0 (resetN - 1) acks) + Nothing : (ack `C.seqX` go s0 (resetN - 1) acks) go [] _ ~(ack : acks) = - NoData : (ack `C.seqX` go [] 0 acks) + Nothing : (ack `C.seqX` go [] 0 acks) go (Nothing : is) _ ~(ack : acks) = - NoData : (ack `C.seqX` go is 0 acks) + Nothing : (ack `C.seqX` go is 0 acks) go (Just dat : is) _ ~(Ack ack : acks) = - Data dat : go (if ack then is else Just dat : is) 0 acks + Just dat : go (if ack then is else Just dat : is) 0 acks {- | Sample protocol to a list of values. Drops values while reset is asserted. Not synthesizable. @@ -1040,15 +977,14 @@ sample :: Circuit () (Df dom b) -> [Maybe b] sample SimulationConfig{..} c = - fmap dataToMaybe $ - P.take timeoutAfter $ - CE.sample_lazy $ - ignoreWhileInReset $ - P.snd $ - toSignals c ((), Ack <$> rst_n) + P.take timeoutAfter $ + CE.sample_lazy $ + ignoreWhileInReset $ + P.snd $ + toSignals c ((), Ack <$> rst_n) where ignoreWhileInReset s = - (uncurry (bool NoData)) + uncurry (bool Nothing) <$> C.bundle (s, rst_n) rst_n = C.fromList (replicate resetCycles False <> repeat True) @@ -1091,10 +1027,10 @@ stall SimulationConfig{..} stallAck stalls = [StallAck] -> [Int] -> Int -> - Signal dom (Data a) -> + Signal dom (Maybe a) -> Signal dom Ack -> ( Signal dom Ack - , Signal dom (Data a) + , Signal dom (Maybe a) ) go [] ss rs fwd bwd = go stallAcks ss rs fwd bwd @@ -1102,19 +1038,19 @@ stall SimulationConfig{..} stallAck stalls = | resetN > 0 = B.bimap (b :-) (f :-) (go sas stalls (resetN - 1) fwd bwd) go (sa : sas) [] _ (f :- fwd) ~(b :- bwd) = - B.bimap (toStallAck (dataToMaybe f) b sa :-) (f :-) (go sas [] 0 fwd bwd) - go (sa : sas) ss _ (NoData :- fwd) ~(b :- bwd) = + B.bimap (toStallAck f b sa :-) (f :-) (go sas [] 0 fwd bwd) + go (sa : sas) ss _ (Nothing :- fwd) ~(b :- bwd) = -- Left hand side does not send data, simply replicate that behavior. Right -- hand side might send an arbitrary acknowledgement, so we simply pass it -- through. - B.bimap (toStallAck Nothing b sa :-) (NoData :-) (go sas ss 0 fwd bwd) + B.bimap (toStallAck Nothing b sa :-) (Nothing :-) (go sas ss 0 fwd bwd) go (_sa : sas) (s : ss) _ (f0 :- fwd) ~(Ack b0 :- bwd) = let -- Stall as long as s > 0. If s ~ 0, we wait for the RHS to acknowledge -- the data. As long as RHS does not acknowledge the data, we keep sending -- the same data. (f1, b1, s1) = case compare 0 s of - LT -> (NoData, Ack False, pred s : ss) -- s > 0 + LT -> (Nothing, Ack False, pred s : ss) -- s > 0 EQ -> (f0, Ack b0, if b0 then ss else s : ss) -- s ~ 0 GT -> error ("Unexpected negative stall: " <> show s) -- s < 0 in diff --git a/clash-protocols/src/Protocols/DfConv.hs b/clash-protocols/src/Protocols/DfConv.hs index cec2087d..5ea0ee13 100644 --- a/clash-protocols/src/Protocols/DfConv.hs +++ b/clash-protocols/src/Protocols/DfConv.hs @@ -112,7 +112,7 @@ import Protocols.Axi4.ReadData import Protocols.Axi4.WriteAddress import Protocols.Axi4.WriteData import Protocols.Axi4.WriteResponse -import Protocols.Df (Data (..), Df) +import Protocols.Df (Df) import qualified Protocols.Df as Df import Protocols.Internal import qualified Protocols.Vec as Vec @@ -213,15 +213,15 @@ toDfCircuitHelper _ s0 blankOtp stateFn = let rstLow = unsafeToActiveHigh reset in mealy transFn s0 ((,) <$> rstLow <*> inp) - transFn _ (True, _) = (s0, ((Ack False, NoData), blankOtp)) + transFn _ (True, _) = (s0, ((Ack False, Nothing), blankOtp)) transFn s (False, ((toOtp, Ack inpAck), inp)) = let ((otp, inputted, otpAck), s') = runState - (stateFn inp inpAck (Df.dataToMaybe toOtp)) + (stateFn inp inpAck toOtp) s in - (s', ((Ack otpAck, Df.maybeToData inputted), otp)) + (s', ((Ack otpAck, inputted), otp)) {- | Helper function to make it easier to implement 'fromDfCircuit' in 'DfConv'. 'Ack's are automatically converted to/from 'Bool's, and 'Df.Data's to/from @@ -280,7 +280,7 @@ instance (NFDataX dat) => DfConv (Df dom dat) where type FwdPayload (Df dom dat) = dat toDfCircuit _ = Circuit (uncurry f) where - f ~(a, _) c = ((c, P.pure NoData), a) + f ~(a, _) c = ((c, P.pure Nothing), a) fromDfCircuit _ = Circuit (uncurry f) where f a ~(b, _) = (b, (a, P.pure (Ack False))) @@ -372,7 +372,7 @@ instance (addrReceived, dataReceived) <- get put (addrReceived, dataReceived || _wready dataAck) P.pure - $ if (not addrReceived || dataReceived) + $ if not addrReceived || dataReceived then (M2S_NoWriteData, False) else ( M2S_WriteData @@ -550,7 +550,7 @@ instance ) succResizing :: (KnownNat n) => Index n -> Index (n + 1) - succResizing n = (resize n) + 1 + succResizing n = resize n + 1 sendData dfDatIn dataAck = do (burstLenLeft, readId) <- get @@ -576,7 +576,7 @@ dfToDfConvInp :: ) => Proxy df -> Circuit df (Df (Dom df) (FwdPayload df)) -dfToDfConvInp = mapCircuit id id P.fst (,P.pure NoData) . fromDfCircuit +dfToDfConvInp = mapCircuit id id P.fst (,P.pure Nothing) . fromDfCircuit -- | Convert 'DfConv' into a /one-way/ 'Df' port, at the data output end dfToDfConvOtp :: @@ -888,7 +888,7 @@ catMaybes :: Circuit dfA dfB catMaybes dfA dfB = fromDfCircuit dfA - |> tupCircuits (Df.catMaybes) idC + |> tupCircuits Df.catMaybes idC |> toDfCircuit dfB -- | Like 'Data.Maybe.mapMaybe' @@ -1392,7 +1392,7 @@ registerFwd :: Circuit dfA dfB registerFwd dfA dfB = fromDfCircuit dfA - |> tupCircuits (Df.registerFwd) idC + |> tupCircuits Df.registerFwd idC |> toDfCircuit dfB {- | Place register on /backward/ part of a circuit. This is implemented using @@ -1412,7 +1412,7 @@ registerBwd :: Circuit dfA dfB registerBwd dfA dfB = fromDfCircuit dfA - |> tupCircuits (Df.registerBwd) idC + |> tupCircuits Df.registerBwd idC |> toDfCircuit dfB -- | A fifo buffer with user-provided depth. Uses blockram to store data @@ -1435,7 +1435,6 @@ fifo dfA dfB fifoDepth = fromDfCircuit dfA |> tupCircuits (Df.fifo fifoDepth) idC |> toDfCircuit dfB - where {- | Emit values given in list. Emits no data while reset is asserted. Not synthesizable. @@ -1524,7 +1523,7 @@ simulate :: [Maybe (FwdPayload dfA)] -> -- | Outputs [Maybe (FwdPayload dfB)] -simulate dfA dfB conf circ inputs = Df.simulate conf circ' inputs +simulate dfA dfB conf circ = Df.simulate conf circ' where circ' clk rst en = withClockResetEnable clk rst en (dfToDfConvOtp dfA) @@ -1549,7 +1548,7 @@ dfConvTestBench :: Proxy dfA -> Proxy dfB -> [Bool] -> - [Data (BwdPayload dfB)] -> + [Maybe (BwdPayload dfB)] -> Circuit dfA dfB -> Circuit (Df (Dom dfA) (FwdPayload dfA)) @@ -1591,7 +1590,7 @@ dfConvTestBenchRev :: ) => Proxy dfA -> Proxy dfB -> - [Data (FwdPayload dfA)] -> + [Maybe (FwdPayload dfA)] -> [Bool] -> Circuit dfA dfB -> Circuit diff --git a/clash-protocols/tests/Tests/Protocols/Avalon.hs b/clash-protocols/tests/Tests/Protocols/Avalon.hs index c7f3d62c..5cc904b8 100644 --- a/clash-protocols/tests/Tests/Protocols/Avalon.hs +++ b/clash-protocols/tests/Tests/Protocols/Avalon.hs @@ -27,7 +27,6 @@ import Test.Tasty.TH (testGroupGenerator) import Protocols import Protocols.Avalon.MemMap import Protocols.Avalon.Stream -import qualified Protocols.Df as Df import qualified Protocols.DfConv as DfConv import Protocols.Hedgehog import Protocols.Internal @@ -107,7 +106,7 @@ prop_avalon_convert_manager_subordinate = Proxy Proxy (repeat True) - (repeat (Df.Data readImpt)) + (repeat (Just readImpt)) ckt ) where @@ -130,7 +129,7 @@ prop_avalon_convert_manager_subordinate_rev = DfConv.dfConvTestBenchRev Proxy Proxy - (repeat (Df.Data $ Left readReqImpt)) + (repeat (Just $ Left readReqImpt)) (repeat True) ckt ) @@ -155,7 +154,7 @@ prop_avalon_convert_subordinate_manager = Proxy Proxy (repeat True) - (repeat (Df.Data readImpt)) + (repeat (Just readImpt)) ckt ) where @@ -178,7 +177,7 @@ prop_avalon_convert_subordinate_manager_rev = DfConv.dfConvTestBenchRev Proxy Proxy - (repeat (Df.Data $ Left readReqImpt)) + (repeat (Just $ Left readReqImpt)) (repeat True) ckt ) diff --git a/clash-protocols/tests/Tests/Protocols/Axi4.hs b/clash-protocols/tests/Tests/Protocols/Axi4.hs index 9d4dfb68..4ca10e58 100644 --- a/clash-protocols/tests/Tests/Protocols/Axi4.hs +++ b/clash-protocols/tests/Tests/Protocols/Axi4.hs @@ -33,7 +33,6 @@ import Protocols.Axi4.Stream import Protocols.Axi4.WriteAddress import Protocols.Axi4.WriteData import Protocols.Axi4.WriteResponse -import qualified Protocols.Df as Df import qualified Protocols.DfConv as DfConv import Protocols.Hedgehog import Protocols.Internal @@ -66,7 +65,7 @@ prop_axi4_convert_write_id = Proxy Proxy (repeat True) - (repeat $ Df.Data (toKeepType ROkay, 0)) + (repeat $ Just (toKeepType ROkay, 0)) ckt ) where @@ -125,7 +124,7 @@ prop_axi4_convert_write_id = <*> (toKeepType <$> Gen.enumBounded) <*> DfTest.genSmallInt - genBurstLen = toKeepType <$> pure 0 + genBurstLen = pure (toKeepType 0) genBurst = toKeepType <$> (pure BmFixed C.<|> pure BmIncr C.<|> pure BmWrap) genStrobe = genVec $ pure Nothing C.<|> (Just <$> Gen.enumBounded) @@ -139,7 +138,7 @@ prop_axi4_convert_write_id_rev = DfConv.dfConvTestBenchRev Proxy Proxy - (repeat $ Df.Data fwdInfo) + (repeat $ Just fwdInfo) (repeat True) ckt ) @@ -206,7 +205,7 @@ prop_axi4_convert_read_id = Proxy Proxy (repeat True) - (repeat $ Df.Data (0, 0, toKeepType ROkay)) + (repeat $ Just (0, 0, toKeepType ROkay)) ckt ) where @@ -226,7 +225,7 @@ prop_axi4_convert_read_id = <$> Gen.enumBounded <*> Gen.enumBounded <*> (toKeepType <$> Gen.enumBounded) - <*> (Gen.integral (Range.linear 0 10)) + <*> Gen.integral (Range.linear 0 10) <*> ( toKeepType <$> ( pure Bs1 C.<|> pure Bs2 @@ -268,7 +267,7 @@ prop_axi4_convert_read_id_rev = DfConv.dfConvTestBenchRev Proxy Proxy - (repeat $ Df.Data fwdInfo) + (repeat $ Just fwdInfo) (repeat True) ckt ) @@ -343,9 +342,9 @@ prop_axi4_stream_fifo_id = genInfo = Axi4StreamM2S - <$> (genVec Gen.enumBounded) - <*> (genVec Gen.enumBounded) - <*> (genVec Gen.enumBounded) + <$> genVec Gen.enumBounded + <*> genVec Gen.enumBounded + <*> genVec Gen.enumBounded <*> Gen.enumBounded <*> Gen.enumBounded <*> Gen.enumBounded diff --git a/clash-protocols/tests/Tests/Protocols/Df.hs b/clash-protocols/tests/Tests/Protocols/Df.hs index 373ff9c7..54d6eda8 100644 --- a/clash-protocols/tests/Tests/Protocols/Df.hs +++ b/clash-protocols/tests/Tests/Protocols/Df.hs @@ -10,7 +10,6 @@ module Tests.Protocols.Df where -- base import Data.Coerce (coerce) import Data.Foldable (fold) -import Data.List (mapAccumL) import Data.Maybe (catMaybes, fromMaybe) import GHC.Stack (HasCallStack) import Prelude @@ -25,7 +24,7 @@ import qualified Data.HashMap.Strict as HashMap import qualified Data.HashSet as HashSet -- extra -import Data.List (partition, transpose) +import Data.List (mapAccumL, partition, transpose) -- deepseq import Control.DeepSeq (NFData) @@ -82,14 +81,12 @@ genSmallPlusInt = coerce <$> genSmallInt genData :: Gen a -> Gen [a] genData genA = do n <- genSmallInt - dat <- Gen.list (Range.singleton n) genA - pure dat + Gen.list (Range.singleton n) genA genVecData :: (C.KnownNat n, 1 <= n) => Gen a -> Gen (C.Vec n [a]) genVecData genA = do n <- genSmallInt - dat <- genVec (Gen.list (Range.singleton n) genA) - pure dat + genVec (Gen.list (Range.singleton n) genA) -- Same as 'idWithModel', but specialized on 'Df' idWithModelDf :: diff --git a/clash-protocols/tests/Tests/Protocols/DfConv.hs b/clash-protocols/tests/Tests/Protocols/DfConv.hs index 776ae787..fbd670cc 100644 --- a/clash-protocols/tests/Tests/Protocols/DfConv.hs +++ b/clash-protocols/tests/Tests/Protocols/DfConv.hs @@ -34,7 +34,6 @@ import Test.Tasty.TH (testGroupGenerator) -- clash-protocols (me!) import Protocols -import qualified Protocols.Df as Df import qualified Protocols.DfConv as DfConv import Protocols.Hedgehog import Protocols.Internal @@ -181,7 +180,7 @@ prop_select = ckt :: (C.HiddenClockResetEnable dom) => Circuit (C.Vec 3 (Df dom Int), Df dom (C.Index 3)) (Df dom Int) - ckt = DfConv.select (Proxy @(Df _ Int), (Proxy @(Df _ (C.Index 3)))) (Proxy @(Df _ Int)) + ckt = DfConv.select (Proxy @(Df _ Int), Proxy @(Df _ (C.Index 3))) (Proxy @(Df _ Int)) goModel :: C.Vec 3 [Int] -> C.Index 3 -> (C.Vec 3 [Int], Int) goModel vec ix = let (i : is) = vec C.!! ix in (C.replace ix is vec, i) @@ -220,7 +219,7 @@ prop_test_bench_id = Proxy Proxy (repeat True) - (repeat (Df.Data 0)) + (repeat (Just 0)) ckt ) where @@ -241,7 +240,7 @@ prop_test_bench_rev_id = DfConv.dfConvTestBenchRev Proxy Proxy - (repeat (Df.Data 0)) + (repeat (Just 0)) (repeat True) ckt ) From 53c02fa98660e09d0d257f1247e77bfb9c8a8ad4 Mon Sep 17 00:00:00 2001 From: t-wallet Date: Fri, 19 Jul 2024 11:17:58 +0200 Subject: [PATCH 2/5] fix sample_lazy eta reduction not working on ci --- clash-protocols/src/Protocols/Avalon/Stream.hs | 4 ++-- clash-protocols/src/Protocols/Axi4/Stream.hs | 4 ++-- clash-protocols/src/Protocols/Df.hs | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/clash-protocols/src/Protocols/Avalon/Stream.hs b/clash-protocols/src/Protocols/Avalon/Stream.hs index b55cc177..55e67a2e 100644 --- a/clash-protocols/src/Protocols/Avalon/Stream.hs +++ b/clash-protocols/src/Protocols/Avalon/Stream.hs @@ -211,8 +211,8 @@ instance simToSigFwd _ = fromList_lazy simToSigBwd _ = fromList_lazy - sigToSimFwd _ = sample_lazy - sigToSimBwd _ = sample_lazy + sigToSimFwd _ s = sample_lazy s + sigToSimBwd _ s = sample_lazy s stallC conf (head -> (stallAck, stalls)) = withClockResetEnable clockGen resetGen enableGen diff --git a/clash-protocols/src/Protocols/Axi4/Stream.hs b/clash-protocols/src/Protocols/Axi4/Stream.hs index 5ae6f366..01f7ee06 100644 --- a/clash-protocols/src/Protocols/Axi4/Stream.hs +++ b/clash-protocols/src/Protocols/Axi4/Stream.hs @@ -151,8 +151,8 @@ instance simToSigFwd _ = fromList_lazy simToSigBwd _ = fromList_lazy - sigToSimFwd _ = sample_lazy - sigToSimBwd _ = sample_lazy + sigToSimFwd _ s = sample_lazy s + sigToSimBwd _ s = sample_lazy s stallC conf (C.head -> (stallAck, stalls)) = withClockResetEnable clockGen resetGen enableGen $ diff --git a/clash-protocols/src/Protocols/Df.hs b/clash-protocols/src/Protocols/Df.hs index b2b17896..be47c4e6 100644 --- a/clash-protocols/src/Protocols/Df.hs +++ b/clash-protocols/src/Protocols/Df.hs @@ -174,8 +174,8 @@ instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom simToSigFwd _ = C.fromList_lazy simToSigBwd _ = C.fromList_lazy - sigToSimFwd _ = C.sample_lazy - sigToSimBwd _ = C.sample_lazy + sigToSimFwd _ s = C.sample_lazy s + sigToSimBwd _ s = C.sample_lazy s stallC conf (C.head -> (stallAck, stalls)) = stall conf stallAck stalls From 67eaa378c9eeaf4a10dd543d66d3dd33d25c6f9c Mon Sep 17 00:00:00 2001 From: t-wallet Date: Fri, 19 Jul 2024 11:42:22 +0200 Subject: [PATCH 3/5] Change README to use Maybe instead of Data --- README.md | 48 ++++++++++++++++++++---------------------------- 1 file changed, 20 insertions(+), 28 deletions(-) diff --git a/README.md b/README.md index bdeb1e9b..bb034d68 100644 --- a/README.md +++ b/README.md @@ -79,9 +79,9 @@ The protocols `Df` imposes a contract each component should follow. These are, w This invariant allows developers to insert arbitrary reset delays without worrying their design breaks. Caution should still be taken though, see [Note [Deasserting resets]](#note-deasserting-resets). -* When _Fwd a_ does not contain data (i.e., is `NoData`), its corresponding _Bwd a_ may contain any value, including an error/bottom. When driving a bottom, a component should use `errorX` to make sure it can be evaluated using `seqX`. Test harnesses in `Protocols.Hedgehog` occasionally drive `errorX "No defined Ack"` when seeing `NoData` to test this. +* When _Fwd a_ does not contain data (i.e., is `Nothing`), its corresponding _Bwd a_ may contain any value, including an error/bottom. When driving a bottom, a component should use `errorX` to make sure it can be evaluated using `seqX`. Test harnesses in `Protocols.Hedgehog` occasionally drive `errorX "No defined Ack"` when seeing `Nothing` to test this. -* A circuit driving `Data x` must keep driving the same value until it receives an acknowledgment. This is not yet checked by test harnesses. +* A circuit driving `Just x` must keep driving the same value until it receives an acknowledgment. This is not yet checked by test harnesses. ### Note [Deasserting resets] Care should be taken when deasserting resets. Given the following circuit: @@ -111,7 +111,7 @@ should be deasserted as follows: `a`, `b,` `c`, `d`/`e`, `f`. Resets might also This order is imposed by the fact that there is an invariant stating a component in reset must not acknowledge data while in reset, but there is - for performance reasons - no invariant stating a component must not send data while in reset. ## Tutorial: `catMaybes` -At this point you should have familiarized with the basic structures of the `Df`: its dataconstructors (`Data`, `NoData`, and `Ack`) and its invariants, as well as the structure of a `Circuit` itself. To quickly try things it's useful to keep a repl around. With `stack`: +At this point you should have familiarized with the basic structures of the `Df`: its dataconstructors (`Just`, `Nothing`, and `Ack`) and its invariants, as well as the structure of a `Circuit` itself. To quickly try things it's useful to keep a repl around. With `stack`: ``` stack exec --package clash-protocols ghci @@ -155,15 +155,7 @@ Then, we define the type and name of the component we'd like to write: catMaybes :: Circuit (Df dom (Maybe a)) (Df dom a) ``` -I.e., a circuit that takes a `Df` stream of `Maybe a` on the left hand side (LHS) and produces a stream of `a` on the right hand side (RHS). Note that the data carried on `Df`s _forward_ path very much looks like a `Maybe` in the first place: - -``` ->>> :kind! Fwd (Df C.System Int) -.. -= Signal "System" (Df.Data Int) -``` - -..because `Data Int` itself has two constructors: `Data Int` and `NoData`. In effect, we'd like squash `Data (Just a)` into `Data a`, and `Data Nothing` into `NoData`. Not unlike the way [join](https://hackage.haskell.org/package/base-4.14.0.0/docs/Control-Monad.html#v:join) would work on two `Maybe`s. +I.e., a circuit that takes a `Df` stream of `Maybe a` on the left hand side (LHS) and produces a stream of `a` on the right hand side (RHS). In effect, we'd like squash `Just (Just a)` into `Just a`, and `Just Nothing` into `Nothing`. Exactly like the way [join](https://hackage.haskell.org/package/base-4.14.0.0/docs/Control-Monad.html#v:join) would work on two `Maybe`s. As the types of `Circuit`s become quite verbose and complex quickly, I like to let GHC do the heavy lifting. For example, I would write: @@ -177,8 +169,8 @@ At this point, GHC will tell us: CatMaybes.hs:8:21: error: Variable not in scope: go - :: (C.Signal dom (Df.Data (Maybe a)), C.Signal dom (Df.Ack a)) - -> (C.Signal dom (Df.Ack (Maybe a)), C.Signal dom (Df.Data a)) + :: (C.Signal dom (Maybe (Maybe a)), C.Signal dom (Df.Ack a)) + -> (C.Signal dom (Df.Ack (Maybe a)), C.Signal dom (Maybe a)) | 8 | catMaybes = Circuit go | ^^ @@ -206,8 +198,8 @@ Now GHC will tell us: CatMaybes.hs:8:35: error: Variable not in scope: go - :: C.Signal dom (Df.Data (Maybe a), Df.Ack a) - -> C.Signal dom (Df.Ack (Maybe a), Df.Data a) + :: C.Signal dom (Maybe (Maybe a), Df.Ack a) + -> C.Signal dom (Df.Ack (Maybe a), Maybe a) | 8 | catMaybes = Circuit (C.unbundle . go . C.bundle) | ^^ @@ -225,30 +217,30 @@ after which GHC will tell us: CatMaybes.hs:8:40: error: Variable not in scope: go - :: (Df.Data (Maybe a), Df.Ack a) - -> (Df.Ack (Maybe a), Df.Data a) + :: (Maybe (Maybe a), Df.Ack a) + -> (Df.Ack (Maybe a), Maybe a) | 8 | catMaybes = Circuit (C.unbundle . fmap go . C.bundle) | ^^ ``` -This is something we can write, surely! If the LHS does not send data, there's not much we can do. We send `NoData` to the RHS and send a /nack/: +This is something we can write, surely! If the LHS does not send data, there's not much we can do. We send `Nothing` to the RHS and send a /nack/: ```haskell - go (Df.NoData, _) = (Df.Ack False, Df.NoData) + go (Nothing, _) = (Df.Ack False, Nothing) ``` -If we _do_ receive data from the LHS but it turns out to be _Nothing_, we'd like to acknowledge that we received the data and send `NoData` to the RHS: +If we _do_ receive data from the LHS but it turns out to be _Nothing_, we'd like to acknowledge that we received the data and send `Nothing` to the RHS: ```haskell -go (Df.Data Nothing, _) = (Df.Ack True, Df.NoData) +go (Just Nothing, _) = (Df.Ack True, Nothing) ``` Finally, if the LHS sends data and it turns out to be a _Just_, we'd like to acknowledge that we received it and pass it onto the RHS. But we should be careful, we should only acknowledge it if our RHS received our data! In effect, we can just passthrough the ack: ```haskell -go (Df.Data (Just d), Df.Ack ack) = (Df.Ack ack, Df.Data d) +go (Just (Just d), Df.Ack ack) = (Df.Ack ack, Just d) ``` ### Testing @@ -356,8 +348,8 @@ Writing a `Df` component can be tricky business. Even for relatively simple circ Let's introduce one: ```diff -- go (Df.Data Nothing, _) = (Df.Ack True, Df.NoData) -+ go (Df.Data Nothing, _) = (Df.Ack False, Df.NoData) +- go (Just Nothing, _) = (Df.Ack True, Nothing) ++ go (Just Nothing, _) = (Df.Ack False, Nothing) ``` Rerunning the tests will give us a big error, which starts out as: @@ -454,8 +446,8 @@ The test tells us that no output was sampled, even though it expected to sample Let's revert the "mistake" we made and make another: ```diff -- go (Df.Data (Just d), Df.Ack ack) = (Df.Ack ack, Df.Data d) -+ go (Df.Data (Just d), Df.Ack ack) = (Df.Ack True, Df.Data d) +- go (Just (Just d), Df.Ack ack) = (Df.Ack ack, Just d) ++ go (Just (Just d), Df.Ack ack) = (Df.Ack True, Just d) ``` Again, we get a pretty big error report. Let's skip right to the interesting bits: @@ -482,7 +474,7 @@ Circuit did not produce enough output. Expected 1 more values. Sampled only 0: [] ``` -In this case, Hedgehog pretty much constrained us to pretty much one case in our implementation: the one where it matches on `Df.Data (Just d)`. Weirdly, no backpressure was needed to trigger this error, but we still see dropped values. This usually means we generated an _ack_ while the reset was asserted. And sure enough, we don't check for this. (Note that the "right" implementation moved the responsibility of this problem to the component on the RHS, hence not failing.) +In this case, Hedgehog pretty much constrained us to pretty much one case in our implementation: the one where it matches on `Just (Just d)`. Weirdly, no backpressure was needed to trigger this error, but we still see dropped values. This usually means we generated an _ack_ while the reset was asserted. And sure enough, we don't check for this. (Note that the "right" implementation moved the responsibility of this problem to the component on the RHS, hence not failing.) At this point it might be tempting to use `Df.forceResetSanity` to force proper reset behavior. To do so, apply the patch: From 5a9fe260ea3f3187ae1892c2c180d623ea1ec76d Mon Sep 17 00:00:00 2001 From: t-wallet Date: Fri, 19 Jul 2024 12:02:27 +0200 Subject: [PATCH 4/5] Change docs as well --- .../src/Protocols/Plugin/Types.hs | 10 +- clash-protocols/src/Protocols/Df.hs | 9 +- clash-protocols/src/Protocols/DfConv.hs | 22 ++- clash-protocols/src/Protocols/Internal.hs | 162 +++++++++++++++++- 4 files changed, 174 insertions(+), 29 deletions(-) diff --git a/clash-protocols-base/src/Protocols/Plugin/Types.hs b/clash-protocols-base/src/Protocols/Plugin/Types.hs index bee4b8f6..45f7624c 100644 --- a/clash-protocols-base/src/Protocols/Plugin/Types.hs +++ b/clash-protocols-base/src/Protocols/Plugin/Types.hs @@ -83,11 +83,7 @@ synthesis domain the protocol will use. This is the same /dom/ as used in send. Again, this is similar to the /a/ in /Signal dom a/. As said previously, we'd like the sender to either send /no data/ or -/some data/. We can capture this in a data type very similar to /Maybe/: - -@ - data Data a = NoData | Data a -@ +/some data/. We can capture this in a /Maybe/. On the way back, we'd like to either acknowledge or not acknowledge sent data. Similar to /Bool/ we define: @@ -101,7 +97,7 @@ With these three definitions we're ready to make an instance for /Fwd/ and @ instance Protocol (Df dom a) where - type Fwd (Df dom a) = Signal dom (Data a) + type Fwd (Df dom a) = Signal dom (Maybe a) type Bwd (Df dom a) = Signal dom Ack @ @@ -116,7 +112,7 @@ instantiated with our types. The following: @ +-----------+ - Signal dom (Data a) | | Signal dom (Data b) + Signal dom (Maybe a) | | Signal dom (Maybe b) +------------------------>+ +-------------------------> | | | | diff --git a/clash-protocols/src/Protocols/Df.hs b/clash-protocols/src/Protocols/Df.hs index be47c4e6..9dfc50af 100644 --- a/clash-protocols/src/Protocols/Df.hs +++ b/clash-protocols/src/Protocols/Df.hs @@ -132,16 +132,11 @@ import Protocols.Internal >>> import qualified Data.Bifunctor as B -} -{- | Like 'Protocols.Df', but without metadata. - -__N.B.__: For performance reasons 'Protocols.Data' is strict on -its data field. That is, if 'Protocols.Data' is evaluated to WHNF, -its fields will be evaluated to WHNF too. --} +-- | Simple unidirectional valid-ready protocol. data Df (dom :: C.Domain) (a :: Type) instance Protocol (Df dom a) where - -- \| Forward part of simple dataflow: @Signal dom (Data meta a)@ + -- \| Forward part of simple dataflow: @Signal dom (Maybe a)@ type Fwd (Df dom a) = Signal dom (Maybe a) -- \| Backward part of simple dataflow: @Signal dom Bool@ diff --git a/clash-protocols/src/Protocols/DfConv.hs b/clash-protocols/src/Protocols/DfConv.hs index 5ea0ee13..4fb05273 100644 --- a/clash-protocols/src/Protocols/DfConv.hs +++ b/clash-protocols/src/Protocols/DfConv.hs @@ -151,8 +151,8 @@ class (Protocol df) => DfConv df where -- pipelining, etc. so that a circuit connected to the 'Df' end doesn't have -- to worry about all that. There are two Df channels, one for fwd data and -- one for bwd data, so data can be sent both ways at once. This circuit is - -- expected to follow all of the conventions of 'Df'; for example, 'Df.Data' - -- should stay the same between clock cycles unless acknowledged. + -- expected to follow all of the conventions of 'Df'; for example, data on the + -- fwd channel should stay the same between clock cycles unless acknowledged. toDfCircuit :: (HiddenClockResetEnable (Dom df)) => Proxy df -> @@ -174,10 +174,9 @@ class (Protocol df) => DfConv df where type FwdPayload df = () {- | Helper function to make it easier to implement 'toDfCircuit' in 'DfConv'. -'Ack's are automatically converted to/from 'Bool's, and 'Df.Data's to/from -'Maybe'. A default @otpMsg@ value is given for if reset is currently on. The -'State' machine is run every clock cycle. Parameters: initial state, default -@otpMsg@, and 'State' machine function +'Ack's are automatically converted to/from 'Bool's. A default @otpMsg@ value is +given for if reset is currently on. The 'State' machine is run every clock cycle. +Parameters: initial state, default @otpMsg@, and 'State' machine function -} toDfCircuitHelper :: ( HiddenClockResetEnable dom @@ -224,10 +223,9 @@ toDfCircuitHelper _ s0 blankOtp stateFn = (s', ((Ack otpAck, inputted), otp)) {- | Helper function to make it easier to implement 'fromDfCircuit' in 'DfConv'. -'Ack's are automatically converted to/from 'Bool's, and 'Df.Data's to/from -'Maybe'. A default @otpMsg@ value is given for if reset is currently on. The -'State' machine is run every clock cycle. Parameters: initial state, default -@otpMsg@, and 'State' machine function +'Ack's are automatically converted to/from 'Bool's. A default @otpMsg@ value is +given for if reset is currently on. The 'State' machine is run every clock cycle. +Parameters: initial state, default @otpMsg@, and 'State' machine function -} fromDfCircuitHelper :: ( HiddenClockResetEnable dom @@ -1533,7 +1531,7 @@ simulate dfA dfB conf circ = Df.simulate conf circ' {- | Given behavior along the backward channel, turn an arbitrary 'DfConv' circuit into an easily-testable 'Df' circuit representing the forward channel. Behavior along the backward channel is specified by a @[Bool]@ -(a list of acknowledges to provide), and a @[Data (BwdPayload dfB)]@ (a list +(a list of acknowledges to provide), and a @[Maybe (BwdPayload dfB)]@ (a list of data values to feed in). -} dfConvTestBench :: @@ -1576,7 +1574,7 @@ dfConvTestBench dfA dfB bwdAcks bwdPayload circ = {- | Given behavior along the forward channel, turn an arbitrary 'DfConv' circuit into an easily-testable 'Df' circuit representing the backward channel. Behavior along the forward channel is specified by a -@[Data (FwdPayload dfA)]@ (a list of data values to feed in), and a @[Bool]@ +@[Maybe (FwdPayload dfA)]@ (a list of data values to feed in), and a @[Bool]@ (a list of acknowledges to provide). -} dfConvTestBenchRev :: diff --git a/clash-protocols/src/Protocols/Internal.hs b/clash-protocols/src/Protocols/Internal.hs index d8962d4b..4a25bebd 100644 --- a/clash-protocols/src/Protocols/Internal.hs +++ b/clash-protocols/src/Protocols/Internal.hs @@ -190,6 +190,162 @@ prod2C (Circuit a) (Circuit c) = --------------------------------- SIMULATION ----------------------------------- +{- | Specifies option for simulation functions. Don't use this constructor +directly, as it may be extend with other options in the future. Use 'def' +instead. +-} +data SimulationConfig = SimulationConfig + { resetCycles :: Int + -- ^ Assert reset for a number of cycles before driving the protocol + -- + -- Default: 100 + , timeoutAfter :: Int + -- ^ Timeout after /n/ cycles. Only affects sample functions. + -- + -- Default: 'maxBound' + , ignoreReset :: Bool + -- ^ Ignore cycles while in reset (sampleC) + -- + -- Default: False + } + deriving (Show) + +instance Default SimulationConfig where + def = + SimulationConfig + { resetCycles = 100 + , timeoutAfter = maxBound + , ignoreReset = False + } + +{- | Determines what kind of acknowledgement signal 'stallC' will send when its +input component is not sending any data. Note that, in the Df protocol, +protocols may send arbitrary acknowledgement signals when this happens. +-} +data StallAck + = -- | Send Nack + StallWithNack + | -- | Send Ack + StallWithAck + | -- | Send @errorX "No defined ack"@ + StallWithErrorX + | -- | Passthrough acknowledgement of RHS component + StallTransparently + | -- | Cycle through all modes + StallCycle + deriving (Eq, Bounded, Enum, Show) + +{- | Class that defines how to /drive/, /sample/, and /stall/ a "Circuit" of +some shape. The "Backpressure" instance requires that the /backward/ type of the +circuit can be generated from a list of Booleans. +-} +class (C.KnownNat (SimulateChannels a), Backpressure a, Simulate a) => Drivable a where + -- TODO: documentatie verplaatsen + -- Type a /Circuit/ driver needs or sampler yields. For example: + -- + -- >>> :kind! (forall dom a. SimulateFwdType (Df dom a)) + -- ... + -- = [Maybe a] + -- + -- This means sampling a @Circuit () (Df dom a)@ with 'sampleC' yields + -- @[Maybe a]@. + + -- | Similar to 'SimulateFwdType', but without backpressure information. For + -- example: + -- + -- >>> :kind! (forall dom a. ExpectType (Df dom a)) + -- ... + -- = [a] + -- + -- Useful in situations where you only care about the "pure functionality" of + -- a circuit, not its timing information. Leveraged by various functions + -- in "Protocols.Hedgehog" and 'simulateCS'. + type ExpectType a :: Type + + -- | Convert a /ExpectType a/, a type representing data without backpressure, + -- into a type that does, /SimulateFwdType a/. + toSimulateType :: + -- | Type witness + Proxy a -> + -- | Expect type: input for a protocol /without/ stall information + ExpectType a -> + -- | Expect type: input for a protocol /with/ stall information + SimulateFwdType a + + -- | Convert a /ExpectType a/, a type representing data without backpressure, + -- into a type that does, /SimulateFwdType a/. + fromSimulateType :: + -- | Type witness + Proxy a -> + -- | Expect type: input for a protocol /with/ stall information + SimulateFwdType a -> + -- | Expect type: input for a protocol /without/ stall information + ExpectType a + + -- | Create a /driving/ circuit. Can be used in combination with 'sampleC' + -- to simulate a circuit. Related: 'simulateC'. + driveC :: + SimulationConfig -> + SimulateFwdType a -> + Circuit () a + + -- | Sample a circuit that is trivially drivable. Use 'driveC' to create + -- such a circuit. Related: 'simulateC'. + sampleC :: + SimulationConfig -> + Circuit () a -> + SimulateFwdType a + +{- | Defines functions necessary for implementation of the 'simulateCircuit' function. This +kind of simulation requires a lists for both the forward and the backward direction. + +This class requires the definition of the types that the test supplies and returns. Its +functions are converters from these /simulation types/ to types on the 'Signal' level. +The 'simulateCircuit' function can thus receive the necessary simulation types, convert +them to types on the 'Signal' level, pass those signals to the circuit, and convert the +result of the circuit back to the simulation types giving the final result. +-} +class (C.KnownNat (SimulateChannels a), Protocol a) => Simulate a where + -- | The type that a test must provide to the 'simulateCircuit' function in the forward direction. + -- Usually this is some sort of list. + type SimulateFwdType a :: Type + + -- | The type that a test must provide to the 'simulateCircuit' function in the backward direction. + -- Usually this is some sort of list + type SimulateBwdType a :: Type + + -- | The number of simulation channels this channel has after flattening it. + -- For example, @(Df dom a, Df dom a)@ has 2, while + -- @Vec 4 (Df dom a, Df dom a)@ has 8. + type SimulateChannels a :: C.Nat + + -- | Convert the forward simulation type to the 'Fwd' of @a@. + simToSigFwd :: Proxy a -> SimulateFwdType a -> Fwd a + + -- | Convert the backward simulation type to the 'Bwd' of @a@. + simToSigBwd :: Proxy a -> SimulateBwdType a -> Bwd a + + -- | Convert a signal of type @Bwd a@ to the backward simulation type. + sigToSimFwd :: Proxy a -> Fwd a -> SimulateFwdType a + + -- | Convert a signal of type @Fwd a@ to the forward simulation type. + sigToSimBwd :: Proxy a -> Bwd a -> SimulateBwdType a + + -- | Create a /stalling/ circuit. For each simulation channel (see + -- 'SimulateChannels') a tuple determines how the component stalls: + -- + -- * 'StallAck': determines how the backward (acknowledgement) channel + -- should behave whenever the component does not receive data from the + -- left hand side or when it's intentionally stalling. + -- + -- * A list of 'Int's that determine how many stall cycles to insert on + -- every cycle the left hand side component produces data. I.e., stalls + -- are /not/ inserted whenever the left hand side does /not/ produce data. + stallC :: + SimulationConfig -> + C.Vec (SimulateChannels a) (StallAck, [Int]) -> + Circuit a a + instance Simulate () where type SimulateFwdType () = () type SimulateBwdType () = () @@ -333,11 +489,11 @@ To figure out what input you need to supply, either solve the type >>> :kind! (forall dom a. SimulateFwdType (Df dom a)) ... -= [Protocols.Df.Data a] += [Maybe a] This would mean a @Circuit (Df dom a) (Df dom b)@ would need -@[Data a]@ as the last argument of 'simulateC' and would result in -@[Data b]@. Note that for this particular type you can neither supply +@[Maybe a]@ as the last argument of 'simulateC' and would result in +@[Maybe b]@. Note that for this particular type you can neither supply stalls nor introduce backpressure. If you want to to this use 'Df.stall'. -} simulateC :: From ccbfb1fea40faf1aa49fddc39e2fd01c41b6a50f Mon Sep 17 00:00:00 2001 From: Rowan Goemans Date: Thu, 8 May 2025 12:04:57 +0200 Subject: [PATCH 5/5] Fix rebase fallout of Df.Data -> Maybe migration --- .../src/Protocols/Avalon/Stream.hs | 1 - clash-protocols/src/Protocols/Axi4/Stream.hs | 5 +- clash-protocols/src/Protocols/Df.hs | 16 +- .../src/Protocols/Hedgehog/Internal.hs | 9 +- clash-protocols/src/Protocols/Internal.hs | 156 ------------------ .../src/Protocols/PacketStream/Base.hs | 8 +- .../Protocols/PacketStream/Depacketizers.hs | 13 +- .../src/Protocols/PacketStream/Packetizers.hs | 13 +- 8 files changed, 25 insertions(+), 196 deletions(-) diff --git a/clash-protocols/src/Protocols/Avalon/Stream.hs b/clash-protocols/src/Protocols/Avalon/Stream.hs index 55e67a2e..7d1d6616 100644 --- a/clash-protocols/src/Protocols/Avalon/Stream.hs +++ b/clash-protocols/src/Protocols/Avalon/Stream.hs @@ -252,7 +252,6 @@ instance ) => Test (AvalonStream dom conf dataType) where - expectToLengths Proxy = pure . P.length expectN Proxy = expectN (Proxy @(Df.Df dom _)) instance IdleCircuit (AvalonStream dom conf dataType) where diff --git a/clash-protocols/src/Protocols/Axi4/Stream.hs b/clash-protocols/src/Protocols/Axi4/Stream.hs index 01f7ee06..2dfafbb7 100644 --- a/clash-protocols/src/Protocols/Axi4/Stream.hs +++ b/clash-protocols/src/Protocols/Axi4/Stream.hs @@ -173,8 +173,8 @@ instance withClockResetEnable clockGen resetGen enableGen $ DfConv.drive Proxy conf vals sampleC conf ckt = - withClockResetEnable clockGen resetGen enableGen - $ DfConv.sample Proxy conf ckt + withClockResetEnable clockGen resetGen enableGen $ + DfConv.sample Proxy conf ckt instance ( KnownAxi4StreamConfig conf @@ -187,7 +187,6 @@ instance ) => Test (Axi4Stream dom conf userType) where - expectToLengths Proxy = pure . P.length expectN Proxy = expectN (Proxy @(Df.Df dom _)) instance IdleCircuit (Axi4Stream dom conf userType) where diff --git a/clash-protocols/src/Protocols/Df.hs b/clash-protocols/src/Protocols/Df.hs index 9dfc50af..2a0fd113 100644 --- a/clash-protocols/src/Protocols/Df.hs +++ b/clash-protocols/src/Protocols/Df.hs @@ -154,14 +154,6 @@ toMaybe :: Bool -> a -> Maybe a toMaybe False _ = Nothing toMaybe True a = Just a -{- | - If the t'Data' is v'NoData', it returns the given value; otherwise, - it returns the value contained in the v'Data'. --} -dataDefault :: a -> Data a -> a -dataDefault a NoData = a -dataDefault _ (Data a) = a - instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom a) where type SimulateFwdType (Df dom a) = [Maybe a] type SimulateBwdType (Df dom a) = [Ack] @@ -339,7 +331,7 @@ const b = -- | Never produce a value. empty :: Circuit () (Df dom a) -empty = Circuit (P.const ((), P.pure NoData)) +empty = Circuit (P.const ((), P.pure Nothing)) -- | Drive a constant value composed of /a/. pure :: a -> Circuit () (Df dom a) @@ -795,18 +787,18 @@ roundrobinCollect Skip = Nothing -> (C.satSucc C.SatWrap i, (C.repeat (Ack False), Nothing)) roundrobinCollect Parallel = - Circuit (B.first C.unbundle . C.mealyB go NoData . B.first C.bundle) + Circuit (B.first C.unbundle . C.mealyB go Nothing . B.first C.bundle) where go im (fwds, bwd@(Ack ack)) = (nextIm, (bwds, fwd)) where nextSrc = C.fold @(n C.- 1) (<|>) (C.zipWith (<$) C.indicesI fwds) - i = fromMaybe (fromMaybe maxBound nextSrc) im + i = Maybe.fromMaybe (Maybe.fromMaybe maxBound nextSrc) im bwds = C.replace i bwd (C.repeat (Ack False)) fwd = fwds C.!! i nextIm = - if isJust fwd && ack + if Maybe.isJust fwd && ack then im else nextSrc diff --git a/clash-protocols/src/Protocols/Hedgehog/Internal.hs b/clash-protocols/src/Protocols/Hedgehog/Internal.hs index 2a2df4f8..60bfe4f8 100644 --- a/clash-protocols/src/Protocols/Hedgehog/Internal.hs +++ b/clash-protocols/src/Protocols/Hedgehog/Internal.hs @@ -21,7 +21,6 @@ import Prelude -- clash-protocols import Protocols -import qualified Protocols.Df as Df import Protocols.Hedgehog.Types import Protocols.Internal.TH @@ -59,12 +58,12 @@ instance (TestType a, C.KnownDomain dom) => Test (Df dom a) where (HasCallStack, H.MonadTest m) => Proxy (Df dom a) -> ExpectOptions -> - [Df.Data a] -> + [Maybe a] -> m [a] expectN Proxy (ExpectOptions{eoSampleMax, eoStopAfterEmpty}) sampled = do go eoSampleMax eoStopAfterEmpty sampled where - go :: (HasCallStack) => Int -> Int -> [Df.Data a] -> m [a] + go :: (HasCallStack) => Int -> Int -> [Maybe a] -> m [a] go _timeout _n [] = -- This really should not happen, protocols should produce data indefinitely error "unexpected end of signal" @@ -80,10 +79,10 @@ instance (TestType a, C.KnownDomain dom) => Test (Df dom a) where go _ 0 _ = -- Saw enough valid samples, return to user pure [] - go sampleTimeout _emptyTimeout (Df.Data a : as) = + go sampleTimeout _emptyTimeout (Just a : as) = -- Valid sample (a :) <$> go (sampleTimeout - 1) eoStopAfterEmpty as - go sampleTimeout emptyTimeout (Df.NoData : as) = + go sampleTimeout emptyTimeout (Nothing : as) = -- Empty sample go sampleTimeout (emptyTimeout - 1) as diff --git a/clash-protocols/src/Protocols/Internal.hs b/clash-protocols/src/Protocols/Internal.hs index 4a25bebd..27c1095c 100644 --- a/clash-protocols/src/Protocols/Internal.hs +++ b/clash-protocols/src/Protocols/Internal.hs @@ -190,162 +190,6 @@ prod2C (Circuit a) (Circuit c) = --------------------------------- SIMULATION ----------------------------------- -{- | Specifies option for simulation functions. Don't use this constructor -directly, as it may be extend with other options in the future. Use 'def' -instead. --} -data SimulationConfig = SimulationConfig - { resetCycles :: Int - -- ^ Assert reset for a number of cycles before driving the protocol - -- - -- Default: 100 - , timeoutAfter :: Int - -- ^ Timeout after /n/ cycles. Only affects sample functions. - -- - -- Default: 'maxBound' - , ignoreReset :: Bool - -- ^ Ignore cycles while in reset (sampleC) - -- - -- Default: False - } - deriving (Show) - -instance Default SimulationConfig where - def = - SimulationConfig - { resetCycles = 100 - , timeoutAfter = maxBound - , ignoreReset = False - } - -{- | Determines what kind of acknowledgement signal 'stallC' will send when its -input component is not sending any data. Note that, in the Df protocol, -protocols may send arbitrary acknowledgement signals when this happens. --} -data StallAck - = -- | Send Nack - StallWithNack - | -- | Send Ack - StallWithAck - | -- | Send @errorX "No defined ack"@ - StallWithErrorX - | -- | Passthrough acknowledgement of RHS component - StallTransparently - | -- | Cycle through all modes - StallCycle - deriving (Eq, Bounded, Enum, Show) - -{- | Class that defines how to /drive/, /sample/, and /stall/ a "Circuit" of -some shape. The "Backpressure" instance requires that the /backward/ type of the -circuit can be generated from a list of Booleans. --} -class (C.KnownNat (SimulateChannels a), Backpressure a, Simulate a) => Drivable a where - -- TODO: documentatie verplaatsen - -- Type a /Circuit/ driver needs or sampler yields. For example: - -- - -- >>> :kind! (forall dom a. SimulateFwdType (Df dom a)) - -- ... - -- = [Maybe a] - -- - -- This means sampling a @Circuit () (Df dom a)@ with 'sampleC' yields - -- @[Maybe a]@. - - -- | Similar to 'SimulateFwdType', but without backpressure information. For - -- example: - -- - -- >>> :kind! (forall dom a. ExpectType (Df dom a)) - -- ... - -- = [a] - -- - -- Useful in situations where you only care about the "pure functionality" of - -- a circuit, not its timing information. Leveraged by various functions - -- in "Protocols.Hedgehog" and 'simulateCS'. - type ExpectType a :: Type - - -- | Convert a /ExpectType a/, a type representing data without backpressure, - -- into a type that does, /SimulateFwdType a/. - toSimulateType :: - -- | Type witness - Proxy a -> - -- | Expect type: input for a protocol /without/ stall information - ExpectType a -> - -- | Expect type: input for a protocol /with/ stall information - SimulateFwdType a - - -- | Convert a /ExpectType a/, a type representing data without backpressure, - -- into a type that does, /SimulateFwdType a/. - fromSimulateType :: - -- | Type witness - Proxy a -> - -- | Expect type: input for a protocol /with/ stall information - SimulateFwdType a -> - -- | Expect type: input for a protocol /without/ stall information - ExpectType a - - -- | Create a /driving/ circuit. Can be used in combination with 'sampleC' - -- to simulate a circuit. Related: 'simulateC'. - driveC :: - SimulationConfig -> - SimulateFwdType a -> - Circuit () a - - -- | Sample a circuit that is trivially drivable. Use 'driveC' to create - -- such a circuit. Related: 'simulateC'. - sampleC :: - SimulationConfig -> - Circuit () a -> - SimulateFwdType a - -{- | Defines functions necessary for implementation of the 'simulateCircuit' function. This -kind of simulation requires a lists for both the forward and the backward direction. - -This class requires the definition of the types that the test supplies and returns. Its -functions are converters from these /simulation types/ to types on the 'Signal' level. -The 'simulateCircuit' function can thus receive the necessary simulation types, convert -them to types on the 'Signal' level, pass those signals to the circuit, and convert the -result of the circuit back to the simulation types giving the final result. --} -class (C.KnownNat (SimulateChannels a), Protocol a) => Simulate a where - -- | The type that a test must provide to the 'simulateCircuit' function in the forward direction. - -- Usually this is some sort of list. - type SimulateFwdType a :: Type - - -- | The type that a test must provide to the 'simulateCircuit' function in the backward direction. - -- Usually this is some sort of list - type SimulateBwdType a :: Type - - -- | The number of simulation channels this channel has after flattening it. - -- For example, @(Df dom a, Df dom a)@ has 2, while - -- @Vec 4 (Df dom a, Df dom a)@ has 8. - type SimulateChannels a :: C.Nat - - -- | Convert the forward simulation type to the 'Fwd' of @a@. - simToSigFwd :: Proxy a -> SimulateFwdType a -> Fwd a - - -- | Convert the backward simulation type to the 'Bwd' of @a@. - simToSigBwd :: Proxy a -> SimulateBwdType a -> Bwd a - - -- | Convert a signal of type @Bwd a@ to the backward simulation type. - sigToSimFwd :: Proxy a -> Fwd a -> SimulateFwdType a - - -- | Convert a signal of type @Fwd a@ to the forward simulation type. - sigToSimBwd :: Proxy a -> Bwd a -> SimulateBwdType a - - -- | Create a /stalling/ circuit. For each simulation channel (see - -- 'SimulateChannels') a tuple determines how the component stalls: - -- - -- * 'StallAck': determines how the backward (acknowledgement) channel - -- should behave whenever the component does not receive data from the - -- left hand side or when it's intentionally stalling. - -- - -- * A list of 'Int's that determine how many stall cycles to insert on - -- every cycle the left hand side component produces data. I.e., stalls - -- are /not/ inserted whenever the left hand side does /not/ produce data. - stallC :: - SimulationConfig -> - C.Vec (SimulateChannels a) (StallAck, [Int]) -> - Circuit a a - instance Simulate () where type SimulateFwdType () = () type SimulateBwdType () = () diff --git a/clash-protocols/src/Protocols/PacketStream/Base.hs b/clash-protocols/src/Protocols/PacketStream/Base.hs index c5c31016..54f5e97d 100644 --- a/clash-protocols/src/Protocols/PacketStream/Base.hs +++ b/clash-protocols/src/Protocols/PacketStream/Base.hs @@ -227,7 +227,7 @@ instance DfConv.DfConv (PacketStream dom dataWidth meta) where ( fmap coerce bwdIn , pure (deepErrorX "PacketStream toDfCircuit: undefined") ) - , Df.dataToMaybe <$> P.fst fwdIn + , P.fst fwdIn ) fromDfCircuit _ = fromSignals go @@ -235,7 +235,7 @@ instance DfConv.DfConv (PacketStream dom dataWidth meta) where go (fwdIn, bwdIn) = ( coerce <$> P.fst bwdIn , - ( fmap Df.maybeToData fwdIn + ( fwdIn , pure (deepErrorX "PacketStream fromDfCircuit: undefined") ) ) @@ -289,9 +289,7 @@ instance Test (PacketStream dom dataWidth meta) where expectN Proxy options sampled = - expectN (Proxy @(Df.Df dom _)) options - $ Df.maybeToData - <$> sampled + expectN (Proxy @(Df.Df dom _)) options sampled {- | Undefined PacketStream null byte. Will throw an error if evaluated. The source diff --git a/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs b/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs index 735a6920..c1ba9094 100644 --- a/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs +++ b/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs @@ -21,7 +21,6 @@ import Clash.Prelude import Clash.Sized.Vector.Extra import Protocols -import qualified Protocols.Df as Df import Protocols.PacketStream.Base import Data.Constraint (Dict (Dict)) @@ -282,8 +281,8 @@ depacketizeToDfT :: (header -> meta -> a) -> DfDepacketizerState headerBytes dataWidth -> (Maybe (PacketStreamM2S dataWidth meta), Ack) -> - (DfDepacketizerState headerBytes dataWidth, (PacketStreamS2M, Df.Data a)) -depacketizeToDfT _ DfParse{..} (Just (PacketStreamM2S{..}), _) = (nextStOut, (PacketStreamS2M readyOut, Df.NoData)) + (DfDepacketizerState headerBytes dataWidth, (PacketStreamS2M, Maybe a)) +depacketizeToDfT _ DfParse{..} (Just (PacketStreamM2S{..}), _) = (nextStOut, (PacketStreamS2M readyOut, Nothing)) where nextAborted = _dfAborted || _abort nextParseBuf = fst (shiftInAtN _dfParseBuf _data) @@ -312,12 +311,12 @@ depacketizeToDfT toOut st@DfConsumePadding{..} (Just (PacketStreamM2S{..}), Ack (nextSt, fwdOut) = if isJust _last - then (def, if nextAborted then Df.NoData else Df.Data outDf) - else (st{_dfAborted = nextAborted}, Df.NoData) + then (def, if nextAborted then Nothing else Just outDf) + else (st{_dfAborted = nextAborted}, Nothing) - readyOut = isNothing (Df.dataToMaybe fwdOut) || readyIn + readyOut = isNothing fwdOut || readyIn nextStOut = if readyOut then nextSt else st -depacketizeToDfT _ st (Nothing, Ack readyIn) = (st, (PacketStreamS2M readyIn, Df.NoData)) +depacketizeToDfT _ st (Nothing, Ack readyIn) = (st, (PacketStreamS2M readyIn, Nothing)) {- | Reads bytes at the start of each packet into a header structure, and diff --git a/clash-protocols/src/Protocols/PacketStream/Packetizers.hs b/clash-protocols/src/Protocols/PacketStream/Packetizers.hs index d35fe927..3ea4281e 100644 --- a/clash-protocols/src/Protocols/PacketStream/Packetizers.hs +++ b/clash-protocols/src/Protocols/PacketStream/Packetizers.hs @@ -19,7 +19,6 @@ module Protocols.PacketStream.Packetizers ( import Clash.Prelude import Protocols -import qualified Protocols.Df as Df import Protocols.PacketStream.Base import Clash.Sized.Vector.Extra (takeLe) @@ -366,11 +365,11 @@ packetizeFromDfT :: -- | Mapping from `Df` input to the header that will be packetized (a -> header) -> DfPacketizerState metaOut headerBytes dataWidth -> - (Df.Data a, PacketStreamS2M) -> + (Maybe a, PacketStreamS2M) -> ( DfPacketizerState metaOut headerBytes dataWidth , (Ack, Maybe (PacketStreamM2S dataWidth metaOut)) ) -packetizeFromDfT toMetaOut toHeader DfIdle (Df.Data dataIn, bwdIn) = (nextStOut, (Ack False, Just outPkt)) +packetizeFromDfT toMetaOut toHeader DfIdle (Just dataIn, bwdIn) = (nextStOut, (Ack False, Just outPkt)) where (dataOut, hdrBuf) = splitAt (SNat @dataWidth) (bitCoerce (toHeader dataIn)) outPkt = PacketStreamM2S dataOut Nothing (toMetaOut dataIn) False @@ -378,7 +377,7 @@ packetizeFromDfT toMetaOut toHeader DfIdle (Df.Data dataIn, bwdIn) = (nextStOut, -- fwdIn is always Data in this state, because we assert backpressure in Idle before we go here -- Thus, we don't need to store the metadata in the state. -packetizeFromDfT toMetaOut _ st@DfInsert{..} (Df.Data dataIn, bwdIn) = (nextStOut, (bwdOut, Just outPkt)) +packetizeFromDfT toMetaOut _ st@DfInsert{..} (Just dataIn, bwdIn) = (nextStOut, (bwdOut, Just outPkt)) where (dataOut, newHdrBuf) = splitAt (SNat @dataWidth) (_dfHdrBuf ++ repeat @dataWidth (nullByte "packetizeFromDfT")) @@ -391,7 +390,7 @@ packetizeFromDfT toMetaOut _ st@DfInsert{..} (Df.Data dataIn, bwdIn) = (nextStOu bwdOut = Ack (_ready bwdIn && _dfCounter == maxBound) nextSt = if _dfCounter == maxBound then DfIdle else DfInsert (succ _dfCounter) newHdrBuf nextStOut = if _ready bwdIn then nextSt else st -packetizeFromDfT _ _ s (Df.NoData, bwdIn) = (s, (Ack (_ready bwdIn), Nothing)) +packetizeFromDfT _ _ s (Nothing, bwdIn) = (s, (Ack (_ready bwdIn), Nothing)) {- | Starts a packet stream upon receiving some data over a `Df` channel. @@ -425,8 +424,8 @@ packetizeFromDfC toMetaOut toHeader = case strictlyPositiveDivRu @headerBytes @d -- the entire payload in one clock cycle. SNatLE -> Circuit (unbundle . fmap go . bundle) where - go (Df.NoData, _) = (Ack False, Nothing) - go (Df.Data dataIn, bwdIn) = (Ack (_ready bwdIn), Just outPkt) + go (Nothing, _) = (Ack False, Nothing) + go (Just dataIn, bwdIn) = (Ack (_ready bwdIn), Just outPkt) where outPkt = PacketStreamM2S dataOut (Just l) (toMetaOut dataIn) False dataOut =