From 5b378a170291be4bbcb18e377e08b14872c0b4cf Mon Sep 17 00:00:00 2001 From: Ben Gamari Date: Mon, 9 Sep 2024 05:52:37 -0400 Subject: [PATCH] Introduce BiDf protocol This introduces a new protocol, `BiDf`, which captures the common pattern of a request `Df` channel paired with a `Df` for returning corresponding responses. --- clash-protocols/clash-protocols.cabal | 2 + clash-protocols/src/Protocols/BiDf.hs | 102 ++++++++++++++++++ clash-protocols/tests/Tests/Protocols.hs | 4 +- clash-protocols/tests/Tests/Protocols/BiDf.hs | 56 ++++++++++ 4 files changed, 163 insertions(+), 1 deletion(-) create mode 100644 clash-protocols/src/Protocols/BiDf.hs create mode 100644 clash-protocols/tests/Tests/Protocols/BiDf.hs diff --git a/clash-protocols/clash-protocols.cabal b/clash-protocols/clash-protocols.cabal index 1017ec5b..2b2b9720 100644 --- a/clash-protocols/clash-protocols.cabal +++ b/clash-protocols/clash-protocols.cabal @@ -144,6 +144,7 @@ library Protocols.Axi4.WriteAddress Protocols.Axi4.WriteData Protocols.Axi4.WriteResponse + Protocols.BiDf Protocols.Df Protocols.DfConv Protocols.Hedgehog @@ -175,6 +176,7 @@ test-suite unittests main-is: unittests.hs other-modules: Tests.Protocols + Tests.Protocols.BiDf Tests.Protocols.Df Tests.Protocols.DfConv Tests.Protocols.Avalon diff --git a/clash-protocols/src/Protocols/BiDf.hs b/clash-protocols/src/Protocols/BiDf.hs new file mode 100644 index 00000000..175cc8f8 --- /dev/null +++ b/clash-protocols/src/Protocols/BiDf.hs @@ -0,0 +1,102 @@ +{-# 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, +) 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. +-- +-- - Responses must be issued in the order that their corresponding requests arrived. +-- +-- - Both the request and response channels must obey usual 'Df' correctness +-- conditions. +-- +-- - 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' diff --git a/clash-protocols/tests/Tests/Protocols.hs b/clash-protocols/tests/Tests/Protocols.hs index a09bc008..23b01913 100644 --- a/clash-protocols/tests/Tests/Protocols.hs +++ b/clash-protocols/tests/Tests/Protocols.hs @@ -3,6 +3,7 @@ module Tests.Protocols (tests, main) where import Test.Tasty import qualified Tests.Protocols.Avalon import qualified Tests.Protocols.Axi4 +import qualified Tests.Protocols.BiDf import qualified Tests.Protocols.Df import qualified Tests.Protocols.DfConv import qualified Tests.Protocols.Wishbone @@ -11,7 +12,8 @@ tests :: TestTree tests = testGroup "Protocols" - [ Tests.Protocols.Df.tests + [ Tests.Protocols.BiDf.tests + , Tests.Protocols.Df.tests , Tests.Protocols.DfConv.tests , Tests.Protocols.Avalon.tests , Tests.Protocols.Axi4.tests diff --git a/clash-protocols/tests/Tests/Protocols/BiDf.hs b/clash-protocols/tests/Tests/Protocols/BiDf.hs new file mode 100644 index 00000000..b05d6fdf --- /dev/null +++ b/clash-protocols/tests/Tests/Protocols/BiDf.hs @@ -0,0 +1,56 @@ +{-# OPTIONS_GHC -fplugin Protocols.Plugin #-} +{-# LANGUAGE TemplateHaskell #-} + +module Tests.Protocols.BiDf (tests) 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) + +-- | Ensure that 'BiDf.toDfs' composed with 'BiDf.fromDfs' behaves as an +-- identity. +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 + +-- | Ensure that 'BiDf.loopback' behaves as an identity. +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 + +tests :: TestTree +tests = + $(testGroupGenerator) \ No newline at end of file