From fad03d9bb68bc791b913c4a1bfef629e622b3303 Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Mon, 14 Dec 2020 17:25:01 +0100 Subject: [PATCH 1/2] Add more functions and tests + laziness issue fix --- clash-protocols.cabal | 16 ++- src/Protocols.hs | 30 ++++- src/Protocols/Df.hs | 2 +- src/Protocols/Df.hs-boot | 9 ++ src/Protocols/Df/Simple.hs | 141 ++++++++++++++++++-- src/Protocols/Df/Simple.hs-boot | 9 ++ src/Protocols/Hedgehog/Internal.hs | 39 +++++- {tests => src}/Test/Tasty/Hedgehog/Extra.hs | 0 tests/Tests/Protocols/Df/Simple.hs | 137 +++++++++++++++++-- tests/Util.hs | 5 +- tests/tests.hs | 3 + 11 files changed, 359 insertions(+), 32 deletions(-) create mode 100644 src/Protocols/Df.hs-boot create mode 100644 src/Protocols/Df/Simple.hs-boot rename {tests => src}/Test/Tasty/Hedgehog/Extra.hs (100%) diff --git a/clash-protocols.cabal b/clash-protocols.cabal index 04a00bbf..7cd882af 100644 --- a/clash-protocols.cabal +++ b/clash-protocols.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: clash-protocols -synopsis: a battery-included library for performant dataflow protocols +synopsis: a battery-included library for (dataflow) protocols Homepage: https://gitlab.com/martijnbastiaan/clash-protocols version: 0.1 category: Hardware @@ -11,7 +11,7 @@ maintainer: Martijn Bastiaan description: Suggested reading order: . - * 'Protocols' + * 'Protocols' + README.md * 'Protocols.Df.Simple' * 'Protocols.DfLike' * 'Protocols.Plugin' @@ -121,6 +121,10 @@ library , ghc >= 8.6 , pretty-show + -- To be removed; we need 'Test.Tasty.Hedgehog.Extra' to fix upstream issues + , tasty >= 1.2 && < 1.3 + , tasty-hedgehog + exposed-modules: Protocols Protocols.Df @@ -130,12 +134,16 @@ library Protocols.Hedgehog.Internal Protocols.Plugin + -- 'testProperty' is broken upstream, it reports wrong test names + -- TODO: test / upstream ^ + Test.Tasty.Hedgehog.Extra + other-modules: Data.Bifunctor.Extra default-language: Haskell2010 -test-suite test-library +test-suite unittests import: common-options hs-source-dirs: tests type: exitcode-stdio-1.0 @@ -147,8 +155,6 @@ test-suite test-library Tests.Protocols.Df.Simple Tests.Protocols.Plugin - Test.Tasty.Hedgehog.Extra - Util build-depends: clash-protocols, diff --git a/src/Protocols.hs b/src/Protocols.hs index ebad79c7..466c12c4 100644 --- a/src/Protocols.hs +++ b/src/Protocols.hs @@ -26,9 +26,14 @@ module Protocols , (|>), (<|) , fromSignals, toSignals - -- * Basic protocols + -- * Protocol types + , Df + , Dfs + + -- * Basic circuits , idC , repeatC + , prod2C -- * Simulation , Simulate(SimulateType, SimulateChannels, driveC, sampleC, stallC) @@ -54,6 +59,9 @@ import Data.Kind (Type) import Data.Tuple (swap) import GHC.Generics (Generic) +import {-# SOURCE #-} Protocols.Df (Df) +import {-# SOURCE #-} Protocols.Df.Simple (Dfs) + -- | A /protocol/, in its most general form, corresponds to a component with two -- pairs of an input and output. As a diagram: -- @@ -323,7 +331,7 @@ fromSignals = coerce idC :: forall a. Circuit a a idC = Circuit swap --- | Copy a protocol /n/ times. Note that this will copy hardware. If you are +-- | Copy a circuit /n/ times. Note that this will copy hardware. If you are -- looking for a circuit that turns a single channel into multiple, check out -- 'Protocols.Df.fanout' or 'Protocols.Df.Simple.fanout'. repeatC :: @@ -333,6 +341,22 @@ repeatC :: repeatC (Circuit f) = Circuit (C.unzip . C.map f . uncurry C.zip) +-- | Combine two separate circuits into one. If you are looking to combine +-- multiple streams into a single stream, checkout 'Protocols.Df.fanin' or +-- 'Protocols.Df.zip'. +prod2C :: + forall a c b d. + Circuit a b -> + Circuit c d -> + Circuit (a, c) (b, d) +prod2C (Circuit a) (Circuit c) = + Circuit (\((aFwd, cFwd), (bBwd, dBwd)) -> + let + (aBwd, bFwd) = a (aFwd, bBwd) + (cBwd, dFwd) = c (cFwd, dBwd) + in + ((aBwd, cBwd), (bFwd, dFwd))) + --------------------------------- SIMULATION ----------------------------------- -- | Specifies option for simulation functions. Don't use this constructor -- directly, as it may be extend with other options in the future. Use 'def' @@ -428,7 +452,7 @@ instance (Simulate a, Simulate b) => Simulate (a, b) where driveC conf (fwd1, fwd2) = let (Circuit f1, Circuit f2) = (driveC conf fwd1, driveC conf fwd2) in - Circuit (\(_, (bwd1, bwd2)) -> ((), (snd (f1 ((), bwd1)), snd (f2 ((), bwd2))))) + Circuit (\(_, ~(bwd1, bwd2)) -> ((), (snd (f1 ((), bwd1)), snd (f2 ((), bwd2))))) sampleC conf (Circuit f) = let diff --git a/src/Protocols/Df.hs b/src/Protocols/Df.hs index 7b36f0ab..4bdcccc9 100644 --- a/src/Protocols/Df.hs +++ b/src/Protocols/Df.hs @@ -518,7 +518,7 @@ stall rst stallAck stalls = Circuit $ -- the data. As long as RHS does not acknowledge the data, we keep sending -- the same data. (f1, b1, s1) = case compare 0 s of - LT -> (NoData, Ack False, pred s:ss) -- s > 0 + LT -> (NoData, Ack False, pred s:ss) -- s > 0 EQ -> (f0, b0, if coerce b0 then ss else s:ss) -- s ~ 0 GT -> error ("Unexpected negative stall: " <> show s) -- s < 0 in diff --git a/src/Protocols/Df.hs-boot b/src/Protocols/Df.hs-boot new file mode 100644 index 00000000..960d5505 --- /dev/null +++ b/src/Protocols/Df.hs-boot @@ -0,0 +1,9 @@ +{-# LANGUAGE RoleAnnotations #-} + +module Protocols.Df where + +import Data.Kind (Type) +import Clash.Prelude (Domain) + +data Df (dom :: Domain) (meta :: Type) (a :: Type) +type role Df phantom phantom phantom diff --git a/src/Protocols/Df/Simple.hs b/src/Protocols/Df/Simple.hs index 0c963c04..8519c7f4 100644 --- a/src/Protocols/Df/Simple.hs +++ b/src/Protocols/Df/Simple.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE FlexibleContexts #-} {-| Defines data structures and operators to create a Dataflow protocol that only carries data, no metadata. For documentation see: @@ -11,13 +9,18 @@ carries data, no metadata. For documentation see: {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# OPTIONS_GHC -fpedantic-bottoms -feager-blackholing #-} module Protocols.Df.Simple where -import Prelude hiding ((!!), map) +import Clash.Signal.Internal (Signal(..)) + +import Prelude hiding ((!!), map, zip, zipWith) import Control.Applicative (Alternative((<|>)), Applicative(liftA2)) -import qualified Data.Bifunctor.Extra as Bifunctor +import qualified Data.Bifunctor as B +import qualified Data.Bifunctor.Extra as B import Data.Bool (bool) import Data.Coerce (coerce) import Data.Default (Default) @@ -27,7 +30,8 @@ import qualified Data.List.NonEmpty import Data.Maybe (fromMaybe) import qualified Prelude as P -import Clash.Prelude (Domain, Signal, type (<=), type (-), (!!)) +import Clash.Prelude + (Domain, type (<=), type (-), type (+), (!!)) import qualified Clash.Prelude as C import qualified Clash.Explicit.Prelude as CE @@ -125,26 +129,31 @@ instance DfLike dom (Dfs dom a) where fromDf = let go = \case {Df.Data () a -> Data a; Df.NoData -> NoData} in - Df.mapInternal (Bifunctor.swapMap go coerce) + Df.mapInternal (B.swapMap go coerce) toDf = let go = \case {Data a -> Df.Data () a; NoData -> Df.NoData} in - Df.mapInternal (Bifunctor.swapMap go coerce) + Df.mapInternal (B.swapMap go coerce) -- | Interpret simple dataflow carrying a tuple as 'Df' with /meta/ and /payload/ asDf :: Circuit (Dfs dom (meta, payload)) (Df dom meta payload) -asDf = Df.mapInternal (Bifunctor.swapMap go coerce) +asDf = Df.mapInternal (B.swapMap go coerce) where go (Data (meta, a)) = Df.Data meta a go NoData = Df.NoData -- | Interpret 'Df' as simple dataflow carrying a tuple of /meta/ and /payload/ asDfs :: Circuit (Df dom meta payload) (Dfs dom (meta, payload)) -asDfs = Df.mapInternal (Bifunctor.swapMap go coerce) +asDfs = Df.mapInternal (B.swapMap go coerce) where go (Df.Data meta a) = Data (meta, a) go Df.NoData = NoData +-- | Force a /nack/ on the backward channel and /no data/ on the forward +-- channel if reset is asserted. +forceAckLow :: C.HiddenClockResetEnable dom => Circuit (Dfs dom a) (Dfs dom a) +forceAckLow = DfLike.forceAckLow + -- | Like 'P.map', but over payload (/a/) of a Dfs stream. map :: (a -> b) -> Circuit (Dfs dom a) (Dfs dom b) map = DfLike.map @@ -189,10 +198,118 @@ mapLeft = DfLike.mapLeft mapRight :: (b -> c) -> Circuit (Dfs dom (Either a b)) (Dfs dom (Either a c)) mapRight = DfLike.mapRight --- | Like 'Data.Either.either', but over payload of a 'Dfs' stream. +-- | Like 'Data.Either.either', but over a 'Dfs' stream. either :: (a -> c) -> (b -> c) -> Circuit (Dfs dom (Either a b)) (Dfs dom c) either f g = DfLike.map (P.either f g) +-- | Like 'P.zipWith', but over two 'Dfs' streams. +zipWith :: + forall a b c dom. + (a -> b -> c) -> + Circuit + (Dfs dom a, Dfs dom b) + (Dfs dom c) +zipWith f = + Circuit (B.first C.unbundle . C.unbundle . fmap go . C.bundle . B.first C.bundle) + where + go ((Data a, Data b), Ack ack) = ((Ack ack, Ack ack), Data (f a b)) + go _ = ((Ack False, Ack False), NoData) + +-- | Like 'P.zip', but over two 'Dfs' streams. +zip :: forall a b dom. Circuit (Dfs dom a, Dfs dom b) (Dfs dom (a, b)) +zip = zipWith (,) + +-- | Like 'P.partition', but over 'Dfs' streams +partition :: (a -> Bool) -> Circuit (Dfs dom a) (Dfs dom a, Dfs dom a) +partition f = + Circuit (B.second C.unbundle . C.unbundle . fmap go . C.bundle . B.second C.bundle) + where + go (Data a, (ackT, ackF)) + | f a = (ackT, (Data a, NoData)) + | otherwise = (ackF, (NoData, Data a)) + go _ = (Ack False, (NoData, NoData)) + +-- | Route a 'Dfs' stream to another corresponding to the index +route :: + forall n a dom. C.KnownNat n => + Circuit (Dfs dom (C.Index n, a)) (C.Vec n (Dfs dom a)) +route = + Circuit (B.second C.unbundle . C.unbundle . fmap go . C.bundle . B.second C.bundle) + where + go :: (Data (C.Index n, a), C.Vec n (Ack a)) -> (Ack (C.Index n, a), C.Vec n (Data a)) + go (Data (i, a), acks) = (coerce (acks C.!! i), C.replace i (Data a) (C.repeat NoData)) + go _ = (Ack False, C.repeat NoData) + +-- | Select data from the channel indicated by the 'Dfs' stream carrying +-- @Index n@. +select :: + forall n a dom. + C.KnownNat n => + Circuit (C.Vec n (Dfs dom a), Dfs dom (C.Index n)) (Dfs dom a) +select = selectUntil (P.const True) + +-- | Select /selectN/ samples from channel /n/. +selectN :: + forall n selectN a dom. + ( C.HiddenClockResetEnable dom + , C.KnownNat selectN + , C.KnownNat n + ) => + Circuit + (C.Vec n (Dfs dom a), Dfs dom (C.Index n, C.Index selectN)) + (Dfs dom a) +selectN = Circuit $ + B.first (B.first C.unbundle . C.unbundle) + . C.mealyB go (0 :: C.Index (selectN + 1)) + . B.first (C.bundle . B.first C.bundle) + where + go c0 ((dats, dat), Ack iAck) + -- Select zero samples: don't send any data to RHS, acknowledge index stream + -- but no data stream. + | Data (_, 0) <- dat + = (c0, ((nacks, Ack True), NoData)) + + -- Acknowledge data if RHS acknowledges ours. Acknowledge index stream if + -- we're done. + | Data (streamI, nSelect) <- dat + , Data d <- dats C.!! streamI + = let + c1 = if iAck then succ c0 else c0 + oAckIndex = c1 == C.extend nSelect + c2 = if oAckIndex then 0 else c1 + datAcks = C.replace streamI (Ack iAck) nacks + in + (c2, ((datAcks, Ack oAckIndex), Data d)) + + -- No index from LHS, nothing to do + | otherwise + = (c0, ((nacks, Ack False), NoData)) + where + nacks = C.repeat (Ack False) + +-- | Selects samples from channel /n/ until the predicate holds. The cycle in +-- which the predicate turns true is included. +selectUntil :: + forall n a dom. + C.KnownNat n => + (a -> Bool) -> + Circuit + (C.Vec n (Dfs dom a), Dfs dom (C.Index n)) + (Dfs dom a) +selectUntil f = Circuit $ + B.first (B.first C.unbundle . C.unbundle) . C.unbundle + . fmap go + . C.bundle . B.first (C.bundle . B.first C.bundle) + where + nacks = C.repeat (Ack False) + + go ((dats, dat), ack) + | Data i <- dat + , Data d <- dats C.!! i + = ((C.replace i ack nacks, if f d then coerce ack else Ack False), Data d) + | otherwise + = ((nacks, Ack False), NoData) + -- | Mealy machine acting on raw Dfs stream mealy :: ( C.HiddenClockResetEnable dom @@ -226,14 +343,14 @@ fanout = DfLike.fanout -- | Merge data of multiple 'Dfs' streams using Monoid's '<>'. fanin :: forall n dom a . - (C.KnownNat n, C.HiddenClockResetEnable dom, Monoid a, 1 <= n) => + (C.KnownNat n, Monoid a, 1 <= n) => Circuit (C.Vec n (Dfs dom a)) (Dfs dom a) fanin = bundleVec |> map (C.fold @_ @(n-1) (<>)) -- | Bundle a vector of 'Dfs' streams into one. bundleVec :: forall n dom a . - (C.KnownNat n, C.HiddenClockResetEnable dom, 1 <= n) => + (C.KnownNat n, 1 <= n) => Circuit (C.Vec n (Dfs dom a)) (Dfs dom (C.Vec n a)) bundleVec = Circuit (T.first C.unbundle . C.unbundle . fmap go . C.bundle . T.first C.bundle) diff --git a/src/Protocols/Df/Simple.hs-boot b/src/Protocols/Df/Simple.hs-boot new file mode 100644 index 00000000..dd21de31 --- /dev/null +++ b/src/Protocols/Df/Simple.hs-boot @@ -0,0 +1,9 @@ +{-# LANGUAGE RoleAnnotations #-} + +module Protocols.Df.Simple where + +import Data.Kind (Type) +import Clash.Prelude (Domain) + +data Dfs (dom :: Domain) (a :: Type) +type role Dfs phantom phantom diff --git a/src/Protocols/Hedgehog/Internal.hs b/src/Protocols/Hedgehog/Internal.hs index af41f46e..404ccd64 100644 --- a/src/Protocols/Hedgehog/Internal.hs +++ b/src/Protocols/Hedgehog/Internal.hs @@ -23,7 +23,7 @@ import Protocols.Df.Simple (Dfs) -- clash-prelude import qualified Clash.Prelude as C -import Clash.Prelude (type (<=), type (*)) +import Clash.Prelude (type (<=), type (*), type (+)) -- deepseq import Control.DeepSeq @@ -212,6 +212,43 @@ instance (C.zip (C.unconcatI nExpecteds) sampled) (uncurry (expectN (Proxy @a) opts)) +instance + ( Test a, Test b + , 1 <= (SimulateChannels a + SimulateChannels b) ) => Test (a, b) where + type ExpectType (a, b) = (ExpectType a, ExpectType b) + + expectToSimulateType :: + Proxy (a, b) -> + (ExpectType a, ExpectType b) -> + (SimulateType a, SimulateType b) + expectToSimulateType Proxy (t1, t2) = + ( expectToSimulateType (Proxy @a) t1 + , expectToSimulateType (Proxy @b) t2 ) + + expectToLengths :: + Proxy (a, b) -> + (ExpectType a, ExpectType b) -> + C.Vec (SimulateChannels a + SimulateChannels b) Int + expectToLengths Proxy (t1, t2) = + expectToLengths (Proxy @a) t1 C.++ expectToLengths (Proxy @b) t2 + + expectN :: + forall m. + (HasCallStack, H.MonadTest m) => + Proxy (a, b) -> + ExpectOptions -> + C.Vec (SimulateChannels a + SimulateChannels b) Int -> + (SimulateType a, SimulateType b) -> + m (ExpectType a, ExpectType b) + expectN Proxy opts nExpecteds (sampledA, sampledB) = do + -- TODO: This creates some pretty terrible error messages, as one + -- TODO: simulate channel is checked at a time. + trimmedA <- expectN (Proxy @a) opts nExpectedsA sampledA + trimmedB <- expectN (Proxy @b) opts nExpectedsB sampledB + pure (trimmedA, trimmedB) + where + (nExpectedsA, nExpectedsB) = C.splitAtI nExpecteds + -- | Fails with an error that shows the difference between two values. failDiffWith :: (H.MonadTest m, Show a, Show b, HasCallStack) => diff --git a/tests/Test/Tasty/Hedgehog/Extra.hs b/src/Test/Tasty/Hedgehog/Extra.hs similarity index 100% rename from tests/Test/Tasty/Hedgehog/Extra.hs rename to src/Test/Tasty/Hedgehog/Extra.hs diff --git a/tests/Tests/Protocols/Df/Simple.hs b/tests/Tests/Protocols/Df/Simple.hs index db48a70b..878913eb 100644 --- a/tests/Tests/Protocols/Df/Simple.hs +++ b/tests/Tests/Protocols/Df/Simple.hs @@ -1,5 +1,6 @@ {-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE MonomorphismRestriction #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} -- Hashable (Index n) module Tests.Protocols.Df.Simple where @@ -7,6 +8,7 @@ module Tests.Protocols.Df.Simple where import Data.Coerce (coerce) import Data.Foldable (fold) import Data.Maybe (catMaybes) +import Data.List (mapAccumL) import GHC.Stack (HasCallStack) import Prelude @@ -14,12 +16,18 @@ import Prelude import qualified Clash.Prelude as C import Clash.Prelude (type (<=)) +-- containers +import qualified Data.HashMap.Strict as HashMap + -- extra -import Data.List (transpose) +import Data.List (transpose, partition) -- deepseq import Control.DeepSeq (NFData) +-- hashable +import Data.Hashable (Hashable) + -- hedgehog import Hedgehog import qualified Hedgehog.Gen as Gen @@ -49,6 +57,8 @@ instance Semigroup PlusInt where instance Monoid PlusInt where mempty = PlusInt 0 +instance Hashable (C.Index n) + genMaybe :: Gen a -> Gen (Maybe a) genMaybe genA = Gen.choice [Gen.constant Nothing, Just <$> genA] @@ -220,27 +230,136 @@ prop_unbundleVec = prop_bundleVec :: Property prop_bundleVec = - idWithModelSingleDomain - @C.System + idWithModel defExpectOptions (C.repeat <$> genData genSmallPlusInt) - (C.exposeClockResetEnable (map vecFromList . transpose . C.toList)) - (C.exposeClockResetEnable (Dfs.bundleVec @3 @C.System @PlusInt)) + (map vecFromList . transpose . C.toList) + (Dfs.bundleVec @3 @C.System @PlusInt) prop_fanin :: Property prop_fanin = + idWithModel + defExpectOptions + (genVecData genSmallPlusInt) + (map fold . transpose . C.toList) + (Dfs.fanin @3 @C.System @PlusInt) + +prop_zipWith :: Property +prop_zipWith = + idWithModel + defExpectOptions + ( do + as <- genData genSmallInt + bs <- genData genSmallInt + let n = min (length as) (length bs) + pure (take n as, take n bs) ) + (uncurry (zipWith (+))) + (Dfs.zipWith @Int @Int @_ @C.System (+)) + +prop_zip :: Property +prop_zip = + idWithModel + defExpectOptions + ( do + as <- genData genSmallInt + bs <- genData genSmallInt + let n = min (length as) (length bs) + pure (take n as, take n bs) ) + (uncurry zip) + (Dfs.zip @Int @Int @C.System) + +prop_partition :: Property +prop_partition = + idWithModel + defExpectOptions + (genData genSmallInt) + (partition (>5)) + (Dfs.partition @Int @C.System (>5)) + +prop_route :: Property +prop_route = + idWithModel + defExpectOptions + (zip <$> genData Gen.enumBounded <*> genData genSmallInt) + (\inp -> C.map (\i -> map snd (filter ((==i) . fst) inp)) C.indicesI) + (Dfs.route @3 @Int @C.System) + +prop_select :: Property +prop_select = + idWithModel + defExpectOptions + goGen + (snd . uncurry (mapAccumL goModel)) + (Dfs.select @3 @Int @C.System) + where + goModel :: C.Vec 3 [Int] -> C.Index 3 -> (C.Vec 3 [Int], Int) + goModel vec ix = let (i:is) = vec C.!! ix in (C.replace ix is vec, i) + + goGen :: Gen (C.Vec 3 [Int], [C.Index 3]) + goGen = do + n <- genSmallInt + ixs <- Gen.list (Range.singleton n) Gen.enumBounded + let tall i = HashMap.findWithDefault 0 i (tally ixs) + dats <- mapM (\i -> Gen.list (Range.singleton (tall i)) genSmallInt) C.indicesI + pure (dats, ixs) + +prop_selectN :: Property +prop_selectN = idWithModelSingleDomain @C.System defExpectOptions - (genVecData genSmallPlusInt) - (C.exposeClockResetEnable (map fold . transpose . C.toList)) - (C.exposeClockResetEnable (Dfs.fanin @3 @C.System @PlusInt)) + goGen + (\_ _ _ -> concat . snd . uncurry (mapAccumL goModel)) + (C.exposeClockResetEnable (Dfs.selectN @3 @10 @Int @C.System)) + where + goModel :: C.Vec 3 [Int] -> (C.Index 3, C.Index 10) -> (C.Vec 3 [Int], [Int]) + goModel vec (ix, len) = + let (as, bs) = splitAt (fromIntegral len) (vec C.!! ix) in + (C.replace ix bs vec, as) + + goGen :: Gen (C.Vec 3 [Int], [(C.Index 3, C.Index 10)]) + goGen = do + n <- genSmallInt + ixs <- Gen.list (Range.singleton n) Gen.enumBounded + lenghts <- Gen.list (Range.singleton n) Gen.enumBounded + let + tallied = tallyOn fst (fromIntegral . snd) (zip ixs lenghts) + tall i = HashMap.findWithDefault 0 i tallied + dats <- mapM (\i -> Gen.list (Range.singleton (tall i)) genSmallInt) C.indicesI + pure (dats, zip ixs lenghts) + +prop_selectUntil :: Property +prop_selectUntil = + idWithModel + defExpectOptions + goGen + (concat . snd . uncurry (mapAccumL goModel)) + (Dfs.selectUntil @3 @(Int, Bool) @C.System snd) + where + goModel :: C.Vec 3 [(Int, Bool)] -> C.Index 3 -> (C.Vec 3 [(Int, Bool)], [(Int, Bool)]) + goModel vec ix = + let (as, (b:bs)) = break snd (vec C.!! ix) in + (C.replace ix bs vec, as <> [b]) + + goGen :: Gen (C.Vec 3 [(Int, Bool)], [C.Index 3]) + goGen = do + n <- genSmallInt + ixs <- Gen.list (Range.singleton n) Gen.enumBounded + dats <- mapM (\i -> goChannelInput (HashMap.lookup i (tally ixs))) C.indicesI + pure (dats, ixs) + + goChannelInput :: Maybe Int -> Gen [(Int, Bool)] + goChannelInput Nothing = pure [] + goChannelInput (Just n) = do + inputs0 <- Gen.list (Range.singleton n) (Gen.list (Range.linear 1 10) genSmallInt) + let tagEnd xs = zip (init xs) (repeat False) <> [(last xs, True)] + pure (concatMap tagEnd inputs0) tests :: TestTree tests = -- TODO: Move timeout option to hedgehog for better error messages. -- TODO: Does not seem to work for combinatorial loops like @let x = x in x@?? - localOption (mkTimeout 120_000_000 {- 120 seconds -}) + localOption (mkTimeout 12_000_000 {- 12 seconds -}) $ localOption (HedgehogTestLimit (Just 1000)) $(testGroupGenerator) diff --git a/tests/Util.hs b/tests/Util.hs index 537ea82f..42ab44c4 100644 --- a/tests/Util.hs +++ b/tests/Util.hs @@ -32,4 +32,7 @@ genVec gen = sequence (C.repeat gen) -- | Count the number of times an element occurs in a list tally :: (Hashable a, Eq a) => [a] -> HashMap a Int -tally xs = HashMap.fromListWith (+) (zip xs (repeat 1)) +tally = tallyOn id (const 1) + +tallyOn :: (Hashable b, Eq b) => (a -> b) -> (a -> Int) -> [a] -> HashMap b Int +tallyOn f g xs = HashMap.fromListWith (+) (zip (map f xs) (map g xs)) diff --git a/tests/tests.hs b/tests/tests.hs index 4b90ce0d..4aad420c 100644 --- a/tests/tests.hs +++ b/tests/tests.hs @@ -1,3 +1,6 @@ + +module Main where + import Prelude import Test.Tasty import Control.Concurrent (setNumCapabilities) From 82c4670676fe5a11aeca63590618d9b396fb58e1 Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Mon, 14 Dec 2020 17:25:10 +0100 Subject: [PATCH 2/2] Fill README.md --- .ci/build_docs.sh | 6 + .ci/test_cabal.sh | 2 +- .ci/test_stack.sh | 1 + README.md | 587 ++++++++++++++++++++++++++++- cabal.project | 6 + clash-protocols.cabal | 14 +- hie.yaml | 2 +- src/Protocols.hs | 514 +------------------------ src/Protocols/Df.hs | 19 +- src/Protocols/Df.hs-boot | 9 - src/Protocols/Df/Lazy.hs | 3 - src/Protocols/Df/Simple.hs | 22 +- src/Protocols/Df/Simple.hs-boot | 9 - src/Protocols/Df/Simple/Lazy.hs | 3 - src/Protocols/DfLike.hs | 4 +- src/Protocols/Hedgehog/Internal.hs | 4 +- src/Protocols/Internal.hs | 516 +++++++++++++++++++++++++ src/Test/Tasty/Hedgehog/Extra.hs | 6 + stack.yaml | 7 +- tests/Tests/Protocols/Df.hs | 1 - tests/Tests/Protocols/Df/Simple.hs | 7 +- 21 files changed, 1167 insertions(+), 575 deletions(-) delete mode 100644 src/Protocols/Df.hs-boot delete mode 100644 src/Protocols/Df/Lazy.hs delete mode 100644 src/Protocols/Df/Simple.hs-boot delete mode 100644 src/Protocols/Df/Simple/Lazy.hs create mode 100644 src/Protocols/Internal.hs diff --git a/.ci/build_docs.sh b/.ci/build_docs.sh index 46ffc9eb..81fa37a4 100755 --- a/.ci/build_docs.sh +++ b/.ci/build_docs.sh @@ -1,6 +1,12 @@ #!/bin/bash set -xeou pipefail +# Build dependencies first, so they don't end up in logs +cabal build \ + --enable-documentation \ + --allow-newer=circuit-notation:ghc \ + clash-protocols + # circuit-notation currently _compiles on 8.10, but isn't usable. The only # other GHC version it supports is 8.6.5, but this GHC bundles a Haddock that # cannot generate documentation for clash-prelude. Hence, we build docs with diff --git a/.ci/test_cabal.sh b/.ci/test_cabal.sh index 3823685f..3b9c1304 100755 --- a/.ci/test_cabal.sh +++ b/.ci/test_cabal.sh @@ -2,5 +2,5 @@ set -xeou pipefail cabal build all -fci -cabal run test-library -fci --enable-tests +cabal run unittests -fci --enable-tests cabal sdist diff --git a/.ci/test_stack.sh b/.ci/test_stack.sh index 11953403..526dc706 100755 --- a/.ci/test_stack.sh +++ b/.ci/test_stack.sh @@ -1,5 +1,6 @@ #!/bin/bash set -xeou pipefail +stack --version stack build stack test diff --git a/README.md b/README.md index ff17993f..17fe9a18 100644 --- a/README.md +++ b/README.md @@ -1,22 +1,597 @@ + # Clash Protocols +A battery-included library for writing on-chip protocols, such as AMBA AXI and Altera Avalon. -## TODO + +# Table of Contents +- [Introduction](#introduction) +- [Using `Dfs`/`Df` `Circuit`s](#using-dfsdf-circuits) + - [Invariants](#invariants) + - [Note [Deasserting resets]](#note-deasserting-resets) + - [Tutorial: `catMaybes`](#tutorial-catmaybes) + - [Implementation](#implementation) + - [Testing](#testing) + - [Debugging](#debugging) + - [Connecting multiple circuits](#connecting-multiple-circuits) +- [License](#license) +- [Project goals](#project-goals) +- [Contributing](#contributing) +- [TODO](#todo) + +# Introduction +`clash-protocols` exists to make it easy to develop and use on-chip communication protocols, with a focus on protocols in need of bidirectional communication, such as _AMBA AXI_. To familiarize yourself with `clash-protocols`, read [hackage.haskell.org/package/clash-protocols](http://hackage.haskell.org/package/clash-protocols). To read the next section, read at least: + +* `Protocols` +* `Protocols.Df.Simple` + +The next section will guide you through the creation of a single `Dfs` based circuit. + +# Using `Dfs`/`Df` `Circuit`s +The basic handshaking of `Dfs` and `Df` are heavily inspired by _AMBA AXI_: + + * `Df` circuits _send_ data to their right hand side + * `Df` circuits _receive_ data from their left hand side. + * `Df` circuits _send_ acknowledgments to their left hand side + * `Df` circuits _receive_ acknowledgments from their right hand side + +## Invariants + +The protocols `Df` and `Dfs` impose a contract each component should follow. These are, where possible, checked by the various test harnesses in `Protocols.Hedgehog`. + +* _Fwd a_ cannot depend on the _Bwd a_. In other words, deciding whether or not to send data cannot depend on the acknowledgment of that same data. + +* A component may not assert an acknowledgment while its reset is asserted. Doing so can lead to data loss. For example, imagine two circuits _A_ and _B_ both driven by different resets and connected as follows: + + ``` + Reset domain A Reset domain B + + +----------------------+ +----------------------+ + | | | | + | | | | + | +-----------+ | | +------------+ | + | | | | Fwd a | | | | + | +->+ +----------------------------->+ +--> | + | | | | | | | | + | | | | | | | | + | | | | | | | | + | | | | | | | | + | | | | Bwd a | | | | + | <--+ +<-----------------------------+ +<-+ | + | | | | | | | | + | +-----------+ | | +------------+ | + | | | | + | | | | + +----------------------+ +----------------------+ + ``` + + If: + * Circuit _A_ drives data; and + * Circuit _B_'s reset is asserted; and + * Circuit _B_ sends an acknowledgment + + ..circuit _A_ will consider its data send and will not try again on the next cycle. However, _B_'s reset is asserted so it will most likely not process anything. Test harnesses test this by driving a circuit under test before deasserting its reset. + + This invariant allows developers to insert arbitrary reset delays without worrying their design breaks. Caution should still be taken though, see [Note [Deasserting resets]](#note-deasserting-resets). + +* When _Fwd a_ does not contain data (i.e., is `NoData`), its corresponding _Bwd a_ may contain any value, including an error/bottom. When driving a bottom, a component should use `errorX` to make sure it can be evaluated using `seqX`. Test harnesses in `Protocols.Hedgehog` occasionally drive `errorX "No defined Ack"` when seeing `NoData` to test this. + +* A circuit driving `Data x` must keep driving the same value until it receives an acknowledgment. This is not yet checked by test harnesses. + +### Note [Deasserting resets] +Care should be taken when deasserting resets. Given the following circuit: + +``` + withReset rstA a + |> withReset rstB b + |> withReset rstC c +``` + +or schematically: + +``` +a > b > c +``` + +Component `a`'s reset should be deasserted first, then `b`'s, then `c`s. More generally, a [topological sort](https://en.wikipedia.org/wiki/Topological_sorting) determines the order in which to deassert resets. For example: + +``` +a > b > c > d + ^ v + f < e +``` + +should be deasserted as follows: `a`, `b,` `c`, `d`/`e`, `f`. Resets might also be deasserted simultaneously. For example, `a`'s and `b`'s reset might be deasserted at the same cycle. + +This order is imposed by the fact that there is an invariant stating a component in reset must not acknowledge data while in reset, but there is - for performance reasons - no invariant stating a component must not send data while in reset. + +## Tutorial: `catMaybes` +At this point you should have familiarized with the basic structures of the `Dfs`: its dataconstructors (`Data`, `NoData`, and `Ack`) and its invariants, as well as the structure of a `Circuit` itself. To quickly try things it's useful to keep a repl around. With `stack`: + +``` +stack exec --package clash-protocols ghci +``` + +with `cabal`, clone this project and run: + +``` +cabal update +cabal repl clash-protocols +``` + +Both should give you the same shell. Import the necessary modules: + +```bash +>>> import qualified Clash.Prelude as C +>>> import qualified Protocols.Df.Simple as Dfs +``` + +You should now be able to query various things. For example: + +```bash +>>> :t toSignals +toSignals :: Circuit a b -> (Fwd a, Bwd b) -> (Bwd a, Fwd b) +``` + +### Implementation +Similar to the console we start by importing all the necessary modules: + +```haskell +module CatMaybes where + +import Protocols +import qualified Clash.Prelude as C +import qualified Protocols.Df.Simple as Dfs +``` + +Then, we define the type and name of the component we'd like to write: + +```haskell +catMaybes :: Circuit (Dfs dom (Maybe a)) (Dfs dom a) +``` + +I.e., a circuit that takes a `Dfs` stream of `Maybe a` on the left hand side (LHS) and produces a stream of `a` on the right hand side (RHS). Note that the data carried on `Dfs`s _forward_ path very much looks like a `Maybe` in the first place: + +``` +>>> :kind! Fwd (Dfs C.System Int) +.. += Signal "System" (Dfs.Data Int) +``` + +..because `Data Int` itself has two constructors: `Data Int` and `NoData`. In effect, we'd like squash `Data (Just a)` into `Data a`, and `Data Nothing` into `NoData`. Not unlike the way [join](https://hackage.haskell.org/package/base-4.14.0.0/docs/Control-Monad.html#v:join) would work on two `Maybe`s. + +As the types of `Circuit`s become quite verbose and complex quickly, I like to let GHC do the heavy lifting. For example, I would write: + +```haskell +catMaybes = Circuit go +``` + +At this point, GHC will tell us: + +```haskell +CatMaybes.hs:8:21: error: + Variable not in scope: + go + :: (C.Signal dom (Dfs.Data (Maybe a)), C.Signal dom (Dfs.Ack a)) + -> (C.Signal dom (Dfs.Ack (Maybe a)), C.Signal dom (Dfs.Data a)) + | +8 | catMaybes = Circuit go + | ^^ +``` + +This is something we can work with. We need to accept: + +* A _data_ signal coming from the LHS +* An _acknowledgment_ signal coming from the RHS + +and we need to return: + +* An _acknowledgment_ signal coming to the LHS +* A _data_ signal going to the RHS + +We can't really work on multiple signals at the same time, so we need to bundle them. Similarly, we unbundle the output of our function: + +``` +catMaybes = Circuit (C.unbundle . go . C.bundle) +``` + +Now GHC will tell us: + +```haskell +CatMaybes.hs:8:35: error: + Variable not in scope: + go + :: C.Signal dom (Dfs.Data (Maybe a), Dfs.Ack a) + -> C.Signal dom (Dfs.Ack (Maybe a), Dfs.Data a) + | +8 | catMaybes = Circuit (C.unbundle . go . C.bundle) + | ^^ +``` + +Finally, we don't need any state for this function, so we might as well make our lives a little bit easier by using `fmap` to "get rid of" the `Signal`s: + +```haskell +catMaybes = Circuit (C.unbundle . fmap go . C.bundle) +``` + +after which GHC will tell us: + +``` +CatMaybes.hs:8:40: error: + Variable not in scope: + go + :: (Dfs.Data (Maybe a), Dfs.Ack a) + -> (Dfs.Ack (Maybe a), Dfs.Data a) + | +8 | catMaybes = Circuit (C.unbundle . fmap go . C.bundle) + | ^^ +``` + + +This is something we can write, surely! If the LHS does not send data, there's not much we can do. We send `NoData` to the RHS and send a /nack/: + +```haskell + go (Dfs.NoData, _) = (Dfs.Ack False, Dfs.NoData) +``` + +If we _do_ receive data from the LHS but it turns out to be _Nothing_, we'd like to acknowledge that we received the data and send `NoData` to the RHS: + +```haskell +go (Dfs.Data Nothing, _) = (Dfs.Ack True, Dfs.NoData) +``` + +Finally, if the LHS sends data and it turns out to be a _Just_, we'd like to acknowledge that we received it and pass it onto the RHS. But we should be careful, we should only acknowledge it if our RHS received our data! In effect, we can just passthrough the ack: + +```haskell +go (Dfs.Data (Just d), Dfs.Ack ack) = (Dfs.Ack ack, Dfs.Data d) +``` + +### Testing +We'll use `Hedgehog` for testing our circuit. Conveniently, `Protocols.Hedgehog` defines some pretty handy helpers! Let's import everything: + +```haskell +import qualified Protocols.Hedgehog as H +import qualified Hedgehog as H +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range +``` + +Before we get to testing our circuit, we first need a Hedgehog generator that can generate input data for our circuit. Let's define it: + +```haskell +genCatMaybesInput :: H.Gen [Maybe Int] +genCatMaybesInput = + Gen.list (Range.linear 0 100) (genMaybe (genInt 10 20)) + where + genMaybe genA = Gen.choice [Gen.constant Nothing, Just <$> genA] + genInt a b = Gen.integral (Range.linear a b) +``` + +The explanation for the definition is out of scope for this tutorial, but it basically says: this generator generates a list with 0 to 100 elements, each a `Just` or a `Nothing`. If it is a `Just` it will contain an `Int` between 10 and 20. If you'd like to learn more about Hedgehog head over to [hackage.haskell.org/package/hedgehog](http://hackage.haskell.org/package/hedgehog). + +For `Dfs` circuits we can define a pretty strong property: a `Circuit (Dfs dom a) (Dfs dom a)` is functionally the same as a function `[a] -> [a]` if we strip all the backpressure and `Signal` abstractions. Similarly, we for our `Circuit (Dfs dom (Maybe a)) (Dfs dom a)` our _pure model_ would be `[Maybe a] -> [a]`, i.e. [`Data.catMaybes`](https://hackage.haskell.org/package/base-4.14.0.0/docs/Data-Maybe.html#v:catMaybes)! + +The function `Protocols.Hedgehog.idWithModel` takes advantage of exactly that fact. You tell it: + +* How to generate input data +* What function to consider the _pure model_ +* What Circuit to consider its dataflow equivalent + +In code, this looks like: + +```haskell +import qualified Data.Maybe as Maybe + +[..] + +prop_catMaybes :: H.Property +prop_catMaybes = + H.idWithModel + H.defExpectOptions + genCatMaybesInput + Maybe.catMaybes + (catMaybes @C.System) +``` + +From that point on, it will do the rest. By driving the circuit with arbitrary input and backpressure (among other things), it effectively tests whether a circuit implements the invariants of the `Dfs` protocol and whether it is (functionally) equivalent to its pure model. To actually run the tests we need some more boilerplate: + + + +```haskell +import Test.Tasty +import Test.Tasty.TH (testGroupGenerator) +import Test.Tasty.Hedgehog.Extra (testProperty) + +[..] + +main :: IO () +main = defaultMain $(testGroupGenerator) +``` + +Once that is done, we can run our tests: + +``` +*CatMaybes> main +CatMaybes + prop_catMaybes: OK (0.06s) + ✓ prop_catMaybes passed 100 tests. + +All 1 tests passed (0.06s) +``` + +Yay, all done! + +### Debugging +**HEADS UP**: [Hedgehog](https://hackage.haskell.org/package/hedgehog) expects to find source files locally in order to display pretty error messages. If you want pretty error messages in your package, please use [this _patched_ version of Hedgehog](https://github.com/martijnbastiaan/haskell-hedgehog/commits/find-source-files). When using cabal add the following to your `cabal.project`: + +``` +source-repository-package + type: git + location: https://github.com/martijnbastiaan/haskell-hedgehog.git + tag: f7d25b0a1927b7c06d69535d5dcfcade560ec624 + subdir: hedgehog +``` + +Stack users can add the following to `stack.yaml`: + +``` +extra-deps: +- git: git@github.com:martijnbastiaan/haskell-hedgehog + commit: f7d25b0a1927b7c06d69535d5dcfcade560ec624 + subdirs: + - hedgehog +``` + +We'll try and upstream these patches. + +---------------- + +Writing a `Dfs` component can be tricky business. Even for relatively simple circuits such as `catMaybes` it's easy to send a wrong acknowledgment. The test harness is supposed to catch this, but its output isn't always easy to parse. We'll go over a few common mistakes. + +Let's introduce one: + +```diff +- go (Dfs.Data Nothing, _) = (Dfs.Ack True, Dfs.NoData) ++ go (Dfs.Data Nothing, _) = (Dfs.Ack False, Dfs.NoData) +``` + +Rerunning the tests will give us a big error, which starts out as: + +``` +CatMaybes + prop_catMaybes: FAIL (0.11s) + ✗ prop_catMaybes failed at src/Protocols/Hedgehog/Internal.hs:167:7 + after 9 tests and 3 shrinks. +``` + +This notes our test has failed after _9 tests_. To produce a small example Hedgehog has tried to shrink the test to a minimal test case, reflected in its _and 3 shrinks_. The test fails at `src/Protocols/Hedgehog/Internal.hs:167:7`. Usually, you'd see your own files here, but in our case we used `idWithModel` - an externally defined property. Hedgehog will try and be helpful by printing the source code of the property interspersed with the data it generated. + +So we get: + +```haskell + ┏━━ src/Protocols/Hedgehog.hs ━━━ + 74 ┃ propWithModel :: + 75 ┃ forall a b . + 76 ┃ (Test a, Test b, HasCallStack) => + 77 ┃ -- | Options, see 'ExpectOptions' + 78 ┃ ExpectOptions -> + 79 ┃ -- | Test data generator + 80 ┃ H.Gen (ExpectType a) -> + 81 ┃ -- | Model + 82 ┃ (ExpectType a -> ExpectType b) -> + 83 ┃ -- | Implementation + 84 ┃ Circuit a b -> + 85 ┃ -- | Property to test for. Function is given the data produced by the model + 86 ┃ -- as a first argument, and the sampled data as a second argument. + 87 ┃ (ExpectType b -> ExpectType b -> H.PropertyT IO ()) -> + 88 ┃ H.Property + 89 ┃ propWithModel eOpts genData model prot prop = H.property $ do + 90 ┃ dat <- H.forAll genData + ┃ │ [ Nothing , Just 10 ] +``` + +`propWithModel` is used internally by `idWithModel`. In essence, `propWithModel` is the generalized version of `idWithModel`: it allows users to specify their own properties instead of a hardcoded equality test. Right at line 90 and the line below it, we can see something interesting happen: + +```haskell + 90 ┃ dat <- H.forAll genData + ┃ │ [ Nothing , Just 10 ] +``` + +At this point Hedgehog used our data generator to generate the input supplied to our circuit. Although it isn't perfect, Hedgehog tried to minimize the example so we can be pretty sure `Nothing` _then_ `Just 10` means something. In other words, we can be reasonably sure that this failure wouldn't have happened with just `Nothing` or just `Just 10`. (Note that this is correct: our `catMaybes` only gets stuck after having seen a `Nothing`. However, the test harness can't see the difference between a filtered `Nothing` and stuckness, hence the additional `Just 10`.) + +We move on. + +```haskell + 91 ┃ let n = maximum (expectToLengths (Proxy @a) dat) + 92 ┃ + 93 ┃ -- TODO: Different distributions? + 94 ┃ let genStall = Gen.integral (Range.linear 0 10) + 95 ┃ + 96 ┃ -- Generate stalls for LHS part of the protocol. The first line determines + 97 ┃ -- whether to stall or not. The second determines how many cycles to stall + 98 ┃ -- on each _valid_ cycle. + 99 ┃ lhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels a) genStallMode)) + ┃ │ +100 ┃ lhsStalls <- H.forAll (traverse (genStalls genStall n) lhsStallModes) + ┃ │ <(StallWithNack,[])> +101 ┃ +102 ┃ -- Generate stalls for RHS part of the protocol. The first line determines +103 ┃ -- whether to stall or not. The second determines how many cycles to stall +104 ┃ -- on each _valid_ cycle. +105 ┃ rhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels b) genStallMode)) + ┃ │ +106 ┃ rhsStalls <- H.forAll (traverse (genStalls genStall n) rhsStallModes) + ┃ │ <(StallWithNack,[])> + +``` + +Again, the unnumbered lines are the most interesting: + +``` + 99 ┃ lhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels a) genStallMode)) + ┃ │ +100 ┃ lhsStalls <- H.forAll (traverse (genStalls genStall n) lhsStallModes) + ┃ │ <(StallWithNack,[])> +``` + +This tells us that the test decided to _not_ produce any stalls on the LHS. The next line says basically the same. We'll get back to that soon. This logic is repeated for stalling the RHS too, with the same results. At this point, we can be pretty sure it has nothing to do with stalls either. + +The last interesting bit of the test report is: + +``` +Circuit did not produce enough output. Expected 1 more values. Sampled only 0: + +[] +``` + +The test tells us that no output was sampled, even though it expected to sample a single value. At this point there is no structured way to actually spot the error, but by now it should be pretty clear. + +Let's revert the "mistake" we made and make another: + +```diff +- go (Dfs.Data (Just d), Dfs.Ack ack) = (Dfs.Ack ack, Dfs.Data d) ++ go (Dfs.Data (Just d), Dfs.Ack ack) = (Dfs.Ack True, Dfs.Data d) +``` + +Again, we get a pretty big error report. Let's skip right to the interesting bits: + +```haskell + 90 ┃ dat <- H.forAll genData + ┃ │ [ Just 10 ] +``` +```haskell + 99 ┃ lhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels a) genStallMode)) + ┃ │ +100 ┃ lhsStalls <- H.forAll (traverse (genStalls genStall n) lhsStallModes) + ┃ │ <(StallWithNack,[])> +``` +```haskell +105 ┃ rhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels b) genStallMode)) + ┃ │ +106 ┃ rhsStalls <- H.forAll (traverse (genStalls genStall n) rhsStallModes) + ┃ │ <(StallWithNack,[])> +``` +``` +Circuit did not produce enough output. Expected 1 more values. Sampled only 0: + +[] +``` + +In this case, Hedgehog pretty much constrained us to pretty much one case in our implementation: the one where it matches on `Dfs.Data (Just d)`. Weirdly, no backpressure was needed to trigger this error, but we still see dropped values. This usually means we generated an _ack_ while the reset was asserted. And sure enough, we don't check for this. (Note that the "right" implementation moved the responsibility of this problem to the component on the RHS, hence not failing.) + +At this point it might be tempting to use `Dfs.forceAckLow` to force proper reset behavior. To do so, apply the patch: + +```diff +- catMaybes :: Circuit (Dfs dom (Maybe a)) (Dfs dom a) +- catMaybes = Circuit (C.unbundle . fmap go . C.bundle ++ catMaybes :: C.HiddenClockResetEnable dom => Circuit (Dfs dom (Maybe a)) (Dfs dom a) ++ catMaybes = Dfs.forceAckLow |> Circuit (C.unbundle . fmap go . C.bundle +``` + +Because our function is now stateful, we also need to change the test to: + +```haskell +prop_catMaybes :: H.Property +prop_catMaybes = + H.idWithModelSingleDomain + H.defExpectOptions + genCatMaybesInput + (\_ _ _ -> Maybe.catMaybes) + (C.exposeClockResetEnable (catMaybes @C.System)) +``` + +Of course, the actual bug is still in there so we expect the test to fail still. And sure enough: + +```haskell + 90 ┃ dat <- H.forAll genData + ┃ │ [ Just 10 ] +``` + +```haskell + 99 ┃ lhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels a) genStallMode)) + ┃ │ +100 ┃ lhsStalls <- H.forAll (traverse (genStalls genStall n) lhsStallModes) + ┃ │ <(StallWithNack,[])> +``` + +```haskell +105 ┃ rhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels b) genStallMode)) + ┃ │ +106 ┃ rhsStalls <- H.forAll (traverse (genStalls genStall n) rhsStallModes) + ┃ │ <(StallWithNack,[1])> +``` + +``` +Circuit did not produce enough output. Expected 1 more values. Sampled only 0: + +[] +``` + +This time the LHS of the circuit was not stalled, but the RHS was. Let's bisect: + +``` +105 ┃ rhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels b) genStallMode)) + ┃ │ +``` + +At 105, Hedgehog decided to stall the RHS. Note that if we had multiple input channels, we would have seen multiple items in this vector. The next line decides how to stall: + +``` +106 ┃ rhsStalls <- H.forAll (traverse (genStalls genStall n) rhsStallModes) + ┃ │ <(StallWithNack,[1])> +``` + +The first part of the tuple, `StallWithNack`, indicates what the stall circuit does when it does _not_ receive data from the circuit. While it will stall with _nacks_ in this case, it could have stalled with _acks_ or even undefineds too as the protocol doesn't restrict that. The second part of the tuple, `[1]`, determines how many cycles whenever the circuit sends data. If it would have read: + +```haskell +[4,5,6] +``` + +instead, this would have mean that the circuit would be stalled for _4_ cycles on its first valid data cycle, _5_ on the next, and _6_ on the next valid data cycle after that. Hedgehog only generated one member in our case, as it expects to sample just a single value too. + +At this point we're forced to conclude that `forceAckWithLow` did not fix our woes and we should persue a proper fix. + +## Connecting multiple circuits +**HEADS UP**: The following instructions only work on GHC 8.6.5. Due to internal GHC changes we can't easily port this to newer versions. This is in the works. + +----------------------- + +Check out [tests/Tests/Protocols/Plugin.hs](https://github.com/clash-lang/clash-protocols/blob/main/tests/Tests/Protocols/Plugin.hs) for examples on how to use `Protocols.Plugin` to wire up circuits using a convenient syntax. + + +# License +`clash-protocols` is licensed under BSD2. See [LICENSE](LICENSE). + +# Project goals + +- Include basic dataflow protocols (e.g., `Df`/`Dfs`) and industry supported ones (e.g., AMBA AXI) +- Include lots of basic operators on circuits and its protocols +- Export a consistent interface across protocols +- 100% documentation coverage, preferably with lots of examples + +This project does not aim to: + +- Provide board or vendor specific primitives + +# Contributing +No formal guidelines yet, but feel free to open a PR! + +# TODO 0.1 -- [ ] README -- [ ] Fix DSL plugin -- [ ] Add more convenient functions: `fanin`, `roundrobin`, .. +- [x] README +- [x] Add more convenient functions: `fanin`, `roundrobin`, .. - [ ] Make `Dfs` base implementation instead of `Df` (performance / cleanliness) -- [ ] Decide what to do with `Protocols.Ack` +- [x] Decide what to do with `Protocols.Ack` - [ ] Check dead doc links on CI -- [ ] Upstream all changes to `circuit-notation` (where possible) +- [x] Upstream all changes to `circuit-notation` (where possible) - [ ] Add examples on how to use DSL plugin - [ ] Port and upstream examples `circuit-notation` - [ ] Blogpost introducing explaining the _why_ of `clash-protocols` 0.2 +- [ ] Make DSL plugin work with GHC 8.10 - [ ] AXI AMBA (in terms of `DfLike`!) - [ ] Test framework for "chunked" designs - [ ] Improve errors for multichannel tests diff --git a/cabal.project b/cabal.project index 28e105e7..4a00e0b9 100644 --- a/cabal.project +++ b/cabal.project @@ -7,3 +7,9 @@ package clash-prelude -- Clash, and triggers Template Haskell bugs on Windows. Hence, we disable -- it by default. This will be the default for Clash >=1.4. flags: -large-tuples + +source-repository-package + type: git + location: https://github.com/martijnbastiaan/haskell-hedgehog.git + tag: f7d25b0a1927b7c06d69535d5dcfcade560ec624 + subdir: hedgehog diff --git a/clash-protocols.cabal b/clash-protocols.cabal index 7cd882af..038cd6ab 100644 --- a/clash-protocols.cabal +++ b/clash-protocols.cabal @@ -17,6 +17,10 @@ description: * 'Protocols.Plugin' * 'Protocols.Hedgehog' +data-files: + src/Protocols/Hedgehog.hs + src/Protocols/Hedgehog/*.hs + flag ci Description: Running on CI? Used to set fail-on-warning flag. Manual: True @@ -117,12 +121,12 @@ library , extra , data-default , deepseq - , hedgehog >= 1.0.3 + , hedgehog >= 1.0.2 , ghc >= 8.6 , pretty-show -- To be removed; we need 'Test.Tasty.Hedgehog.Extra' to fix upstream issues - , tasty >= 1.2 && < 1.3 + , tasty >= 1.2 && < 1.5 , tasty-hedgehog exposed-modules: @@ -132,14 +136,18 @@ library Protocols.Df.Simple Protocols.Hedgehog Protocols.Hedgehog.Internal + Protocols.Internal Protocols.Plugin -- 'testProperty' is broken upstream, it reports wrong test names -- TODO: test / upstream ^ Test.Tasty.Hedgehog.Extra + autogen-modules: Paths_clash_protocols + other-modules: Data.Bifunctor.Extra + Paths_clash_protocols default-language: Haskell2010 @@ -164,6 +172,6 @@ test-suite unittests extra, hashable, hedgehog, - tasty >= 1.2 && < 1.3, + tasty >= 1.2 && < 1.5, tasty-hedgehog, tasty-th diff --git a/hie.yaml b/hie.yaml index 668beb71..a2907379 100644 --- a/hie.yaml +++ b/hie.yaml @@ -3,7 +3,7 @@ cradle: - path: "./src" config: {cradle: {cabal: {component: "lib:clash-protocols"}}} - path: "./tests" - config: {cradle: {cabal: {component: "test-suite:test-library"}}} + config: {cradle: {cabal: {component: "test-suite:unittests"}}} - path: "./bin/Clash.hs" config: {cradle: {cabal: {component: "clash"}}} - path: "./bin/Clashi.hs" diff --git a/src/Protocols.hs b/src/Protocols.hs index 466c12c4..1379a412 100644 --- a/src/Protocols.hs +++ b/src/Protocols.hs @@ -9,11 +9,6 @@ i.e. using: Definitions of 'Circuit', 'Fwd', 'Bwd', 'Protocols.Dfs.Dfs', inspired by definitions in @circuit-notation@ at . -} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE TypeFamilyDependencies #-} -{-# LANGUAGE UndecidableInstances #-} module Protocols ( -- * Circuit definition @@ -45,509 +40,6 @@ module Protocols , circuit ) where -import GHC.Base (Any) -import Prelude hiding (map, const) - -import Clash.Prelude (Signal, type (+), type (*)) -import qualified Clash.Prelude as C -import qualified Clash.Explicit.Prelude as CE - -import Control.Applicative (Const(..)) -import Data.Coerce (coerce) -import Data.Default (Default(def)) -import Data.Kind (Type) -import Data.Tuple (swap) -import GHC.Generics (Generic) - -import {-# SOURCE #-} Protocols.Df (Df) -import {-# SOURCE #-} Protocols.Df.Simple (Dfs) - --- | A /protocol/, in its most general form, corresponds to a component with two --- pairs of an input and output. As a diagram: --- --- @ --- Circuit a b --- --- +-----------+ --- Fwd a | | Fwd b --- +------->+ +--------> --- | | --- | | --- Bwd a | | Bwd b --- <--------+ +<-------+ --- | | --- +-----------+ --- @ --- --- The first pair, @(Fwd a, Bwd a)@ can be thought of the data sent to and from --- the component on the left hand side of this protocol. For this pair, @Fwd a@ --- is the data sent from the protocol on the left hand side (not pictured), while --- @Bwd a@ is the data sent to the left hand side from the current protocol. --- --- Similarly, the second pair, @(Fwd b, Bwd)@, can be thought of as the data --- sent to and from the right hand side of this protocol. In this case, @Fwd b@ --- is the data sent from the current protocol to the one on the right hand side, --- while @Bwd b@ is the data received from the right hand side. --- --- In Haskell terms, we would say this is simply a function taking two inputs, --- @Fwd a@ and @Bwd b@, yielding a pair of outputs @Fwd b@ and @Bwd a@. This is --- in fact exactly its definition: --- --- @ --- newtype Circuit a b = --- Circuit ( (Fwd a, Bwd b) -> (Bwd a, Fwd b) ) --- @ --- --- Note that the type parameters /a/ and /b/ don't directly correspond to the --- types of the inputs and outputs of this function. Instead, the type families --- @Fwd@ and @Bwd@ decide this. The type parameters can be thought of as --- deciders for what /protocol/ the left hand side and right hand side must --- speak. --- --- Let's make it a bit more concrete by building such a protocol. For this --- example, we'd like to build a protocol that sends data to a protocol, while --- allowing the protocol to signal whether it processed the sent data or not. Similarly, --- we'd like the sender to be able to indicate that it doesn't have any data to --- send. These kind of protocols fall under the umbrella of "dataflow" protocols, --- so lets call it /DataFlowSimple/ or /Dfs/ for short: --- --- @ --- data Dfs (dom :: Domain) (a :: Type) --- @ --- --- We're only going to use it on the type level, so we won't need any --- constructors for this datatype. The first type parameter indicates the --- synthesis domain the protocol will use. This is the same /dom/ as used in --- /Signal dom a/. The second type indicates what data the protocol needs to --- send. Again, this is similar to the /a/ in /Signal dom a/. --- --- As said previously, we'd like the sender to either send /no data/ or --- /some data/. We can capture this in a data type very similar to /Maybe/: --- --- @ --- data Data a = NoData | Data a --- @ --- --- On the way back, we'd like to either acknowledge or not acknowledge sent --- data. Similar to /Bool/ we define: --- --- @ --- data Ack a = DfNack | Ack --- @ --- --- (For technical reasons[1] we need the type variable /a/ in this definition, --- even though we don't use it on the right hand side.) --- --- With these three definitions we're ready to make an instance for /Fwd/ and --- /Bwd/: --- --- @ --- instance Fwd (Dfs dom a) = Signal dom (Data a) --- instance Bwd (Dfs dom a) = Signal dom (Ack a) --- @ --- --- Having defined all this, we can take a look at /Circuit/ once more: now --- instantiated with our types. The following: --- --- @ --- f :: Circuit (Dfs dom a) (Dfs dom b) --- @ --- --- ..now corresponds to the following protocol: --- --- @ --- +-----------+ --- Signal dom (Data a) | | Signal dom (Data b) --- +------------------------>+ +-------------------------> --- | | --- | | --- Signal dom (Ack a) | | Signal dom (Ack b) --- <-------------------------+ +<------------------------+ --- | | --- +-----------+ --- @ --- --- There's a number of advantages over manually writing out these function --- types: --- --- 1. It reduces syntactical noise in type signatures --- --- 2. It eliminates the need for manually routing acknowledgement lines --- --- Footnotes: --- --- 1. Fwd and Bwd are injective type families. I.e., something on --- the right hand side of a type instance must uniquely identify the left --- hand side and vice versa. This helps type inference and error messages --- substantially, in exchange for a slight syntactical artifact. As a --- result, any type variables on the left hand side must occur on the right --- hand side too. --- -newtype Circuit a b = - Circuit ( (Fwd a, Bwd b) -> (Bwd a, Fwd b) ) - --- | Protocol-agnostic acknowledgement -newtype Ack = Ack Bool - deriving (Generic, C.NFDataX) - --- | Circuit protocol with /CSignal dom a/ in its forward direction, and --- /CSignal dom ()/ in its backward direction. Convenient for exposing --- protocol internals. -data CSignal dom a = CSignal (Signal dom a) - --- | A protocol describes the in- and outputs of one side of a 'Circuit'. -class Protocol a where - -- | Sender to receiver type family. See 'Circuit' for an explanation on the - -- existence of 'Fwd'. - type Fwd (a :: Type) = (r :: Type) | r -> a - - -- | Receiver to sender type family. See 'Circuit' for an explanation on the - -- existence of 'Bwd'. - type Bwd (a :: Type) = (r :: Type) | r -> a - -instance Protocol () where - type Fwd () = () - type Bwd () = () - -instance Protocol (a, b) where - type Fwd (a, b) = (Fwd a, Fwd b) - type Bwd (a, b) = (Bwd a, Bwd b) - -instance Protocol (a, b, c) where - type Fwd (a, b, c) = (Fwd a, Fwd b, Fwd c) - type Bwd (a, b, c) = (Bwd a, Bwd b, Bwd c) - -instance Protocol (a, b, c, d) where - type Fwd (a, b, c, d) = (Fwd a, Fwd b, Fwd c, Fwd d) - type Bwd (a, b, c, d) = (Bwd a, Bwd b, Bwd c, Bwd d) - -instance C.KnownNat n => Protocol (C.Vec n a) where - type Fwd (C.Vec n a) = C.Vec n (Fwd a) - type Bwd (C.Vec n a) = C.Vec n (Bwd a) - --- XXX: Type families with Signals on LHS are currently broken on Clash: -instance Protocol (CSignal dom a) where - type Fwd (CSignal dom a) = CSignal dom a - type Bwd (CSignal dom a) = CSignal dom (Const () a) - --- | Circuit combinator --- --- @ --- Circuit a c --- --- +---------------------------------+ --- --- Circuit a b |> Circuit b c --- --- +-----------+ +-----------+ --- Fwd a | | Fwd b | | Fwd c --- +------->+ +-------->+ +--------> --- | | | | --- | | | | --- Bwd a | | Bwd b | | Bwd c --- <--------+ +<--------+ +<-------+ --- | | | | --- +-----------+ +-----------+ --- @ --- -infixr 1 |> -(|>) :: Circuit a b -> Circuit b c -> Circuit a c -(Circuit fab) |> (Circuit fbc) = Circuit $ \(s2rAc, r2sAc) -> - let - ~(r2sAb, s2rAb) = fab (s2rAc, r2sBc) - ~(r2sBc, s2rBc) = fbc (s2rAb, r2sAc) - in - (r2sAb, s2rBc) - --- | Conversion from booleans to protocol specific acknowledgement values. -class Protocol a => Backpressure a where - -- | Interpret list of booleans as a list of acknowledgements at every cycle. - -- Implementations don't have to account for finite lists. - boolsToBwd :: [Bool] -> Bwd a - -instance Backpressure () where - boolsToBwd _ = () - -instance (Backpressure a, Backpressure b) => Backpressure (a, b) where - boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs) - -instance (Backpressure a, Backpressure b, Backpressure c) => Backpressure (a, b, c) where - boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs, boolsToBwd bs) - -instance (C.KnownNat n, Backpressure a) => Backpressure (C.Vec n a) where - boolsToBwd bs = C.repeat (boolsToBwd bs) - -instance Backpressure (CSignal dom a) where - boolsToBwd _ = CSignal (pure (Const ())) - --- | Flipped protocol combinator --- --- @ --- Circuit a c --- --- +---------------------------------+ --- --- Circuit b c <| Circuit a b --- --- +-----------+ +-----------+ --- Fwd c | | Fwd b | | Fwd a --- <--------+ +<--------+ +<-------+ --- | | | | --- | | | | --- Bwd c | | Bwd b | | Bwd a --- +------->+ +-------->+ +--------> --- | | | | --- +-----------+ +-----------+ --- @ --- -infixr 1 <| -(<|) :: Circuit b c -> Circuit a b -> Circuit a c -(<|) = flip (|>) - --- | View Circuit as its internal representation. -toSignals :: Circuit a b -> ((Fwd a, Bwd b) -> (Bwd a, Fwd b)) -toSignals = coerce - --- | View signals as a Circuit -fromSignals :: ((Fwd a, Bwd b) -> (Bwd a, Fwd b)) -> Circuit a b -fromSignals = coerce - --- | Circuit equivalent of 'id'. Useful for explicitly assigning a type to --- another protocol, or to return a result when using the circuit-notation --- plugin. --- --- Examples: --- --- @ --- idC \@(Df dom a) <| somePolymorphicProtocol --- @ --- --- @ --- swap :: Circuit (Dfs dom a, Dfs dom b) (Dfs dom b, Dfs dom a) --- swap = circuit $ \(a, b) -> do --- idC -< (b, a) --- @ --- -idC :: forall a. Circuit a a -idC = Circuit swap - --- | Copy a circuit /n/ times. Note that this will copy hardware. If you are --- looking for a circuit that turns a single channel into multiple, check out --- 'Protocols.Df.fanout' or 'Protocols.Df.Simple.fanout'. -repeatC :: - forall n a b. - Circuit a b -> - Circuit (C.Vec n a) (C.Vec n b) -repeatC (Circuit f) = - Circuit (C.unzip . C.map f . uncurry C.zip) - --- | Combine two separate circuits into one. If you are looking to combine --- multiple streams into a single stream, checkout 'Protocols.Df.fanin' or --- 'Protocols.Df.zip'. -prod2C :: - forall a c b d. - Circuit a b -> - Circuit c d -> - Circuit (a, c) (b, d) -prod2C (Circuit a) (Circuit c) = - Circuit (\((aFwd, cFwd), (bBwd, dBwd)) -> - let - (aBwd, bFwd) = a (aFwd, bBwd) - (cBwd, dFwd) = c (cFwd, dBwd) - in - ((aBwd, cBwd), (bFwd, dFwd))) - ---------------------------------- SIMULATION ----------------------------------- --- | Specifies option for simulation functions. Don't use this constructor --- directly, as it may be extend with other options in the future. Use 'def' --- instead. -data SimulationConfig = SimulationConfig - { -- | Assert reset for a number of cycles before driving the protocol - resetCycles :: Int - - -- | Timeout after /n/ cycles. Only affects sample functions. - , timeoutAfter :: Int - } - deriving (Show) - -instance Default SimulationConfig where - def = SimulationConfig - { resetCycles = 100 - , timeoutAfter = maxBound } - --- | Determines what kind of acknowledgement signal 'stallC' will send when its --- input component is not sending any data. Note that, in the Df protocol, --- protocols may send arbitrary acknowledgement signals when this happens. -data StallAck - -- | Send Nack - = StallWithNack - -- | Send Ack - | StallWithAck - -- | Send @errorX "No defined ack"@ - | StallWithErrorX - -- | Passthrough acknowledgement of RHS component - | StallTransparently - -- | Cycle through all modes - | StallCycle - deriving (Eq, Bounded, Enum, Show) - --- | Class that defines how to /drive/, /sample/, and /stall/ a "Circuit" of - -- some shape. -class (C.KnownNat (SimulateChannels a), Backpressure a) => Simulate a where - -- Type a /Circuit/ driver needs or sampler yields. For example: - -- - -- >>> :kind! (forall dom a. SimulateType (Dfs dom a)) - -- ... - -- = [Maybe (meta, a)] - -- - -- This means sampling a @Circuit () (Dfs dom a)@ yields @[Maybe a]@. - type SimulateType a :: Type - - -- | The number of simulation channel this channel has after flattening it. - -- For example, @(Dfs dom a, Dfs dom a)@ has 2, while - -- @Vec 4 (Dfs dom a, Dfs dom a)@ has 8. - type SimulateChannels a :: C.Nat - - -- | Create a /driving/ protocol component. Can be used in combination with - -- 'sampleC' to simulate a protocol component. Related: 'simulateC'. - driveC :: - SimulationConfig -> - SimulateType a -> - Circuit () a - - -- | Sample a protocol component that is trivially drivable. Use 'driveC' - -- to create such a component. Related: 'simulateC'. - sampleC :: - SimulationConfig -> - Circuit () a -> - SimulateType a - - -- | Create a /stalling/ protocol component. For each simulation channel - -- (see 'SimulateChannels') a tuple determines how the component stalls: - -- - -- * 'StallAck': determines how the backward (acknowledgement) channel - -- should behave whenever the component does not receive data from the - -- left hand side or when it's intentionally stalling. - -- - -- * A list of 'Int's that determine how many stall cycles to insert on - -- every cycle the left hand side component produces data. I.e., stalls - -- are /not/ inserted whenever the left hand side does /not/ produce data. - -- - stallC :: - SimulationConfig -> - C.Vec (SimulateChannels a) (StallAck, [Int]) -> - Circuit a a - -instance Simulate () where - type SimulateType () = () - type SimulateChannels () = 0 - - driveC _ _ = idC - sampleC _ _ = () - stallC _ _ = idC - -instance (Simulate a, Simulate b) => Simulate (a, b) where - type SimulateType (a, b) = (SimulateType a, SimulateType b) - type SimulateChannels (a, b) = SimulateChannels a + SimulateChannels b - - driveC conf (fwd1, fwd2) = - let (Circuit f1, Circuit f2) = (driveC conf fwd1, driveC conf fwd2) in - Circuit (\(_, ~(bwd1, bwd2)) -> ((), (snd (f1 ((), bwd1)), snd (f2 ((), bwd2))))) - - sampleC conf (Circuit f) = - let - bools = replicate (resetCycles conf) False <> repeat True - (_, (fwd1, fwd2)) = f ((), (boolsToBwd bools, boolsToBwd bools)) - in - ( sampleC conf (Circuit $ \_ -> ((), fwd1)) - , sampleC conf (Circuit $ \_ -> ((), fwd2)) ) - - stallC conf stalls = - let - (stallsL, stallsR) = C.splitAtI @(SimulateChannels a) @(SimulateChannels b) stalls - Circuit stalledL = stallC @a conf stallsL - Circuit stalledR = stallC @b conf stallsR - in - Circuit $ \((fwdL0, fwdR0), (bwdL0, bwdR0)) -> - let - (fwdL1, bwdL1) = stalledL (fwdL0, bwdL0) - (fwdR1, bwdR1) = stalledR (fwdR0, bwdR0) - in - ((fwdL1, fwdR1), (bwdL1, bwdR1)) - --- TODO TemplateHaskell? --- instance SimulateType (a, b, c) --- instance SimulateType (a, b, c, d) - -instance (C.KnownNat n, Simulate a) => Simulate (C.Vec n a) where - type SimulateType (C.Vec n a) = C.Vec n (SimulateType a) - type SimulateChannels (C.Vec n a) = n * SimulateChannels a - - driveC conf fwds = - let protocols = C.map (($ ()) . curry . toSignals . driveC conf) fwds in - Circuit (\(_, bwds) -> ((), C.map snd (C.zipWith ($) protocols bwds))) - - sampleC conf (Circuit f) = - let - bools = replicate (resetCycles conf) False <> repeat True - (_, fwds) = f ((), (C.repeat (boolsToBwd bools))) - in - C.map (\fwd -> sampleC conf (Circuit $ \_ -> ((), fwd))) fwds - - stallC conf stalls0 = - let - stalls1 = C.unconcatI @n @(SimulateChannels a) stalls0 - stalled = C.map (toSignals . stallC @a conf) stalls1 - in - Circuit $ \(fwds, bwds) -> C.unzip (C.zipWith ($) stalled (C.zip fwds bwds)) - -instance Default (CSignal dom (Const () a)) where - def = CSignal (pure (Const ())) - -instance (C.NFDataX a, C.ShowX a, Show a) => Simulate (CSignal dom a) where - type SimulateType (CSignal dom a) = [a] - type SimulateChannels (CSignal dom a) = 1 - - driveC _conf [] = error "CSignal.driveC: Can't drive with empty list" - driveC SimulationConfig{resetCycles} fwd0@(f:_) = - let fwd1 = C.fromList_lazy (replicate resetCycles f <> fwd0 <> repeat f) in - Circuit ( \_ -> ((), CSignal fwd1) ) - - sampleC SimulationConfig{resetCycles} (Circuit f) = - drop resetCycles (CE.sample_lazy ((\(CSignal s) -> s) (snd (f ((), def))))) - - stallC _ _ = idC - --- | Simulate a protocol. Not synthesizable. --- --- To figure out what input you need to supply, either solve the type --- "SimulateType" manually, or let the repl do the work for you! Example: --- --- >>> :kind! (forall dom meta a. SimulateType (Df dom meta a)) --- ... --- = [Maybe (meta, a)] --- --- This would mean a @Circuit (Df dom meta a) (Df dom meta b)@ would need --- @[(meta, a)]@ as the last argument of 'simulateC' and would result in --- @[(meta, b)]@. Note that for this particular type you can neither supply --- stalls nor introduce backpressure. If you want to to this use 'Df.stall'. -simulateC :: - forall a b. - (Simulate a, Simulate b) => - -- | Circuit to simulate - Circuit a b -> - -- | Simulation configuration. Note that some options only apply to 'sampleC' - -- and some only to 'driveC'. - SimulationConfig -> - -- | Circuit input - SimulateType a -> - -- | Circuit output - SimulateType b -simulateC c conf as = - sampleC conf (driveC conf as |> c) - --- | Picked up by "Protocols.Plugin" to process protocol DSL. See --- "Protocols.Plugin" for more information. -circuit :: Any -circuit = - error "'protocol' called: did you forget to enable \"Protocols.Plugin\"?" +import Protocols.Internal +import Protocols.Df (Df) +import Protocols.Df.Simple (Dfs) diff --git a/src/Protocols/Df.hs b/src/Protocols/Df.hs index 4bdcccc9..bafc75fb 100644 --- a/src/Protocols/Df.hs +++ b/src/Protocols/Df.hs @@ -15,6 +15,8 @@ This module is designed to be imported using qualified, i.e.: {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE NamedFieldPuns #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + module Protocols.Df ( -- * Type definitions Df @@ -53,8 +55,8 @@ module Protocols.Df , forceAckLow ) where -import Protocols hiding (Ack(..)) -import qualified Protocols +import Protocols.Internal hiding (Ack(..)) +import qualified Protocols.Internal as Protocols import qualified Prelude as P import Prelude hiding (map, const, fst, snd, pure, either, filter) @@ -65,14 +67,14 @@ import qualified Data.Bifunctor.Extra as Bifunctor import qualified Data.Bifunctor as Bifunctor import Data.Bifunctor (Bifunctor) import Data.Coerce (coerce) -import Data.Kind (Type) import Data.List ((\\)) +import Data.Kind (Type) import qualified Data.Maybe as Maybe import qualified Data.Tuple.Extra as T import GHC.Stack (HasCallStack) import GHC.Generics (Generic) -import Clash.Prelude (Signal, Domain, type (<=), type (-)) +import Clash.Prelude (Signal, type (<=), type (-)) import qualified Clash.Prelude as C import qualified Clash.Explicit.Prelude as CE import Clash.Signal.Internal (Signal((:-))) @@ -90,12 +92,11 @@ import Clash.Signal.Internal (Signal((:-))) -- 2. The data channel should remain stable (i.e., not change) until the -- receiver has sent an acknowledgement. -- --- __N.B.__: For performance reasons 'Data' is strict on its fields. That is, --- if it is evaluated to WHNF, its fields will also be evaluated to WHNF. If you --- need lazy behavior, check out "Protocols.Df.Lazy". +-- __N.B.__: For performance reasons 'Protocols.Df.Data' is strict on its +-- fields. That is, if it is evaluated to WHNF, its fields will also be +-- evaluated to WHNF. -- -data Df (dom :: Domain) (meta :: Type) (a :: Type) - +data Df (dom :: C.Domain) (meta :: Type) (a :: Type) instance Protocol (Df dom meta a) where -- | Forward part of base dataflow: @Signal dom (Data meta a)@ type Fwd (Df dom meta a) = Signal dom (Data meta a) diff --git a/src/Protocols/Df.hs-boot b/src/Protocols/Df.hs-boot deleted file mode 100644 index 960d5505..00000000 --- a/src/Protocols/Df.hs-boot +++ /dev/null @@ -1,9 +0,0 @@ -{-# LANGUAGE RoleAnnotations #-} - -module Protocols.Df where - -import Data.Kind (Type) -import Clash.Prelude (Domain) - -data Df (dom :: Domain) (meta :: Type) (a :: Type) -type role Df phantom phantom phantom diff --git a/src/Protocols/Df/Lazy.hs b/src/Protocols/Df/Lazy.hs deleted file mode 100644 index 9a3e13e2..00000000 --- a/src/Protocols/Df/Lazy.hs +++ /dev/null @@ -1,3 +0,0 @@ -{-| Not yet implemented -} - -module Protocols.Df.Lazy where diff --git a/src/Protocols/Df/Simple.hs b/src/Protocols/Df/Simple.hs index 8519c7f4..74cacb3c 100644 --- a/src/Protocols/Df/Simple.hs +++ b/src/Protocols/Df/Simple.hs @@ -6,11 +6,13 @@ carries data, no metadata. For documentation see: * 'Protocols.Df.Simple.Dfs' -} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} -{-# OPTIONS_GHC -fpedantic-bottoms -feager-blackholing #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} module Protocols.Df.Simple where @@ -30,13 +32,12 @@ import qualified Data.List.NonEmpty import Data.Maybe (fromMaybe) import qualified Prelude as P -import Clash.Prelude - (Domain, type (<=), type (-), type (+), (!!)) +import Clash.Prelude (type (<=), type (-), type (+), (!!)) import qualified Clash.Prelude as C import qualified Clash.Explicit.Prelude as CE -import Protocols hiding (Ack(..)) -import qualified Protocols +import Protocols.Internal hiding (Ack(..)) +import qualified Protocols.Internal as Protocols import qualified Protocols.Df as Df import Protocols.Df (Df) import qualified Protocols.DfLike as DfLike @@ -44,12 +45,13 @@ import Protocols.DfLike (DfLike) import GHC.Stack (HasCallStack) --- | Like 'Protocols.Df.Df', but without metadata. + +-- | Like 'Protocols.Df', but without metadata. -- --- __N.B.__: For performance reasons 'Data' is strict on its data field. That --- is, if 'Data' is evaluated to WHNF, its fields will be evaluated to WHNF --- too. If you need lazy behavior, check out "Protocols.Df.Simple.Lazy". -data Dfs (dom :: Domain) (a :: Type) +-- __N.B.__: For performance reasons 'Protocols.Df.Simple.Data' is strict on +-- its data field. That is, if 'Protocols.Df.Simple.Data' is evaluated to WHNF, +-- its fields will be evaluated to WHNF too. +data Dfs (dom :: C.Domain) (a :: Type) instance Protocol (Dfs dom a) where -- | Forward part of simple dataflow: @Signal dom (Data meta a)@ diff --git a/src/Protocols/Df/Simple.hs-boot b/src/Protocols/Df/Simple.hs-boot deleted file mode 100644 index dd21de31..00000000 --- a/src/Protocols/Df/Simple.hs-boot +++ /dev/null @@ -1,9 +0,0 @@ -{-# LANGUAGE RoleAnnotations #-} - -module Protocols.Df.Simple where - -import Data.Kind (Type) -import Clash.Prelude (Domain) - -data Dfs (dom :: Domain) (a :: Type) -type role Dfs phantom phantom diff --git a/src/Protocols/Df/Simple/Lazy.hs b/src/Protocols/Df/Simple/Lazy.hs deleted file mode 100644 index 0f5c5932..00000000 --- a/src/Protocols/Df/Simple/Lazy.hs +++ /dev/null @@ -1,3 +0,0 @@ -{-| Not yet implemented -} - -module Protocols.Df.Simple.Lazy where diff --git a/src/Protocols/DfLike.hs b/src/Protocols/DfLike.hs index a5a85620..77be49eb 100644 --- a/src/Protocols/DfLike.hs +++ b/src/Protocols/DfLike.hs @@ -34,8 +34,8 @@ module Protocols.DfLike , forceAckLow ) where -import Protocols hiding (Ack(..)) -import qualified Protocols +import Protocols.Internal hiding (Ack(..)) +import qualified Protocols.Internal as Protocols import qualified Protocols.Df as Df import Protocols.Df (Df) diff --git a/src/Protocols/Hedgehog/Internal.hs b/src/Protocols/Hedgehog/Internal.hs index 404ccd64..441119eb 100644 --- a/src/Protocols/Hedgehog/Internal.hs +++ b/src/Protocols/Hedgehog/Internal.hs @@ -18,8 +18,8 @@ import Data.Proxy (Proxy(Proxy)) -- clash-protocols import Protocols -import Protocols.Df (Df) -import Protocols.Df.Simple (Dfs) +import Protocols.Df () +import Protocols.Df.Simple () -- clash-prelude import qualified Clash.Prelude as C diff --git a/src/Protocols/Internal.hs b/src/Protocols/Internal.hs new file mode 100644 index 00000000..417d7e82 --- /dev/null +++ b/src/Protocols/Internal.hs @@ -0,0 +1,516 @@ +{-| +Internal module to prevent hs-boot files (breaks Haddock) +-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Protocols.Internal where + +import GHC.Base (Any) +import Prelude hiding (map, const) + +import Clash.Prelude (Signal, type (+), type (*)) +import qualified Clash.Prelude as C +import qualified Clash.Explicit.Prelude as CE + +import Control.Applicative (Const(..)) +import Data.Coerce (coerce) +import Data.Default (Default(def)) +import Data.Kind (Type) +import Data.Tuple (swap) +import GHC.Generics (Generic) + +-- | A /Circuit/, in its most general form, corresponds to a component with two +-- pairs of an input and output. As a diagram: +-- +-- @ +-- Circuit a b +-- +-- +-----------+ +-- Fwd a | | Fwd b +-- +------->+ +--------> +-- | | +-- | | +-- Bwd a | | Bwd b +-- <--------+ +<-------+ +-- | | +-- +-----------+ +-- @ +-- +-- The first pair, @(Fwd a, Bwd a)@ can be thought of the data sent to and from +-- the component on the left hand side of this circuit. For this pair, @Fwd a@ +-- is the data sent from the circuit on the left hand side (not pictured), while +-- @Bwd a@ is the data sent to the left hand side from the current circuit. +-- +-- Similarly, the second pair, @(Fwd b, Bwd)@, can be thought of as the data +-- sent to and from the right hand side of this circuit. In this case, @Fwd b@ +-- is the data sent from the current circuit to the one on the right hand side, +-- while @Bwd b@ is the data received from the right hand side. +-- +-- In Haskell terms, we would say this is simply a function taking two inputs, +-- @Fwd a@ and @Bwd b@, yielding a pair of outputs @Fwd b@ and @Bwd a@. This is +-- in fact exactly its definition: +-- +-- @ +-- newtype Circuit a b = +-- Circuit ( (Fwd a, Bwd b) -> (Bwd a, Fwd b) ) +-- @ +-- +-- Note that the type parameters /a/ and /b/ don't directly correspond to the +-- types of the inputs and outputs of this function. Instead, the type families +-- @Fwd@ and @Bwd@ decide this. The type parameters can be thought of as +-- deciders for what /protocol/ the left hand side and right hand side must +-- speak. +-- +-- Let's make it a bit more concrete by building such a protocol. For this +-- example, we'd like to build a protocol that sends data to a circuit, while +-- allowing the circuit to signal whether it processed the sent data or not. Similarly, +-- we'd like the sender to be able to indicate that it doesn't have any data to +-- send. These kind of protocols fall under the umbrella of "dataflow" protocols, +-- so lets call it /DataFlowSimple/ or /Dfs/ for short: +-- +-- @ +-- data Dfs (dom :: Domain) (a :: Type) +-- @ +-- +-- We're only going to use it on the type level, so we won't need any +-- constructors for this datatype. The first type parameter indicates the +-- synthesis domain the protocol will use. This is the same /dom/ as used in +-- /Signal dom a/. The second type indicates what data the protocol needs to +-- send. Again, this is similar to the /a/ in /Signal dom a/. +-- +-- As said previously, we'd like the sender to either send /no data/ or +-- /some data/. We can capture this in a data type very similar to /Maybe/: +-- +-- @ +-- data Data a = NoData | Data a +-- @ +-- +-- On the way back, we'd like to either acknowledge or not acknowledge sent +-- data. Similar to /Bool/ we define: +-- +-- @ +-- data Ack a = DfNack | Ack +-- @ +-- +-- (For technical reasons[1] we need the type variable /a/ in this definition, +-- even though we don't use it on the right hand side.) +-- +-- With these three definitions we're ready to make an instance for /Fwd/ and +-- /Bwd/: +-- +-- @ +-- instance Protocol (Dfs dom a) where +-- type Fwd (Dfs dom a) = Signal dom (Data a) +-- type Bwd (Dfs dom a) = Signal dom (Ack a) +-- @ +-- +-- Having defined all this, we can take a look at /Circuit/ once more: now +-- instantiated with our types. The following: +-- +-- @ +-- f :: Circuit (Dfs dom a) (Dfs dom b) +-- @ +-- +-- ..now corresponds to the following protocol: +-- +-- @ +-- +-----------+ +-- Signal dom (Data a) | | Signal dom (Data b) +-- +------------------------>+ +-------------------------> +-- | | +-- | | +-- Signal dom (Ack a) | | Signal dom (Ack b) +-- <-------------------------+ +<------------------------+ +-- | | +-- +-----------+ +-- @ +-- +-- There's a number of advantages over manually writing out these function +-- types: +-- +-- 1. It reduces syntactical noise in type signatures +-- +-- 2. It eliminates the need for manually routing acknowledgement lines +-- +-- Footnotes: +-- +-- 1. Fwd and Bwd are injective type families. I.e., something on +-- the right hand side of a type instance must uniquely identify the left +-- hand side and vice versa. This helps type inference and error messages +-- substantially, in exchange for a slight syntactical artifact. As a +-- result, any type variables on the left hand side must occur on the right +-- hand side too. +-- +newtype Circuit a b = + Circuit ( (Fwd a, Bwd b) -> (Bwd a, Fwd b) ) + +-- | Protocol-agnostic acknowledgement +newtype Ack = Ack Bool + deriving (Generic, C.NFDataX) + +-- | Circuit protocol with /CSignal dom a/ in its forward direction, and +-- /CSignal dom ()/ in its backward direction. Convenient for exposing +-- protocol internals. +data CSignal dom a = CSignal (Signal dom a) + + +-- | A protocol describes the in- and outputs of one side of a 'Circuit'. +class Protocol a where + -- | Sender to receiver type family. See 'Circuit' for an explanation on the + -- existence of 'Fwd'. + type Fwd (a :: Type) = (r :: Type) | r -> a + + -- | Receiver to sender type family. See 'Circuit' for an explanation on the + -- existence of 'Bwd'. + type Bwd (a :: Type) = (r :: Type) | r -> a + +instance Protocol () where + type Fwd () = () + type Bwd () = () + +instance Protocol (a, b) where + type Fwd (a, b) = (Fwd a, Fwd b) + type Bwd (a, b) = (Bwd a, Bwd b) + +instance Protocol (a, b, c) where + type Fwd (a, b, c) = (Fwd a, Fwd b, Fwd c) + type Bwd (a, b, c) = (Bwd a, Bwd b, Bwd c) + +instance Protocol (a, b, c, d) where + type Fwd (a, b, c, d) = (Fwd a, Fwd b, Fwd c, Fwd d) + type Bwd (a, b, c, d) = (Bwd a, Bwd b, Bwd c, Bwd d) + +instance C.KnownNat n => Protocol (C.Vec n a) where + type Fwd (C.Vec n a) = C.Vec n (Fwd a) + type Bwd (C.Vec n a) = C.Vec n (Bwd a) + +-- XXX: Type families with Signals on LHS are currently broken on Clash: +instance Protocol (CSignal dom a) where + type Fwd (CSignal dom a) = CSignal dom a + type Bwd (CSignal dom a) = CSignal dom (Const () a) + +-- | Left-to-right circuit composition. +-- +-- @ +-- Circuit a c +-- +-- +---------------------------------+ +-- +-- Circuit a b |> Circuit b c +-- +-- +-----------+ +-----------+ +-- Fwd a | | Fwd b | | Fwd c +-- +------->+ +-------->+ +--------> +-- | | | | +-- | | | | +-- Bwd a | | Bwd b | | Bwd c +-- <--------+ +<--------+ +<-------+ +-- | | | | +-- +-----------+ +-----------+ +-- @ +-- +infixr 1 |> +(|>) :: Circuit a b -> Circuit b c -> Circuit a c +(Circuit fab) |> (Circuit fbc) = Circuit $ \(s2rAc, r2sAc) -> + let + ~(r2sAb, s2rAb) = fab (s2rAc, r2sBc) + ~(r2sBc, s2rBc) = fbc (s2rAb, r2sAc) + in + (r2sAb, s2rBc) + +-- | Conversion from booleans to protocol specific acknowledgement values. +class Protocol a => Backpressure a where + -- | Interpret list of booleans as a list of acknowledgements at every cycle. + -- Implementations don't have to account for finite lists. + boolsToBwd :: [Bool] -> Bwd a + +instance Backpressure () where + boolsToBwd _ = () + +instance (Backpressure a, Backpressure b) => Backpressure (a, b) where + boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs) + +instance (Backpressure a, Backpressure b, Backpressure c) => Backpressure (a, b, c) where + boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs, boolsToBwd bs) + +instance (C.KnownNat n, Backpressure a) => Backpressure (C.Vec n a) where + boolsToBwd bs = C.repeat (boolsToBwd bs) + +instance Backpressure (CSignal dom a) where + boolsToBwd _ = CSignal (pure (Const ())) + +-- | Right-to-left circuit composition. +-- +-- @ +-- Circuit a c +-- +-- +---------------------------------+ +-- +-- Circuit b c <| Circuit a b +-- +-- +-----------+ +-----------+ +-- Fwd c | | Fwd b | | Fwd a +-- <--------+ +<--------+ +<-------+ +-- | | | | +-- | | | | +-- Bwd c | | Bwd b | | Bwd a +-- +------->+ +-------->+ +--------> +-- | | | | +-- +-----------+ +-----------+ +-- @ +-- +infixr 1 <| +(<|) :: Circuit b c -> Circuit a b -> Circuit a c +(<|) = flip (|>) + +-- | View Circuit as its internal representation. +toSignals :: Circuit a b -> ((Fwd a, Bwd b) -> (Bwd a, Fwd b)) +toSignals = coerce + +-- | View signals as a Circuit +fromSignals :: ((Fwd a, Bwd b) -> (Bwd a, Fwd b)) -> Circuit a b +fromSignals = coerce + +-- | Circuit equivalent of 'id'. Useful for explicitly assigning a type to +-- another protocol, or to return a result when using the circuit-notation +-- plugin. +-- +-- Examples: +-- +-- @ +-- idC \@(Df dom a) <| somePolymorphicProtocol +-- @ +-- +-- @ +-- swap :: Circuit (Dfs dom a, Dfs dom b) (Dfs dom b, Dfs dom a) +-- swap = circuit $ \(a, b) -> do +-- idC -< (b, a) +-- @ +-- +idC :: forall a. Circuit a a +idC = Circuit swap + +-- | Copy a circuit /n/ times. Note that this will copy hardware. If you are +-- looking for a circuit that turns a single channel into multiple, check out +-- 'Protocols.Df.fanout' or 'Protocols.Df.Simple.fanout'. +repeatC :: + forall n a b. + Circuit a b -> + Circuit (C.Vec n a) (C.Vec n b) +repeatC (Circuit f) = + Circuit (C.unzip . C.map f . uncurry C.zip) + +-- | Combine two separate circuits into one. If you are looking to combine +-- multiple streams into a single stream, checkout 'Protocols.Df.fanin' or +-- 'Protocols.Df.zip'. +prod2C :: + forall a c b d. + Circuit a b -> + Circuit c d -> + Circuit (a, c) (b, d) +prod2C (Circuit a) (Circuit c) = + Circuit (\((aFwd, cFwd), (bBwd, dBwd)) -> + let + (aBwd, bFwd) = a (aFwd, bBwd) + (cBwd, dFwd) = c (cFwd, dBwd) + in + ((aBwd, cBwd), (bFwd, dFwd))) + +--------------------------------- SIMULATION ----------------------------------- +-- | Specifies option for simulation functions. Don't use this constructor +-- directly, as it may be extend with other options in the future. Use 'def' +-- instead. +data SimulationConfig = SimulationConfig + { -- | Assert reset for a number of cycles before driving the protocol + resetCycles :: Int + + -- | Timeout after /n/ cycles. Only affects sample functions. + , timeoutAfter :: Int + } + deriving (Show) + +instance Default SimulationConfig where + def = SimulationConfig + { resetCycles = 100 + , timeoutAfter = maxBound } + +-- | Determines what kind of acknowledgement signal 'stallC' will send when its +-- input component is not sending any data. Note that, in the Df protocol, +-- protocols may send arbitrary acknowledgement signals when this happens. +data StallAck + -- | Send Nack + = StallWithNack + -- | Send Ack + | StallWithAck + -- | Send @errorX "No defined ack"@ + | StallWithErrorX + -- | Passthrough acknowledgement of RHS component + | StallTransparently + -- | Cycle through all modes + | StallCycle + deriving (Eq, Bounded, Enum, Show) + +-- | Class that defines how to /drive/, /sample/, and /stall/ a "Circuit" of + -- some shape. +class (C.KnownNat (SimulateChannels a), Backpressure a) => Simulate a where + -- Type a /Circuit/ driver needs or sampler yields. For example: + -- + -- >>> :kind! (forall dom a. SimulateType (Dfs dom a)) + -- ... + -- = [Maybe (meta, a)] + -- + -- This means sampling a @Circuit () (Dfs dom a)@ yields @[Maybe a]@. + type SimulateType a :: Type + + -- | The number of simulation channel this channel has after flattening it. + -- For example, @(Dfs dom a, Dfs dom a)@ has 2, while + -- @Vec 4 (Dfs dom a, Dfs dom a)@ has 8. + type SimulateChannels a :: C.Nat + + -- | Create a /driving/ circuit. Can be used in combination with 'sampleC' + -- to simulate a circuit. Related: 'simulateC'. + driveC :: + SimulationConfig -> + SimulateType a -> + Circuit () a + + -- | Sample a circuit that is trivially drivable. Use 'driveC' to create + -- such a circuit. Related: 'simulateC'. + sampleC :: + SimulationConfig -> + Circuit () a -> + SimulateType a + + -- | Create a /stalling/ circuit. For each simulation channel (see + -- 'SimulateChannels') a tuple determines how the component stalls: + -- + -- * 'StallAck': determines how the backward (acknowledgement) channel + -- should behave whenever the component does not receive data from the + -- left hand side or when it's intentionally stalling. + -- + -- * A list of 'Int's that determine how many stall cycles to insert on + -- every cycle the left hand side component produces data. I.e., stalls + -- are /not/ inserted whenever the left hand side does /not/ produce data. + -- + stallC :: + SimulationConfig -> + C.Vec (SimulateChannels a) (StallAck, [Int]) -> + Circuit a a + +instance Simulate () where + type SimulateType () = () + type SimulateChannels () = 0 + + driveC _ _ = idC + sampleC _ _ = () + stallC _ _ = idC + +instance (Simulate a, Simulate b) => Simulate (a, b) where + type SimulateType (a, b) = (SimulateType a, SimulateType b) + type SimulateChannels (a, b) = SimulateChannels a + SimulateChannels b + + driveC conf (fwd1, fwd2) = + let (Circuit f1, Circuit f2) = (driveC conf fwd1, driveC conf fwd2) in + Circuit (\(_, ~(bwd1, bwd2)) -> ((), (snd (f1 ((), bwd1)), snd (f2 ((), bwd2))))) + + sampleC conf (Circuit f) = + let + bools = replicate (resetCycles conf) False <> repeat True + (_, (fwd1, fwd2)) = f ((), (boolsToBwd bools, boolsToBwd bools)) + in + ( sampleC conf (Circuit $ \_ -> ((), fwd1)) + , sampleC conf (Circuit $ \_ -> ((), fwd2)) ) + + stallC conf stalls = + let + (stallsL, stallsR) = C.splitAtI @(SimulateChannels a) @(SimulateChannels b) stalls + Circuit stalledL = stallC @a conf stallsL + Circuit stalledR = stallC @b conf stallsR + in + Circuit $ \((fwdL0, fwdR0), (bwdL0, bwdR0)) -> + let + (fwdL1, bwdL1) = stalledL (fwdL0, bwdL0) + (fwdR1, bwdR1) = stalledR (fwdR0, bwdR0) + in + ((fwdL1, fwdR1), (bwdL1, bwdR1)) + +-- TODO TemplateHaskell? +-- instance SimulateType (a, b, c) +-- instance SimulateType (a, b, c, d) + +instance (C.KnownNat n, Simulate a) => Simulate (C.Vec n a) where + type SimulateType (C.Vec n a) = C.Vec n (SimulateType a) + type SimulateChannels (C.Vec n a) = n * SimulateChannels a + + driveC conf fwds = + let circuits = C.map (($ ()) . curry . toSignals . driveC conf) fwds in + Circuit (\(_, bwds) -> ((), C.map snd (C.zipWith ($) circuits bwds))) + + sampleC conf (Circuit f) = + let + bools = replicate (resetCycles conf) False <> repeat True + (_, fwds) = f ((), (C.repeat (boolsToBwd bools))) + in + C.map (\fwd -> sampleC conf (Circuit $ \_ -> ((), fwd))) fwds + + stallC conf stalls0 = + let + stalls1 = C.unconcatI @n @(SimulateChannels a) stalls0 + stalled = C.map (toSignals . stallC @a conf) stalls1 + in + Circuit $ \(fwds, bwds) -> C.unzip (C.zipWith ($) stalled (C.zip fwds bwds)) + +instance Default (CSignal dom (Const () a)) where + def = CSignal (pure (Const ())) + +instance (C.NFDataX a, C.ShowX a, Show a) => Simulate (CSignal dom a) where + type SimulateType (CSignal dom a) = [a] + type SimulateChannels (CSignal dom a) = 1 + + driveC _conf [] = error "CSignal.driveC: Can't drive with empty list" + driveC SimulationConfig{resetCycles} fwd0@(f:_) = + let fwd1 = C.fromList_lazy (replicate resetCycles f <> fwd0 <> repeat f) in + Circuit ( \_ -> ((), CSignal fwd1) ) + + sampleC SimulationConfig{resetCycles} (Circuit f) = + drop resetCycles (CE.sample_lazy ((\(CSignal s) -> s) (snd (f ((), def))))) + + stallC _ _ = idC + +-- | Simulate a circuit. Not synthesizable. +-- +-- To figure out what input you need to supply, either solve the type +-- "SimulateType" manually, or let the repl do the work for you! Example: +-- +-- >>> :kind! (forall dom meta a. SimulateType (Df dom meta a)) +-- ... +-- = [Maybe (meta, a)] +-- +-- This would mean a @Circuit (Df dom meta a) (Df dom meta b)@ would need +-- @[(meta, a)]@ as the last argument of 'simulateC' and would result in +-- @[(meta, b)]@. Note that for this particular type you can neither supply +-- stalls nor introduce backpressure. If you want to to this use 'Df.stall'. +simulateC :: + forall a b. + (Simulate a, Simulate b) => + -- | Circuit to simulate + Circuit a b -> + -- | Simulation configuration. Note that some options only apply to 'sampleC' + -- and some only to 'driveC'. + SimulationConfig -> + -- | Circuit input + SimulateType a -> + -- | Circuit output + SimulateType b +simulateC c conf as = + sampleC conf (driveC conf as |> c) + +-- | Picked up by "Protocols.Plugin" to process protocol DSL. See +-- "Protocols.Plugin" for more information. +circuit :: Any +circuit = + error "'protocol' called: did you forget to enable \"Protocols.Plugin\"?" diff --git a/src/Test/Tasty/Hedgehog/Extra.hs b/src/Test/Tasty/Hedgehog/Extra.hs index 14de65ed..fa67fb78 100644 --- a/src/Test/Tasty/Hedgehog/Extra.hs +++ b/src/Test/Tasty/Hedgehog/Extra.hs @@ -1,3 +1,8 @@ +{-| +Extras for module 'Test.Tasty.Hedgehog'. Functions in this module should be +upstreamed if possible. +-} + module Test.Tasty.Hedgehog.Extra (testProperty) where import Prelude @@ -5,5 +10,6 @@ import Hedgehog (Property) import qualified Test.Tasty.Hedgehog as H import Test.Tasty (TestTree) +-- | Like 'Test.Tasty.Hedgehog.testProperty', but inserts correct name testProperty :: [Char] -> Property -> TestTree testProperty nm = H.testProperty ("prop_" <> nm) diff --git a/stack.yaml b/stack.yaml index 747e29f7..53ab604c 100644 --- a/stack.yaml +++ b/stack.yaml @@ -4,8 +4,11 @@ extra-deps: - ghc-typelits-extra-0.4@sha256:e1ba4ebf14cb7025dd940380dfb15db444f7e8bced7e30bdad6e1707f0af7622,4813 - ghc-typelits-knownnat-0.7.2@sha256:63054c8108f21a4bc5ace477227476b72a4e3792f35f37f2d406eef262ae4346,4711 - ghc-typelits-natnormalise-0.7.2@sha256:0fc48a3744aa25e5e53a054a8bb1fe6410752e497f446d75db9bd67bb258d05e,3495 -- hedgehog-1.0.3@sha256:dd9a25bf904fe444d5de471d0933261ef2c9a1110330460e037e0fef86fac89e,4622 - clash-prelude-1.2.5@sha256:2ea4d0506adfccd0e817a67e47de132290a856535dd69bcc71e7fbce24ece3f2,15307 +- git: https://github.com/martijnbastiaan/haskell-hedgehog.git + commit: 41e87d110d3b2b7b522d29d7c0500672f2640dcc + subdirs: + - hedgehog flags: clash-prelude: @@ -14,3 +17,5 @@ flags: # Clash, and triggers Template Haskell bugs on Windows. Hence, we disable # it by default. This will be the default for Clash >=1.4. large-tuples: false + +allow-newer: true diff --git a/tests/Tests/Protocols/Df.hs b/tests/Tests/Protocols/Df.hs index 0d41a91c..c83c25ef 100644 --- a/tests/Tests/Protocols/Df.hs +++ b/tests/Tests/Protocols/Df.hs @@ -27,7 +27,6 @@ import Test.Tasty.TH (testGroupGenerator) -- clash-protocols (me!) import Protocols -import Protocols.Df (Df) import qualified Protocols.Df as Df import Protocols.Hedgehog diff --git a/tests/Tests/Protocols/Df/Simple.hs b/tests/Tests/Protocols/Df/Simple.hs index 878913eb..2caef8b7 100644 --- a/tests/Tests/Protocols/Df/Simple.hs +++ b/tests/Tests/Protocols/Df/Simple.hs @@ -7,7 +7,7 @@ module Tests.Protocols.Df.Simple where -- base import Data.Coerce (coerce) import Data.Foldable (fold) -import Data.Maybe (catMaybes) +import Data.Maybe (catMaybes, fromMaybe) import Data.List (mapAccumL) import GHC.Stack (HasCallStack) import Prelude @@ -41,7 +41,6 @@ import Test.Tasty.TH (testGroupGenerator) -- clash-protocols (me!) import Protocols -import Protocols.Df.Simple (Dfs) import qualified Protocols.Df.Simple as Dfs import Protocols.Hedgehog @@ -299,7 +298,7 @@ prop_select = goGen = do n <- genSmallInt ixs <- Gen.list (Range.singleton n) Gen.enumBounded - let tall i = HashMap.findWithDefault 0 i (tally ixs) + let tall i = fromMaybe 0 (HashMap.lookup i (tally ixs)) dats <- mapM (\i -> Gen.list (Range.singleton (tall i)) genSmallInt) C.indicesI pure (dats, ixs) @@ -324,7 +323,7 @@ prop_selectN = lenghts <- Gen.list (Range.singleton n) Gen.enumBounded let tallied = tallyOn fst (fromIntegral . snd) (zip ixs lenghts) - tall i = HashMap.findWithDefault 0 i tallied + tall i = fromMaybe 0 (HashMap.lookup i tallied) dats <- mapM (\i -> Gen.list (Range.singleton (tall i)) genSmallInt) C.indicesI pure (dats, zip ixs lenghts)