-
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.
This introduces a new protocol, `BiDf`, which captures the common pattern of a request `Df` channel paired with a `Df` for returning corresponding responses.
- Loading branch information
Showing
4 changed files
with
234 additions
and
1 deletion.
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,136 @@ | ||
{-# OPTIONS_GHC -fplugin Protocols.Plugin #-} | ||
|
||
-- | Bi-directional request/response-style 'Df' channels. | ||
module Protocols.BiDf ( | ||
BiDf, | ||
-- * Conversion | ||
fromDfs, | ||
toDfs, | ||
fromBiDf, | ||
toBiDf, | ||
-- * Trivial combinators | ||
void, | ||
loopback, | ||
-- * Mapping | ||
dimap, | ||
-- * Fan-in | ||
fanin | ||
) where | ||
|
||
import Prelude () | ||
|
||
import Clash.Prelude | ||
|
||
import Protocols | ||
import qualified Protocols.Df as Df | ||
|
||
-- | A 'Protocol' allowing requests to be passed downstream, with corresponding | ||
-- responses being passed back upstream. Responses are provided in the order that | ||
-- their corresponding requests were submitted. | ||
-- | ||
-- *Correctness conditions* | ||
-- | ||
-- - The response channel must not produce a value before the request channel | ||
-- has produced a value. | ||
-- | ||
-- - Each request must be paired with exactly one response. | ||
-- | ||
-- - There must not be a combinational path from the request channel to the | ||
-- response channel. | ||
-- | ||
type BiDf dom req resp = | ||
(Df dom req, Reverse (Df dom resp)) | ||
|
||
-- | Convert a circuit of 'Df's to a 'BiDf' circuit. | ||
toBiDf | ||
:: Circuit (Df dom req) (Df dom resp) | ||
-> Circuit (BiDf dom req resp) () | ||
toBiDf c = circuit $ \bidf -> do | ||
resp <- c -< req | ||
req <- toDfs -< (bidf, resp) | ||
idC -< () | ||
|
||
-- | Convert a 'BiDf' circuit to a circuit of 'Df's. | ||
fromBiDf | ||
:: Circuit (BiDf dom req resp) () | ||
-> Circuit (Df dom req) (Df dom resp) | ||
fromBiDf c = circuit $ \req -> do | ||
(biDf, resp) <- fromDfs -< req | ||
c -< biDf | ||
idC -< resp | ||
|
||
-- | Convert a pair of a request and response 'Df`s into a 'BiDf'. | ||
toDfs :: Circuit (BiDf dom req resp, Df dom resp) (Df dom req) | ||
toDfs = fromSignals $ \(~((reqData, respAck), respData), reqAck) -> | ||
(((reqAck, respData), respAck), reqData) | ||
|
||
-- | Convert a 'BiDf' into a pair of request and response 'Df`s. | ||
fromDfs :: Circuit (Df dom req) (BiDf dom req resp, Df dom resp) | ||
fromDfs = fromSignals $ \(reqData, ~((reqAck, respData), respAck)) -> | ||
(reqAck, ((reqData, respAck), respData)) | ||
|
||
-- | Ignore all requests, never providing responses. | ||
void :: (HiddenClockResetEnable dom) => Circuit (BiDf dom req resp') () | ||
void = circuit $ \biDf -> do | ||
req <- toDfs -< (biDf, resp) | ||
resp <- Df.empty -< () | ||
Df.void -< req | ||
|
||
-- | Return mapped requests as responses. | ||
loopback | ||
:: (HiddenClockResetEnable dom, NFDataX req) | ||
=> (req -> resp) | ||
-> Circuit (BiDf dom req resp) () | ||
loopback f = circuit $ \biDf -> do | ||
req <- toDfs -< (biDf, resp) | ||
resp <- Df.map f <| Df.registerFwd -< req | ||
idC -< () | ||
|
||
-- | Map both requests and responses. | ||
dimap | ||
:: (req -> req') | ||
-> (resp -> resp') | ||
-> Circuit (BiDf dom req resp') (BiDf dom req' resp) | ||
dimap f g = circuit $ \biDf -> do | ||
req <- toDfs -< (biDf, resp') | ||
req' <- Df.map f -< req | ||
resp' <- Df.map g -< resp | ||
(biDf', resp) <- fromDfs -< req' | ||
idC -< biDf' | ||
|
||
-- | Merge a number of 'BiDf's, preferring requests from the last channel. | ||
fanin | ||
:: forall n dom req resp. | ||
( KnownNat n | ||
, 1 <= n | ||
, NFDataX req | ||
, NFDataX resp | ||
, HiddenClockResetEnable dom | ||
) | ||
=> Circuit (Vec n (BiDf dom req resp)) (BiDf dom req resp) | ||
fanin = fromSignals $ \(upFwds, (reqAck, respData)) -> | ||
let reqDatas :: Vec n (Signal dom (Df.Data req)) | ||
reqDatas = map fst upFwds | ||
respAcks :: Vec n (Signal dom Ack) | ||
respAcks = map snd upFwds | ||
|
||
((reqAcks, respAck), (respDatas, reqData)) = | ||
toSignals fanin' ((reqDatas, respData), (respAcks, reqAck)) | ||
in (zip reqAcks respDatas, (reqData, respAck)) | ||
where | ||
fanin' | ||
:: Circuit (Vec n (Df dom req), Df dom resp) | ||
(Vec n (Df dom resp), Df dom req) | ||
fanin' = circuit $ \(reqs, resp) -> do | ||
[fwd0, fwd1] | ||
<- Df.fanout | ||
<| Df.roundrobinCollect @n Df.Parallel | ||
<| Df.unbundleVec | ||
<| Df.map (zip indicesI) | ||
<| Df.bundleVec | ||
-< reqs | ||
|
||
activeN <- Df.map fst -< fwd1 | ||
resps <- Df.route <| Df.zip -< (activeN, resp) | ||
req <- Df.map snd -< fwd0 | ||
idC -< (resps, req) |
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,93 @@ | ||
{-# OPTIONS_GHC -fplugin Protocols.Plugin #-} | ||
{-# LANGUAGE TemplateHaskell #-} | ||
|
||
module Tests.Protocols.BiDf where | ||
|
||
-- clash-prelude | ||
import Clash.Prelude | ||
import qualified Clash.Sized.Vector as Vector | ||
import Clash.Hedgehog.Sized.Vector | ||
|
||
-- clash-protocols | ||
import Protocols | ||
import Protocols.Hedgehog | ||
import Protocols.BiDf as BiDf | ||
|
||
-- hedgehog | ||
import Hedgehog | ||
import qualified Hedgehog.Gen as Gen | ||
import qualified Hedgehog.Range as Range | ||
|
||
-- tasty | ||
import Test.Tasty | ||
import Test.Tasty.Hedgehog.Extra (testProperty) | ||
import Test.Tasty.TH (testGroupGenerator) | ||
|
||
prop_toDfs_fromDfs_id :: Property | ||
prop_toDfs_fromDfs_id = | ||
idWithModelSingleDomain @System defExpectOptions gen (\_ _ _ -> id) (exposeClockResetEnable impl) | ||
where | ||
gen :: Gen [Int] | ||
gen = Gen.list (Range.linear 0 10) (Gen.integral (Range.linear 0 100)) | ||
|
||
impl :: forall dom a. (HiddenClockResetEnable dom, NFDataX a) | ||
=> Circuit (Df dom a) (Df dom a) | ||
impl = BiDf.toDfs <| BiDf.fromDfs | ||
|
||
prop_loopback_id :: Property | ||
prop_loopback_id = | ||
idWithModelSingleDomain @System defExpectOptions gen (\_ _ _ -> id) (exposeClockResetEnable impl) | ||
where | ||
gen :: Gen [Int] | ||
gen = Gen.list (Range.linear 0 10) (Gen.integral (Range.linear 0 100)) | ||
|
||
impl :: forall dom a. (HiddenClockResetEnable dom, NFDataX a) | ||
=> Circuit (Df dom a) (Df dom a) | ||
impl = circuit $ \req -> do | ||
(biDf, resp) <- BiDf.fromDfs -< req | ||
BiDf.loopback id -< biDf | ||
idC -< resp | ||
|
||
prop_fanin_id :: Property | ||
prop_fanin_id = | ||
idWithModelSingleDomain @System defExpectOptions gen (\_ _ _ -> id) (exposeClockResetEnable impl) | ||
where | ||
gen :: Gen [Int] | ||
gen = Gen.list (Range.linear 0 10) (Gen.integral (Range.linear 0 100)) | ||
|
||
impl :: forall dom a. (HiddenClockResetEnable dom, NFDataX a) | ||
=> Circuit (Df dom a) (Df dom a) | ||
impl = circuit $ \req -> do | ||
(biDf, resp) <- BiDf.fromDfs -< req | ||
BiDf.loopback id <| BiDf.fanin @1 -< [biDf] | ||
idC -< resp | ||
|
||
prop_fanin :: Property | ||
prop_fanin = | ||
idWithModelSingleDomain @System expectOpts gen (\_ _ _ -> model) (exposeClockResetEnable impl) | ||
where | ||
expectOpts = defExpectOptions | ||
|
||
gen :: Gen (Vec 10 [Int]) | ||
gen = genVec @Gen @10 $ Gen.list (Range.linear 0 10) (Gen.integral (Range.linear 0 100)) | ||
|
||
model :: Vec 10 [Int] -> Vec 10 [Int] | ||
model = fmap $ fmap succ | ||
|
||
impl :: forall dom. (HiddenClockResetEnable dom) | ||
=> Circuit (Vec 10 (Df dom Int)) (Vec 10 (Df dom Int)) | ||
impl = circuit $ \reqs -> do | ||
(biDfs, resps) <- unbundleC <| repeatC BiDf.fromDfs -< reqs | ||
BiDf.loopback succ <| BiDf.fanin @10 -< biDfs | ||
idC -< resps | ||
|
||
unbundleC :: forall n a b. Circuit (Vec n (a, b)) (Vec n a, Vec n b) | ||
unbundleC = fromSignals $ \(fwd, (bwdA, bwdB)) -> | ||
let fwdA :: Vec n (Fwd a) | ||
fwdB :: Vec n (Fwd b) | ||
(fwdA, fwdB) = Vector.unzip fwd | ||
in (Vector.zip bwdA bwdB, (fwdA, fwdB)) | ||
|
||
tests :: TestTree | ||
tests = | ||
$(testGroupGenerator) |