diff --git a/clash-protocols.cabal b/clash-protocols.cabal index 862be025..815ea564 100644 --- a/clash-protocols.cabal +++ b/clash-protocols.cabal @@ -179,7 +179,7 @@ library Protocols.Internal.Units.TH Protocols.Plugin Protocols.Plugin.Internal - Protocols.ReqResp + Protocols.BiDf Protocols.Wishbone Protocols.Wishbone.Standard Protocols.Wishbone.Standard.Hedgehog diff --git a/src/Protocols/BiDf.hs b/src/Protocols/BiDf.hs new file mode 100644 index 00000000..1aee37eb --- /dev/null +++ b/src/Protocols/BiDf.hs @@ -0,0 +1,128 @@ +{-# OPTIONS_GHC -fplugin=Protocols.Plugin #-} + +{- | +Module : Protocols.BiDf +Description : A simple request-response protocol. + +This module defines `BiDf`, a basic protocol for request-response communication systems based on two `Df` streams. + +[@Request stream@] +The request stream is a stream with the same format as `Df`, where the payload forms a request. For each accepted +request, the circuit must produce a response. This response can be delayed by any number of cycles. The request +stream must obey all rules of the `Df` stream. + +[@Response stream@] +The response stream is a `Df` that should produce a response for each accepted request. The response can be delayed +by any number of cycles and must obey all rules of the `Df` stream. + +Protocol Rules: +* The request stream must obey all rules of the `Df` stream. +* The response stream must obey all rules of the `Df` stream. +-} +module Protocols.BiDf where + +import qualified Clash.Prelude as C +import Data.Kind (Type) +import Data.Tuple +import Protocols + +import qualified Protocols.Df as Df + +-- type BiDf (dom :: C.Domain) (req :: Type) (resp :: Type) = (Df dom req, Reverse (Df dom resp)) + +-- | A combination of two `Df` streams, one for requests and one for responses. +type BiDf (dom :: C.Domain) (req :: Type) (resp :: Type) = + (Df dom req, Reverse (Df dom resp)) + +{- | Receive a request-response circuit of type `Circuit (Df dom req) (Df dom resp)` +and transform it into a circuit of type `BiDf dom req resp` +-} +toBiDfSub :: + forall dom req resp. + Circuit (Df dom req) (Df dom resp) -> + Circuit (BiDf dom req resp) () +toBiDfSub (Circuit df) = Circuit ((,()) . df . fst) + +{- | Receive a request-response circuit of type `BiDf dom req resp` +and transform it into a circuit of type `Circuit (Df dom req) (Df dom resp)` +-} +fromBiDfSub :: + forall dom req resp. + Circuit (BiDf dom req resp) () -> + Circuit (Df dom req) (Df dom resp) +fromBiDfSub (Circuit biDf) = Circuit (fst . biDf . (,())) + +{- | Receive a request-response circuit of type `Circuit (Df dom req) (Df dom resp)` +and transform it into a circuit of type `Circuit () (BiDf dom req resp)` +-} +toBiDfMan :: + forall dom req resp. + Circuit (Df dom resp) (Df dom req) -> + Circuit () (BiDf dom req resp) +toBiDfMan (Circuit df) = Circuit (((),) . swap . df . swap . snd) + +{- | Receive a request-response circuit of type `Circuit () (BiDf dom req resp)` +and transform it into a circuit of type `Circuit (Df dom req) (Df dom req)` +-} +fromBiDfMan :: + forall dom req resp. + Circuit () (BiDf dom req resp) -> + Circuit (Df dom resp) (Df dom req) +fromBiDfMan (Circuit biDf) = Circuit (swap . snd . biDf . ((),) . swap) + +-- | Prepend a circuit to the `Df dom req` stream of `BiDf dom req resp` +prependReq :: + forall dom req resp. + Circuit (Df dom req) (Df dom req) -> + Circuit (BiDf dom req resp) (BiDf dom req resp) +prependReq df = Circuit biDf + where + biDf ((reqDat0, respAck), (reqAck0, respDat)) = + ((reqAck1, respDat), (reqDat1, respAck)) + where + (reqAck1, reqDat1) = toSignals df (reqDat0, reqAck0) + +-- | Append a circuit to the `Df dom resp` stream of `BiDf dom req resp` +appendResp :: + forall dom req resp. + Circuit (Df dom resp) (Df dom resp) -> + Circuit (BiDf dom req resp) (BiDf dom req resp) +appendResp df = Circuit biDf + where + biDf ((reqDat, respAck0), (reqAck, respDat0)) = + ((reqAck, respDat1), (reqDat, respAck1)) + where + (respAck1, respDat1) = toSignals df (respDat0, respAck0) + +forceResetSanity :: + forall dom req resp. + (C.HiddenClockResetEnable dom) => + Circuit (BiDf dom req resp) (BiDf dom req resp) +forceResetSanity = prependReq Df.forceResetSanity |> appendResp Df.forceResetSanity + +-- Below you'll find some example code that uses the BiDf protocol. +-- We either remove it before merging or we keep it as a reference for future development. + +memoryDf :: Circuit (Df dom addr) (Df dom dat) +memoryDf = undefined + +{- | Observes the incoming request and starts producing incremental outgoing requests. +As soong as it receives responses from its subordinate, it offers them to its superior +and acknowledges the incoming request. +-} +prefetcher :: Circuit (BiDf dom addr dat) (BiDf dom addr dat) +prefetcher = undefined + +type InstructionBus dom addrW = BiDf dom (C.Unsigned addrW) (C.BitVector 32) + +cpu :: + Circuit + (CSignal dom (C.BitVector n)) + (InstructionBus dom addrW, CSignal dom C.Bit) +cpu = undefined + +someExample :: Circuit (CSignal dom (C.BitVector n)) (CSignal dom C.Bit) +someExample = circuit $ \interrupts -> do + (cpuBus, uart) <- cpu -< interrupts + toBiDfSub memoryDf <| prefetcher -< cpuBus + idC -< uart diff --git a/src/Protocols/ReqResp.hs b/src/Protocols/ReqResp.hs deleted file mode 100644 index fc589a67..00000000 --- a/src/Protocols/ReqResp.hs +++ /dev/null @@ -1,46 +0,0 @@ -{- | -Simple protocol for request-response communication. -The forward channel channel has type @Signal dom (Maybe req)@ and is used to send requests. -The backward channel has type @Signal dom (Maybe resp)@ and is used to send responses. -The protocol must obey the following rules: -* When the forward channel is @Just a@, it must not change until the transaction is completed. -* The forward channel can not depend on the backward channel. -* When the forward channel is @Nothing@, the backward channel may be undefined. --} -module Protocols.ReqResp where - -import qualified Clash.Prelude as C -import Data.Kind (Type) -import Protocols -import Protocols.Internal.Classes -import Prelude as P - -{- | For simple request-response protocols. The forward channel is used to send requests -and the backward channel is used to send responses. -Rules: -* When the forward channel is @Just a@, it must not change until the transaction - is completed. -* The forward channel can not depend on the backward channel. -* When the forward channel is @Nothing@, the backward channel may be undefined. --} -data ReqResp (dom :: C.Domain) (req :: Type) (resp :: Type) - -instance Protocol (ReqResp dom req resp) where - -- \| Forward channel for ReqResp protocol: - type Fwd (ReqResp dom req resp) = C.Signal dom (Maybe req) - - -- \| Backward channel for ReqResp protocol: - type Bwd (ReqResp dom req resp) = C.Signal dom (Maybe resp) - -instance IdleCircuit (ReqResp dom req resp) where - idleFwd _ = pure Nothing - idleBwd _ = pure Nothing - -{- | Force a @Nothing@ on the backward channel and @Nothing@ on the forward -channel if reset is asserted. --} -forceResetSanity :: - forall dom req resp. - (C.HiddenReset dom) => - Circuit (ReqResp dom req resp) (ReqResp dom req resp) -forceResetSanity = forceResetSanityGeneric