Add PacketStream protocol.

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:

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

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))

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

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

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 ->

clash-protocols/src/Protocols/Internal.hs

@@ -59,7 +59,7 @@
 
 -- | Protocol-agnostic acknowledgement
 newtype Ack = Ack Bool
   deriving (Generic, C.NFDataX, Show, C.Bundle, Eq, Ord)
 
 -- | Acknowledge. Used in circuit-notation plugin to drive ignore components.
 instance Default Ack where
@@ -306,7 +306,7 @@
   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 @@
      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.

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. <[email protected]>
+
+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

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. <[email protected]>
+
+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