diff --git a/clash-protocols/clash-protocols.cabal b/clash-protocols/clash-protocols.cabal index 00386f30..6143620d 100644 --- a/clash-protocols/clash-protocols.cabal +++ b/clash-protocols/clash-protocols.cabal @@ -116,6 +116,7 @@ library , clash-protocols-base , circuit-notation , clash-prelude-hedgehog + , constraints , data-default ^>= 0.7.1.1 , deepseq , extra @@ -144,6 +145,16 @@ library Protocols.Axi4.WriteAddress Protocols.Axi4.WriteData Protocols.Axi4.WriteResponse + Protocols.PacketStream + Protocols.PacketStream.Base + Protocols.PacketStream.AsyncFifo + Protocols.PacketStream.Converters + Protocols.PacketStream.Depacketizers + Protocols.PacketStream.Hedgehog + Protocols.PacketStream.PacketFifo + Protocols.PacketStream.Packetizers + Protocols.PacketStream.Padding + Protocols.PacketStream.Routing Protocols.Df Protocols.DfConv Protocols.Hedgehog @@ -166,6 +177,9 @@ library autogen-modules: Paths_clash_protocols other-modules: + Data.Constraint.Nat.Extra + Data.Maybe.Extra + Clash.Sized.Vector.Extra Paths_clash_protocols Protocols.Hedgehog.Types Protocols.Internal.Types @@ -179,6 +193,7 @@ test-suite unittests ghc-options: -threaded -with-rtsopts=-N main-is: unittests.hs other-modules: + Tests.Haxioms Tests.Protocols Tests.Protocols.Df Tests.Protocols.DfConv @@ -187,6 +202,16 @@ test-suite unittests Tests.Protocols.Plugin Tests.Protocols.Vec Tests.Protocols.Wishbone + Tests.Protocols.PacketStream + Tests.Protocols.PacketStream.AsyncFifo + Tests.Protocols.PacketStream.Base + Tests.Protocols.PacketStream.Converters + Tests.Protocols.PacketStream.Depacketizers + Tests.Protocols.PacketStream.Packetizers + Tests.Protocols.PacketStream.PacketFifo + Tests.Protocols.PacketStream.Padding + Tests.Protocols.PacketStream.Routing + Util build-depends: diff --git a/clash-protocols/src/Clash/Sized/Vector/Extra.hs b/clash-protocols/src/Clash/Sized/Vector/Extra.hs new file mode 100644 index 00000000..7ba97c79 --- /dev/null +++ b/clash-protocols/src/Clash/Sized/Vector/Extra.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE NoImplicitPrelude #-} + +module Clash.Sized.Vector.Extra ( + dropLe, + takeLe, +) where + +import Clash.Prelude + +-- | Like 'drop' but uses a 'Data.Type.Ord.<=' constraint +dropLe :: + forall + (n :: Nat) + (m :: Nat) + (a :: Type). + (n <= m) => + -- | How many elements to take + SNat n -> + -- | input vector + Vec m a -> + Vec (m - n) a +dropLe SNat vs = leToPlus @n @m $ dropI vs + +-- | Like 'take' but uses a 'Data.Type.Ord.<=' constraint +takeLe :: + forall + (n :: Nat) + (m :: Nat) + (a :: Type). + (n <= m) => + -- | How many elements to take + SNat n -> + -- | input vector + Vec m a -> + Vec n a +takeLe SNat vs = leToPlus @n @m $ takeI vs diff --git a/clash-protocols/src/Data/Constraint/Nat/Extra.hs b/clash-protocols/src/Data/Constraint/Nat/Extra.hs new file mode 100644 index 00000000..d80a5e80 --- /dev/null +++ b/clash-protocols/src/Data/Constraint/Nat/Extra.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} + +{- +NOTE [constraint solver addition] + +The functions in this module enable us introduce trivial constraints that are not +solved by the constraint solver. +-} +module Data.Constraint.Nat.Extra where + +import Clash.Prelude +import Data.Constraint +import Unsafe.Coerce (unsafeCoerce) + +{- | Postulates that multiplying some number /a/ by some constant /b/, and +subsequently dividing that result by /b/ equals /a/. +-} +cancelMulDiv :: forall a b. (1 <= b) => Dict (DivRU (a * b) b ~ a) +cancelMulDiv = unsafeCoerce (Dict :: Dict (0 ~ 0)) + +-- | if (1 <= b) then (Mod a b + 1 <= b) +leModulusDivisor :: forall a b. (1 <= b) => Dict (Mod a b + 1 <= b) +leModulusDivisor = unsafeCoerce (Dict :: Dict (0 <= 0)) + +-- | if (1 <= a) and (1 <= b) then (1 <= DivRU a b) +strictlyPositiveDivRu :: forall a b. (1 <= a, 1 <= b) => Dict (1 <= DivRU a b) +strictlyPositiveDivRu = unsafeCoerce (Dict :: Dict (0 <= 0)) + +-- | if (1 <= a) then (b <= ceil(b/a) * a) +leTimesDivRu :: forall a b. (1 <= a) => Dict (b <= a * DivRU b a) +leTimesDivRu = unsafeCoerce (Dict :: Dict (0 <= 0)) + +-- | if (1 <= a) then (a * ceil(b/a) ~ b + Mod (a - Mod b a) a) +eqTimesDivRu :: forall a b. (1 <= a) => Dict (a * DivRU b a ~ b + Mod (a - Mod b a) a) +eqTimesDivRu = unsafeCoerce (Dict :: Dict (0 ~ 0)) diff --git a/clash-protocols/src/Data/Maybe/Extra.hs b/clash-protocols/src/Data/Maybe/Extra.hs new file mode 100644 index 00000000..dd22dc40 --- /dev/null +++ b/clash-protocols/src/Data/Maybe/Extra.hs @@ -0,0 +1,8 @@ +module Data.Maybe.Extra ( + toMaybe, +) where + +-- | Wrap a value in a @Just@ if @True@ +toMaybe :: Bool -> a -> Maybe a +toMaybe True x = Just x +toMaybe False _ = Nothing diff --git a/clash-protocols/src/Protocols/Df.hs b/clash-protocols/src/Protocols/Df.hs index 29eddc56..73c14079 100644 --- a/clash-protocols/src/Protocols/Df.hs +++ b/clash-protocols/src/Protocols/Df.hs @@ -804,16 +804,18 @@ roundrobin = in (i1, (Ack ack, datOut1)) --- | Collect mode in 'roundrobinCollect' +-- | Collect modes for dataflow arbiters. data CollectMode - = -- | Collect in a /roundrobin/ fashion. If a component does not produce - -- data, wait until it does. + = -- | Collect in a /round-robin/ fashion. If a source does not produce + -- data, wait until it does. Use with care, as there is a risk of + -- starvation if a selected source is idle for a long time. NoSkip - | -- | Collect in a /roundrobin/ fashion. If a component does not produce - -- data, skip it and check the next component on the next cycle. + | -- | Collect in a /round-robin/ fashion. If a source does not produce + -- data, skip it and check the next source on the next cycle. Skip - | -- | Check all components in parallel. Biased towards the /last/ Df - -- channel. + | -- | Check all sources in parallel. Biased towards the /last/ source. + -- If the number of sources is high, this is more expensive than other + -- modes. Parallel {- | Opposite of 'roundrobin'. Useful to collect data from workers that only diff --git a/clash-protocols/src/Protocols/DfConv.hs b/clash-protocols/src/Protocols/DfConv.hs index 02652a6c..cec2087d 100644 --- a/clash-protocols/src/Protocols/DfConv.hs +++ b/clash-protocols/src/Protocols/DfConv.hs @@ -1212,7 +1212,7 @@ fanout :: , FwdPayload dfA ~ FwdPayload dfB , NFDataX (FwdPayload dfA) , KnownNat numB - , numB ~ (decNumB + 1) + , 1 <= numB ) => Proxy dfA -> Proxy dfB -> diff --git a/clash-protocols/src/Protocols/Internal.hs b/clash-protocols/src/Protocols/Internal.hs index aa36ef07..34ef214e 100644 --- a/clash-protocols/src/Protocols/Internal.hs +++ b/clash-protocols/src/Protocols/Internal.hs @@ -306,7 +306,7 @@ instance (C.KnownDomain dom) => Simulate (CSignal dom a) where type SimulateChannels (CSignal dom a) = 1 simToSigFwd Proxy list = C.fromList_lazy list - simToSigBwd Proxy () = def + simToSigBwd Proxy () = pure () sigToSimFwd Proxy sig = C.sample_lazy sig sigToSimBwd Proxy _ = () @@ -324,7 +324,7 @@ instance (C.NFDataX a, C.ShowX a, Show a, C.KnownDomain dom) => Drivable (CSigna in Circuit (\_ -> ((), fwd1)) sampleC SimulationConfig{resetCycles, ignoreReset} (Circuit f) = - let sampled = CE.sample_lazy (snd (f ((), def))) + let sampled = CE.sample_lazy (snd (f ((), pure ()))) in if ignoreReset then drop resetCycles sampled else sampled {- | Simulate a circuit. Includes samples while reset is asserted. diff --git a/clash-protocols/src/Protocols/PacketStream.hs b/clash-protocols/src/Protocols/PacketStream.hs new file mode 100644 index 00000000..45e63999 --- /dev/null +++ b/clash-protocols/src/Protocols/PacketStream.hs @@ -0,0 +1,48 @@ +{- | +Copyright : (C) 2024, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +Provides the PacketStream protocol, a simple streaming protocol for transferring packets of data between components. + +Apart from the protocol definition, some components, all of which are generic in @dataWidth@, are also provided: + +1. Several small utilities such as filtering a stream based on its metadata. +2. Fifos +3. Components which upsize or downsize @dataWidth@ +4. Components which read from the stream (depacketizers) +5. Components which write to the stream (packetizers) +6. Components which split and merge a stream based on its metadata +-} +module Protocols.PacketStream ( + module Protocols.PacketStream.Base, + + -- * Fifos + module Protocols.PacketStream.PacketFifo, + module Protocols.PacketStream.AsyncFifo, + + -- * Converters + module Protocols.PacketStream.Converters, + + -- * Depacketizers + module Protocols.PacketStream.Depacketizers, + + -- * Packetizers + module Protocols.PacketStream.Packetizers, + + -- * Padding removal + module Protocols.PacketStream.Padding, + + -- * Routing components + module Protocols.PacketStream.Routing, +) +where + +import Protocols.PacketStream.AsyncFifo +import Protocols.PacketStream.Base +import Protocols.PacketStream.Converters +import Protocols.PacketStream.Depacketizers +import Protocols.PacketStream.PacketFifo +import Protocols.PacketStream.Packetizers +import Protocols.PacketStream.Padding +import Protocols.PacketStream.Routing diff --git a/clash-protocols/src/Protocols/PacketStream/AsyncFifo.hs b/clash-protocols/src/Protocols/PacketStream/AsyncFifo.hs new file mode 100644 index 00000000..f017d461 --- /dev/null +++ b/clash-protocols/src/Protocols/PacketStream/AsyncFifo.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_HADDOCK hide #-} + +{- | +Copyright : (C) 2024, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +Provides `asyncFifoC` for crossing clock domains in the packet stream protocol. +-} +module Protocols.PacketStream.AsyncFifo (asyncFifoC) where + +import Data.Maybe.Extra (toMaybe) + +import Clash.Explicit.Prelude (asyncFIFOSynchronizer) +import Clash.Prelude + +import Protocols +import Protocols.PacketStream.Base + +{- | Asynchronous FIFO circuit that can be used to safely cross clock domains. +Uses `Clash.Explicit.Prelude.asyncFIFOSynchronizer` internally. +-} +asyncFifoC :: + forall + (wDom :: Domain) + (rDom :: Domain) + (depth :: Nat) + (dataWidth :: Nat) + (meta :: Type). + (KnownDomain wDom) => + (KnownDomain rDom) => + (KnownNat depth) => + (KnownNat dataWidth) => + (2 <= depth) => + (1 <= dataWidth) => + (NFDataX meta) => + -- | 2^depth is the number of elements this component can store + SNat depth -> + -- | Clock signal in the write domain + Clock wDom -> + -- | Reset signal in the write domain + Reset wDom -> + -- | Enable signal in the write domain + Enable wDom -> + -- | Clock signal in the read domain + Clock rDom -> + -- | Reset signal in the read domain + Reset rDom -> + -- | Enable signal in the read domain + Enable rDom -> + Circuit (PacketStream wDom dataWidth meta) (PacketStream rDom dataWidth meta) +asyncFifoC depth wClk wRst wEn rClk rRst rEn = + exposeClockResetEnable forceResetSanity wClk wRst wEn |> fromSignals ckt + where + ckt (fwdIn, bwdIn) = (bwdOut, fwdOut) + where + (element, isEmpty, isFull) = asyncFIFOSynchronizer depth wClk rClk wRst rRst wEn rEn readReq fwdIn + notEmpty = not <$> isEmpty + -- If the FIFO is empty, we output Nothing. Else, we output the oldest element. + fwdOut = toMaybe <$> notEmpty <*> element + -- Assert backpressure when the FIFO is full. + bwdOut = PacketStreamS2M . not <$> isFull + -- Next component is ready to read if the fifo is not empty and it does not assert backpressure. + readReq = notEmpty .&&. _ready <$> bwdIn diff --git a/clash-protocols/src/Protocols/PacketStream/Base.hs b/clash-protocols/src/Protocols/PacketStream/Base.hs new file mode 100644 index 00000000..c5c31016 --- /dev/null +++ b/clash-protocols/src/Protocols/PacketStream/Base.hs @@ -0,0 +1,649 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_HADDOCK hide #-} + +{- | +Copyright : (C) 2024, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +Definitions and instances of the PacketStream protocol. +-} +module Protocols.PacketStream.Base ( + -- * Protocol definition + PacketStreamM2S (..), + PacketStreamS2M (..), + PacketStream, + + -- * Constants + nullByte, + + -- * CSignal conversion + toCSignal, + unsafeFromCSignal, + unsafeDropBackpressure, + + -- * Basic operations on the PacketStream protocol + empty, + consume, + forceResetSanity, + zeroOutInvalidBytesC, + stripTrailingEmptyC, + unsafeAbortOnBackpressureC, + + -- * Components imported from DfConv + void, + fanout, + registerBwd, + registerFwd, + registerBoth, + + -- * Operations on metadata + fstMeta, + sndMeta, + mapMeta, + filterMeta, + firstMeta, + secondMeta, + bimapMeta, + eitherMeta, + + -- * Operations on metadata (Signal versions) + mapMetaS, + filterMetaS, + firstMetaS, + secondMetaS, + bimapMetaS, + eitherMetaS, +) where + +import qualified Prelude as P + +import Control.DeepSeq (NFData) + +import Clash.Prelude hiding (empty, sample) + +import qualified Data.Bifunctor as B +import Data.Coerce (coerce) +import qualified Data.Maybe as Maybe +import Data.Proxy + +import Protocols +import qualified Protocols.Df as Df +import qualified Protocols.DfConv as DfConv +import Protocols.Hedgehog (Test (..)) +import Protocols.Idle + +{- | +Data sent from manager to subordinate. + +Heavily inspired by the M2S data of AMBA AXI4-Stream, but simplified: + +- @_tdata@ is moved into @_data@, which serves the exact same purpose: the actual + data of the transfer. +- @_tkeep@ is changed to `_last`. +- @_tstrb@ is removed as there are no position bytes. +- @_tid@ is removed, because packets may not be interrupted by other packets. +- @_tdest@ is moved into `_meta`. +- @_tuser@ is moved into `_meta`. +- @_tvalid@ is modeled by wrapping this type into a @Maybe@. +-} +data PacketStreamM2S (dataWidth :: Nat) (meta :: Type) = PacketStreamM2S + { _data :: Vec dataWidth (BitVector 8) + -- ^ The bytes to be transmitted. + , _last :: Maybe (Index (dataWidth + 1)) + -- ^ If this is @Just@ then it signals that this transfer is the end of a + -- packet and contains the number of valid bytes in '_data', starting from + -- index @0@. + -- + -- If it is @Nothing@ then this transfer is not yet the end of a packet and all + -- bytes are valid. This implies that no null bytes are allowed in the middle of + -- a packet, only after a packet. + , _meta :: meta + -- ^ Metadata of a packet. Must be constant during a packet. + , _abort :: Bool + -- ^ Iff true, the packet corresponding to this transfer is invalid. The subordinate + -- must either drop the packet or forward the `_abort`. + } + deriving (Generic, ShowX, Show, NFData, Bundle, Functor) + +deriving instance + (KnownNat dataWidth, NFDataX meta) => + NFDataX (PacketStreamM2S dataWidth meta) + +{- | +Two PacketStream transfers are equal if and only if: + +1. They have the same `_last` +2. They have the same `_meta`. +3. They have the same `_abort`. +4. All bytes in `_data` which are enabled by `_last` are equal. + +Data bytes that are not enabled are not considered in the equality check, +because the protocol allows them to be /undefined/. + +=== Examples + +>>> t1 = PacketStreamM2S (0x11 :> 0x22 :> 0x33 :> Nil) Nothing () False +>>> t2 = PacketStreamM2S (0x11 :> 0x22 :> 0x33 :> Nil) (Just 2) () False +>>> t3 = PacketStreamM2S (0x11 :> 0x22 :> 0xFF :> Nil) (Just 2) () False +>>> t4 = PacketStreamM2S (0x11 :> 0x22 :> undefined :> Nil) (Just 2) () False + +>>> t1 == t1 +True +>>> t2 == t3 +True +>>> t1 /= t2 +True +>>> t3 == t4 +True +-} +instance (KnownNat dataWidth, Eq meta) => Eq (PacketStreamM2S dataWidth meta) where + t1 == t2 = lastEq && metaEq && abortEq && dataEq + where + lastEq = _last t1 == _last t2 + metaEq = _meta t1 == _meta t2 + abortEq = _abort t1 == _abort t2 + + -- Bitmask used for data equality. If the index of a data byte is larger + -- than or equal to the size of `_data`, it is a null byte and must be + -- disregarded in the equality check. + mask = case _last t1 of + Nothing -> repeat False + Just size -> imap (\i _ -> resize i >= size) (_data t1) + + dataEq = case compareSNat (SNat @dataWidth) d0 of + SNatLE -> True + SNatGT -> + leToPlus @1 @dataWidth + $ fold (&&) + $ zipWith3 (\b1 b2 isNull -> isNull || b1 == b2) (_data t1) (_data t2) mask + +-- | Used by circuit-notation to create an empty stream +instance Default (Maybe (PacketStreamM2S dataWidth meta)) where + def = Nothing + +deriveAutoReg ''PacketStreamM2S + +{- | +Data sent from the subordinate to manager. + +The only information transmitted is whether the subordinate is ready to receive data. +-} +newtype PacketStreamS2M = PacketStreamS2M + { _ready :: Bool + -- ^ Iff True, the subordinate is ready to receive data. + } + deriving (Bundle, Eq, Generic, NFData, NFDataX, Show, ShowX) + +-- | Used by circuit-notation to create a sink that always acknowledges +instance Default PacketStreamS2M where + def = PacketStreamS2M True + +deriveAutoReg ''PacketStreamS2M + +{- | +Simple valid-ready streaming protocol for transferring packets between components. + +Invariants: + +1. A manager must not check the `Bwd` channel when it is sending @Nothing@ over the `Fwd` channel. +2. A manager must keep sending the same data until the subordinate has acknowledged it, i.e. upon observing `_ready` as @True@. +3. A manager must keep the metadata (`_meta`) of an entire packet it sends constant. +4. A subordinate which receives a transfer with `_abort` asserted must either forward this `_abort` or drop the packet. +5. A packet may not be interrupted by another packet. + +This protocol allows the last transfer of a packet to have zero valid bytes in +'_data', so it also allows 0-byte packets. Note that concrete implementations +of the protocol are free to disallow 0-byte packets or packets with a trailing +zero-byte transfer for whatever reason. + +The value of data bytes which are not enabled is /undefined/. +-} +data PacketStream (dom :: Domain) (dataWidth :: Nat) (meta :: Type) + +instance Protocol (PacketStream dom dataWidth meta) where + type + Fwd (PacketStream dom dataWidth meta) = + Signal dom (Maybe (PacketStreamM2S dataWidth meta)) + type Bwd (PacketStream dom dataWidth meta) = Signal dom PacketStreamS2M + +instance IdleCircuit (PacketStream dom dataWidth meta) where + idleBwd _ = pure (PacketStreamS2M False) + idleFwd _ = pure Nothing + +instance Backpressure (PacketStream dom dataWidth meta) where + boolsToBwd _ = fromList_lazy . fmap PacketStreamS2M + +instance DfConv.DfConv (PacketStream dom dataWidth meta) where + type Dom (PacketStream dom dataWidth meta) = dom + type FwdPayload (PacketStream dom dataWidth meta) = PacketStreamM2S dataWidth meta + + toDfCircuit _ = fromSignals go + where + go (fwdIn, bwdIn) = + ( + ( fmap coerce bwdIn + , pure (deepErrorX "PacketStream toDfCircuit: undefined") + ) + , Df.dataToMaybe <$> P.fst fwdIn + ) + + fromDfCircuit _ = fromSignals go + where + go (fwdIn, bwdIn) = + ( coerce <$> P.fst bwdIn + , + ( fmap Df.maybeToData fwdIn + , pure (deepErrorX "PacketStream fromDfCircuit: undefined") + ) + ) + +instance + (KnownDomain dom) => + Simulate (PacketStream dom dataWidth meta) + where + type + SimulateFwdType (PacketStream dom dataWidth meta) = + [Maybe (PacketStreamM2S dataWidth meta)] + type SimulateBwdType (PacketStream dom dataWidth meta) = [PacketStreamS2M] + type SimulateChannels (PacketStream dom dataWidth meta) = 1 + + simToSigFwd _ = fromList_lazy + simToSigBwd _ = fromList_lazy + sigToSimFwd _ s = sample_lazy s + sigToSimBwd _ s = sample_lazy s + + stallC conf (head -> (stallAck, stalls)) = + withClockResetEnable clockGen resetGen enableGen + $ DfConv.stall Proxy Proxy conf stallAck stalls + +instance + (KnownDomain dom) => + Drivable (PacketStream dom dataWidth meta) + where + type + ExpectType (PacketStream dom dataWidth meta) = + [PacketStreamM2S dataWidth meta] + + toSimulateType Proxy = fmap Just + fromSimulateType Proxy = Maybe.catMaybes + + driveC conf vals = + withClockResetEnable clockGen resetGen enableGen + $ DfConv.drive Proxy conf vals + sampleC conf ckt = + withClockResetEnable clockGen resetGen enableGen + $ DfConv.sample Proxy conf ckt + +instance + ( KnownNat dataWidth + , NFDataX meta + , NFData meta + , ShowX meta + , Show meta + , Eq meta + , KnownDomain dom + ) => + Test (PacketStream dom dataWidth meta) + where + expectN Proxy options sampled = + expectN (Proxy @(Df.Df dom _)) options + $ Df.maybeToData + <$> sampled + +{- | +Undefined PacketStream null byte. Will throw an error if evaluated. The source +of the error should be supplied for a more informative error message; otherwise +it is unclear which component threw the error. +-} +nullByte :: + -- | Component which caused the error + String -> + BitVector 8 +nullByte src = + deepErrorX + $ src + <> ": value of PacketStream null byte is undefined. " + <> "Data bytes that are not enabled must not be evaluated." + +{- | +Circuit to convert a 'CSignal' into a 'PacketStream'. +This is unsafe, because it ignores all incoming backpressure. +-} +unsafeFromCSignal :: + forall dom dataWidth meta. + Circuit + (CSignal dom (Maybe (PacketStreamM2S dataWidth meta))) + (PacketStream dom dataWidth meta) +unsafeFromCSignal = Circuit (\(fwdInS, _) -> (pure (), fwdInS)) + +-- | Converts a 'PacketStream' into a 'CSignal': always acknowledges. +toCSignal :: + forall dom dataWidth meta. + (HiddenClockResetEnable dom) => + Circuit + (PacketStream dom dataWidth meta) + (CSignal dom (Maybe (PacketStreamM2S dataWidth meta))) +toCSignal = forceResetSanity |> Circuit (\(fwdIn, _) -> (pure (PacketStreamS2M True), fwdIn)) + +-- | Drop all backpressure signals. +unsafeDropBackpressure :: + (HiddenClockResetEnable dom) => + Circuit + (PacketStream dom dwIn meta) + (PacketStream dom dwOut meta) -> + Circuit + (CSignal dom (Maybe (PacketStreamM2S dwIn meta))) + (CSignal dom (Maybe (PacketStreamM2S dwOut meta))) +unsafeDropBackpressure ckt = unsafeFromCSignal |> ckt |> toCSignal + +{- | +Sets '_abort' upon receiving backpressure from the subordinate. + +__UNSAFE__: because @fwdOut@ depends on @bwdIn@, this may introduce +combinatorial loops. You need to make sure that a sequential element is +inserted along this path. It is possible to use one of the skid buffers to +ensure this. For example: + +>>> safeAbortOnBackpressureC1 = unsafeAbortOnBackpressureC |> registerFwd +>>> safeAbortOnBackpressureC2 = unsafeAbortOnBackpressureC |> registerBwd + +Note that `registerFwd` utilizes less resources than `registerBwd`. +-} +unsafeAbortOnBackpressureC :: + forall (dataWidth :: Nat) (meta :: Type) (dom :: Domain). + (HiddenClockResetEnable dom) => + Circuit + (CSignal dom (Maybe (PacketStreamM2S dataWidth meta))) + (PacketStream dom dataWidth meta) +unsafeAbortOnBackpressureC = + Circuit $ \(fwdInS, bwdInS) -> (pure (), go <$> bundle (fwdInS, bwdInS)) + where + go (fwdIn, bwdIn) = + fmap (\pkt -> pkt{_abort = _abort pkt || not (_ready bwdIn)}) fwdIn + +{- | +Force a /nack/ on the backward channel and /Nothing/ on the forward +channel if reset is asserted. +-} +forceResetSanity :: + forall dom dataWidth meta. + (HiddenClockResetEnable dom) => + Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta) +forceResetSanity = forceResetSanityGeneric + +{- | +Strips trailing zero-byte transfers from packets in the stream. That is, +if a packet consists of more than one transfer and '_last' of the last +transfer in that packet is @Just 0@, the last transfer of that packet will +be dropped and '_last' of the transfer before that will be set to @maxBound@. +If such a trailing zero-byte transfer had '_abort' asserted, it will be +preserved. + +Has one clock cycle latency, but runs at full throughput. +-} +stripTrailingEmptyC :: + forall (dataWidth :: Nat) (meta :: Type) (dom :: Domain). + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (NFDataX meta) => + Circuit + (PacketStream dom dataWidth meta) + (PacketStream dom dataWidth meta) +stripTrailingEmptyC = forceResetSanity |> fromSignals (mealyB go (False, False, Nothing)) + where + go (notFirst, flush, cache) (Nothing, bwdIn) = + ((notFirst, flush', cache'), (PacketStreamS2M True, fwdOut)) + where + fwdOut = if flush then cache else Nothing + (flush', cache') + | flush && _ready bwdIn = (False, Nothing) + | otherwise = (flush, cache) + go (notFirst, flush, cache) (Just transferIn, bwdIn) = (nextStOut, (bwdOut, fwdOut)) + where + (notFirst', flush', cache', fwdOut) = case _last transferIn of + Nothing -> (True, False, Just transferIn, cache) + Just i -> + let trailing = i == 0 && notFirst + in ( False + , not trailing + , if trailing then Nothing else Just transferIn + , if trailing + then (\x -> x{_last = Just maxBound, _abort = _abort x || _abort transferIn}) <$> cache + else cache + ) + + bwdOut = PacketStreamS2M (Maybe.isNothing cache || _ready bwdIn) + + nextStOut + | Maybe.isNothing cache || _ready bwdIn = (notFirst', flush', cache') + | otherwise = (notFirst, flush, cache) + +-- | Sets data bytes that are not enabled in a @PacketStream@ to @0x00@. +zeroOutInvalidBytesC :: + forall (dom :: Domain) (dataWidth :: Nat) (meta :: Type). + (KnownNat dataWidth) => + (1 <= dataWidth) => + Circuit + (PacketStream dom dataWidth meta) + (PacketStream dom dataWidth meta) +zeroOutInvalidBytesC = Circuit $ \(fwdIn, bwdIn) -> (bwdIn, fmap (go <$>) fwdIn) + where + go transferIn = transferIn{_data = dataOut} + where + dataOut = case _last transferIn of + Nothing -> _data transferIn + Just i -> + imap + (\(j :: Index dataWidth) byte -> if resize j < i then byte else 0x00) + (_data transferIn) + +{- | +Copy data of a single `PacketStream` to multiple. LHS will only receive +an acknowledgement when all RHS receivers have acknowledged data. +-} +fanout :: + forall n dataWidth meta dom. + (HiddenClockResetEnable dom) => + (KnownNat n) => + (KnownNat dataWidth) => + (1 <= n) => + (NFDataX meta) => + Circuit + (PacketStream dom dataWidth meta) + (Vec n (PacketStream dom dataWidth meta)) +fanout = DfConv.fanout Proxy Proxy + +{- | +Place a register on the /forward/ part of a circuit. +This adds combinational delay on the /backward/ path. +-} +registerFwd :: + forall dataWidth meta dom. + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (NFDataX meta) => + Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta) +registerFwd = DfConv.registerFwd Proxy Proxy + +{- | +Place a register on the /backward/ part of a circuit. +This adds combinational delay on the /forward/ path. +-} +registerBwd :: + forall dataWidth meta dom. + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (NFDataX meta) => + Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta) +registerBwd = DfConv.registerBwd Proxy Proxy + +{- | +A pipeline skid buffer: places registers on both the /backward/ and /forward/ +part of a circuit. This completely breaks up the combinatorial path between +the left and right side of this component. In order to achieve this, it has to +buffer @Fwd@ twice. + +Another benefit of this component is that the circuit on the left hand side +may now use @Bwd@ in order to compute its @Fwd@, because this cannot +introduce combinatorial loops anymore. + +Runs at full throughput, but causes 2 clock cycles of latency. +-} +registerBoth :: + forall dataWidth meta dom. + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (NFDataX meta) => + Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta) +registerBoth = registerBwd |> registerFwd + +-- | Never produces a value. +empty :: Circuit () (PacketStream dom dataWidth meta) +empty = Circuit (const ((), pure Nothing)) + +-- | Always acknowledges incoming data. +consume :: (HiddenReset dom) => Circuit (PacketStream dom dataWidth meta) () +consume = Circuit (const (pure (PacketStreamS2M True), ())) + +-- | Never acknowledges incoming data. +void :: (HiddenClockResetEnable dom) => Circuit (PacketStream dom dataWidth meta) () +void = DfConv.void Proxy + +-- | Like 'P.fst', but over the metadata of a 'PacketStream'. +fstMeta :: Circuit (PacketStream dom dataWidth (a, b)) (PacketStream dom dataWidth a) +fstMeta = mapMeta P.fst + +-- | Like 'P.snd', but over the metadata of a 'PacketStream'. +sndMeta :: Circuit (PacketStream dom dataWidth (a, b)) (PacketStream dom dataWidth b) +sndMeta = mapMeta P.snd + +-- | Like 'Data.List.map', but over the metadata of a 'PacketStream'. +mapMeta :: + -- | Function to apply on the metadata + (metaIn -> metaOut) -> + Circuit (PacketStream dom dataWidth metaIn) (PacketStream dom dataWidth metaOut) +mapMeta f = mapMetaS (pure f) + +{- | +Like 'mapMeta' but can reason over signals, +this circuit combinator is akin to `Clash.HaskellPrelude.<*>`. +-} +mapMetaS :: + -- | Function to apply on the metadata, wrapped in a @Signal@ + Signal dom (metaIn -> metaOut) -> + Circuit (PacketStream dom dataWidth metaIn) (PacketStream dom dataWidth metaOut) +mapMetaS fS = Circuit $ \(fwdIn, bwdIn) -> (bwdIn, go <$> bundle (fwdIn, fS)) + where + go (inp, f) = (\inPkt -> inPkt{_meta = f (_meta inPkt)}) <$> inp + +-- | Like 'Data.List.filter', but over the metadata of a 'PacketStream'. +filterMeta :: + -- | Predicate which specifies whether to keep a fragment based on its metadata + (meta -> Bool) -> + Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta) +filterMeta p = filterMetaS (pure p) + +{- | +Like 'filterMeta' but can reason over signals, +this circuit combinator is akin to `Clash.HaskellPrelude.<*>`. +-} +filterMetaS :: + -- | Predicate which specifies whether to keep a fragment based on its metadata, + -- wrapped in a @Signal@ + Signal dom (meta -> Bool) -> + Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta) +filterMetaS pS = Circuit $ \(fwdIn, bwdIn) -> unbundle (go <$> bundle (fwdIn, bwdIn, pS)) + where + go (Nothing, bwdIn, _) = (bwdIn, Nothing) + go (Just inPkt, bwdIn, predicate) + | predicate (_meta inPkt) = (bwdIn, Just inPkt) + | otherwise = (PacketStreamS2M True, Nothing) + +-- | Like 'Data.Either.either', but over the metadata of a 'PacketStream'. +eitherMeta :: + (a -> c) -> + (b -> c) -> + Circuit + (PacketStream dom dataWidth (Either a b)) + (PacketStream dom dataWidth c) +eitherMeta f g = eitherMetaS (pure f) (pure g) + +{- | +Like 'eitherMeta' but can reason over signals, +this circuit combinator is akin to `Clash.HaskellPrelude.<*>`. +-} +eitherMetaS :: + Signal dom (a -> c) -> + Signal dom (b -> c) -> + Circuit + (PacketStream dom dataWidth (Either a b)) + (PacketStream dom dataWidth c) +eitherMetaS fS gS = mapMetaS (liftA2 P.either fS gS) + +-- | Like 'Data.Bifunctor.bimap', but over the metadata of a 'PacketStream'. +bimapMeta :: + (B.Bifunctor p) => + (a -> b) -> + (c -> d) -> + Circuit + (PacketStream dom dataWidth (p a c)) + (PacketStream dom dataWidth (p b d)) +bimapMeta f g = bimapMetaS (pure f) (pure g) + +{- | +Like 'bimapMeta' but can reason over signals, +this circuit combinator is akin to `Clash.HaskellPrelude.<*>`. +-} +bimapMetaS :: + (B.Bifunctor p) => + Signal dom (a -> b) -> + Signal dom (c -> d) -> + Circuit + (PacketStream dom dataWidth (p a c)) + (PacketStream dom dataWidth (p b d)) +bimapMetaS fS gS = mapMetaS (liftA2 B.bimap fS gS) + +-- | Like 'Data.Bifunctor.first', but over the metadata of a 'PacketStream'. +firstMeta :: + (B.Bifunctor p) => + (a -> b) -> + Circuit + (PacketStream dom dataWidth (p a c)) + (PacketStream dom dataWidth (p b c)) +firstMeta f = firstMetaS (pure f) + +{- | +Like 'firstMeta' but can reason over signals, +this circuit combinator is akin to `Clash.HaskellPrelude.<*>`. +-} +firstMetaS :: + (B.Bifunctor p) => + Signal dom (a -> b) -> + Circuit + (PacketStream dom dataWidth (p a c)) + (PacketStream dom dataWidth (p b c)) +firstMetaS fS = mapMetaS (B.first <$> fS) + +-- | Like 'Data.Bifunctor.second', but over the metadata of a 'PacketStream'. +secondMeta :: + (B.Bifunctor p) => + (b -> c) -> + Circuit + (PacketStream dom dataWidth (p a b)) + (PacketStream dom dataWidth (p a c)) +secondMeta f = secondMetaS (pure f) + +{- | +Like 'secondMeta' but can reason over signals, +this circuit combinator is akin to `Clash.HaskellPrelude.<*>`. +-} +secondMetaS :: + (B.Bifunctor p) => + Signal dom (b -> c) -> + Circuit + (PacketStream dom dataWidth (p a b)) + (PacketStream dom dataWidth (p a c)) +secondMetaS fS = mapMetaS (B.second <$> fS) diff --git a/clash-protocols/src/Protocols/PacketStream/Converters.hs b/clash-protocols/src/Protocols/PacketStream/Converters.hs new file mode 100644 index 00000000..ebbf932b --- /dev/null +++ b/clash-protocols/src/Protocols/PacketStream/Converters.hs @@ -0,0 +1,335 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_HADDOCK hide #-} + +{- | +Copyright : (C) 2024, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +Provides an upconverter and downconverter for changing the data width of +packet streams. +-} +module Protocols.PacketStream.Converters ( + downConverterC, + upConverterC, + unsafeUpConverterC, +) where + +import Clash.Prelude + +import Data.Maybe (fromMaybe, isJust) +import Data.Maybe.Extra +import Data.Type.Equality ((:~:) (Refl)) + +import Protocols (CSignal, Circuit (..), fromSignals, idC, (|>)) +import Protocols.PacketStream.Base + +-- | State of 'upConverter'. +data UpConverterState (dwIn :: Nat) (n :: Nat) (meta :: Type) = UpConverterState + { _ucBuf :: Vec (dwIn * n) (BitVector 8) + -- ^ The data buffer we are filling. + , _ucIdx :: Index n + -- ^ Where in _ucBuf we need to write the next data. + , _ucIdx2 :: Index (dwIn * n + 1) + -- ^ Used when @dwIn@ is not a power of two to determine the adjusted '_last', + -- to avoid multiplication (infers an expensive DSP slice). + -- If @dwIn@ is a power of two then we can multiply by shifting left with + -- a constant, which is free in hardware in terms of resource usage. + , _ucFlush :: Bool + -- ^ If true, we should output the current state as a PacketStream transfer. + , _ucAborted :: Bool + -- ^ Whether the current transfer we are building is aborted. + , _ucLastIdx :: Maybe (Index (dwIn * n + 1)) + -- ^ If Just, the current buffer contains the last byte of the current packet. + , _ucMeta :: meta + -- ^ Metadata of the current transfer we are a building. + } + deriving (Generic, NFDataX, Show, ShowX) + +-- | Computes the next state for 'upConverter'. +nextState :: + forall (dwIn :: Nat) (meta :: Type) (n :: Nat). + (1 <= dwIn) => + (1 <= n) => + (KnownNat dwIn) => + (KnownNat n) => + (NFDataX meta) => + UpConverterState dwIn n meta -> + Maybe (PacketStreamM2S dwIn meta) -> + PacketStreamS2M -> + UpConverterState dwIn n meta +nextState st@(UpConverterState{..}) Nothing (PacketStreamS2M inReady) = + nextSt + where + outReady = not _ucFlush || inReady + -- If we can accept data we can always set _ucFlush to false, + -- since we only change state if we can transmit and receive data + nextStRaw = + st + { _ucFlush = False + , _ucAborted = not _ucFlush && _ucAborted + , _ucLastIdx = Nothing + } + nextSt = if outReady then nextStRaw else st +nextState st@(UpConverterState{..}) (Just PacketStreamM2S{..}) (PacketStreamS2M inReady) = + nextSt + where + nextAbort = (not _ucFlush && _ucAborted) || _abort + -- If we are not flushing we can accept data to be stored in _ucBuf, + -- but when we are flushing we can only accept if the current + -- output fragment is accepted by the sink + outReady = not _ucFlush || inReady + bufFull = _ucIdx == maxBound + + nextBuf = + bitCoerce + $ replace + _ucIdx + (pack _data :: BitVector (8 * dwIn)) + (bitCoerce _ucBuf :: Vec n (BitVector (8 * dwIn))) + + nextFlush = isJust _last || bufFull + nextIdx = if nextFlush then 0 else _ucIdx + 1 + + -- If @dwIn@ is not a power of two, we need to do some extra bookkeeping to + -- avoid multiplication to calculate _last. If not, _ucIdx2 stays at 0 and is + -- never used, and should therefore be optimized out by synthesis tools. + (nextIdx2, nextLastIdx) = case sameNat (SNat @(FLog 2 dwIn)) (SNat @(CLog 2 dwIn)) of + Just Refl -> + ( 0 + , (\i -> shiftL (resize _ucIdx) (natToNum @(Log 2 dwIn)) + resize i) <$> _last + ) + Nothing -> + ( if nextFlush then 0 else _ucIdx2 + natToNum @dwIn + , (\i -> _ucIdx2 + resize i) <$> _last + ) + + nextStRaw = + UpConverterState + { _ucBuf = nextBuf + , _ucIdx = nextIdx + , _ucIdx2 = nextIdx2 + , _ucFlush = nextFlush + , _ucAborted = nextAbort + , _ucLastIdx = nextLastIdx + , _ucMeta = _meta + } + nextSt = if outReady then nextStRaw else st + +upConverter :: + forall (dwIn :: Nat) (meta :: Type) (dom :: Domain) (n :: Nat). + (HiddenClockResetEnable dom) => + (1 <= dwIn) => + (1 <= n) => + (KnownNat dwIn) => + (KnownNat n) => + (NFDataX meta) => + ( Signal dom (Maybe (PacketStreamM2S dwIn meta)) + , Signal dom PacketStreamS2M + ) -> + ( Signal dom PacketStreamS2M + , Signal dom (Maybe (PacketStreamM2S (dwIn * n) meta)) + ) +upConverter = mealyB go s0 + where + errPrefix = "upConverterT: undefined initial " + s0 = + UpConverterState + { _ucBuf = repeat (nullByte "upConverter") + , _ucIdx = 0 + , _ucIdx2 = 0 + , _ucFlush = False + , _ucAborted = False + , _ucLastIdx = deepErrorX (errPrefix <> " _ucLastIdx") + , _ucMeta = deepErrorX (errPrefix <> " _ucMeta") + } + go st@(UpConverterState{..}) (fwdIn, bwdIn) = + (nextState st fwdIn bwdIn, (PacketStreamS2M outReady, fwdOut)) + where + outReady = not _ucFlush || _ready bwdIn + + fwdOut = + toMaybe _ucFlush + $ PacketStreamM2S + { _data = _ucBuf + , _last = _ucLastIdx + , _meta = _ucMeta + , _abort = _ucAborted + } + +{- | +Converts packet streams of arbitrary data width @dwIn@ to packet streams of +a bigger (or equal) data width @dwIn * n@, where @n > 0@. +When @n ~ 1@, this component is just the identity circuit, `idC`. + +If '_abort' is asserted on any of the input sub-transfers, it will be asserted +on the corresponding output transfer as well. All zero-byte transfers are +preserved. + +Has one cycle of latency, all M2S outputs are registered. +Provides full throughput. +-} +upConverterC :: + forall (dwIn :: Nat) (n :: Nat) (meta :: Type) (dom :: Domain). + (HiddenClockResetEnable dom) => + (1 <= dwIn) => + (1 <= n) => + (KnownNat dwIn) => + (KnownNat n) => + (NFDataX meta) => + -- | Upconverter circuit + Circuit (PacketStream dom dwIn meta) (PacketStream dom (dwIn * n) meta) +upConverterC = case sameNat d1 (SNat @n) of + Just Refl -> idC + _ -> forceResetSanity |> fromSignals upConverter + +{- | +Unsafe version of 'upConverterC'. + +Because 'upConverterC' runs at full throughput, i.e. it only asserts backpressure +if the subordinate asserts backpressure, we supply this variant which drops all +backpressure signals. This can be used when the source circuit does not support +backpressure. Using this variant in that case will improve timing and probably +reduce resource usage. +-} +unsafeUpConverterC :: + forall (dwIn :: Nat) (meta :: Type) (dom :: Domain) (n :: Nat). + (HiddenClockResetEnable dom) => + (1 <= dwIn) => + (1 <= n) => + (KnownNat dwIn) => + (KnownNat n) => + (NFDataX meta) => + -- | Unsafe upconverter circuit + Circuit + (CSignal dom (Maybe (PacketStreamM2S dwIn meta))) + (CSignal dom (Maybe (PacketStreamM2S (dwIn * n) meta))) +unsafeUpConverterC = case sameNat d1 (SNat @n) of + Just Refl -> idC + _ -> unsafeDropBackpressure (fromSignals upConverter) + +-- | State of 'downConverterT'. +data DownConverterState (dwOut :: Nat) (n :: Nat) (meta :: Type) = DownConverterState + { _dcBuf :: Vec (dwOut * n) (BitVector 8) + -- ^ Registered _data of the last transfer. + , _dcLast :: Bool + -- ^ Is the last transfer the end of a packet? + , _dcMeta :: meta + -- ^ Registered _meta of the last transfer. + , _dcAborted :: Bool + -- ^ Registered _abort of the last transfer. All sub-transfers corresponding + -- to this transfer need to be marked with the same _abort value. + , _dcSize :: Index (dwOut * n + 1) + -- ^ Number of valid bytes in _dcBuf. + , _dcZeroByteTransfer :: Bool + -- ^ Is the current transfer we store a zero-byte transfer? In this case, + -- _dcSize is 0 but we still need to transmit something in order to + -- preserve zero-byte transfers. + } + deriving (Generic, NFDataX) + +-- | State transition function of 'downConverterC', in case @n > 1@. +downConverterT :: + forall (dwOut :: Nat) (n :: Nat) (meta :: Type). + (KnownNat dwOut) => + (KnownNat n) => + (1 <= dwOut) => + (1 <= n) => + (NFDataX meta) => + DownConverterState dwOut n meta -> + (Maybe (PacketStreamM2S (dwOut * n) meta), PacketStreamS2M) -> + ( DownConverterState dwOut n meta + , (PacketStreamS2M, Maybe (PacketStreamM2S dwOut meta)) + ) +downConverterT st@(DownConverterState{..}) (fwdIn, bwdIn) = + (nextSt, (PacketStreamS2M readyOut, fwdOut)) + where + (shiftedBuf, dataOut) = + leToPlus @dwOut @(dwOut * n) + $ shiftOutFrom0 (SNat @dwOut) _dcBuf + + -- Either we preserve a zero-byte transfer or we have some real data to transmit. + fwdOut = + toMaybe (_dcSize > 0 || _dcZeroByteTransfer) + $ PacketStreamM2S + { _data = dataOut + , _last = + if _dcZeroByteTransfer + then Just 0 + else toMaybe (_dcSize <= natToNum @dwOut && _dcLast) (resize _dcSize) + , _meta = _dcMeta + , _abort = _dcAborted + } + + -- If the state buffer is empty, or if the state buffer is not empty and + -- the final sub-transfer is acknowledged this clock cycle, we can acknowledge + -- newly received valid data and load it into our registers. + emptyState = _dcSize == 0 && not _dcZeroByteTransfer + readyOut = + isJust fwdIn + && (emptyState || (_dcSize <= natToNum @dwOut && _ready bwdIn)) + + nextSt + | readyOut = newState (fromJustX fwdIn) + | not emptyState && _ready bwdIn = + st + { _dcBuf = shiftedBuf + , _dcSize = satSub SatBound _dcSize (natToNum @dwOut) + , _dcZeroByteTransfer = False + } + | otherwise = st + + -- Computes a new state from a valid incoming transfer. + newState PacketStreamM2S{..} = + DownConverterState + { _dcBuf = _data + , _dcMeta = _meta + , _dcSize = fromMaybe (natToNum @(dwOut * n)) _last + , _dcLast = isJust _last + , _dcAborted = _abort + , _dcZeroByteTransfer = _last == Just 0 + } + +{- | +Converts packet streams of a data width which is a multiple of @n@, i.e. +@dwOut * n@, to packet streams of a smaller (or equal) data width @dwOut@, +where @n > 0@. +When @n ~ 1@, this component is just the identity circuit, `idC`. + +If '_abort' is asserted on an input transfer, it will be asserted on all +corresponding output sub-transfers as well. All zero-byte transfers are +preserved. + +Has one clock cycle of latency, all M2S outputs are registered. +Throughput is optimal, a transfer of @k@ valid bytes is transmitted in @k@ +clock cycles. To be precise, throughput is at least @(1 / n)%@, so at +least @50%@ if @n = 2@ for example. We specify /at least/, +because the throughput may be on the last transfer of a packet, when not all +bytes have to be valid. If there is only one valid byte in the last transfer, +then the throughput will always be @100%@ for that particular transfer. +-} +downConverterC :: + forall (dwOut :: Nat) (n :: Nat) (meta :: Type) (dom :: Domain). + (HiddenClockResetEnable dom) => + (KnownNat dwOut) => + (KnownNat n) => + (1 <= dwOut) => + (1 <= n) => + (NFDataX meta) => + -- | Downconverter circuit + Circuit (PacketStream dom (dwOut * n) meta) (PacketStream dom dwOut meta) +downConverterC = case sameNat d1 (SNat @n) of + Just Refl -> idC + _ -> forceResetSanity |> fromSignals (mealyB downConverterT s0) + where + errPrefix = "downConverterT: undefined initial " + s0 = + DownConverterState + { _dcBuf = deepErrorX (errPrefix <> "_dcBuf") + , _dcLast = deepErrorX (errPrefix <> "_dcLast") + , _dcMeta = deepErrorX (errPrefix <> "_dcMeta") + , _dcAborted = deepErrorX (errPrefix <> "_dcAborted") + , _dcSize = 0 + , _dcZeroByteTransfer = False + } diff --git a/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs b/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs new file mode 100644 index 00000000..735a6920 --- /dev/null +++ b/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs @@ -0,0 +1,359 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-} +{-# OPTIONS_GHC -fplugin Protocols.Plugin #-} +{-# OPTIONS_HADDOCK hide #-} + +{- | +Copyright : (C) 2024, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +Utility circuits for reading from a packet stream. +-} +module Protocols.PacketStream.Depacketizers ( + depacketizerC, + depacketizeToDfC, +) where + +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)) +import Data.Constraint.Nat.Extra +import Data.Data ((:~:) (Refl)) +import Data.Maybe + +{- | Vectors of this size are able to hold @headerBytes `DivRU` dataWidth@ + transfers of size @dataWidth@, which is bigger than or equal to @headerBytes@. +-} +type BufSize (headerBytes :: Nat) (dataWidth :: Nat) = + dataWidth * headerBytes `DivRU` dataWidth + +{- | Since the header might be unaligned compared to the data width + we need to store a partial fragment when forwarding. + The number of bytes we need to store depends on our "unalignedness". + + Ex. We parse a header of 17 bytes and our @dataWidth@ is 4 bytes. + That means at the end of the header we can have up to 3 bytes left + in the fragment which we may need to forward. +-} +type ForwardBytes (headerBytes :: Nat) (dataWidth :: Nat) = + (dataWidth - (headerBytes `Mod` dataWidth)) `Mod` dataWidth + +-- | Depacketizer constraints. +type DepacketizerCt (headerBytes :: Nat) (dataWidth :: Nat) = + ( KnownNat headerBytes + , KnownNat dataWidth + , 1 <= headerBytes + , 1 <= dataWidth + , BufSize headerBytes dataWidth ~ headerBytes + ForwardBytes headerBytes dataWidth + , headerBytes `Mod` dataWidth <= dataWidth + , ForwardBytes headerBytes dataWidth <= dataWidth + ) + +{- | Depacketizer state. Either we are parsing a header, or we are forwarding + the rest of the packet along with the parsed header in its metadata. +-} +data DepacketizerState (headerBytes :: Nat) (dataWidth :: Nat) + = Parse + { _aborted :: Bool + -- ^ Whether the packet is aborted. We need this, because _abort might + -- have been set in the bytes to be parsed. + , _buf :: Vec (BufSize headerBytes dataWidth) (BitVector 8) + -- ^ The first @headerBytes@ of this buffer are for the parsed header. + -- The bytes after that are data bytes that could not be sent immediately + -- due to misalignment of @dataWidth@ and @headerBytes@. + , _counter :: Index (headerBytes `DivRU` dataWidth) + -- ^ @maxBound + 1@ is the number of fragments we need to parse. + } + | Forward + { _aborted :: Bool + , _buf :: Vec (BufSize headerBytes dataWidth) (BitVector 8) + , _counter :: Index (headerBytes `DivRU` dataWidth) + , _lastFwd :: Bool + -- ^ True iff we have seen @_last@ set but the number of data bytes was too + -- big to send immediately along with our buffered bytes. + } + deriving (Show, ShowX, Generic) + +deriving instance + (DepacketizerCt headerBytes dataWidth) => + NFDataX (DepacketizerState headerBytes dataWidth) + +-- | Initial state of @depacketizerT@. +instance + (DepacketizerCt headerBytes dataWidth) => + Default (DepacketizerState headerBytes dataWidth) + where + def :: DepacketizerState headerBytes dataWidth + def = Parse False (deepErrorX "depacketizerT: undefined initial buffer") maxBound + +-- | Depacketizer state transition function. +depacketizerT :: + forall + (headerBytes :: Nat) + (header :: Type) + (metaIn :: Type) + (metaOut :: Type) + (dataWidth :: Nat). + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (NFDataX metaIn) => + (DepacketizerCt headerBytes dataWidth) => + (header -> metaIn -> metaOut) -> + DepacketizerState headerBytes dataWidth -> + (Maybe (PacketStreamM2S dataWidth metaIn), PacketStreamS2M) -> + ( DepacketizerState headerBytes dataWidth + , (PacketStreamS2M, Maybe (PacketStreamM2S dataWidth metaOut)) + ) +depacketizerT _ Parse{..} (Just PacketStreamM2S{..}, _) = (nextStOut, (PacketStreamS2M outReady, Nothing)) + where + nextAborted = _aborted || _abort + nextCounter = pred _counter + nextParseBuf = fst (shiftInAtN _buf _data) + + prematureEnd idx = case sameNat d0 (SNat @(headerBytes `Mod` dataWidth)) of + Just Refl -> idx /= maxBound + _ -> idx < natToNum @(headerBytes `Mod` dataWidth) + + -- Upon seeing _last being set, move back to the initial state if the + -- right amount of bytes were not parsed yet, or if they were, but there + -- were no data bytes after that. + nextStOut = case (_counter == 0, _last) of + (False, Nothing) -> + Parse nextAborted nextParseBuf nextCounter + (False, Just _) -> + def + (True, Just idx) + | prematureEnd idx -> + def + (True, _) -> + Forward nextAborted nextParseBuf nextCounter (isJust _last) + + outReady + | Forward{_lastFwd = True} <- nextStOut = False + | otherwise = True +depacketizerT toMetaOut st@Forward{..} (Just pkt@PacketStreamM2S{..}, bwdIn) = (nextStOut, (PacketStreamS2M outReady, Just outPkt)) + where + nextAborted = _aborted || _abort + nextBuf = header ++ nextFwdBytes + newLast = adjustLast <$> _last + (header, fwdBytes) = splitAt (SNat @headerBytes) _buf + (dataOut, nextFwdBytes) = splitAt (SNat @dataWidth) (fwdBytes ++ _data) + + -- Only use if headerBytes `Mod` dataWidth > 0. + adjustLast :: + Index (dataWidth + 1) -> Either (Index (dataWidth + 1)) (Index (dataWidth + 1)) + adjustLast idx + | _lastFwd = Right (idx - x) + | idx <= x = Left (idx + y) + | otherwise = Right (idx - x) + where + x = natToNum @(headerBytes `Mod` dataWidth) + y = natToNum @(ForwardBytes headerBytes dataWidth) + + outPkt = case sameNat d0 (SNat @(headerBytes `Mod` dataWidth)) of + Just Refl -> + pkt + { _data = _data + , _last = if _lastFwd then Just 0 else _last + , _meta = toMetaOut (bitCoerce header) _meta + , _abort = nextAborted + } + Nothing -> + pkt + { _data = dataOut + , _last = + if _lastFwd + then either Just Just =<< newLast + else either Just (const Nothing) =<< newLast + , _meta = toMetaOut (bitCoerce header) _meta + , _abort = nextAborted + } + + nextForwardSt = Forward nextAborted nextBuf maxBound + nextSt = case sameNat d0 (SNat @(headerBytes `Mod` dataWidth)) of + Just Refl + | isJust _last -> def + | otherwise -> nextForwardSt False + Nothing -> + case (_lastFwd, newLast) of + (False, Nothing) -> nextForwardSt False + (False, Just (Right _)) -> nextForwardSt True + _ -> def + + nextStOut = if _ready bwdIn then nextSt else st + + outReady + | Forward{_lastFwd = True} <- nextStOut = False + | otherwise = _ready bwdIn +depacketizerT _ st (Nothing, bwdIn) = (st, (bwdIn, Nothing)) + +{- | +Reads bytes at the start of each packet into `_meta`. If a packet contains +less valid bytes than @headerBytes + 1@, it will silently drop that packet. + +If @dataWidth@ divides @headerBytes@, this component runs at full throughput. +Otherwise, it gives backpressure for one clock cycle per packet larger than +@headerBytes + 1@ valid bytes. +-} +depacketizerC :: + forall + (headerBytes :: Nat) + (header :: Type) + (metaIn :: Type) + (metaOut :: Type) + (dataWidth :: Nat) + (dom :: Domain). + (HiddenClockResetEnable dom) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (NFDataX metaIn) => + (KnownNat headerBytes) => + (KnownNat dataWidth) => + (1 <= headerBytes) => + (1 <= dataWidth) => + -- | Mapping from the parsed header and input `_meta` to the output `_meta` + (header -> metaIn -> metaOut) -> + Circuit (PacketStream dom dataWidth metaIn) (PacketStream dom dataWidth metaOut) +depacketizerC toMetaOut = forceResetSanity |> fromSignals ckt + where + ckt = case ( eqTimesDivRu @dataWidth @headerBytes + , leModulusDivisor @headerBytes @dataWidth + , leModulusDivisor @(dataWidth - (headerBytes `Mod` dataWidth)) @dataWidth + ) of + (Dict, Dict, Dict) -> mealyB (depacketizerT toMetaOut) def + +-- | Df depacketizer constraints. +type DepacketizeToDfCt (headerBytes :: Nat) (dataWidth :: Nat) = + ( KnownNat headerBytes + , KnownNat dataWidth + , 1 <= headerBytes + , 1 <= dataWidth + , headerBytes <= headerBytes `DivRU` dataWidth * dataWidth + ) + +data DfDepacketizerState (headerBytes :: Nat) (dataWidth :: Nat) + = DfParse + { _dfAborted :: Bool + -- ^ Whether the current packet is aborted. We need this, because _abort + -- might have been set in the bytes to be parsed. + , _dfParseBuf :: Vec (BufSize headerBytes dataWidth) (BitVector 8) + -- ^ Buffer for the header that we need to parse. + , _dfCounter :: Index (headerBytes `DivRU` dataWidth) + -- ^ @maxBound + 1@ is the number of fragments we need to parse. + } + | DfConsumePadding + { _dfAborted :: Bool + , _dfParseBuf :: Vec (BufSize headerBytes dataWidth) (BitVector 8) + } + deriving (Generic, Show, ShowX) + +deriving instance + (DepacketizeToDfCt headerBytes dataWidth) => + (NFDataX (DfDepacketizerState headerBytes dataWidth)) + +-- | Initial state of @depacketizeToDfT@. +instance + (DepacketizeToDfCt headerBytes dataWidth) => + Default (DfDepacketizerState headerBytes dataWidth) + where + def :: DfDepacketizerState headerBytes dataWidth + def = DfParse False (deepErrorX "depacketizeToDfT: undefined initial buffer") maxBound + +-- | Df depacketizer transition function. +depacketizeToDfT :: + forall + (headerBytes :: Nat) + (header :: Type) + (meta :: Type) + (a :: Type) + (dataWidth :: Nat). + (NFDataX meta) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (DepacketizeToDfCt headerBytes dataWidth) => + (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)) + where + nextAborted = _dfAborted || _abort + nextParseBuf = fst (shiftInAtN _dfParseBuf _data) + + prematureEnd idx = + case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of + SNatGT -> idx < (natToNum @(headerBytes `Mod` dataWidth)) + _ -> idx < (natToNum @dataWidth) + + (nextStOut, readyOut) = + case (_dfCounter == 0, _last) of + (False, Nothing) -> + (DfParse nextAborted nextParseBuf (pred _dfCounter), True) + (False, Just _) -> + (def, True) + (True, Just idx) -> + if nextAborted || prematureEnd idx + then (def, True) + else (DfConsumePadding nextAborted nextParseBuf, False) + (True, Nothing) -> + (DfConsumePadding nextAborted nextParseBuf, True) +depacketizeToDfT toOut st@DfConsumePadding{..} (Just (PacketStreamM2S{..}), Ack readyIn) = (nextStOut, (PacketStreamS2M readyOut, fwdOut)) + where + nextAborted = _dfAborted || _abort + outDf = toOut (bitCoerce (takeLe (SNat @headerBytes) _dfParseBuf)) _meta + + (nextSt, fwdOut) = + if isJust _last + then (def, if nextAborted then Df.NoData else Df.Data outDf) + else (st{_dfAborted = nextAborted}, Df.NoData) + + readyOut = isNothing (Df.dataToMaybe fwdOut) || readyIn + nextStOut = if readyOut then nextSt else st +depacketizeToDfT _ st (Nothing, Ack readyIn) = (st, (PacketStreamS2M readyIn, Df.NoData)) + +{- | +Reads bytes at the start of each packet into a header structure, and +transforms this header structure along with the input metadata to an output +structure @a@, which is transmitted over a @Df@ channel. Such a structure +is sent once per packet over the @Df@ channel, but only if the packet was big +enough (contained at least @headerBytes@ valid data bytes) and did not +contain any transfer with @_abort@ set. +The remainder of the packet (padding) is dropped. + +If the packet is not padded, or if the packet is padded but the padding fits +in the last transfer of the packet together with valid data bytes, this +component will give one clock cycle of backpressure per packet (for efficiency +reasons). Otherwise, it runs at full throughput. +-} +depacketizeToDfC :: + forall + (headerBytes :: Nat) + (header :: Type) + (meta :: Type) + (a :: Type) + (dataWidth :: Nat) + (dom :: Domain). + (HiddenClockResetEnable dom) => + (NFDataX meta) => + (NFDataX a) => + (BitPack header) => + (KnownNat headerBytes) => + (KnownNat dataWidth) => + (1 <= headerBytes) => + (1 <= dataWidth) => + (BitSize header ~ headerBytes * 8) => + -- | Mapping from the parsed header and input `_meta` to the `Df` output + (header -> meta -> a) -> + Circuit (PacketStream dom dataWidth meta) (Df dom a) +depacketizeToDfC toOut = forceResetSanity |> fromSignals ckt + where + ckt = case leTimesDivRu @dataWidth @headerBytes of + Dict -> mealyB (depacketizeToDfT toOut) def diff --git a/clash-protocols/src/Protocols/PacketStream/Hedgehog.hs b/clash-protocols/src/Protocols/PacketStream/Hedgehog.hs new file mode 100644 index 00000000..4e0549b7 --- /dev/null +++ b/clash-protocols/src/Protocols/PacketStream/Hedgehog.hs @@ -0,0 +1,510 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE NoImplicitPrelude #-} + +{- | +Copyright : (C) 2024, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +Provides Hedgehog generators, models and utility functions for testing +`PacketStream` circuits. +-} +module Protocols.PacketStream.Hedgehog ( + -- * Utility functions + chopBy, + chopPacket, + chunkByPacket, + chunkToPacket, + fullPackets, + smearAbort, + + -- * Models + dropAbortedPackets, + downConvert, + upConvert, + depacketizerModel, + depacketizeToDfModel, + dropTailModel, + packetizerModel, + packetizeFromDfModel, + + -- * Hedgehog generators + AbortMode (..), + PacketOptions (..), + defPacketOptions, + genValidPacket, + genPackets, +) where + +import Clash.Hedgehog.Sized.Vector (genVec) +import Clash.Prelude +import qualified Clash.Sized.Vector as Vec + +import qualified Data.List as L +import Data.Maybe (fromJust, isJust) + +import Hedgehog (Gen, Range) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Protocols.PacketStream.Base + +-- | Partition a list based on given function. +chunkBy :: (a -> Bool) -> [a] -> [[a]] +chunkBy _ [] = [] +chunkBy predicate list = L.filter (not . null) (chunkByHelper predicate list []) + +-- Helper function to accumulate chunks. +chunkByHelper :: (a -> Bool) -> [a] -> [a] -> [[a]] +chunkByHelper _ [] acc = [L.reverse acc] +chunkByHelper predicate (x : xs) acc + | predicate x = L.reverse (x : acc) : chunkByHelper predicate xs [] + | otherwise = chunkByHelper predicate xs (x : acc) + +-- | Partition a list of `PacketStream` transfers into complete packets. +chunkByPacket :: + [PacketStreamM2S dataWidth meta] -> + [[PacketStreamM2S dataWidth meta]] +chunkByPacket = chunkBy (isJust . _last) + +{- | +If a packet contains a transfer with `_abort` set, set the `_abort` of +all following transfers in the same packet. +-} +smearAbort :: + [PacketStreamM2S dataWidth meta] -> + [PacketStreamM2S dataWidth meta] +smearAbort [] = [] +smearAbort (x : xs) = L.reverse $ L.foldl' go [x] xs + where + go [] _ = [] + go l@(a : _) (PacketStreamM2S dat last' meta abort) = + PacketStreamM2S dat last' meta (_abort a || abort) : l + +-- | Partition a list into groups of given size +chopBy :: Int -> [a] -> [[a]] +chopBy _ [] = [] +chopBy n xs = as : chopBy n bs where (as, bs) = L.splitAt n xs + +{- | +Merge a list of `PacketStream` transfers with data width @1@ to +a single `PacketStream` transfer with data width @dataWidth@. +-} +chunkToPacket :: + (KnownNat dataWidth) => + [PacketStreamM2S 1 meta] -> + PacketStreamM2S dataWidth meta +chunkToPacket xs = + PacketStreamM2S + { _last = + (\i -> let l = fromIntegral (L.length xs) in if i == 0 then l - 1 else l) + <$> _last lastTransfer + , _abort = any _abort xs + , _meta = _meta lastTransfer + , _data = L.foldr ((+>>) . head . _data) (repeat (nullByte "chunkToPacket")) xs + } + where + lastTransfer = L.last xs + +{- | +Split a single `PacketStream` transfer with data width @dataWidth@ to +a list of `PacketStream` transfers with data width @1@. +-} +chopPacket :: + forall dataWidth meta. + (1 <= dataWidth) => + (KnownNat dataWidth) => + PacketStreamM2S dataWidth meta -> + [PacketStreamM2S 1 meta] +chopPacket PacketStreamM2S{..} = packets + where + lasts = case _last of + Nothing -> L.repeat Nothing + Just size -> + if size == 0 + then [Just 0] + else L.replicate (fromIntegral size - 1) Nothing L.++ [Just (1 :: Index 2)] + + datas = case _last of + Nothing -> toList _data + Just size -> L.take (max 1 (fromIntegral size)) $ toList _data + + packets = + ( \(size, dat) -> + PacketStreamM2S (pure dat) size _meta _abort + ) + <$> L.zip lasts datas + +-- | Set `_last` of the last transfer in the list to @Just 1@ +fullPackets :: + (KnownNat dataWidth) => + [PacketStreamM2S dataWidth meta] -> + [PacketStreamM2S dataWidth meta] +fullPackets [] = [] +fullPackets fragments = + let lastFragment = (L.last fragments){_last = Just 1} + in L.init fragments L.++ [lastFragment] + +-- | Drops packets if one of the transfers in the packet has `_abort` set. +dropAbortedPackets :: + [PacketStreamM2S dataWidth meta] -> + [PacketStreamM2S dataWidth meta] +dropAbortedPackets packets = L.concat $ L.filter (not . any _abort) (chunkByPacket packets) + +{- | +Splits a list of `PacketStream` transfers with data width @1@ into +a list of `PacketStream` transfers with data width @dataWidth@ +-} +downConvert :: + forall dataWidth meta. + (1 <= dataWidth) => + (KnownNat dataWidth) => + [PacketStreamM2S dataWidth meta] -> + [PacketStreamM2S 1 meta] +downConvert = L.concatMap chopPacket + +{- | +Merges a list of `PacketStream` transfers with data width @dataWidth@ into +a list of `PacketStream` transfers with data width @1@ +-} +upConvert :: + forall dataWidth meta. + (1 <= dataWidth) => + (KnownNat dataWidth) => + [PacketStreamM2S 1 meta] -> + [PacketStreamM2S dataWidth meta] +upConvert packets = + L.map + chunkToPacket + (chunkByPacket packets >>= chopBy (natToNum @dataWidth)) + +-- | Model of the generic `Protocols.PacketStream.depacketizerC`. +depacketizerModel :: + forall + (dataWidth :: Nat) + (headerBytes :: Nat) + (metaIn :: Type) + (header :: Type) + (metaOut :: Type). + (KnownNat dataWidth) => + (KnownNat headerBytes) => + (1 <= dataWidth) => + (1 <= headerBytes) => + (NFDataX metaIn) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (header -> metaIn -> metaOut) -> + [PacketStreamM2S dataWidth metaIn] -> + [PacketStreamM2S dataWidth metaOut] +depacketizerModel toMetaOut ps = L.concat dataWidthPackets + where + hdrBytes = natToNum @headerBytes + + parseHdr :: + ([PacketStreamM2S 1 metaIn], [PacketStreamM2S 1 metaIn]) -> + [PacketStreamM2S 1 metaOut] + parseHdr (hdrF, fwdF) = fmap (\f -> f{_meta = metaOut}) fwdF' + where + fwdF' = case fwdF of + [] -> + [ PacketStreamM2S + (Vec.singleton (nullByte "depacketizerModel")) + (Just 0) + (deepErrorX "depacketizerModel: should be replaced") + (_abort (L.last hdrF)) + ] + _ -> fwdF + + hdr = bitCoerce $ Vec.unsafeFromList @headerBytes $ _data <$> hdrF + metaOut = toMetaOut hdr (_meta $ L.head hdrF) + + bytePackets :: [[PacketStreamM2S 1 metaIn]] + bytePackets = + L.filter + ( \fs -> + let len' = L.length fs + in len' > hdrBytes || len' == hdrBytes && _last (L.last fs) == Just 1 + ) + $ downConvert + . smearAbort + <$> chunkByPacket ps + + parsedPackets :: [[PacketStreamM2S 1 metaOut]] + parsedPackets = L.map go bytePackets + + go = parseHdr . L.splitAt hdrBytes + + dataWidthPackets :: [[PacketStreamM2S dataWidth metaOut]] + dataWidthPackets = L.map upConvert parsedPackets + +-- | Model of the generic `Protocols.PacketStream.depacketizeToDfC`. +depacketizeToDfModel :: + forall + (dataWidth :: Nat) + (headerBytes :: Nat) + (a :: Type) + (header :: Type) + (metaIn :: Type). + (KnownNat dataWidth) => + (KnownNat headerBytes) => + (1 <= dataWidth) => + (1 <= headerBytes) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (header -> metaIn -> a) -> + [PacketStreamM2S dataWidth metaIn] -> + [a] +depacketizeToDfModel toOut ps = L.map parseHdr bytePackets + where + parseHdr :: [PacketStreamM2S 1 metaIn] -> a + parseHdr hdrF = + toOut + (bitCoerce $ Vec.unsafeFromList $ L.map _data hdrF) + (_meta $ L.head hdrF) + + bytePackets :: [[PacketStreamM2S 1 metaIn]] + bytePackets = + L.filter + ( \pkt -> + (L.length pkt > natToNum @headerBytes) + || (L.length pkt == natToNum @headerBytes && _last (L.last pkt) == Just 1) + ) + (chunkByPacket $ downConvert (dropAbortedPackets ps)) + +-- | Model of 'Protocols.PacketStream.dropTailC'. +dropTailModel :: + forall dataWidth meta n. + (KnownNat dataWidth) => + (1 <= dataWidth) => + (1 <= n) => + SNat n -> + [PacketStreamM2S dataWidth meta] -> + [PacketStreamM2S dataWidth meta] +dropTailModel SNat packets = L.concatMap go (chunkByPacket packets) + where + go :: [PacketStreamM2S dataWidth meta] -> [PacketStreamM2S dataWidth meta] + go packet = + upConvert + $ L.init trimmed + L.++ [(L.last trimmed){_last = _last $ L.last bytePkts, _abort = aborted}] + where + aborted = L.any _abort packet + bytePkts = downConvert packet + trimmed = L.take (L.length bytePkts - natToNum @n) bytePkts + +-- | Model of the generic `Protocols.PacketStream.packetizerC`. +packetizerModel :: + forall + (dataWidth :: Nat) + (headerBytes :: Nat) + (metaIn :: Type) + (header :: Type) + (metaOut :: Type). + (KnownNat dataWidth) => + (KnownNat headerBytes) => + (1 <= dataWidth) => + (1 <= headerBytes) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (metaIn -> metaOut) -> + (metaIn -> header) -> + [PacketStreamM2S dataWidth metaIn] -> + [PacketStreamM2S dataWidth metaOut] +packetizerModel toMetaOut toHeader ps = L.concatMap (upConvert . prependHdr) bytePackets + where + prependHdr :: [PacketStreamM2S 1 metaIn] -> [PacketStreamM2S 1 metaOut] + prependHdr fragments = hdr L.++ L.map (\f -> f{_meta = metaOut}) fragments + where + h = L.head fragments + metaOut = toMetaOut (_meta h) + hdr = L.map go (toList $ bitCoerce (toHeader (_meta h))) + go byte = PacketStreamM2S (singleton byte) Nothing metaOut (_abort h) + + bytePackets :: [[PacketStreamM2S 1 metaIn]] + bytePackets = downConvert . smearAbort <$> chunkByPacket ps + +-- | Model of the generic `Protocols.PacketStream.packetizeFromDfC`. +packetizeFromDfModel :: + forall + (dataWidth :: Nat) + (headerBytes :: Nat) + (a :: Type) + (header :: Type) + (metaOut :: Type). + (KnownNat dataWidth) => + (KnownNat headerBytes) => + (1 <= dataWidth) => + (1 <= headerBytes) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (a -> metaOut) -> + (a -> header) -> + [a] -> + [PacketStreamM2S dataWidth metaOut] +packetizeFromDfModel toMetaOut toHeader = L.concatMap (upConvert . dfToPacket) + where + dfToPacket :: a -> [PacketStreamM2S 1 metaOut] + dfToPacket d = + fullPackets + $ L.map + (\byte -> PacketStreamM2S (singleton byte) Nothing (toMetaOut d) False) + (toList $ bitCoerce (toHeader d)) + +-- | Abort generation options for packet generation. +data AbortMode + = Abort + { amPacketGen :: Gen Bool + -- ^ Determines the chance to generate aborted fragments in a packet. + , amTransferGen :: Gen Bool + -- ^ Determines the frequency of aborted fragments in a packet. + } + | NoAbort + +-- | Various configuration options for packet generation. +data PacketOptions = PacketOptions + { poAllowEmptyPackets :: Bool + -- ^ Whether to allow the generation of zero-byte packets. + , poAllowTrailingEmpty :: Bool + -- ^ Whether to allow the generation of trailing zero-byte transfers. + , poAbortMode :: AbortMode + -- ^ If set to @NoAbort@, no transfers in the packet will have '_abort' set. + -- Else, randomly generate them according to some distribution. See 'AbortMode'. + } + +{- | +Default packet generation options: + +- Allow the generation of a zero-byte packet; +- Allow the generation of a trailing zero-byte transfer; +- 50% chance to generate aborted transfers. If aborts are generated, 10% of + transfers will be aborted. +-} +defPacketOptions :: PacketOptions +defPacketOptions = + PacketOptions + { poAllowEmptyPackets = True + , poAllowTrailingEmpty = True + , poAbortMode = + Abort + { amPacketGen = Gen.enumBounded + , amTransferGen = + Gen.frequency + [ (90, Gen.constant False) + , (10, Gen.constant True) + ] + } + } + +{- | +Generate packets with a user-supplied generator and a linear range. +-} +genPackets :: + forall (dataWidth :: Nat) (meta :: Type). + (1 <= dataWidth) => + (KnownNat dataWidth) => + -- | Minimum amount of packets to generate. + Int -> + -- | Maximum amount of packets to generate. + Int -> + -- | Packet generator. + Gen [PacketStreamM2S dataWidth meta] -> + Gen [PacketStreamM2S dataWidth meta] +genPackets minB maxB pktGen = L.concat <$> Gen.list (Range.linear minB maxB) pktGen +{-# INLINE genPackets #-} + +{- | +Generate a valid packet, i.e. a packet of which all transfers carry the same +`_meta` and with all bytes in `_data` that are not enabled set to 0x00. +-} +genValidPacket :: + forall (dataWidth :: Nat) (meta :: Type). + (1 <= dataWidth) => + (KnownNat dataWidth) => + -- | Configuration options for packet generation. + PacketOptions -> + -- | Generator for the metadata. + Gen meta -> + -- | The amount of transfers with @_last = Nothing@ to generate. + -- This function will always generate an extra transfer with @_last = Just i@. + Range Int -> + Gen [PacketStreamM2S dataWidth meta] +genValidPacket PacketOptions{..} metaGen size = + let + abortGen = case poAbortMode of + NoAbort -> Gen.constant False + Abort pktGen transferGen -> do + allowAborts <- pktGen + (if allowAborts then transferGen else Gen.constant False) + in + do + meta <- metaGen + transfers <- Gen.list size (genTransfer meta abortGen) + lastTransfer <- + genLastTransfer + meta + ( (null transfers && poAllowEmptyPackets) + || (not (null transfers) && poAllowTrailingEmpty) + ) + abortGen + pure (transfers L.++ [lastTransfer]) + +-- | Generate a single transfer which is not yet the end of a packet. +genTransfer :: + forall (dataWidth :: Nat) (meta :: Type). + (1 <= dataWidth) => + (KnownNat dataWidth) => + -- | We need to use the same metadata + -- for every transfer in a packet to satisfy the protocol + -- invariant that metadata is constant for an entire packet. + meta -> + -- | Whether to set '_abort'. + Gen Bool -> + Gen (PacketStreamM2S dataWidth meta) +genTransfer meta abortGen = + PacketStreamM2S + <$> genVec Gen.enumBounded + <*> Gen.constant Nothing + <*> Gen.constant meta + <*> abortGen + +{- | +Generate the last transfer of a packet, i.e. a transfer with @_last@ set as @Just@. +All bytes which are not enabled are forced /undefined/. +-} +genLastTransfer :: + forall (dataWidth :: Nat) (meta :: Type). + (1 <= dataWidth) => + (KnownNat dataWidth) => + -- | We need to use the same metadata + -- for every transfer in a packet to satisfy the protocol + -- invariant that metadata is constant for an entire packet. + meta -> + -- | Whether we are allowed to generate a 0-byte transfer. + Bool -> + -- | Whether to set '_abort'. + Gen Bool -> + Gen (PacketStreamM2S dataWidth meta) +genLastTransfer meta allowEmpty abortGen = + setNull + <$> ( PacketStreamM2S + <$> genVec Gen.enumBounded + <*> (Just <$> Gen.enum (if allowEmpty then 0 else 1) maxBound) + <*> Gen.constant meta + <*> abortGen + ) + +setNull :: + forall (dataWidth :: Nat) (meta :: Type). + (KnownNat dataWidth) => + PacketStreamM2S dataWidth meta -> + PacketStreamM2S dataWidth meta +setNull transfer = + let i = fromJust (_last transfer) + in transfer + { _data = + fromJust + ( Vec.fromList + $ L.take (fromIntegral i) (toList (_data transfer)) + L.++ L.replicate ((natToNum @dataWidth) - fromIntegral i) (nullByte "setNull") + ) + } diff --git a/clash-protocols/src/Protocols/PacketStream/PacketFifo.hs b/clash-protocols/src/Protocols/PacketStream/PacketFifo.hs new file mode 100644 index 00000000..bb6ba99a --- /dev/null +++ b/clash-protocols/src/Protocols/PacketStream/PacketFifo.hs @@ -0,0 +1,330 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_HADDOCK hide #-} + +{- | +Copyright : (C) 2024, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +Optimized store and forward FIFO circuit for packet streams. +-} +module Protocols.PacketStream.PacketFifo ( + packetFifoC, + FullMode (..), +) where + +import Clash.Prelude + +import Data.Maybe +import Data.Maybe.Extra (toMaybe) + +import Protocols +import Protocols.PacketStream.Base + +type PacketStreamContent (dataWidth :: Nat) (meta :: Type) = + (Vec dataWidth (BitVector 8), Maybe (Index (dataWidth + 1))) + +-- | Specifies the behaviour of `packetFifoC` when it is full. +data FullMode + = -- | Assert backpressure when the FIFO is full. + Backpressure + | -- | Drop new packets when the FIFO is full. + -- The FIFO never asserts backpressure. + Drop + +toPacketStreamContent :: + PacketStreamM2S dataWidth meta -> PacketStreamContent dataWidth meta +toPacketStreamContent PacketStreamM2S{..} = (_data, _last) + +toPacketStreamM2S :: + PacketStreamContent dataWidth meta -> meta -> PacketStreamM2S dataWidth meta +toPacketStreamM2S (d, l) m = PacketStreamM2S d l m False + +data PacketFifoState contentDepth metaDepth = PacketFifoState + { _canRead :: Bool + -- ^ We need this to avoid read-write conflicts. + , _dropping :: Bool + -- ^ Whether we are dropping the current packet. + , _basePtr :: Unsigned contentDepth + -- ^ Points to the base address of the current packet, i.e. the address of + -- the first transfer. + , _cReadPtr :: Unsigned contentDepth + -- ^ Read pointer in the content block ram. + , _cWritePtr :: Unsigned contentDepth + -- ^ Write pointer in the content block ram. + , _mReadPtr :: Unsigned metaDepth + -- ^ Read pointer in the metadata block ram. + , _mWritePtr :: Unsigned metaDepth + -- ^ Write pointer in the metadata block ram. + } + deriving (Generic, NFDataX, Show, ShowX) + +-- | State transition function of 'packetFifoC', mode @Backpressure@. +packetFifoT :: + forall + (dataWidth :: Nat) + (meta :: Type) + (contentDepth :: Nat) + (metaDepth :: Nat). + (KnownNat dataWidth) => + (KnownNat contentDepth) => + (KnownNat metaDepth) => + (1 <= contentDepth) => + (1 <= metaDepth) => + (NFDataX meta) => + PacketFifoState contentDepth metaDepth -> + ( Maybe (PacketStreamM2S dataWidth meta) + , PacketStreamS2M + , PacketStreamContent dataWidth meta + , meta + ) -> + ( PacketFifoState contentDepth metaDepth + , ( Unsigned contentDepth + , Unsigned metaDepth + , Maybe (Unsigned contentDepth, PacketStreamContent dataWidth meta) + , Maybe (Unsigned metaDepth, meta) + , PacketStreamS2M + , Maybe (PacketStreamM2S dataWidth meta) + ) + ) +packetFifoT st@PacketFifoState{..} (fwdIn, bwdIn, cRam, mRam) = + (nextSt, (cReadPtr', mReadPtr', cWriteCmd, mWriteCmd, bwdOut, fwdOut)) + where + -- Status signals + pktTooBig = _cWritePtr + 1 == _cReadPtr && fifoEmpty + (lastPkt, dropping) = case fwdIn of + Nothing -> (False, _dropping || pktTooBig) + Just PacketStreamM2S{..} -> (isJust _last, _dropping || pktTooBig || _abort) + + fifoEmpty = _mReadPtr == _mWritePtr + fifoSinglePacket = _mReadPtr + 1 == _mWritePtr + fifoFull = + (_cWritePtr + 1 == _cReadPtr) + || (_mWritePtr + 1 == _mReadPtr && lastPkt) + + -- Enables + readEn = _canRead && not fifoEmpty + cReadEn = readEn && _ready bwdIn + mReadEn = readEn && _ready bwdIn && isJust (snd cRam) + + -- Output + bwdOut = PacketStreamS2M (not fifoFull || dropping) + fwdOut = + if readEn + then Just (toPacketStreamM2S cRam mRam) + else Nothing + + -- New state + + -- Our block RAM is read-before-write, so we cannot use the read value next + -- clock cycle if there is a read-write conflict. Such a conflict might happen + -- when we finish writing a packet into the FIFO while: + -- 1. The FIFO is empty. + -- 2. The FIFO has one packet inside and we finish outputting it this clock cycle. + canRead' = not (lastPkt && (fifoEmpty || (mReadEn && fifoSinglePacket))) + dropping' = dropping && not lastPkt + + basePtr' = if lastPkt && _ready bwdOut then cWritePtr' else _basePtr + cReadPtr' = if cReadEn then _cReadPtr + 1 else _cReadPtr + mReadPtr' = if mReadEn then _mReadPtr + 1 else _mReadPtr + + (cWriteCmd, cWritePtr') = + if not dropping && not fifoFull + then + ( (\t -> (_cWritePtr, toPacketStreamContent t)) <$> fwdIn + , _cWritePtr + 1 + ) + else + ( Nothing + , if dropping then _basePtr else _cWritePtr + ) + + -- Write the metadata into RAM upon the last transfer of a packet, and + -- advance the write pointer. This allows us to write the data of a packet + -- into RAM even if the metadata RAM is currently full (hoping that it will + -- free up before we read the end of the packet). It also prevents unnecessary + -- writes in case a packet is aborted or too big. + (mWriteCmd, mWritePtr') = + if not dropping && not fifoFull && lastPkt + then ((\t -> (_mWritePtr, _meta t)) <$> fwdIn, _mWritePtr + 1) + else (Nothing, _mWritePtr) + + nextSt = case fwdIn of + Nothing -> st{_canRead = True, _cReadPtr = cReadPtr', _mReadPtr = mReadPtr'} + Just _ -> + PacketFifoState + { _canRead = canRead' + , _dropping = dropping' + , _basePtr = basePtr' + , _cReadPtr = cReadPtr' + , _cWritePtr = cWritePtr' + , _mReadPtr = mReadPtr' + , _mWritePtr = mWritePtr' + } + +-- | Implementation of 'packetFifoC', mode @Drop@. +packetFifoImpl :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (meta :: Type) + (contentSizeBits :: Nat) + (metaSizeBits :: Nat). + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (1 <= contentSizeBits) => + (1 <= metaSizeBits) => + (NFDataX meta) => + -- | Depth of the content of the packet buffer, this is equal to 2^contentSizeBits + SNat contentSizeBits -> + -- | Depth of the content of the meta buffer, this is equal to 2^metaSizeBits + SNat metaSizeBits -> + -- | Input packetStream + ( Signal dom (Maybe (PacketStreamM2S dataWidth meta)) + , Signal dom PacketStreamS2M + ) -> + -- | Output CSignal s + ( Signal dom PacketStreamS2M + , Signal dom (Maybe (PacketStreamM2S dataWidth meta)) + ) +packetFifoImpl SNat SNat (fwdIn, bwdIn) = (PacketStreamS2M . not <$> fullBuffer, fwdOut) + where + fwdOut = toMaybe <$> (not <$> emptyBuffer) <*> (toPacketStreamM2S <$> ramContent <*> ramMeta) + + -- The backing ram + ramContent = + blockRam1 + NoClearOnReset + (SNat @(2 ^ contentSizeBits)) + (errorX "initial block ram content") + cReadAddr' + writeCommand + ramMeta = + blockRam1 + NoClearOnReset + (SNat @(2 ^ metaSizeBits)) + (errorX "initial block ram meta content") + mReadAddr' + mWriteCommand + + -- The write commands to the RAM + writeCommand = + toMaybe + <$> writeEnable + <*> bundle (cWordAddr, toPacketStreamContent . fromJustX <$> fwdIn) + mWriteCommand = toMaybe <$> nextPacketIn <*> bundle (mWriteAddr, _meta . fromJustX <$> fwdIn) + + -- Addresses for the content data + cWordAddr, cPacketAddr, cReadAddr :: Signal dom (Unsigned contentSizeBits) + cWordAddr = register 0 $ mux dropping' cPacketAddr $ mux writeEnable (cWordAddr + 1) cWordAddr + cPacketAddr = register 0 $ mux nextPacketIn (cWordAddr + 1) cPacketAddr + cReadAddr' = mux readEnable (cReadAddr + 1) cReadAddr + cReadAddr = register 0 cReadAddr' + + -- Addresses for the meta data + mWriteAddr, mReadAddr :: Signal dom (Unsigned metaSizeBits) + mWriteAddr = register 0 mWriteAddr' + mWriteAddr' = mux nextPacketIn (mWriteAddr + 1) mWriteAddr + + mReadAddr' = mux mReadEnable (mReadAddr + 1) mReadAddr + mReadAddr = register 0 mReadAddr' + -- only read the next value if we've outputted the last word of a packet + mReadEnable = lastWordOut .&&. readEnable + + -- Registers : status + dropping', dropping, emptyBuffer :: Signal dom Bool + -- start dropping packet on abort + dropping' = abortIn .||. dropping + dropping = register False $ dropping' .&&. (not <$> lastWordIn) + -- the buffer is empty if the metaBuffer is empty as the meta buffer + -- only updates when a packet is complete + emptyBuffer = register 0 mWriteAddr .==. mReadAddr + + -- Only write if there is space and we're not dropping + writeEnable = writeRequest .&&. (not <$> fullBuffer) .&&. (not <$> dropping') + -- Read when the word has been received + readEnable = (not <$> emptyBuffer) .&&. (_ready <$> bwdIn) + + -- The status signals + fullBuffer = ((cWordAddr + 1) .==. cReadAddr) .||. ((mWriteAddr + 1) .==. mReadAddr) + writeRequest = isJust <$> fwdIn + lastWordIn = maybe False (isJust . _last) <$> fwdIn + lastWordOut = maybe False (isJust . _last) <$> fwdOut + abortIn = maybe False _abort <$> fwdIn + nextPacketIn = lastWordIn .&&. writeEnable + +{- | +FIFO circuit optimized for the PacketStream protocol. Contains two FIFOs, one +for packet data ('_data', '_last') and one for packet metadata ('_meta'). +Because metadata is constant per packet, the metadata FIFO can be significantly +shallower, saving resources. + +Moreover, the output of the FIFO has some other properties: + +- All packets which contain a transfer with '_abort' set are dropped. +- All packets that are bigger than or equal to @2^contentDepth - 1@ transfers are dropped. +- There are no gaps in output packets, i.e. @Nothing@ in between valid transfers of a packet. + +The circuit is able to satisfy these properties because it first loads an entire +packet before it may transmit it. That is also why packets bigger than the +content FIFO need to be dropped. + +Two modes can be selected: + +- @Backpressure@: assert backpressure like normal when the FIFO is full. +- @Drop@: never give backpressure, instead drop the current packet we are loading. +-} +packetFifoC :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (meta :: Type) + (contentDepth :: Nat) + (metaDepth :: Nat). + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (1 <= contentDepth) => + (1 <= metaDepth) => + (NFDataX meta) => + -- | The content FIFO will contain @2^contentDepth@ entries. + SNat contentDepth -> + -- | The metadata FIFO will contain @2^metaDepth@ entries. + SNat metaDepth -> + -- | The backpressure behaviour of the FIFO when it is full. + FullMode -> + Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta) +packetFifoC cSize@SNat mSize@SNat fullMode = + let + ckt (fwdIn, bwdIn) = (bwdOut, fwdOut) + where + ramContent = + blockRam1 + NoClearOnReset + (SNat @(2 ^ contentDepth)) + (deepErrorX "initial block ram content") + cReadPtr + cWriteCommand + ramMeta = + blockRam1 + NoClearOnReset + (SNat @(2 ^ metaDepth)) + (deepErrorX "initial block ram meta content") + mReadPtr + mWriteCommand + + (cReadPtr, mReadPtr, cWriteCommand, mWriteCommand, bwdOut, fwdOut) = + mealyB + (packetFifoT @dataWidth @meta @contentDepth @metaDepth) + (PacketFifoState False False 0 0 0 0 0) + (fwdIn, bwdIn, ramContent, ramMeta) + in + case fullMode of + Backpressure -> + forceResetSanity |> fromSignals ckt + Drop -> + toCSignal + |> unsafeAbortOnBackpressureC + |> forceResetSanity + |> fromSignals (packetFifoImpl cSize mSize) diff --git a/clash-protocols/src/Protocols/PacketStream/Packetizers.hs b/clash-protocols/src/Protocols/PacketStream/Packetizers.hs new file mode 100644 index 00000000..d35fe927 --- /dev/null +++ b/clash-protocols/src/Protocols/PacketStream/Packetizers.hs @@ -0,0 +1,438 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-} +{-# OPTIONS_HADDOCK hide #-} + +{- | +Copyright : (C) 2024, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +Utility circuits for appending headers to the beginning of packets. +-} +module Protocols.PacketStream.Packetizers ( + packetizerC, + packetizeFromDfC, +) where + +import Clash.Prelude + +import Protocols +import qualified Protocols.Df as Df +import Protocols.PacketStream.Base + +import Clash.Sized.Vector.Extra (takeLe) +import Data.Constraint (Dict (Dict)) +import Data.Constraint.Nat.Extra (leModulusDivisor, strictlyPositiveDivRu) +import Data.Maybe +import Data.Maybe.Extra +import Data.Type.Equality ((:~:) (Refl)) + +type PacketizerCt (header :: Type) (headerBytes :: Nat) (dataWidth :: Nat) = + ( BitPack header + , BitSize header ~ headerBytes * 8 + , KnownNat headerBytes + , KnownNat dataWidth + , 1 <= headerBytes + , 1 <= dataWidth + ) + +data PacketizerState1 (metaOut :: Type) (headerBytes :: Nat) (dataWidth :: Nat) + = Insert1 + { _aborted1 :: Bool + } + | Forward1 + { _aborted1 :: Bool + , _hdrBuf1 :: Vec headerBytes (BitVector 8) + } + | LastForward1 + { _aborted1 :: Bool + , _hdrBuf1 :: Vec headerBytes (BitVector 8) + } + deriving (Generic, NFDataX, Show, ShowX) + +-- | Packetizer transition function in case @dataWidth > headerBytes@ +packetizerT1 :: + forall + (headerBytes :: Nat) + (dataWidth :: Nat) + (header :: Type) + (metaIn :: Type) + (metaOut :: Type). + (PacketizerCt header headerBytes dataWidth) => + (headerBytes + 1 <= dataWidth) => + (metaIn -> metaOut) -> + (metaIn -> header) -> + PacketizerState1 metaOut headerBytes dataWidth -> + (Maybe (PacketStreamM2S dataWidth metaIn), PacketStreamS2M) -> + ( PacketizerState1 metaOut headerBytes dataWidth + , (PacketStreamS2M, Maybe (PacketStreamM2S dataWidth metaOut)) + ) +packetizerT1 toMetaOut toHeader st (Just inPkt, bwdIn) = + let + go buf = (nextStOut, (bwdOut, Just outPkt)) + where + bytesOut :: Vec (dataWidth - headerBytes) (BitVector 8) + (bytesOut, newBuf) = + leToPlus @headerBytes @dataWidth $ splitAt (SNat @(dataWidth - headerBytes)) (_data inPkt) + nextAborted = _aborted1 st || _abort inPkt + + outPkt = + inPkt + { _data = buf ++ bytesOut + , _last = newLast + , _meta = toMetaOut (_meta inPkt) + , _abort = nextAborted + } + + (nextSt, newLast) = case _last inPkt of + Nothing -> (Forward1 nextAborted newBuf, Nothing) + Just i + | i <= natToNum @(dataWidth - headerBytes) -> + (Insert1 False, Just (i + natToNum @headerBytes)) + | otherwise -> (LastForward1 nextAborted newBuf, Nothing) + + nextStOut = if _ready bwdIn then nextSt else st + bwdOut = case nextStOut of + LastForward1{} -> PacketStreamS2M False + _ -> bwdIn + in + case st of + Insert1{} -> go (bitCoerce (toHeader (_meta inPkt))) + Forward1{..} -> go _hdrBuf1 + LastForward1{..} -> (nextStOut, (bwdIn, Just outPkt)) + where + outPkt = + inPkt + { _data = _hdrBuf1 ++ repeat (nullByte "packetizerT1") + , _last = (\i -> i - natToNum @(dataWidth - headerBytes)) <$> _last inPkt + , _meta = toMetaOut (_meta inPkt) + , _abort = _aborted1 || _abort inPkt + } + nextStOut = if _ready bwdIn then Insert1 False else st +packetizerT1 _ _ s (Nothing, bwdIn) = (s, (bwdIn, Nothing)) + +data PacketizerState2 (metaOut :: Type) (headerBytes :: Nat) (dataWidth :: Nat) + = LoadHeader2 + | Insert2 + { _aborted2 :: Bool + , _hdrBuf2 :: Vec headerBytes (BitVector 8) + , _counter2 :: Index (headerBytes `DivRU` dataWidth) + } + | Forward2 + { _aborted2 :: Bool + } + deriving (Generic, NFDataX, Show, ShowX) + +-- | Packetizer transition function in case @dataWidth <= headerBytes@ and @headerBytes % dataWidth ~ 0@ +packetizerT2 :: + forall + (headerBytes :: Nat) + (dataWidth :: Nat) + (header :: Type) + (metaIn :: Type) + (metaOut :: Type). + (PacketizerCt header headerBytes dataWidth) => + (headerBytes `Mod` dataWidth ~ 0) => + (dataWidth <= headerBytes) => + (metaIn -> metaOut) -> + (metaIn -> header) -> + PacketizerState2 metaOut headerBytes dataWidth -> + (Maybe (PacketStreamM2S dataWidth metaIn), PacketStreamS2M) -> + ( PacketizerState2 metaOut headerBytes dataWidth + , (PacketStreamS2M, Maybe (PacketStreamM2S dataWidth metaOut)) + ) +-- Load the metadata into a buffer. This costs one extra cycle of latency, but it reduces resource usage. +packetizerT2 _ toHeader LoadHeader2 (Just inPkt, _) = + (Insert2 False (bitCoerce (toHeader (_meta inPkt))) 0, (PacketStreamS2M False, Nothing)) +packetizerT2 toMetaOut _ st@Insert2{..} (Just inPkt, bwdIn) = + (nextStOut, (PacketStreamS2M False, Just outPkt)) + where + (newBuf, dataOut) = leToPlus @dataWidth @headerBytes $ shiftOutFrom0 (SNat @dataWidth) _hdrBuf2 + nextAborted = _aborted2 || _abort inPkt + outPkt = + inPkt + { _data = dataOut + , _last = Nothing + , _meta = toMetaOut (_meta inPkt) + , _abort = nextAborted + } + + nextSt + | _counter2 == maxBound = Forward2 nextAborted + | otherwise = Insert2 nextAborted newBuf (succ _counter2) + + nextStOut = if _ready bwdIn then nextSt else st +packetizerT2 toMetaOut _ Forward2{..} (Just inPkt, bwdIn) = + (nextStOut, (bwdIn, Just outPkt)) + where + nextAborted = _aborted2 || _abort inPkt + outPkt = + inPkt + { _meta = toMetaOut (_meta inPkt) + , _abort = nextAborted + } + nextStOut + | isJust (_last inPkt) && _ready bwdIn = LoadHeader2 + | otherwise = Forward2 nextAborted +packetizerT2 _ _ s (Nothing, bwdIn) = (s, (bwdIn, Nothing)) + +data PacketizerState3 (headerBytes :: Nat) (dataWidth :: Nat) + = LoadHeader3 + | Insert3 + { _aborted3 :: Bool + , _hdrBuf3 :: Vec (headerBytes + dataWidth) (BitVector 8) + , _counter3 :: Index (headerBytes `DivRU` dataWidth) + } + | Forward3 + { _aborted3 :: Bool + , _hdrBuf3 :: Vec (headerBytes + dataWidth) (BitVector 8) + } + | LastForward3 + { _aborted3 :: Bool + , _hdrBuf3 :: Vec (headerBytes + dataWidth) (BitVector 8) + } + deriving (Generic, Show, ShowX) + +deriving instance + (KnownNat headerBytes, KnownNat dataWidth) => + NFDataX (PacketizerState3 headerBytes dataWidth) + +-- | Packetizer transition function in case @dataWidth <= headerBytes@ and @headerBytes % dataWidth > 0@ +packetizerT3 :: + forall + (headerBytes :: Nat) + (dataWidth :: Nat) + (header :: Type) + (metaIn :: Type) + (metaOut :: Type). + (PacketizerCt header headerBytes dataWidth) => + (1 <= headerBytes `Mod` dataWidth) => + (headerBytes `Mod` dataWidth <= dataWidth) => + (dataWidth <= headerBytes) => + (metaIn -> metaOut) -> + (metaIn -> header) -> + PacketizerState3 headerBytes dataWidth -> + (Maybe (PacketStreamM2S dataWidth metaIn), PacketStreamS2M) -> + ( PacketizerState3 headerBytes dataWidth + , (PacketStreamS2M, Maybe (PacketStreamM2S dataWidth metaOut)) + ) +packetizerT3 _ toHeader LoadHeader3 (Just inPkt, _bwdIn) = + (nextStOut, (PacketStreamS2M False, Nothing)) + where + nextStOut = Insert3 False (bitCoerce (toHeader (_meta inPkt)) ++ _data inPkt) 0 +packetizerT3 toMetaOut _ st@Insert3{..} (Just inPkt, bwdIn) = + (nextStOut, (bwdOut, Just outPkt)) + where + nextAborted = _aborted3 || _abort inPkt + (newHdrBuf, dataOut') = shiftOutFrom0 (SNat @dataWidth) _hdrBuf3 + + outPkt = + inPkt + { _data = dataOut' + , _last = lastOut + , _meta = toMetaOut (_meta inPkt) + } + + (lastOut, nextSt) = case (_counter3 == maxBound, _last inPkt) of + (False, _) -> (Nothing, Insert3 nextAborted newHdrBuf (succ _counter3)) + (True, Nothing) -> (Nothing, Forward3 nextAborted newHdrBuf) + (True, Just i) -> + if i <= natToNum @(dataWidth - headerBytes `Mod` dataWidth) + then (Just (i + natToNum @(headerBytes `Mod` dataWidth)), LoadHeader3) + else (Nothing, LastForward3 nextAborted newHdrBuf) + nextStOut = if _ready bwdIn then nextSt else st + bwdOut = case nextSt of + LoadHeader3 -> bwdIn + Forward3{} -> bwdIn + _ -> PacketStreamS2M False +packetizerT3 toMetaOut _ st@Forward3{..} (Just inPkt, bwdIn) = + (nextStOut, (bwdOut, Just outPkt)) + where + bytesOut :: Vec (dataWidth - headerBytes `Mod` dataWidth) (BitVector 8) + buf :: Vec (headerBytes `Mod` dataWidth) (BitVector 8) + (bytesOut, buf) = splitAt (SNat @(dataWidth - headerBytes `Mod` dataWidth)) (_data inPkt) + newBuf :: Vec (headerBytes + dataWidth) (BitVector 8) + newBuf = + buf + ++ repeat @(headerBytes + dataWidth - headerBytes `Mod` dataWidth) (nullByte "packetizerT3") + nextAborted = _aborted3 || _abort inPkt + + outPkt = + inPkt + { _data = take (SNat @(headerBytes `Mod` dataWidth)) _hdrBuf3 ++ bytesOut + , _last = lastOut + , _meta = toMetaOut (_meta inPkt) + , _abort = nextAborted + } + + (lastOut, nextSt) = case _last inPkt of + Nothing -> (Nothing, Forward3 nextAborted newBuf) + Just i -> + if i <= natToNum @(dataWidth - headerBytes `Mod` dataWidth) + then (Just (i + natToNum @(headerBytes `Mod` dataWidth)), LoadHeader3) + else (Nothing, LastForward3 nextAborted newBuf) + nextStOut = if _ready bwdIn then nextSt else st + + bwdOut = case nextSt of + LastForward3{} -> PacketStreamS2M False + _ -> bwdIn +packetizerT3 toMetaOut _ st@LastForward3{..} (Just inPkt, bwdIn) = + (nextStOut, (bwdIn, Just outPkt)) + where + outPkt = + inPkt + { _data = takeLe (SNat @dataWidth) _hdrBuf3 + , _last = (\i -> i - natToNum @(dataWidth - headerBytes `Mod` dataWidth)) <$> _last inPkt + , _meta = toMetaOut (_meta inPkt) + , _abort = _aborted3 || _abort inPkt + } + nextStOut = if _ready bwdIn then LoadHeader3 else st +packetizerT3 _ _ s (Nothing, bwdIn) = (s, (bwdIn, Nothing)) + +{- | +Writes a portion of the metadata to the front of the packet stream, and shifts +the stream accordingly. This portion is defined by the @(metaIn -> header)@ +input function. If this function is `id`, the entire metadata is put in front +of the packet stream. +-} +packetizerC :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (metaIn :: Type) + (metaOut :: Type) + (header :: Type) + (headerBytes :: Nat). + (HiddenClockResetEnable dom) => + (NFDataX metaOut) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (KnownNat headerBytes) => + (1 <= dataWidth) => + (1 <= headerBytes) => + (KnownNat dataWidth) => + -- | Mapping from input `_meta` to output `_meta` + (metaIn -> metaOut) -> + -- | Mapping from input `_meta` to the header that will be packetized + (metaIn -> header) -> + Circuit (PacketStream dom dataWidth metaIn) (PacketStream dom dataWidth metaOut) +packetizerC toMetaOut toHeader = fromSignals outCircuit + where + outCircuit = case leModulusDivisor @headerBytes @dataWidth of + Dict -> case compareSNat (SNat @(headerBytes + 1)) (SNat @dataWidth) of + SNatLE -> mealyB (packetizerT1 @headerBytes toMetaOut toHeader) (Insert1 False) + SNatGT -> + case ( sameNat (SNat @(headerBytes `Mod` dataWidth)) d0 + , compareSNat d1 (SNat @(headerBytes `Mod` dataWidth)) + ) of + (Just Refl, _) -> mealyB (packetizerT2 @headerBytes toMetaOut toHeader) LoadHeader2 + (Nothing, SNatLE) -> mealyB (packetizerT3 @headerBytes toMetaOut toHeader) LoadHeader3 + (_, _) -> + clashCompileError + "packetizerC: unreachable. Report this at https://github.com/clash-lang/clash-protocols/issues" + +data DfPacketizerState (metaOut :: Type) (headerBytes :: Nat) (dataWidth :: Nat) + = DfIdle + | DfInsert + { _dfCounter :: Index (headerBytes `DivRU` dataWidth - 1) + , _dfHdrBuf :: Vec (headerBytes - dataWidth) (BitVector 8) + } + deriving (Generic, Show, ShowX) + +deriving instance + (dataWidth <= headerBytes, KnownNat headerBytes, KnownNat dataWidth) => + NFDataX (DfPacketizerState metaOut headerBytes dataWidth) + +-- | packetizeFromDf state transition function in case dataWidth < headerBytes. +packetizeFromDfT :: + forall + (dataWidth :: Nat) + (a :: Type) + (metaOut :: Type) + (header :: Type) + (headerBytes :: Nat). + (NFDataX metaOut) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (KnownNat headerBytes) => + (KnownNat dataWidth) => + (1 <= dataWidth) => + (1 <= headerBytes `DivRU` dataWidth) => + ((dataWidth + 1) <= headerBytes) => + -- | Mapping from `Df` input to output `_meta` + (a -> metaOut) -> + -- | Mapping from `Df` input to the header that will be packetized + (a -> header) -> + DfPacketizerState metaOut headerBytes dataWidth -> + (Df.Data a, PacketStreamS2M) -> + ( DfPacketizerState metaOut headerBytes dataWidth + , (Ack, Maybe (PacketStreamM2S dataWidth metaOut)) + ) +packetizeFromDfT toMetaOut toHeader DfIdle (Df.Data dataIn, bwdIn) = (nextStOut, (Ack False, Just outPkt)) + where + (dataOut, hdrBuf) = splitAt (SNat @dataWidth) (bitCoerce (toHeader dataIn)) + outPkt = PacketStreamM2S dataOut Nothing (toMetaOut dataIn) False + nextStOut = if _ready bwdIn then DfInsert 0 hdrBuf else DfIdle + +-- 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)) + where + (dataOut, newHdrBuf) = + splitAt (SNat @dataWidth) (_dfHdrBuf ++ repeat @dataWidth (nullByte "packetizeFromDfT")) + outPkt = PacketStreamM2S dataOut newLast (toMetaOut dataIn) False + + newLast = toMaybe (_dfCounter == maxBound) $ case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of + SNatGT -> natToNum @(headerBytes `Mod` dataWidth) + _ -> natToNum @dataWidth + + 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)) + +{- | +Starts a packet stream upon receiving some data over a `Df` channel. +The bytes to be packetized and the output metadata are specified by the +input functions. +-} +packetizeFromDfC :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (a :: Type) + (metaOut :: Type) + (header :: Type) + (headerBytes :: Nat). + (HiddenClockResetEnable dom) => + (NFDataX metaOut) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (KnownNat headerBytes) => + (KnownNat dataWidth) => + (1 <= headerBytes) => + (1 <= dataWidth) => + -- | Mapping from `Df` input to output `_meta` + (a -> metaOut) -> + -- | Mapping from `Df` input to the header that will be packetized + (a -> header) -> + Circuit (Df dom a) (PacketStream dom dataWidth metaOut) +packetizeFromDfC toMetaOut toHeader = case strictlyPositiveDivRu @headerBytes @dataWidth of + Dict -> case compareSNat (SNat @headerBytes) (SNat @dataWidth) of + -- We don't need a state machine in this case, as we are able to packetize + -- 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) + where + outPkt = PacketStreamM2S dataOut (Just l) (toMetaOut dataIn) False + dataOut = + bitCoerce (toHeader dataIn) + ++ repeat @(dataWidth - headerBytes) (nullByte "packetizeFromDfC") + l = case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of + SNatGT -> natToNum @(headerBytes `Mod` dataWidth) + _ -> natToNum @dataWidth + SNatGT -> fromSignals (mealyB (packetizeFromDfT toMetaOut toHeader) DfIdle) diff --git a/clash-protocols/src/Protocols/PacketStream/Padding.hs b/clash-protocols/src/Protocols/PacketStream/Padding.hs new file mode 100644 index 00000000..e6f7ad9a --- /dev/null +++ b/clash-protocols/src/Protocols/PacketStream/Padding.hs @@ -0,0 +1,166 @@ +{-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_HADDOCK hide #-} + +{- | +Copyright : (C) 2024, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +Provides a generic component which enforces some expected packet length field +in the metadata. +-} +module Protocols.PacketStream.Padding ( + stripPaddingC, +) where + +import Clash.Prelude + +import qualified Data.Bifunctor as B +import Data.Maybe +import Data.Type.Equality ((:~:) (Refl)) + +import Protocols +import Protocols.PacketStream.Base + +-- | State of `stripPaddingT`. +data StripPaddingState p dataWidth meta + = Counting + { _buffer :: PacketStreamM2S dataWidth meta + -- ^ Contains the last transfer, with `_abort` set if a premature end + -- was detected. If the packet contained padding, `_last` is already + -- correctly adjusted. + , _valid :: Bool + -- ^ Qualifier for _buffer. If false, its value is undefined. + , _counter :: Unsigned p + -- ^ Counts the actual length of the current packet. + } + | Strip + { _buffer :: PacketStreamM2S dataWidth meta + -- ^ We need to wait until forwarding the last transfer, as the padding + -- may be aborted. In this state we do not need _valid, as the buffered + -- transfer is always valid. + } + deriving (Generic, NFDataX) + +-- | State transition function of `stripPaddingC`. +stripPaddingT :: + forall dataWidth meta p. + (KnownNat dataWidth) => + (KnownNat p) => + (meta -> Unsigned p) -> + StripPaddingState p dataWidth meta -> + ( Maybe (PacketStreamM2S dataWidth meta) + , PacketStreamS2M + ) -> + ( StripPaddingState p dataWidth meta + , ( PacketStreamS2M + , Maybe (PacketStreamM2S dataWidth meta) + ) + ) +stripPaddingT _ st@Counting{} (Nothing, bwdIn) = (nextSt, (PacketStreamS2M True, fwdOut)) + where + fwdOut = + if _valid st + then Just (_buffer st) + else Nothing + + nextSt + | isJust fwdOut && _ready bwdIn = st{_valid = False} + | otherwise = st +stripPaddingT toLength st@Counting{} (Just inPkt, bwdIn) = (nextSt, (bwdOut, fwdOut)) + where + expectedLen = toLength (_meta inPkt) + + toAdd :: Unsigned p + toAdd = case _last inPkt of + Nothing -> natToNum @dataWidth + -- Here we do a slightly dangerous resize. Because @dataWidth@ should + -- never be bigger than @2^p@, this is not an issue in practice, so I + -- don't believe it requires a constraint as long as it is well-documented. + Just size -> bitCoerce (resize size :: Index (2 ^ p)) + + carry :: Bool + nextCount :: Unsigned p + (carry, nextCount) = + B.bimap unpack unpack + $ split + $ add (_counter st) toAdd + + -- True if the payload size is smaller than expected. + -- We have to take the carry into account as well, otherwise if the + -- calculation overflows then we will wrongly signal a premature end. + prematureEnd = + isJust (_last inPkt) + && (nextCount < expectedLen) + && not carry + + tooBig = nextCount > expectedLen || carry + + fwdOut = + if _valid st + then Just (_buffer st) + else Nothing + + bwdOut = PacketStreamS2M (isNothing fwdOut || _ready bwdIn) + + nextLast + -- If @dataWidth is 1, the adjusted `_last` is always @Just 0@. + -- Otherwise, we need to do some arithmetic. + | tooBig = case sameNat d1 (SNat @dataWidth) of + Just Refl -> Just 0 + Nothing -> Just $ bitCoerce $ resize $ expectedLen - _counter st + | otherwise = _last inPkt + + nextBuf = inPkt{_last = nextLast, _abort = _abort inPkt || prematureEnd} + nextValid = isJust (_last inPkt) || not tooBig + + nextCounter = + if prematureEnd || isJust (_last inPkt) + then 0 + else nextCount + + nextSt + | isJust fwdOut && not (_ready bwdIn) = st + | isNothing (_last inPkt) && tooBig = Strip nextBuf + | otherwise = Counting nextBuf nextValid nextCounter +stripPaddingT _ st@Strip{} (Nothing, _) = (st, (PacketStreamS2M True, Nothing)) +stripPaddingT _ Strip{_buffer = f} (Just inPkt, _) = + (nextSt, (PacketStreamS2M True, Nothing)) + where + nextAborted = _abort f || _abort inPkt + + nextSt = + if isJust (_last inPkt) + then Counting f{_abort = nextAborted} True 0 + else Strip (f{_abort = nextAborted}) + +{- | +Removes padding from packets according to some expected packet length field +in the metadata. If the actual length of a packet is smaller than expected, +the packet is aborted. + +Has one clock cycle of latency, because all M2S outputs are registered. +Runs at full throughput. + +__NB__: @dataWidth@ /must/ be smaller than @2^p@. Because this should never +occur in practice, this constraint is not enforced on the type-level. +-} +stripPaddingC :: + forall dataWidth meta p dom. + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (KnownNat p) => + (NFDataX meta) => + -- | Function that extracts the expected packet length from the metadata + (meta -> Unsigned p) -> + Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta) +stripPaddingC toLength = + forceResetSanity + |> fromSignals (mealyB (stripPaddingT toLength) s0) + where + s0 = + Counting + { _buffer = deepErrorX "stripPaddingT: undefined initial buffer." + , _valid = False + , _counter = 0 + } diff --git a/clash-protocols/src/Protocols/PacketStream/Routing.hs b/clash-protocols/src/Protocols/PacketStream/Routing.hs new file mode 100644 index 00000000..1b6f7280 --- /dev/null +++ b/clash-protocols/src/Protocols/PacketStream/Routing.hs @@ -0,0 +1,99 @@ +{-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_HADDOCK hide #-} + +{- | +Copyright : (C) 2024, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +Provides a packet arbiter and dispatcher, for merging and splitting packet streams. +-} +module Protocols.PacketStream.Routing ( + packetArbiterC, + packetDispatcherC, + routeBy, +) where + +import Clash.Prelude + +import Protocols +import qualified Protocols.Df as Df +import Protocols.PacketStream.Base + +import qualified Data.Bifunctor as B +import Data.Maybe + +-- | Merges multiple packet streams into one, respecting packet boundaries. +packetArbiterC :: + forall dataWidth sources meta dom. + (HiddenClockResetEnable dom) => + (KnownNat sources) => + (1 <= sources) => + -- | Determines the mode of arbitration. See `Df.CollectMode` + Df.CollectMode -> + Circuit + (Vec sources (PacketStream dom dataWidth meta)) + (PacketStream dom dataWidth meta) +packetArbiterC mode = + Circuit (B.first unbundle . mealyB go (maxBound, True) . B.first bundle) + where + go (i, first) (fwds, bwd@(PacketStreamS2M ack)) = ((i', continue), (bwds, fwd)) + where + bwds = replace i bwd (repeat (PacketStreamS2M False)) + fwd = fwds !! i + + -- We may only switch sources if we are not currently in the middle + -- of forwarding a packet. + continue = case (fwd, mode) of + (Nothing, Df.NoSkip) -> False + (Nothing, _) -> first + (Just transferIn, _) -> isJust (_last transferIn) && ack + + i' = case (mode, continue) of + (_, False) -> i + (Df.NoSkip, _) -> satSucc SatWrap i + (Df.Skip, _) -> satSucc SatWrap i + (Df.Parallel, _) -> + -- Index of last sink with data + fromMaybe maxBound + $ fold @(sources - 1) (<|>) (zipWith (<$) indicesI fwds) + +{- | +Routes packets depending on their metadata, using given routing functions. + +Data is sent to at most one sink, for which the dispatch function evaluates to +@True@ when applied to the input metadata. If none of the predicates hold, the +input packet is dropped. If more than one of the predicates hold, the sink +that occurs first in the vector is picked. + +Sends out packets in the same clock cycle as they are received, this +component has zero latency and runs at full throughput. +-} +packetDispatcherC :: + forall dataWidth sinks meta dom. + (HiddenClockResetEnable dom) => + (KnownNat sinks) => + -- | Dispatch function + Vec sinks (meta -> Bool) -> + Circuit + (PacketStream dom dataWidth meta) + (Vec sinks (PacketStream dom dataWidth meta)) +packetDispatcherC predicates = + Circuit (B.second unbundle . unbundle . fmap go . bundle . B.second bundle) + where + idleOtp = repeat Nothing + go (Nothing, _) = (PacketStreamS2M False, idleOtp) + go (Just x, bwds) = case findIndex id (zipWith ($) predicates (pure $ _meta x)) of + Just i -> (bwds !! i, replace i (Just x) idleOtp) + Nothing -> (PacketStreamS2M True, idleOtp) + +{- | +Routing function for `packetDispatcherC` that matches against values with +an `Eq` instance. Useful to route according to a record field. +-} +routeBy :: + (Eq a) => + (meta -> a) -> + Vec sinks a -> + Vec sinks (meta -> Bool) +routeBy f = map $ \x -> (== x) . f diff --git a/clash-protocols/tests/Tests/Haxioms.hs b/clash-protocols/tests/Tests/Haxioms.hs new file mode 100644 index 00000000..93a18a18 --- /dev/null +++ b/clash-protocols/tests/Tests/Haxioms.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE NumericUnderscores #-} + +module Tests.Haxioms where + +import Numeric.Natural +import Prelude + +import Hedgehog +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +{- | Generate a 'Natural' greater than or equal to /n/. Can generate 'Natural's +up to /n+1000/. This should be enough, given that naturals in this module are +used in proofs. +-} +genNatural :: Natural -> Gen Natural +genNatural min_ = Gen.integral (Range.linear min_ (1000 + min_)) + +-- | Like 'DivRU', but at term-level. +divRU :: Natural -> Natural -> Natural +divRU dividend divider = + case dividend `divMod` divider of + (n, 0) -> n + (n, _) -> n + 1 + +{- | Test whether the following equation holds: + + DivRU (a * b) b ~ a + +Given: + + 1 <= b + +Tests: 'Data.Constraint.Nat.Extra.cancelMulDiv'. +-} +prop_cancelMulDiv :: Property +prop_cancelMulDiv = property $ do + a <- forAll (genNatural 0) + b <- forAll (genNatural 1) + divRU (a * b) b === a + +{- | Test whether the following equation holds: + + Mod a b + 1 <= b + +Given: + + 1 <= b + +Tests: 'Data.Constraint.Nat.Extra.leModulusDivisor'. +-} +prop_leModulusDivisor :: Property +prop_leModulusDivisor = property $ do + a <- forAll (genNatural 0) + b <- forAll (genNatural 1) + assert (a `mod` b + 1 <= b) + +{- | Test whether the following equation holds: + + 1 <= DivRU a b + +Given: + + 1 <= a, 1 <= b + +Tests: 'Data.Constraint.Nat.Extra.strictlyPositiveDivRu'. +-} +prop_strictlyPositiveDivRu :: Property +prop_strictlyPositiveDivRu = property $ do + a <- forAll (genNatural 1) + b <- forAll (genNatural 1) + assert (1 <= divRU a b) + +{- | Test whether the following equation holds: + + b <= a * DivRU b a + +Given: + + 1 <= a + +Tests: 'Data.Constraint.Nat.Extra.leTimesDivRu'. +-} +prop_leTimesDivRu :: Property +prop_leTimesDivRu = property $ do + a <- forAll (genNatural 1) + b <- forAll (genNatural 0) + assert (b <= a * divRU b a) + +{- | Test whether the following equation holds: + + a * DivRU b a ~ b + Mod (a - Mod b a) a + +Given: + + 1 <= a + +Tests: 'Data.Constraint.Nat.Extra.eqTimesDivRu'. +-} +prop_eqTimesDivRu :: Property +prop_eqTimesDivRu = property $ do + a <- forAll (genNatural 1) + b <- forAll (genNatural 0) + a * (b `divRU` a) === b + (a - b `mod` a) `mod` a + +tests :: TestTree +tests = + localOption (mkTimeout 10_000_000 {- 10 seconds -}) $ + localOption + (HedgehogTestLimit (Just 100_000)) + $(testGroupGenerator) diff --git a/clash-protocols/tests/Tests/Protocols.hs b/clash-protocols/tests/Tests/Protocols.hs index 043732ec..aa9bf1ba 100644 --- a/clash-protocols/tests/Tests/Protocols.hs +++ b/clash-protocols/tests/Tests/Protocols.hs @@ -5,6 +5,7 @@ import qualified Tests.Protocols.Avalon import qualified Tests.Protocols.Axi4 import qualified Tests.Protocols.Df import qualified Tests.Protocols.DfConv +import qualified Tests.Protocols.PacketStream import qualified Tests.Protocols.Vec import qualified Tests.Protocols.Wishbone @@ -16,6 +17,7 @@ tests = , Tests.Protocols.DfConv.tests , Tests.Protocols.Avalon.tests , Tests.Protocols.Axi4.tests + , Tests.Protocols.PacketStream.tests , Tests.Protocols.Wishbone.tests , Tests.Protocols.Vec.tests ] diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream.hs b/clash-protocols/tests/Tests/Protocols/PacketStream.hs new file mode 100644 index 00000000..91ba833d --- /dev/null +++ b/clash-protocols/tests/Tests/Protocols/PacketStream.hs @@ -0,0 +1,26 @@ +module Tests.Protocols.PacketStream (tests) where + +import Test.Tasty + +import qualified Tests.Protocols.PacketStream.AsyncFifo +import qualified Tests.Protocols.PacketStream.Base +import qualified Tests.Protocols.PacketStream.Converters +import qualified Tests.Protocols.PacketStream.Depacketizers +import qualified Tests.Protocols.PacketStream.PacketFifo +import qualified Tests.Protocols.PacketStream.Packetizers +import qualified Tests.Protocols.PacketStream.Padding +import qualified Tests.Protocols.PacketStream.Routing + +tests :: TestTree +tests = + testGroup + "PacketStream" + [ Tests.Protocols.PacketStream.AsyncFifo.tests + , Tests.Protocols.PacketStream.Base.tests + , Tests.Protocols.PacketStream.Converters.tests + , Tests.Protocols.PacketStream.Depacketizers.tests + , Tests.Protocols.PacketStream.PacketFifo.tests + , Tests.Protocols.PacketStream.Packetizers.tests + , Tests.Protocols.PacketStream.Padding.tests + , Tests.Protocols.PacketStream.Routing.tests + ] diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/AsyncFifo.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/AsyncFifo.hs new file mode 100644 index 00000000..4da9e9b3 --- /dev/null +++ b/clash-protocols/tests/Tests/Protocols/PacketStream/AsyncFifo.hs @@ -0,0 +1,101 @@ +{-# LANGUAGE NumericUnderscores #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Tests.Protocols.PacketStream.AsyncFifo where + +import Clash.Prelude + +import Hedgehog (Property) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Test.Tasty (TestTree, localOption, mkTimeout) +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +import Protocols.Hedgehog +import Protocols.PacketStream.AsyncFifo (asyncFifoC) +import Protocols.PacketStream.Hedgehog + +createDomain + vSystem + { vName = "TestDom50" + , vPeriod = 20_000 + , vActiveEdge = Rising + , vResetKind = Asynchronous + , vInitBehavior = Unknown + , vResetPolarity = ActiveHigh + } + +createDomain + vSystem + { vName = "TestDom125" + , vPeriod = 8_000 + , vActiveEdge = Rising + , vResetKind = Asynchronous + , vInitBehavior = Unknown + , vResetPolarity = ActiveHigh + } + +clk50 :: Clock TestDom50 +clk50 = clockGen + +clk125 :: Clock TestDom125 +clk125 = clockGen + +-- Assert the reset for a different amount of cycles in each domain +-- to properly test the async fifo. +rst50 :: Reset TestDom50 +rst50 = resetGenN d30 + +rst125 :: Reset TestDom125 +rst125 = resetGenN d40 + +en50 :: Enable TestDom50 +en50 = enableGen + +en125 :: Enable TestDom125 +en125 = enableGen + +generateAsyncFifoIdProp :: + forall (wDom :: Domain) (rDom :: Domain). + (KnownDomain wDom, KnownDomain rDom) => + Clock wDom -> + Reset wDom -> + Enable wDom -> + Clock rDom -> + Reset rDom -> + Enable rDom -> + Property +generateAsyncFifoIdProp wClk wRst wEn rClk rRst rEn = + idWithModel + defExpectOptions + (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 30))) + id + (asyncFifoC @wDom @rDom @4 @1 @Int d4 wClk wRst wEn rClk rRst rEn) + +{- | The async FIFO circuit should forward all of its input data without loss and without producing extra data. + This property tests whether this is true, when the clock of the writer and reader is equally fast (50 MHz). +-} +prop_asyncfifo_writer_speed_equal_to_reader_id :: Property +prop_asyncfifo_writer_speed_equal_to_reader_id = generateAsyncFifoIdProp clk50 rst50 en50 clk50 rst50 en50 + +{- | The async FIFO circuit should forward all of its input data without loss and without producing extra data. + This property tests whether this is true, when the clock of the writer (50 MHz) is slower than the clock of the reader (125 MHz). +-} +prop_asyncfifo_writer_speed_slower_than_reader_id :: Property +prop_asyncfifo_writer_speed_slower_than_reader_id = generateAsyncFifoIdProp clk50 rst50 en50 clk125 rst125 en125 + +{- | The async FIFO circuit should forward all of its input data without loss and without producing extra data. + This property tests whether this is true, when the clock of the writer (125 MHz) is faster than the clock of the reader (50 MHz). +-} +prop_asyncfifo_writer_speed_faster_than_reader_id :: Property +prop_asyncfifo_writer_speed_faster_than_reader_id = generateAsyncFifoIdProp clk125 rst125 en125 clk50 rst50 en50 + +tests :: TestTree +tests = + localOption (mkTimeout 20_000_000 {- 20 seconds -}) $ + localOption + (HedgehogTestLimit (Just 100)) + $(testGroupGenerator) diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Base.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Base.hs new file mode 100644 index 00000000..2ef0e311 --- /dev/null +++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Base.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE NoImplicitPrelude #-} + +module Tests.Protocols.PacketStream.Base ( + tests, +) where + +import Clash.Prelude + +import qualified Data.List as L +import Data.List.Extra (unsnoc) + +import Hedgehog (Property) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Test.Tasty (TestTree, localOption, mkTimeout) +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +import Protocols.Hedgehog +import Protocols.PacketStream.Base +import Protocols.PacketStream.Hedgehog + +prop_strip_trailing_empty :: Property +prop_strip_trailing_empty = + idWithModelSingleDomain + @System + defExpectOptions + (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10))) + (exposeClockResetEnable model') + (exposeClockResetEnable (stripTrailingEmptyC @1 @Char)) + where + model' packets = L.concatMap model (chunkByPacket packets) + + model :: [PacketStreamM2S 1 Char] -> [PacketStreamM2S 1 Char] + model packet = case unsnoc packet of + Nothing -> [] + Just (xs, l) -> case unsnoc xs of + -- Preserve packets that consist of a single zero-byte transfer. + Nothing -> [l] + Just (ys, l2) -> + if _last l == Just 0 + then ys L.++ [l2{_last = Just maxBound, _abort = _abort l2 || _abort l}] + else packet + +tests :: TestTree +tests = + localOption (mkTimeout 20_000_000 {- 20 seconds -}) + $ localOption + (HedgehogTestLimit (Just 500)) + $(testGroupGenerator) diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Converters.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Converters.hs new file mode 100644 index 00000000..88e127c9 --- /dev/null +++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Converters.hs @@ -0,0 +1,99 @@ +{-# LANGUAGE NumericUnderscores #-} + +module Tests.Protocols.PacketStream.Converters ( + tests, +) where + +import Clash.Prelude + +import Hedgehog (Property) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +import Protocols.Hedgehog +import Protocols.PacketStream.Converters +import Protocols.PacketStream.Hedgehog + +generateUpConverterProperty :: + forall (dwIn :: Nat) (n :: Nat). + (1 <= dwIn) => + (1 <= n) => + (1 <= dwIn * n) => + SNat dwIn -> + SNat n -> + Property +generateUpConverterProperty SNat SNat = + idWithModelSingleDomain + defExpectOptions + (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 20))) + (exposeClockResetEnable (upConvert . downConvert)) + (exposeClockResetEnable @System (upConverterC @dwIn @n @Int)) + +generateDownConverterProperty :: + forall (dwOut :: Nat) (n :: Nat). + (1 <= dwOut) => + (1 <= n) => + (1 <= dwOut * n) => + SNat dwOut -> + SNat n -> + Property +generateDownConverterProperty SNat SNat = + idWithModelSingleDomain + defExpectOptions{eoSampleMax = 1000} + (genPackets 1 8 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10))) + (exposeClockResetEnable (upConvert . downConvert)) + (exposeClockResetEnable @System (downConverterC @dwOut @n @Int)) + +prop_upConverter3to9 :: Property +prop_upConverter3to9 = generateUpConverterProperty d3 d3 + +prop_upConverter4to8 :: Property +prop_upConverter4to8 = generateUpConverterProperty d4 d2 + +prop_upConverter3to6 :: Property +prop_upConverter3to6 = generateUpConverterProperty d3 d2 + +prop_upConverter2to4 :: Property +prop_upConverter2to4 = generateUpConverterProperty d2 d2 + +prop_upConverter1to4 :: Property +prop_upConverter1to4 = generateUpConverterProperty d1 d4 + +prop_upConverter1to2 :: Property +prop_upConverter1to2 = generateUpConverterProperty d1 d2 + +prop_upConverter1to1 :: Property +prop_upConverter1to1 = generateUpConverterProperty d1 d1 + +prop_downConverter9to3 :: Property +prop_downConverter9to3 = generateDownConverterProperty d3 d3 + +prop_downConverter8to4 :: Property +prop_downConverter8to4 = generateDownConverterProperty d4 d2 + +prop_downConverter6to3 :: Property +prop_downConverter6to3 = generateDownConverterProperty d3 d2 + +prop_downConverter4to2 :: Property +prop_downConverter4to2 = generateDownConverterProperty d2 d2 + +prop_downConverter4to1 :: Property +prop_downConverter4to1 = generateDownConverterProperty d1 d4 + +prop_downConverter2to1 :: Property +prop_downConverter2to1 = generateDownConverterProperty d1 d2 + +prop_downConverter1to1 :: Property +prop_downConverter1to1 = generateDownConverterProperty d1 d1 + +tests :: TestTree +tests = + localOption (mkTimeout 20_000_000 {- 20 seconds -}) $ + localOption + (HedgehogTestLimit (Just 500)) + $(testGroupGenerator) diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Depacketizers.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Depacketizers.hs new file mode 100644 index 00000000..12e57b32 --- /dev/null +++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Depacketizers.hs @@ -0,0 +1,183 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE NoImplicitPrelude #-} + +module Tests.Protocols.PacketStream.Depacketizers ( + tests, +) where + +import Clash.Prelude + +import Hedgehog (Gen, Property) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) + +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +import Protocols +import Protocols.Hedgehog +import Protocols.PacketStream.Base +import Protocols.PacketStream.Depacketizers +import Protocols.PacketStream.Hedgehog + +{- | +Test @depacketizerC@ with varying data width, number of bytes in the +header, input metadata, and output metadata. +-} +depacketizerPropGen :: + forall + (metaIn :: Type) + (metaOut :: Type) + (dataWidth :: Nat) + (headerBytes :: Nat). + (1 <= dataWidth) => + (1 <= headerBytes) => + (TestType metaIn) => + (TestType metaOut) => + SNat dataWidth -> + SNat headerBytes -> + Gen metaIn -> + (Vec headerBytes (BitVector 8) -> metaIn -> metaOut) -> + Property +depacketizerPropGen SNat SNat metaGen toMetaOut = + idWithModelSingleDomain + @System + defExpectOptions{eoSampleMax = 1000, eoStopAfterEmpty = 1000} + (genPackets 1 4 (genValidPacket defPacketOptions metaGen (Range.linear 0 30))) + (exposeClockResetEnable (depacketizerModel toMetaOut)) + (exposeClockResetEnable ckt) + where + ckt :: + (HiddenClockResetEnable System) => + Circuit + (PacketStream System dataWidth metaIn) + (PacketStream System dataWidth metaOut) + ckt = depacketizerC toMetaOut + +{- | +Test @depacketizeToDfC@ with varying data width, number of bytes in the +header, input metadata, and output type @a@. +-} +depacketizeToDfPropGen :: + forall + (metaIn :: Type) + (a :: Type) + (dataWidth :: Nat) + (headerBytes :: Nat). + (1 <= dataWidth) => + (1 <= headerBytes) => + (BitPack a) => + (BitSize a ~ headerBytes * 8) => + (TestType a) => + (TestType metaIn) => + SNat dataWidth -> + SNat headerBytes -> + Gen metaIn -> + (Vec headerBytes (BitVector 8) -> metaIn -> a) -> + Property +depacketizeToDfPropGen SNat SNat metaGen toOut = + idWithModelSingleDomain + @System + defExpectOptions{eoSampleMax = 1000, eoStopAfterEmpty = 1000} + (genPackets 1 10 (genValidPacket defPacketOptions metaGen (Range.linear 0 20))) + (exposeClockResetEnable (depacketizeToDfModel toOut)) + (exposeClockResetEnable ckt) + where + ckt :: + (HiddenClockResetEnable System) => + Circuit (PacketStream System dataWidth metaIn) (Df System a) + ckt = depacketizeToDfC toOut + +{- | +Do something interesting with both the parsed header and the input +metadata for testing purposes. We just xor every byte in the parsed +header with the byte in the input metadata. +-} +exampleToMetaOut :: + Vec headerBytes (BitVector 8) -> + BitVector 8 -> + Vec headerBytes (BitVector 8) +exampleToMetaOut hdr metaIn = map (`xor` metaIn) hdr + +-- | headerBytes % dataWidth ~ 0 +prop_const_depacketizer_d1_d14 :: Property +prop_const_depacketizer_d1_d14 = + depacketizerPropGen d1 d14 (pure ()) const + +prop_xor_depacketizer_d1_d14 :: Property +prop_xor_depacketizer_d1_d14 = + depacketizerPropGen d1 d14 Gen.enumBounded exampleToMetaOut + +-- | dataWidth < headerBytes +prop_const_depacketizer_d3_d11 :: Property +prop_const_depacketizer_d3_d11 = + depacketizerPropGen d3 d11 (pure ()) const + +prop_xor_depacketizer_d3_d11 :: Property +prop_xor_depacketizer_d3_d11 = + depacketizerPropGen d3 d11 Gen.enumBounded exampleToMetaOut + +-- | dataWidth ~ header byte size +prop_const_depacketizer_d7_d7 :: Property +prop_const_depacketizer_d7_d7 = + depacketizerPropGen d7 d7 (pure ()) const + +prop_xor_depacketizer_d7_d7 :: Property +prop_xor_depacketizer_d7_d7 = + depacketizerPropGen d7 d7 Gen.enumBounded exampleToMetaOut + +-- | dataWidth > header byte size +prop_const_depacketizer_d5_d4 :: Property +prop_const_depacketizer_d5_d4 = + depacketizerPropGen d5 d4 (pure ()) const + +prop_xor_depacketizer_d5_d4 :: Property +prop_xor_depacketizer_d5_d4 = + depacketizerPropGen d5 d4 Gen.enumBounded exampleToMetaOut + +-- | headerBytes % dataWidth ~ 0 +prop_const_depacketize_to_df_d1_d14 :: Property +prop_const_depacketize_to_df_d1_d14 = + depacketizeToDfPropGen d1 d14 (pure ()) const + +prop_xor_depacketize_to_df_d1_d14 :: Property +prop_xor_depacketize_to_df_d1_d14 = + depacketizeToDfPropGen d1 d14 Gen.enumBounded exampleToMetaOut + +-- | dataWidth < headerBytes +prop_const_depacketize_to_df_d3_d11 :: Property +prop_const_depacketize_to_df_d3_d11 = + depacketizeToDfPropGen d3 d11 (pure ()) const + +prop_xor_depacketize_to_df_d3_d11 :: Property +prop_xor_depacketize_to_df_d3_d11 = + depacketizeToDfPropGen d3 d11 Gen.enumBounded exampleToMetaOut + +-- | dataWidth ~ header byte size +prop_const_depacketize_to_df_d7_d7 :: Property +prop_const_depacketize_to_df_d7_d7 = + depacketizeToDfPropGen d7 d7 (pure ()) const + +prop_xor_depacketize_to_df_d7_d7 :: Property +prop_xor_depacketize_to_df_d7_d7 = + depacketizeToDfPropGen d7 d7 Gen.enumBounded exampleToMetaOut + +-- | dataWidth > header byte size +prop_const_depacketize_to_df_d5_d4 :: Property +prop_const_depacketize_to_df_d5_d4 = + depacketizeToDfPropGen d5 d4 (pure ()) const + +prop_xor_depacketize_to_df_d5_d4 :: Property +prop_xor_depacketize_to_df_d5_d4 = + depacketizeToDfPropGen d5 d4 Gen.enumBounded exampleToMetaOut + +tests :: TestTree +tests = + localOption (mkTimeout 20_000_000 {- 20 seconds -}) + $ localOption + (HedgehogTestLimit (Just 500)) + $(testGroupGenerator) diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/PacketFifo.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/PacketFifo.hs new file mode 100644 index 00000000..fbd0438f --- /dev/null +++ b/clash-protocols/tests/Tests/Protocols/PacketStream/PacketFifo.hs @@ -0,0 +1,143 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE NoImplicitPrelude #-} + +module Tests.Protocols.PacketStream.PacketFifo ( + tests, +) where + +import Clash.Prelude + +import Data.Int (Int16) +import qualified Data.List as L + +import Hedgehog +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import qualified Prelude as P + +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +import Protocols +import Protocols.Hedgehog +import Protocols.PacketStream.Base +import Protocols.PacketStream.Hedgehog +import Protocols.PacketStream.PacketFifo + +-- | Drops packets that consist of more than 2^n transfers. +dropBigPackets :: + SNat n -> + [PacketStreamM2S dataWidth meta] -> + [PacketStreamM2S dataWidth meta] +dropBigPackets n packets = + L.concat + $ L.filter + (\p -> L.length p < 2 P.^ snatToInteger n) + (chunkByPacket packets) + +-- | Test for id and proper dropping of aborted packets. +prop_packet_fifo_id :: Property +prop_packet_fifo_id = + idWithModelSingleDomain + @System + defExpectOptions + (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10))) + (exposeClockResetEnable dropAbortedPackets) + (exposeClockResetEnable (packetFifoC @_ @1 @Int16 d10 d10 Backpressure)) + +{- | +Ensure that backpressure because of a full content RAM and dropping of packets +that are too big to fit in the FIFO is tested. +-} +prop_packet_fifo_small_buffer_id :: Property +prop_packet_fifo_small_buffer_id = + idWithModelSingleDomain + @System + defExpectOptions{eoStopAfterEmpty = 1000} + (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 30))) + (exposeClockResetEnable (dropBigPackets d3 . dropAbortedPackets)) + (exposeClockResetEnable (packetFifoC @_ @1 @Int16 d3 d5 Backpressure)) + +{- | +Test for id using a small meta buffer to ensure backpressure using +the meta buffer is tested. +-} +prop_packet_fifo_small_meta_buffer_id :: Property +prop_packet_fifo_small_meta_buffer_id = + idWithModelSingleDomain + @System + defExpectOptions + (genPackets 1 30 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 4))) + (exposeClockResetEnable dropAbortedPackets) + (exposeClockResetEnable (packetFifoC @_ @1 @Int16 d10 d2 Backpressure)) + +-- | test for id and proper dropping of aborted packets +prop_overFlowDrop_packetFifo_id :: Property +prop_overFlowDrop_packetFifo_id = + idWithModelSingleDomain + @System + defExpectOptions{eoStopAfterEmpty = 1000} + (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10))) + (exposeClockResetEnable dropAbortedPackets) + (exposeClockResetEnable (packetFifoC @_ @1 @Int16 d10 d10 Drop)) + +-- | test for proper dropping when full +prop_overFlowDrop_packetFifo_drop :: Property +prop_overFlowDrop_packetFifo_drop = + propWithModelSingleDomain + @System + defExpectOptions + -- make sure the timeout is long as the packetFifo can be quiet for a while while dropping + (liftA3 (\a b c -> a L.++ b L.++ c) genSmall genBig genSmall) + (exposeClockResetEnable id) + (exposeClockResetEnable (packetFifoC @_ @4 @Int16 d3 d5 Drop)) + (\xs ys -> diff ys L.isSubsequenceOf xs) + where + genSmall = + genValidPacket defPacketOptions{poAbortMode = NoAbort} Gen.enumBounded (Range.linear 0 3) + genBig = + genValidPacket + defPacketOptions{poAbortMode = NoAbort} + Gen.enumBounded + (Range.linear 9 9) + +-- | test to check if there are no gaps inside of packets +prop_packetFifo_no_gaps :: Property +prop_packetFifo_no_gaps = property $ do + let maxInputSize = 50 + ckt = + exposeClockResetEnable + (packetFifoC d12 d12 Backpressure) + systemClockGen + resetGen + enableGen + gen = + genPackets + 1 + 10 + ( genValidPacket defPacketOptions{poAbortMode = NoAbort} Gen.enumBounded (Range.linear 0 10) + ) + + packets :: [PacketStreamM2S 4 Int16] <- forAll gen + + let packetSize = 2 P.^ snatToInteger d12 + cfg = SimulationConfig 1 (2 * packetSize) False + cktResult = simulateC ckt cfg (Just <$> packets) + + assert $ noGaps $ L.take (5 * maxInputSize) cktResult + where + noGaps :: [Maybe (PacketStreamM2S 4 Int16)] -> Bool + noGaps (Just (PacketStreamM2S{_last = Nothing}) : Nothing : _) = False + noGaps (_ : xs) = noGaps xs + noGaps _ = True + +tests :: TestTree +tests = + localOption (mkTimeout 20_000_000 {- 20 seconds -}) + $ localOption + (HedgehogTestLimit (Just 500)) + $(testGroupGenerator) diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Packetizers.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Packetizers.hs new file mode 100644 index 00000000..d86677c7 --- /dev/null +++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Packetizers.hs @@ -0,0 +1,206 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE NoImplicitPrelude #-} + +module Tests.Protocols.PacketStream.Packetizers ( + tests, +) where + +import Clash.Hedgehog.Sized.Vector (genVec) +import Clash.Prelude + +import Hedgehog (Property) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +import Protocols +import qualified Protocols.Df as Df +import Protocols.Hedgehog +import Protocols.PacketStream (packetizeFromDfC, packetizerC) +import Protocols.PacketStream.Base +import Protocols.PacketStream.Hedgehog + +{- | +Test @packetizerC@ with varying data width, number of bytes in the +header, input metadata, and output metadata. + +We consider the input metadata to be @Vec metaInBytes (BitVector 8)@ to +avoid unnecessary conversions, because @packetizerC@ requires that the +input metadata is convertible to this type anyway. +-} +packetizerPropGen :: + forall + (dataWidth :: Nat) + (headerBytes :: Nat) + (metaInBytes :: Nat) + (metaOut :: Type). + (KnownNat metaInBytes) => + (1 <= dataWidth) => + (1 <= headerBytes) => + (TestType metaOut) => + SNat dataWidth -> + SNat headerBytes -> + (Vec metaInBytes (BitVector 8) -> metaOut) -> + (Vec metaInBytes (BitVector 8) -> Vec headerBytes (BitVector 8)) -> + Property +packetizerPropGen SNat SNat toMetaOut toHeader = + idWithModelSingleDomain + @System + defExpectOptions + ( genPackets + 1 + 10 + (genValidPacket defPacketOptions (genVec Gen.enumBounded) (Range.linear 0 10)) + ) + (exposeClockResetEnable model) + (exposeClockResetEnable ckt) + where + model = packetizerModel toMetaOut toHeader + ckt :: + (HiddenClockResetEnable System) => + Circuit + (PacketStream System dataWidth (Vec metaInBytes (BitVector 8))) + (PacketStream System dataWidth metaOut) + ckt = packetizerC toMetaOut toHeader + +{- | +Test @packetizeFromDfC@ with varying data width, number of bytes in the +header, input type, and output metadata. + +We consider the input type to be @Vec aBytes (BitVector 8)@ to +avoid unnecessary conversions, because @packetizerC@ requires that the +input type is convertible to this type anyway. +-} +packetizeFromDfPropGen :: + forall + (dataWidth :: Nat) + (headerBytes :: Nat) + (aBytes :: Nat) + (metaOut :: Type). + (KnownNat aBytes) => + (1 <= dataWidth) => + (1 <= headerBytes) => + (TestType metaOut) => + SNat dataWidth -> + SNat headerBytes -> + (Vec aBytes (BitVector 8) -> metaOut) -> + (Vec aBytes (BitVector 8) -> Vec headerBytes (BitVector 8)) -> + Property +packetizeFromDfPropGen SNat SNat toMetaOut toHeader = + idWithModelSingleDomain + @System + defExpectOptions + (Gen.list (Range.linear 1 10) (genVec Gen.enumBounded)) + (exposeClockResetEnable model) + (exposeClockResetEnable ckt) + where + model = packetizeFromDfModel toMetaOut toHeader + ckt :: + (HiddenClockResetEnable System) => + Circuit + (Df.Df System (Vec aBytes (BitVector 8))) + (PacketStream System dataWidth metaOut) + ckt = packetizeFromDfC toMetaOut toHeader + +{- | +Do something interesting with the input metadata to derive the output +metadata for testing purposes. We just xor-reduce the input metadata. +-} +myToMetaOut :: Vec n (BitVector 8) -> BitVector 8 +myToMetaOut = foldr xor 0 + +{- | +Do something interesting with the input metadata to derive the header +for testing purposes. We just xor every byte in the input metadata with +an arbitrary constant and add some bytes. +-} +myToHeader :: + forall metaInBytes headerBytes. + (2 + metaInBytes ~ headerBytes) => + Vec metaInBytes (BitVector 8) -> + Vec headerBytes (BitVector 8) +myToHeader metaIn = map (`xor` 0xAB) metaIn ++ (0x01 :> 0x02 :> Nil) + +-- | headerBytes % dataWidth ~ 0 +prop_const_packetizer_d1_d14 :: Property +prop_const_packetizer_d1_d14 = + packetizerPropGen d1 d14 (const ()) id + +prop_xor_packetizer_d1_d14 :: Property +prop_xor_packetizer_d1_d14 = + packetizerPropGen d1 d14 myToMetaOut myToHeader + +-- | dataWidth < headerBytes +prop_const_packetizer_d3_d11 :: Property +prop_const_packetizer_d3_d11 = + packetizerPropGen d3 d11 (const ()) id + +prop_xor_packetizer_d3_d11 :: Property +prop_xor_packetizer_d3_d11 = + packetizerPropGen d3 d11 myToMetaOut myToHeader + +-- | dataWidth ~ header byte size +prop_const_packetizer_d7_d7 :: Property +prop_const_packetizer_d7_d7 = + packetizerPropGen d7 d7 (const ()) id + +prop_xor_packetizer_d7_d7 :: Property +prop_xor_packetizer_d7_d7 = + packetizerPropGen d7 d7 myToMetaOut myToHeader + +-- | dataWidth > header byte size +prop_const_packetizer_d5_d4 :: Property +prop_const_packetizer_d5_d4 = + packetizerPropGen d5 d4 (const ()) id + +prop_xor_packetizer_d5_d4 :: Property +prop_xor_packetizer_d5_d4 = + packetizerPropGen d5 d4 myToMetaOut myToHeader + +-- | headerBytes % dataWidth ~ 0 +prop_const_packetizeFromDf_d1_d14 :: Property +prop_const_packetizeFromDf_d1_d14 = + packetizeFromDfPropGen d1 d14 (const ()) id + +prop_xor_packetizeFromDf_d1_d14 :: Property +prop_xor_packetizeFromDf_d1_d14 = + packetizeFromDfPropGen d1 d14 myToMetaOut myToHeader + +-- | dataWidth < headerBytes +prop_const_packetizeFromDf_d3_d11 :: Property +prop_const_packetizeFromDf_d3_d11 = + packetizeFromDfPropGen d3 d11 (const ()) id + +prop_xor_packetizeFromDf_d3_d11 :: Property +prop_xor_packetizeFromDf_d3_d11 = + packetizeFromDfPropGen d3 d11 myToMetaOut myToHeader + +-- | dataWidth ~ header byte size +prop_const_packetizeFromDf_d7_d7 :: Property +prop_const_packetizeFromDf_d7_d7 = + packetizeFromDfPropGen d7 d7 (const ()) id + +prop_xor_packetizeFromDf_d7_d7 :: Property +prop_xor_packetizeFromDf_d7_d7 = + packetizeFromDfPropGen d7 d7 myToMetaOut myToHeader + +-- | dataWidth > header byte size +prop_const_packetizeFromDf_d5_d4 :: Property +prop_const_packetizeFromDf_d5_d4 = + packetizeFromDfPropGen d5 d4 (const ()) id + +prop_xor_packetizeFromDf_d5_d4 :: Property +prop_xor_packetizeFromDf_d5_d4 = + packetizeFromDfPropGen d5 d4 myToMetaOut myToHeader + +tests :: TestTree +tests = + localOption (mkTimeout 20_000_000 {- 20 seconds -}) + $ localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator) diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Padding.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Padding.hs new file mode 100644 index 00000000..43ade268 --- /dev/null +++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Padding.hs @@ -0,0 +1,87 @@ +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE NoImplicitPrelude #-} + +module Tests.Protocols.PacketStream.Padding ( + tests, +) where + +import Clash.Prelude + +import qualified Data.List.Extra as L + +import Hedgehog +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +import Protocols.Hedgehog +import Protocols.PacketStream +import Protocols.PacketStream.Hedgehog + +-- | Pure model of `stripPaddingC`. +stripPaddingModel :: + forall p. + (KnownNat p) => + [PacketStreamM2S 1 (Unsigned p)] -> + [PacketStreamM2S 1 (Unsigned p)] +stripPaddingModel packets = L.concatMap go (chunkByPacket packets) + where + go packet + | packetBytes == expectedSize = packet + | packetBytes > expectedSize = + x L.++ [(L.head padding){_last = Just 0, _abort = any _abort padding}] + | otherwise = a L.++ [b{_abort = True}] + where + (a, b) = case L.unsnoc packet of + Nothing -> error "stripPaddingModel: list should not be empty." + Just (xs, l) -> (xs, l) + + packetBytes = L.length packet - (if _last b == Just 0 then 1 else 0) + expectedSize = fromIntegral (_meta b) + + (x, padding) = L.splitAt expectedSize packet + +{- | +Test `stripPaddingC` with a given @dataWidth@ against a pure model. + +We make sure to test integer overflow by making the data type which holds +the expected packet length extra small: @Unsigned 6@. +-} +stripPaddingProperty :: + forall dataWidth. + (1 <= dataWidth) => + SNat dataWidth -> + Property +stripPaddingProperty SNat = + idWithModelSingleDomain + @System + defExpectOptions + (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 20))) + (exposeClockResetEnable (upConvert . stripPaddingModel @6 . downConvert)) + (exposeClockResetEnable (stripPaddingC @dataWidth id)) + +prop_strip_padding_d1 :: Property +prop_strip_padding_d1 = stripPaddingProperty d1 + +prop_strip_padding_d2 :: Property +prop_strip_padding_d2 = stripPaddingProperty d2 + +prop_strip_padding_d4 :: Property +prop_strip_padding_d4 = stripPaddingProperty d4 + +prop_strip_padding_d5 :: Property +prop_strip_padding_d5 = stripPaddingProperty d5 + +prop_strip_padding_d8 :: Property +prop_strip_padding_d8 = stripPaddingProperty d8 + +tests :: TestTree +tests = + localOption (mkTimeout 20_000_000 {- 20 seconds -}) + $ localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator) diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Routing.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Routing.hs new file mode 100644 index 00000000..1ddb7521 --- /dev/null +++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Routing.hs @@ -0,0 +1,160 @@ +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE NoImplicitPrelude #-} + +module Tests.Protocols.PacketStream.Routing ( + tests, +) where + +import Clash.Prelude + +import Hedgehog hiding (Parallel) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +import qualified Protocols.Df as Df +import Protocols.Hedgehog +import Protocols.PacketStream.Base +import Protocols.PacketStream.Hedgehog +import Protocols.PacketStream.Routing + +import qualified Data.List as L + +{- | +Tests a packet arbiter for any data width and number of sources. In particular, +tests that packets from all sources are sent out unmodified in the same order +they were in in the source streams. +-} +makePropPacketArbiter :: + forall sources dataWidth. + (1 <= sources) => + (1 <= dataWidth) => + SNat sources -> + SNat dataWidth -> + Df.CollectMode -> + Property +makePropPacketArbiter SNat SNat mode = + propWithModelSingleDomain + @System + defExpectOptions{eoSampleMax = 1000} + genSources + (exposeClockResetEnable L.concat) + (exposeClockResetEnable (packetArbiterC mode)) + (\xs ys -> partitionPackets xs === partitionPackets ys) + where + (minPackets, maxPackets) = case mode of + -- NoSkip mode needs the same amount of packets generated for each + -- source. Otherwise, starvation happens and the test won't end. + Df.NoSkip -> (5, 5) + _ -> (1, 10) + genSources = mapM setMeta (indicesI @sources) + setMeta j = do + pkts <- + genPackets + @dataWidth + minPackets + maxPackets + (genValidPacket defPacketOptions (pure ()) (Range.linear 0 10)) + pure $ L.map (\pkt -> pkt{_meta = j}) pkts + + partitionPackets packets = + L.sortOn (_meta . L.head . L.head) + $ L.groupBy (\a b -> _meta a == _meta b) + <$> chunkByPacket packets + +{- | +Generic test function for the packet dispatcher, testing for all data widths, +dispatch functions, and some meta types. +-} +makePropPacketDispatcher :: + forall sinks dataWidth meta. + (KnownNat sinks) => + (1 <= sinks) => + (1 <= dataWidth) => + (TestType meta) => + (Bounded meta) => + (Enum meta) => + (BitPack meta) => + SNat dataWidth -> + -- | Dispatch function + Vec sinks (meta -> Bool) -> + Property +makePropPacketDispatcher SNat fs = + idWithModelSingleDomain @System + defExpectOptions{eoSampleMax = 2000, eoStopAfterEmpty = 1000} + (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 6))) + (exposeClockResetEnable (model 0)) + (exposeClockResetEnable (packetDispatcherC fs)) + where + model :: + Index sinks -> + [PacketStreamM2S dataWidth meta] -> + Vec sinks [PacketStreamM2S dataWidth meta] + model _ [] = pure [] + model i (y : ys) + | (fs !! i) (_meta y) = + let next = model 0 ys + in replace i (y : (next !! i)) next + | i < maxBound = model (i + 1) (y : ys) + | otherwise = model 0 ys + +-- | Tests the @NoSkip@ packet arbiter with one source; essentially an id test. +prop_packet_arbiter_noskip_id :: Property +prop_packet_arbiter_noskip_id = makePropPacketArbiter d1 d2 Df.NoSkip + +-- | Tests the @Skip@ packet arbiter with one source; essentially an id test. +prop_packet_arbiter_skip_id :: Property +prop_packet_arbiter_skip_id = makePropPacketArbiter d1 d2 Df.Skip + +-- | Tests the @Parallel@ packet arbiter with one source; essentially an id test. +prop_packet_arbiter_parallel_id :: Property +prop_packet_arbiter_parallel_id = makePropPacketArbiter d1 d2 Df.Parallel + +-- | Tests the @NoSkip@ arbiter with five sources. +prop_packet_arbiter_noskip :: Property +prop_packet_arbiter_noskip = makePropPacketArbiter d5 d2 Df.NoSkip + +-- | Tests the @Skip@ arbiter with five sources. +prop_packet_arbiter_skip :: Property +prop_packet_arbiter_skip = makePropPacketArbiter d5 d2 Df.Skip + +-- | Tests the @Parallel@ arbiter with five sources. +prop_packet_arbiter_parallel :: Property +prop_packet_arbiter_parallel = makePropPacketArbiter d5 d2 Df.Parallel + +{- | +Tests that the packet dispatcher works correctly with one sink that accepts +all packets; essentially an id test. +-} +prop_packet_dispatcher_id :: Property +prop_packet_dispatcher_id = + makePropPacketDispatcher + d4 + ((const True :: Int -> Bool) :> Nil) + +{- | +Tests the packet dispatcher for a data width of four bytes and three +overlapping but incomplete dispatch functions, effectively testing whether +the circuit sends input to the first allowed output channel and drops input +if there are none. +-} +prop_packet_dispatcher :: Property +prop_packet_dispatcher = makePropPacketDispatcher d4 fs + where + fs :: Vec 3 (Index 4 -> Bool) + fs = + (>= 3) + :> (>= 2) + :> (>= 1) + :> Nil + +tests :: TestTree +tests = + localOption (mkTimeout 20_000_000 {- 20 seconds -}) + $ localOption + (HedgehogTestLimit (Just 500)) + $(testGroupGenerator) diff --git a/clash-protocols/tests/unittests.hs b/clash-protocols/tests/unittests.hs index 3bb89bbc..364ff467 100644 --- a/clash-protocols/tests/unittests.hs +++ b/clash-protocols/tests/unittests.hs @@ -1,12 +1,12 @@ module Main where import Control.Concurrent (setNumCapabilities) -import Control.Monad (join) import System.Environment (lookupEnv, setEnv) import Test.Tasty import Text.Read (readMaybe) import Prelude +import qualified Tests.Haxioms import qualified Tests.Protocols main :: IO () @@ -15,7 +15,7 @@ main = do setEnv "TASTY_NUM_THREADS" "2" -- Detect "THREADS" environment variable on CI - nThreads <- join . fmap readMaybe <$> lookupEnv "THREADS" + nThreads <- (readMaybe =<<) <$> lookupEnv "THREADS" case nThreads of Nothing -> pure () Just n -> do @@ -27,5 +27,6 @@ tests :: TestTree tests = testGroup "Tests" - [ Tests.Protocols.tests + [ Tests.Haxioms.tests + , Tests.Protocols.tests ]