|
| 1 | +{-# OPTIONS_GHC -fplugin Protocols.Plugin #-} |
| 2 | + |
| 3 | +-- | Bi-directional request/response-style 'Df' channels. |
| 4 | +module Protocols.BiDf ( |
| 5 | + BiDf, |
| 6 | + -- * Conversion |
| 7 | + fromDfs, |
| 8 | + toDfs, |
| 9 | + fromBiDf, |
| 10 | + toBiDf, |
| 11 | + -- * Trivial combinators |
| 12 | + void, |
| 13 | + loopback, |
| 14 | + -- * Mapping |
| 15 | + dimap, |
| 16 | +) where |
| 17 | + |
| 18 | +import Prelude () |
| 19 | + |
| 20 | +import Clash.Prelude |
| 21 | + |
| 22 | +import Protocols |
| 23 | +import qualified Protocols.Df as Df |
| 24 | + |
| 25 | +-- | A 'Protocol' allowing requests to be passed downstream, with corresponding |
| 26 | +-- responses being passed back upstream. Responses are provided in the order that |
| 27 | +-- their corresponding requests were submitted. |
| 28 | +-- |
| 29 | +-- *Correctness conditions* |
| 30 | +-- |
| 31 | +-- - The response channel must not produce a value before the request channel |
| 32 | +-- has produced a value. |
| 33 | +-- |
| 34 | +-- - Each request must be paired with exactly one response. |
| 35 | +-- |
| 36 | +-- - Responses must be issued in the order that their corresponding requests arrived. |
| 37 | +-- |
| 38 | +-- - Both the request and response channels must obey usual 'Df' correctness |
| 39 | +-- conditions. |
| 40 | +-- |
| 41 | +-- - There must not be a combinational path from the request channel to the |
| 42 | +-- response channel. |
| 43 | +-- |
| 44 | +type BiDf dom req resp = |
| 45 | + (Df dom req, Reverse (Df dom resp)) |
| 46 | + |
| 47 | +-- | Convert a circuit of 'Df's to a 'BiDf' circuit. |
| 48 | +toBiDf |
| 49 | + :: Circuit (Df dom req) (Df dom resp) |
| 50 | + -> Circuit (BiDf dom req resp) () |
| 51 | +toBiDf c = circuit $ \bidf -> do |
| 52 | + resp <- c -< req |
| 53 | + req <- toDfs -< (bidf, resp) |
| 54 | + idC -< () |
| 55 | + |
| 56 | +-- | Convert a 'BiDf' circuit to a circuit of 'Df's. |
| 57 | +fromBiDf |
| 58 | + :: Circuit (BiDf dom req resp) () |
| 59 | + -> Circuit (Df dom req) (Df dom resp) |
| 60 | +fromBiDf c = circuit $ \req -> do |
| 61 | + (biDf, resp) <- fromDfs -< req |
| 62 | + c -< biDf |
| 63 | + idC -< resp |
| 64 | + |
| 65 | +-- | Convert a pair of a request and response 'Df`s into a 'BiDf'. |
| 66 | +toDfs :: Circuit (BiDf dom req resp, Df dom resp) (Df dom req) |
| 67 | +toDfs = fromSignals $ \(~((reqData, respAck), respData), reqAck) -> |
| 68 | + (((reqAck, respData), respAck), reqData) |
| 69 | + |
| 70 | +-- | Convert a 'BiDf' into a pair of request and response 'Df`s. |
| 71 | +fromDfs :: Circuit (Df dom req) (BiDf dom req resp, Df dom resp) |
| 72 | +fromDfs = fromSignals $ \(reqData, ~((reqAck, respData), respAck)) -> |
| 73 | + (reqAck, ((reqData, respAck), respData)) |
| 74 | + |
| 75 | +-- | Ignore all requests, never providing responses. |
| 76 | +void :: (HiddenClockResetEnable dom) => Circuit (BiDf dom req resp') () |
| 77 | +void = circuit $ \biDf -> do |
| 78 | + req <- toDfs -< (biDf, resp) |
| 79 | + resp <- Df.empty -< () |
| 80 | + Df.void -< req |
| 81 | + |
| 82 | +-- | Return mapped requests as responses. |
| 83 | +loopback |
| 84 | + :: (HiddenClockResetEnable dom, NFDataX req) |
| 85 | + => (req -> resp) |
| 86 | + -> Circuit (BiDf dom req resp) () |
| 87 | +loopback f = circuit $ \biDf -> do |
| 88 | + req <- toDfs -< (biDf, resp) |
| 89 | + resp <- Df.map f <| Df.registerFwd -< req |
| 90 | + idC -< () |
| 91 | + |
| 92 | +-- | Map both requests and responses. |
| 93 | +dimap |
| 94 | + :: (req -> req') |
| 95 | + -> (resp -> resp') |
| 96 | + -> Circuit (BiDf dom req resp') (BiDf dom req' resp) |
| 97 | +dimap f g = circuit $ \biDf -> do |
| 98 | + req <- toDfs -< (biDf, resp') |
| 99 | + req' <- Df.map f -< req |
| 100 | + resp' <- Df.map g -< resp |
| 101 | + (biDf', resp) <- fromDfs -< req' |
| 102 | + idC -< biDf' |
0 commit comments