{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fplugin Protocols.Plugin #-}
module Protocols.Df (
Df,
empty,
const,
consume,
void,
pure,
map,
mapS,
bimap,
bimapS,
fst,
snd,
mapMaybe,
catMaybes,
coerce,
compressor,
expander,
compander,
filter,
filterS,
either,
eitherS,
first ,
firstS,
mapLeft,
mapLeftS,
second ,
secondS,
mapRight,
mapRightS,
zipWith,
zipWithS,
zip,
partition,
partitionEithers,
partitionS,
route,
select,
selectN,
selectUntil,
selectUntilS,
fanin,
faninS,
mfanin,
fanout,
bundleVec,
unbundleVec,
roundrobin,
CollectMode (..),
roundrobinCollect,
registerFwd,
registerBwd,
fifo,
toMaybe,
unsafeFromMaybe,
forceResetSanity,
) where
#if !MIN_VERSION_base(4,18,0)
import Control.Applicative (Applicative(liftA2))
#endif
import Control.Applicative (Alternative ((<|>)))
import GHC.Stack (HasCallStack)
import Prelude hiding (
const,
either,
filter,
fst,
map,
pure,
snd,
zip,
zipWith,
(!!),
)
import Data.Bifunctor qualified as B
import Data.Bool (bool)
import Data.Coerce qualified as Coerce
import Data.Kind (Type)
import Data.Maybe qualified as Maybe
import Data.Maybe.Extra qualified as Maybe
import Prelude qualified as P
import Clash.Prelude (type (<=))
import Clash.Prelude qualified as C
import Clash.Signal.Internal (Signal (..))
import Protocols.Idle
import Protocols.Internal
{-# ANN module "HLint: ignore Use const" #-}
data Df (dom :: C.Domain) (a :: Type)
instance Protocol (Df dom a) where
type Fwd (Df dom a) = Signal dom (Maybe a)
type Bwd (Df dom a) = Signal dom Ack
instance IdleCircuit (Df dom a) where
idleFwd _ = C.pure Nothing
idleBwd _ = C.pure (Ack False)
forceResetSanity ::
forall dom a.
( C.KnownDomain dom
, C.HiddenReset dom
) =>
Circuit (Df dom a) (Df dom a)
forceResetSanity = forceResetSanityGeneric
coerce :: (Coerce.Coercible a b) => Circuit (Df dom a) (Df dom b)
coerce = fromSignals $ \(fwdA, bwdB) -> (Coerce.coerce bwdB, Coerce.coerce fwdA)
compressor ::
forall dom s i o.
(C.HiddenClockResetEnable dom, C.NFDataX s) =>
s ->
(s -> i -> (s, Maybe o)) ->
Circuit (Df dom i) (Df dom o)
compressor s0 f = compander s0 $
\s i ->
let (s', o) = f s i
in (s', o, True)
expander ::
forall dom i o s.
(C.HiddenClockResetEnable dom, C.NFDataX s) =>
s ->
(s -> i -> (s, o, Bool)) ->
Circuit (Df dom i) (Df dom o)
expander s0 f = compander s0 $
\s i ->
let (s', o, done) = f s i
in (s', Just o, done)
compander ::
forall dom i o s.
(C.HiddenClockResetEnable dom, C.NFDataX s) =>
s ->
(s -> i -> (s, Maybe o, Bool)) ->
Circuit (Df dom i) (Df dom o)
compander s0 f = forceResetSanity |> Circuit (C.unbundle . go . C.bundle)
where
go :: Signal dom (Maybe i, Ack) -> Signal dom (Ack, Maybe o)
go = C.mealy f' s0
f' :: s -> (Maybe i, Ack) -> (s, (Ack, Maybe o))
f' s (Nothing, _) = (s, (C.deepErrorX "undefined ack", Nothing))
f' s (Just i, Ack ack) = (s'', (Ack ackBack, o))
where
(s', o, doneWithInput) = f s i
mustWaitForAck = Maybe.isJust o
(s'', ackBack) = if mustWaitForAck && not ack then (s, False) else (s', doneWithInput)
map :: (a -> b) -> Circuit (Df dom a) (Df dom b)
map f = mapS (C.pure f)
mapS :: Signal dom (a -> b) -> Circuit (Df dom a) (Df dom b)
mapS fS = Circuit (C.unbundle . liftA2 go fS . C.bundle)
where
go f (fwd, bwd) = (bwd, f <$> fwd)
bimap ::
(B.Bifunctor p) =>
(a -> b) ->
(c -> d) ->
Circuit (Df dom (p a c)) (Df dom (p b d))
bimap f g = bimapS (C.pure f) (C.pure g)
bimapS ::
(B.Bifunctor p) =>
Signal dom (a -> b) ->
Signal dom (c -> d) ->
Circuit (Df dom (p a c)) (Df dom (p b d))
bimapS fS gS = mapS (liftA2 B.bimap fS gS)
fst :: Circuit (Df dom (a, b)) (Df dom a)
fst = map P.fst
snd :: Circuit (Df dom (a, b)) (Df dom b)
snd = map P.snd
first :: (B.Bifunctor p) => (a -> b) -> Circuit (Df dom (p a c)) (Df dom (p b c))
first f = firstS (C.pure f)
firstS ::
(B.Bifunctor p) => Signal dom (a -> b) -> Circuit (Df dom (p a c)) (Df dom (p b c))
firstS fS = mapS (B.first <$> fS)
second :: (B.Bifunctor p) => (b -> c) -> Circuit (Df dom (p a b)) (Df dom (p a c))
second f = secondS (C.pure f)
secondS ::
(B.Bifunctor p) => Signal dom (b -> c) -> Circuit (Df dom (p a b)) (Df dom (p a c))
secondS fS = mapS (B.second <$> fS)
const :: (C.HiddenReset dom) => b -> Circuit (Df dom a) (Df dom b)
const b =
Circuit
( P.const
( Ack
<$> C.unsafeToActiveLow C.hasReset
, P.pure (Just b)
)
)
empty :: Circuit () (Df dom a)
empty = Circuit (P.const ((), P.pure Nothing))
pure :: a -> Circuit () (Df dom a)
pure a = Circuit (P.const ((), P.pure (Just a)))
consume :: (C.HiddenReset dom) => Circuit (Df dom a) ()
consume = Circuit (P.const (P.pure (Ack True), ()))
void :: (C.HiddenReset dom) => Circuit (Df dom a) ()
void =
Circuit
( P.const
( Ack
<$> C.unsafeToActiveLow C.hasReset
, ()
)
)
catMaybes :: Circuit (Df dom (Maybe a)) (Df dom a)
catMaybes = Circuit (C.unbundle . fmap go . C.bundle)
where
go (Nothing, _) = (C.deepErrorX "undefined ack", Nothing)
go (Just Nothing, _) = (Ack True, Nothing)
go (Just (Just a), ack) = (ack, Just a)
mapMaybe :: (a -> Maybe b) -> Circuit (Df dom a) (Df dom b)
mapMaybe f = map f |> catMaybes
filter :: forall dom a. (a -> Bool) -> Circuit (Df dom a) (Df dom a)
filter f = filterS (C.pure f)
filterS :: forall dom a. Signal dom (a -> Bool) -> Circuit (Df dom a) (Df dom a)
filterS fS = Circuit (C.unbundle . liftA2 go fS . C.bundle)
where
go _ (Nothing, _) = (C.deepErrorX "undefined ack", Nothing)
go f (Just d, ack)
| f d = (ack, Just d)
| otherwise = (Ack True, Nothing)
mapLeft :: (a -> b) -> Circuit (Df dom (Either a c)) (Df dom (Either b c))
mapLeft f = mapLeftS (C.pure f)
mapLeftS :: Signal dom (a -> b) -> Circuit (Df dom (Either a c)) (Df dom (Either b c))
mapLeftS = firstS
mapRight :: (b -> c) -> Circuit (Df dom (Either a b)) (Df dom (Either a c))
mapRight = second
mapRightS :: Signal dom (b -> c) -> Circuit (Df dom (Either a b)) (Df dom (Either a c))
mapRightS = secondS
either :: (a -> c) -> (b -> c) -> Circuit (Df dom (Either a b)) (Df dom c)
either f g = eitherS (C.pure f) (C.pure g)
eitherS ::
Signal dom (a -> c) -> Signal dom (b -> c) -> Circuit (Df dom (Either a b)) (Df dom c)
eitherS fS gS = mapS (liftA2 P.either fS gS)
zipWith ::
forall dom a b c.
(a -> b -> c) ->
Circuit
(Df dom a, Df dom b)
(Df dom c)
zipWith f = zipWithS (C.pure f)
zipWithS ::
forall dom a b c.
Signal dom (a -> b -> c) ->
Circuit
(Df dom a, Df dom b)
(Df dom c)
zipWithS fS =
Circuit (B.first C.unbundle . C.unbundle . liftA2 go fS . C.bundle . B.first C.bundle)
where
go f ((Just a, Just b), ack) = ((ack, ack), Just (f a b))
go _ _ = ((Ack False, Ack False), Nothing)
zip :: forall a b dom. Circuit (Df dom a, Df dom b) (Df dom (a, b))
zip = zipWith (,)
partition :: forall dom a. (a -> Bool) -> Circuit (Df dom a) (Df dom a, Df dom a)
partition f = partitionS (C.pure f)
partitionEithers :: forall dom a b. Circuit (Df dom (Either a b)) (Df dom a, Df dom b)
partitionEithers =
Circuit (B.second C.unbundle . C.unbundle . C.liftA go . C.bundle . B.second C.bundle)
where
go (Nothing, _) = (C.deepErrorX "undefined ack", (Nothing, Nothing))
go (Just (Left a), (ackA, _)) = (ackA, (Just a, Nothing))
go (Just (Right b), (_, ackB)) = (ackB, (Nothing, Just b))
partitionS ::
forall dom a. Signal dom (a -> Bool) -> Circuit (Df dom a) (Df dom a, Df dom a)
partitionS fS =
Circuit (B.second C.unbundle . C.unbundle . liftA2 go fS . C.bundle . B.second C.bundle)
where
go f (Just a, (ackT, ackF))
| f a = (ackT, (Just a, Nothing))
| otherwise = (ackF, (Nothing, Just a))
go _ _ = (C.deepErrorX "undefined ack", (Nothing, Nothing))
route ::
forall n dom a.
(C.KnownNat n) =>
Circuit (Df dom (C.Index n, a)) (C.Vec n (Df dom a))
route =
Circuit (B.second C.unbundle . C.unbundle . fmap go . C.bundle . B.second C.bundle)
where
go (Just (i, a), acks) =
( acks C.!! i
, C.replace i (Just a) (C.repeat Nothing)
)
go _ =
(C.deepErrorX "undefined ack", C.repeat Nothing)
select ::
forall n dom a.
(C.KnownNat n) =>
Circuit (C.Vec n (Df dom a), Df dom (C.Index n)) (Df dom a)
select = selectUntil (P.const True)
selectN ::
forall n selectN dom a.
( C.HiddenClockResetEnable dom
, C.KnownNat selectN
, C.KnownNat n
) =>
Circuit
(C.Vec n (Df dom a), Df dom (C.Index n, C.Index selectN))
(Df dom a)
selectN =
Circuit
( B.first (B.first C.unbundle . C.unbundle)
. C.mealyB go (0 :: C.Index (selectN C.+ 1))
. B.first (C.bundle . B.first C.bundle)
)
where
go c0 ((dats, datI), Ack iAck)
| Just (_, 0) <- datI =
(c0, ((nacks, Ack True), Nothing))
| Just (streamI, nSelect) <- datI
, let dat = dats C.!! streamI
, Just d <- dat =
let
c1 = if iAck then succ c0 else c0
oAckIndex = c1 == C.extend nSelect
c2 = if oAckIndex then 0 else c1
datAcks = C.replace streamI (Ack iAck) nacks
in
( c2
,
( (datAcks, Ack oAckIndex)
, Just d
)
)
| otherwise =
(c0, ((nacks, Ack False), Nothing))
where
nacks = C.repeat (Ack False)
selectUntil ::
forall n dom a.
(C.KnownNat n) =>
(a -> Bool) ->
Circuit
(C.Vec n (Df dom a), Df dom (C.Index n))
(Df dom a)
selectUntil f = selectUntilS (C.pure f)
selectUntilS ::
forall n dom a.
(C.KnownNat n) =>
Signal dom (a -> Bool) ->
Circuit
(C.Vec n (Df dom a), Df dom (C.Index n))
(Df dom a)
selectUntilS fS =
Circuit
( B.first (B.first C.unbundle . C.unbundle)
. C.unbundle
. liftA2 go fS
. C.bundle
. B.first (C.bundle . B.first C.bundle)
)
where
nacks = C.repeat (Ack False)
go f ((dats, dat), Ack ack)
| Just i <- dat
, Just d <- dats C.!! i =
(
( C.replace i (Ack ack) nacks
, Ack (f d && ack)
)
, Just d
)
| otherwise =
((nacks, Ack False), Nothing)
fanout ::
forall n dom a.
(C.KnownNat n, C.HiddenClockResetEnable dom, 1 <= n) =>
Circuit (Df dom a) (C.Vec n (Df dom a))
fanout = forceResetSanity |> goC
where
goC =
Circuit $ \(s2r, r2s) ->
B.second C.unbundle (C.mealyB f initState (s2r, C.bundle r2s))
initState = C.repeat False
f acked (dat, acks) =
case dat of
Nothing -> (acked, (C.deepErrorX "undefined ack", C.repeat Nothing))
Just _ ->
let
valids_ = C.map not acked
dats = C.map (bool Nothing dat) valids_
acked1 = C.zipWith (||) acked (C.map (\(Ack a) -> a) acks)
ack = C.fold @(n C.- 1) (&&) acked1
in
( if ack then initState else acked1
, (Ack ack, dats)
)
fanin ::
forall n dom a.
(C.KnownNat n, 1 <= n) =>
(a -> a -> a) ->
Circuit (C.Vec n (Df dom a)) (Df dom a)
fanin f = faninS (C.pure f)
faninS ::
forall n dom a.
(C.KnownNat n, 1 <= n) =>
Signal dom (a -> a -> a) ->
Circuit (C.Vec n (Df dom a)) (Df dom a)
faninS fS = bundleVec |> mapS (C.fold @(n C.- 1) <$> fS)
mfanin ::
forall n dom a.
(C.KnownNat n, Monoid a, 1 <= n) =>
Circuit (C.Vec n (Df dom a)) (Df dom a)
mfanin = fanin (<>)
bundleVec ::
forall n dom a.
(C.KnownNat n, 1 <= n) =>
Circuit (C.Vec n (Df dom a)) (Df dom (C.Vec n a))
bundleVec =
Circuit (B.first C.unbundle . C.unbundle . fmap go . C.bundle . B.first C.bundle)
where
go (iDats0, iAck) = (C.repeat oAck, dat)
where
oAck = maybe (Ack False) (P.const iAck) dat
dat = sequenceA iDats0
unbundleVec ::
forall n dom a.
(C.KnownNat n, C.NFDataX a, C.HiddenClockResetEnable dom, 1 <= n) =>
Circuit (Df dom (C.Vec n a)) (C.Vec n (Df dom a))
unbundleVec =
Circuit (B.second C.unbundle . C.mealyB go initState . B.second C.bundle)
where
initState :: C.Vec n Bool
initState = C.repeat False
go _ (Nothing, _) = (initState, (C.deepErrorX "undefined ack", C.repeat Nothing))
go acked (Just payloadVec, acks) =
let
valids_ = C.map not acked
dats = C.zipWith (bool Nothing . Just) payloadVec valids_
acked1 = C.zipWith (||) acked (C.map (\(Ack a) -> a) acks)
ack = C.fold @(n C.- 1) (&&) acked1
in
( if ack then initState else acked1
, (Ack ack, dats)
)
roundrobin ::
forall n dom a.
(C.KnownNat n, C.HiddenClockResetEnable dom, 1 <= n) =>
Circuit (Df dom a) (C.Vec n (Df dom a))
roundrobin =
Circuit
( B.second C.unbundle
. C.mealyB go (minBound :: C.Index n)
. B.second C.bundle
)
where
go i0 (Nothing, _) = (i0, (C.deepErrorX "undefined ack", C.repeat Nothing))
go i0 (Just dat, acks) =
let
datOut = C.replace i0 (Just dat) (C.repeat Nothing)
i1 = if ack then C.satSucc C.SatWrap i0 else i0
Ack ack = acks C.!! i0
in
(i1, (Ack ack, datOut))
data CollectMode
=
NoSkip
|
Skip
|
Parallel
roundrobinCollect ::
forall n dom a.
(C.KnownNat n, C.HiddenClockResetEnable dom, 1 <= n) =>
CollectMode ->
Circuit (C.Vec n (Df dom a)) (Df dom a)
roundrobinCollect NoSkip =
Circuit (B.first C.unbundle . C.mealyB go minBound . B.first C.bundle)
where
go (i :: C.Index n) (dats, Ack ack) =
case dats C.!! i of
Just d ->
( if ack then C.satSucc C.SatWrap i else i
,
( C.replace i (Ack ack) (C.repeat (Ack False))
, Just d
)
)
Nothing ->
(i, (C.repeat (Ack False), Nothing))
roundrobinCollect Skip =
Circuit (B.first C.unbundle . C.mealyB go minBound . B.first C.bundle)
where
go (i :: C.Index n) (dats, Ack ack) =
case dats C.!! i of
Just d ->
( if ack then C.satSucc C.SatWrap i else i
,
( C.replace i (Ack ack) (C.repeat (Ack False))
, Just d
)
)
Nothing ->
(C.satSucc C.SatWrap i, (C.repeat (Ack False), Nothing))
roundrobinCollect Parallel =
Circuit (B.first C.unbundle . C.mealyB go Nothing . B.first C.bundle)
where
go im (fwds, bwd@(Ack ack)) = (nextIm, (bwds, fwd))
where
nextSrc = C.fold @(n C.- 1) (<|>) (C.zipWith (<$) C.indicesI fwds)
i = Maybe.fromMaybe (Maybe.fromMaybe maxBound nextSrc) im
bwds = C.replace i bwd (C.repeat (Ack False))
fwd = fwds C.!! i
nextIm =
if Maybe.isNothing fwd || ack
then Nothing
else im
registerFwd ::
forall dom a.
(C.NFDataX a, C.HiddenClockResetEnable dom) =>
Circuit (Df dom a) (Df dom a)
registerFwd =
forceResetSanity |> Circuit (C.mealyB go Nothing)
where
go s0 (iDat, Ack iAck) = (s1, (Ack oAck, s0))
where
oAck = Maybe.isNothing s0 || iAck
s1 = if oAck then iDat else s0
registerBwd ::
forall dom a.
(C.NFDataX a, C.HiddenClockResetEnable dom) =>
Circuit (Df dom a) (Df dom a)
registerBwd =
forceResetSanity |> Circuit go
where
go (iDat, iAck) = (Ack <$> oAck, oDat)
where
oAck = C.regEn True valid (Coerce.coerce <$> iAck)
valid = (Maybe.isJust <$> iDat) C..||. fmap not oAck
iDatX0 = C.fromJustX <$> iDat
iDatX1 = C.regEn (C.errorX "registerBwd") oAck iDatX0
oDat = Maybe.toMaybe <$> valid <*> C.mux oAck iDatX0 iDatX1
blockRamUNoClear ::
forall n dom a addr.
( HasCallStack
, C.HiddenClockResetEnable dom
, C.NFDataX a
, Enum addr
, C.NFDataX addr
, 1 <= n
) =>
C.SNat n ->
Signal dom addr ->
Signal dom (Maybe (addr, a)) ->
Signal dom a
#if MIN_VERSION_clash_prelude(1,9,0)
blockRamUNoClear = C.blockRamU C.NoClearOnReset
#else
blockRamUNoClear n =
C.blockRamU C.NoClearOnReset n (C.errorX "No reset function")
#endif
fifo ::
forall dom a depth.
(C.HiddenClockResetEnable dom, C.KnownNat depth, C.NFDataX a, 1 C.<= depth) =>
C.SNat depth ->
Circuit (Df dom a) (Df dom a)
fifo fifoDepth = Circuit $ C.hideReset circuitFunction
where
circuitFunction reset (inpA, inpB) = (otpA, otpB)
where
brRead =
C.readNew
(blockRamUNoClear fifoDepth)
brReadAddr
brWrite
(brReadAddr, brWrite, otpA, otpB) =
C.unbundle $
C.mealy machineAsFunction s0 $
C.bundle
( brRead
, C.unsafeToActiveHigh reset
, inpA
, inpB
)
machineAsFunction _ (_, True, _, _) = (s0, (0, Nothing, Ack False, Nothing))
machineAsFunction (rAddr0, wAddr0, amtLeft0) (brRead0, False, pushData, Ack popped) =
let
maybePush = if amtLeft0 > 0 then pushData else Nothing
brWrite = (wAddr0,) <$> maybePush
(wAddr1, amtLeft1)
| Just _ <- maybePush = (C.satSucc C.SatWrap wAddr0, amtLeft0 - 1)
| otherwise = (wAddr0, amtLeft0)
(brRead1, amtLeft2)
| Just push <- maybePush, amtLeft0 == maxBound = (push, amtLeft1)
| otherwise = (brRead0, amtLeft0)
(rAddr1, amtLeft3)
| amtLeft2 < maxBound && popped = (C.satSucc C.SatWrap rAddr0, amtLeft1 + 1)
| otherwise = (rAddr0, amtLeft1)
brReadAddr = rAddr1
otpAck = Maybe.isJust maybePush
otpDat = if amtLeft2 < maxBound then Just brRead1 else Nothing
in
((rAddr1, wAddr1, amtLeft3), (brReadAddr, brWrite, Ack otpAck, otpDat))
s0 :: (C.Index depth, C.Index depth, C.Index (depth C.+ 1))
s0 = (0, 0, maxBound)
toMaybe :: Circuit (Df dom a) (CSignal dom (Maybe a))
toMaybe = Circuit $ \(maybes, _) -> (C.pure (Ack True), maybes)
unsafeFromMaybe ::
forall n a dom.
( C.HiddenClockResetEnable dom
, C.NFDataX a
, C.KnownNat n
) =>
Circuit
(CSignal dom (Maybe a))
( Df dom a
, CSignal dom (C.Unsigned n)
)
unsafeFromMaybe = circuit $ \maybes -> do
(as0, droppeds) <- Circuit go2 -< maybes
as1 <- forceResetSanity -< as0
idC -< (as1, droppeds)
where
go2 ::
(Signal dom (Maybe a), (Signal dom Ack, ())) ->
((), (Signal dom (Maybe a), Signal dom (C.Unsigned n)))
go2 (fwdA, (ackB, _)) = ((), C.mealyB go1 (Nothing, 0) (fwdA, ackB))
go1 ::
(Maybe a, C.Unsigned n) ->
(Maybe a, Ack) ->
( (Maybe a, C.Unsigned n)
, (Maybe a, C.Unsigned n)
)
go1 (s0, !n0) ~(i, ~(Ack ack)) = ((s1, n1), (o, n1))
where
n1
| Maybe.isJust s0 && Maybe.isJust i && not ack = n0 + 1
| otherwise = n0
o = s0 <|> i
s1
| Maybe.isJust s0 && not ack = s0
| Maybe.isJust s0 && ack = i
| Maybe.isJust i && ack = Nothing
| otherwise = i