-
Notifications
You must be signed in to change notification settings - Fork 7
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Add PacketStream protocol. Co-authored-by: Jasmijn Bookelmann <[email protected]> Co-authored-by: Cato van Ojen <[email protected]>> Co-authored-by: MatthijsMu <[email protected]> Co-authored-by: t-wallet <[email protected]> Co-authored-by: Jasper Laumen <[email protected]> Co-authored-by: Mart Koster <[email protected]> Co-authored-by: Bryan Rinders <[email protected]> Co-authored-by: Daan Weessies <[email protected]>
- Loading branch information
1 parent
4760508
commit ec001d4
Showing
29 changed files
with
4,295 additions
and
13 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
Oops, something went wrong.