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)