|
| 1 | +{-# OPTIONS_GHC -fplugin=Protocols.Plugin #-} |
| 2 | + |
| 3 | +{- | |
| 4 | +Module : Protocols.BiDf |
| 5 | +Description : A simple request-response protocol. |
| 6 | +
|
| 7 | +This module defines `BiDf`, a basic protocol for request-response communication systems based on two `Df` streams. |
| 8 | +
|
| 9 | +[@Request stream@] |
| 10 | +The request stream is a stream with the same format as `Df`, where the payload forms a request. For each accepted |
| 11 | +request, the circuit must produce a response. This response can be delayed by any number of cycles. The request |
| 12 | +stream must obey all rules of the `Df` stream. |
| 13 | +
|
| 14 | +[@Response stream@] |
| 15 | +The response stream is a `Df` that should produce a response for each accepted request. The response can be delayed |
| 16 | +by any number of cycles and must obey all rules of the `Df` stream. |
| 17 | +
|
| 18 | +Protocol Rules: |
| 19 | +* The request stream must obey all rules of the `Df` stream. |
| 20 | +* The response stream must obey all rules of the `Df` stream. |
| 21 | +-} |
| 22 | +module Protocols.BiDf where |
| 23 | + |
| 24 | +import qualified Clash.Prelude as C |
| 25 | +import Data.Kind (Type) |
| 26 | +import Data.Tuple |
| 27 | +import Protocols |
| 28 | + |
| 29 | +import qualified Protocols.Df as Df |
| 30 | + |
| 31 | +-- type BiDf (dom :: C.Domain) (req :: Type) (resp :: Type) = (Df dom req, Reverse (Df dom resp)) |
| 32 | + |
| 33 | +-- | A combination of two `Df` streams, one for requests and one for responses. |
| 34 | +type BiDf (dom :: C.Domain) (req :: Type) (resp :: Type) = |
| 35 | + (Df dom req, Reverse (Df dom resp)) |
| 36 | + |
| 37 | +{- | Receive a request-response circuit of type `Circuit (Df dom req) (Df dom resp)` |
| 38 | +and transform it into a circuit of type `BiDf dom req resp` |
| 39 | +-} |
| 40 | +toBiDfSub :: |
| 41 | + forall dom req resp. |
| 42 | + Circuit (Df dom req) (Df dom resp) -> |
| 43 | + Circuit (BiDf dom req resp) () |
| 44 | +toBiDfSub (Circuit df) = Circuit ((,()) . df . fst) |
| 45 | + |
| 46 | +{- | Receive a request-response circuit of type `BiDf dom req resp` |
| 47 | +and transform it into a circuit of type `Circuit (Df dom req) (Df dom resp)` |
| 48 | +-} |
| 49 | +fromBiDfSub :: |
| 50 | + forall dom req resp. |
| 51 | + Circuit (BiDf dom req resp) () -> |
| 52 | + Circuit (Df dom req) (Df dom resp) |
| 53 | +fromBiDfSub (Circuit biDf) = Circuit (fst . biDf . (,())) |
| 54 | + |
| 55 | +{- | Receive a request-response circuit of type `Circuit (Df dom req) (Df dom resp)` |
| 56 | +and transform it into a circuit of type `Circuit () (BiDf dom req resp)` |
| 57 | +-} |
| 58 | +toBiDfMan :: |
| 59 | + forall dom req resp. |
| 60 | + Circuit (Df dom resp) (Df dom req) -> |
| 61 | + Circuit () (BiDf dom req resp) |
| 62 | +toBiDfMan (Circuit df) = Circuit (((),) . swap . df . swap . snd) |
| 63 | + |
| 64 | +{- | Receive a request-response circuit of type `Circuit () (BiDf dom req resp)` |
| 65 | +and transform it into a circuit of type `Circuit (Df dom req) (Df dom req)` |
| 66 | +-} |
| 67 | +fromBiDfMan :: |
| 68 | + forall dom req resp. |
| 69 | + Circuit () (BiDf dom req resp) -> |
| 70 | + Circuit (Df dom resp) (Df dom req) |
| 71 | +fromBiDfMan (Circuit biDf) = Circuit (swap . snd . biDf . ((),) . swap) |
| 72 | + |
| 73 | +-- | Prepend a circuit to the `Df dom req` stream of `BiDf dom req resp` |
| 74 | +prependReq :: |
| 75 | + forall dom req resp. |
| 76 | + Circuit (Df dom req) (Df dom req) -> |
| 77 | + Circuit (BiDf dom req resp) (BiDf dom req resp) |
| 78 | +prependReq df = Circuit biDf |
| 79 | + where |
| 80 | + biDf ((reqDat0, respAck), (reqAck0, respDat)) = |
| 81 | + ((reqAck1, respDat), (reqDat1, respAck)) |
| 82 | + where |
| 83 | + (reqAck1, reqDat1) = toSignals df (reqDat0, reqAck0) |
| 84 | + |
| 85 | +-- | Append a circuit to the `Df dom resp` stream of `BiDf dom req resp` |
| 86 | +appendResp :: |
| 87 | + forall dom req resp. |
| 88 | + Circuit (Df dom resp) (Df dom resp) -> |
| 89 | + Circuit (BiDf dom req resp) (BiDf dom req resp) |
| 90 | +appendResp df = Circuit biDf |
| 91 | + where |
| 92 | + biDf ((reqDat, respAck0), (reqAck, respDat0)) = |
| 93 | + ((reqAck, respDat1), (reqDat, respAck1)) |
| 94 | + where |
| 95 | + (respAck1, respDat1) = toSignals df (respDat0, respAck0) |
| 96 | + |
| 97 | +forceResetSanity :: |
| 98 | + forall dom req resp. |
| 99 | + (C.HiddenClockResetEnable dom) => |
| 100 | + Circuit (BiDf dom req resp) (BiDf dom req resp) |
| 101 | +forceResetSanity = prependReq Df.forceResetSanity |> appendResp Df.forceResetSanity |
| 102 | + |
| 103 | +-- Below you'll find some example code that uses the BiDf protocol. |
| 104 | +-- We either remove it before merging or we keep it as a reference for future development. |
| 105 | + |
| 106 | +memoryDf :: Circuit (Df dom addr) (Df dom dat) |
| 107 | +memoryDf = undefined |
| 108 | + |
| 109 | +{- | Observes the incoming request and starts producing incremental outgoing requests. |
| 110 | +As soong as it receives responses from its subordinate, it offers them to its superior |
| 111 | +and acknowledges the incoming request. |
| 112 | +-} |
| 113 | +prefetcher :: Circuit (BiDf dom addr dat) (BiDf dom addr dat) |
| 114 | +prefetcher = undefined |
| 115 | + |
| 116 | +type InstructionBus dom addrW = BiDf dom (C.Unsigned addrW) (C.BitVector 32) |
| 117 | + |
| 118 | +cpu :: |
| 119 | + Circuit |
| 120 | + (CSignal dom (C.BitVector n)) |
| 121 | + (InstructionBus dom addrW, CSignal dom C.Bit) |
| 122 | +cpu = undefined |
| 123 | + |
| 124 | +someExample :: Circuit (CSignal dom (C.BitVector n)) (CSignal dom C.Bit) |
| 125 | +someExample = circuit $ \interrupts -> do |
| 126 | + (cpuBus, uart) <- cpu -< interrupts |
| 127 | + toBiDfSub memoryDf <| prefetcher -< cpuBus |
| 128 | + idC -< uart |
0 commit comments