Skip to content

Commit

Permalink
Merge pull request #21 from clash-lang/dfs-as-main
Browse files Browse the repository at this point in the history
Remove Dfs, rewrite DFLike
  • Loading branch information
martijnbastiaan authored Jan 4, 2021
2 parents fb0547e + 0283cfe commit 9795f14
Show file tree
Hide file tree
Showing 18 changed files with 1,599 additions and 1,967 deletions.
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -45,3 +45,6 @@ stack.yaml.lock
/systemverilog

log

# Created by .ci/build_docs.sh
/docs
15 changes: 3 additions & 12 deletions .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,6 @@
after_script:
- tar -cf - $(ls -d /root/.cabal /root/.stack /nix || true) | zstd -T0 -3 > cache.tar.zstd

.common-806:
extends: .common
image: docker.pkg.github.com/clash-lang/clash-protocols/protocols-focal-ghc-cabal-stack-8.6.5:2020-12-07
variables:
GHC_VERSION: "8.6.5"
CABAL_VERSION: "3.2.0.0"

.common-810:
extends: .common
image: docker.pkg.github.com/clash-lang/clash-protocols/protocols-focal-ghc-cabal-stack-8.10.2:2020-12-07
Expand All @@ -44,14 +37,12 @@ haddock:
script:
- .ci/build_docs.sh

# Circuit-notation is broken on 810.
# https://github.com/cchalmers/circuit-notation/pull/8#issuecomment-739844352
cabal-8.6.5:
extends: .common-806
cabal-8.10.2:
extends: .common-810
script:
- .ci/test_cabal.sh

stack:
extends: .common-806
extends: .common-810
script:
- .ci/test_stack.sh
3 changes: 0 additions & 3 deletions .gitmodules

This file was deleted.

78 changes: 37 additions & 41 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ A battery-included library for writing on-chip protocols, such as AMBA AXI and A
<!-- omit in toc -->
# Table of Contents
- [Introduction](#introduction)
- [Using `Dfs`/`Df` `Circuit`s](#using-dfsdf-circuits)
- [Using `Df` `Circuit`s](#using-df-circuits)
- [Invariants](#invariants)
- [Note [Deasserting resets]](#note-deasserting-resets)
- [Tutorial: `catMaybes`](#tutorial-catmaybes)
Expand All @@ -22,12 +22,12 @@ A battery-included library for writing on-chip protocols, such as AMBA AXI and A
`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`
* `Protocols.Df`

The next section will guide you through the creation of a single `Dfs` based circuit.
The next section will guide you through the creation of a single `Df` based circuit.

# Using `Dfs`/`Df` `Circuit`s
The basic handshaking of `Dfs` and `Df` are heavily inspired by _AMBA AXI_:
# Using `Df` `Circuit`s
The basic handshaking of `Df` is heavily inspired by _AMBA AXI_:

* `Df` circuits _send_ data to their right hand side
* `Df` circuits _receive_ data from their left hand side.
Expand All @@ -36,7 +36,7 @@ The basic handshaking of `Dfs` and `Df` are heavily inspired by _AMBA AXI_:

## 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`.
The protocols `Df` imposes 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.

Expand Down Expand Up @@ -105,7 +105,7 @@ should be deasserted as follows: `a`, `b,` `c`, `d`/`e`, `f`. Resets might also
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`:
At this point you should have familiarized with the basic structures of the `Df`: 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
Expand All @@ -122,7 +122,7 @@ 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
>>> import qualified Protocols.Df as Df
```

You should now be able to query various things. For example:
Expand All @@ -140,21 +140,21 @@ module CatMaybes where

import Protocols
import qualified Clash.Prelude as C
import qualified Protocols.Df.Simple as Dfs
import qualified Protocols.Df as Df
```

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)
catMaybes :: Circuit (Df dom (Maybe a)) (Df 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:
I.e., a circuit that takes a `Df` 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 `Df`s _forward_ path very much looks like a `Maybe` in the first place:

```
>>> :kind! Fwd (Dfs C.System Int)
>>> :kind! Fwd (Df C.System Int)
..
= Signal "System" (Dfs.Data Int)
= Signal "System" (Df.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.
Expand All @@ -171,8 +171,8 @@ At this point, GHC will tell us:
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))
:: (C.Signal dom (Df.Data (Maybe a)), C.Signal dom (Df.Ack a))
-> (C.Signal dom (Df.Ack (Maybe a)), C.Signal dom (Df.Data a))
|
8 | catMaybes = Circuit go
| ^^
Expand Down Expand Up @@ -200,8 +200,8 @@ Now GHC will tell us:
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)
:: C.Signal dom (Df.Data (Maybe a), Df.Ack a)
-> C.Signal dom (Df.Ack (Maybe a), Df.Data a)
|
8 | catMaybes = Circuit (C.unbundle . go . C.bundle)
| ^^
Expand All @@ -219,8 +219,8 @@ 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)
:: (Df.Data (Maybe a), Df.Ack a)
-> (Df.Ack (Maybe a), Df.Data a)
|
8 | catMaybes = Circuit (C.unbundle . fmap go . C.bundle)
| ^^
Expand All @@ -230,19 +230,19 @@ CatMaybes.hs:8:40: error:
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)
go (Df.NoData, _) = (Df.Ack False, Df.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)
go (Df.Data Nothing, _) = (Df.Ack True, Df.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)
go (Df.Data (Just d), Df.Ack ack) = (Df.Ack ack, Df.Data d)
```

### Testing
Expand All @@ -268,7 +268,7 @@ genCatMaybesInput =

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)!
For `Df` circuits we can define a pretty strong property: a `Circuit (Df dom a) (Df 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 (Df dom (Maybe a)) (Df 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:

Expand All @@ -292,7 +292,7 @@ prop_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:
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 `Df` protocol and whether it is (functionally) equivalent to its pure model. To actually run the tests we need some more boilerplate:



Expand Down Expand Up @@ -345,13 +345,13 @@ 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.
Writing a `Df` 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)
- go (Df.Data Nothing, _) = (Df.Ack True, Df.NoData)
+ go (Df.Data Nothing, _) = (Df.Ack False, Df.NoData)
```

Rerunning the tests will give us a big error, which starts out as:
Expand Down Expand Up @@ -448,8 +448,8 @@ The test tells us that no output was sampled, even though it expected to sample
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)
- go (Df.Data (Just d), Df.Ack ack) = (Df.Ack ack, Df.Data d)
+ go (Df.Data (Just d), Df.Ack ack) = (Df.Ack True, Df.Data d)
```

Again, we get a pretty big error report. Let's skip right to the interesting bits:
Expand All @@ -476,15 +476,15 @@ 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.)
In this case, Hedgehog pretty much constrained us to pretty much one case in our implementation: the one where it matches on `Df.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:
At this point it might be tempting to use `Df.forceAckLow` to force proper reset behavior. To do so, apply the patch:

```diff
- catMaybes :: Circuit (Dfs dom (Maybe a)) (Dfs dom a)
- catMaybes :: Circuit (Df dom (Maybe a)) (Df 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
+ catMaybes :: C.HiddenClockResetEnable dom => Circuit (Df dom (Maybe a)) (Df dom a)
+ catMaybes = Df.forceAckLow |> Circuit (C.unbundle . fmap go . C.bundle
```

Because our function is now stateful, we also need to change the test to:
Expand Down Expand Up @@ -551,10 +551,6 @@ instead, this would have mean that the circuit would be stalled for _4_ cycles o
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.


Expand All @@ -563,7 +559,7 @@ Check out [tests/Tests/Protocols/Plugin.hs](https://github.com/clash-lang/clash-

# Project goals

- Include basic dataflow protocols (e.g., `Df`/`Dfs`) and industry supported ones (e.g., AMBA AXI)
- Include basic protocols (e.g., `Df`) 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
Expand All @@ -581,7 +577,7 @@ No formal guidelines yet, but feel free to open a PR!

- [x] README
- [x] Add more convenient functions: `fanin`, `roundrobin`, ..
- [ ] Make `Dfs` base implementation instead of `Df` (performance / cleanliness)
- [x] Make `DfLike` base implementation instead of `Df` (performance / cleanliness)
- [x] Decide what to do with `Protocols.Ack`
- [ ] Check dead doc links on CI
- [x] Upstream all changes to `circuit-notation` (where possible)
Expand All @@ -591,7 +587,7 @@ No formal guidelines yet, but feel free to open a PR!

0.2

- [ ] Make DSL plugin work with GHC 8.10
- [x] Make DSL plugin work with GHC 8.10 ([github.com/cchalmers/circuit-notation/pull/9](https://github.com/cchalmers/circuit-notation/pull/9))
- [ ] AXI AMBA (in terms of `DfLike`!)
- [ ] Test framework for "chunked" designs
- [ ] Improve errors for multichannel tests
Expand Down
6 changes: 5 additions & 1 deletion cabal.project
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
packages:
clash-protocols.cabal
deps/circuit-notation/circuit-notation.cabal

package clash-prelude
-- 'large-tuples' generates tuple instances for various classes up to the
Expand All @@ -9,6 +8,11 @@ package clash-prelude
-- it by default. This will be the default for Clash >=1.4.
flags: -large-tuples

source-repository-package
type: git
location: https://github.com/cchalmers/circuit-notation.git
tag: 0fe897cb95bd1be87abed044f4072f104dec2f7d

source-repository-package
type: git
location: https://github.com/martijnbastiaan/haskell-hedgehog.git
Expand Down
9 changes: 3 additions & 6 deletions clash-protocols.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,7 @@ description:
Suggested reading order:
.
* 'Protocols' + README.md
* 'Protocols.Df.Simple'
* 'Protocols.DfLike'
* 'Protocols.Df'
* 'Protocols.Plugin'
* 'Protocols.Hedgehog'

Expand Down Expand Up @@ -83,8 +82,8 @@ common common-options

default-language: Haskell2010
build-depends:
-- GHC >= 8.6
base >= 4.12.0.0,
-- GHC >= 8.10
base >= 4.14.0.0,
Cabal,

-- clash-prelude will set suitable version bounds for the plugins
Expand Down Expand Up @@ -140,7 +139,6 @@ library
Protocols
Protocols.Df
Protocols.DfLike
Protocols.Df.Simple
Protocols.Hedgehog
Protocols.Hedgehog.Internal
Protocols.Internal
Expand All @@ -167,7 +165,6 @@ test-suite unittests
other-modules:
Tests.Protocols
Tests.Protocols.Df
Tests.Protocols.Df.Simple
Tests.Protocols.Plugin

Util
Expand Down
1 change: 0 additions & 1 deletion deps/circuit-notation
Submodule circuit-notation deleted from 8f6348
4 changes: 1 addition & 3 deletions src/Protocols.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ i.e. using:
import Protocols
@
Definitions of 'Circuit', 'Fwd', 'Bwd', 'Protocols.Dfs.Dfs', inspired by
Definitions of 'Circuit', 'Fwd', 'Bwd', 'Protocols.Df.Df', inspired by
definitions in @circuit-notation@ at <https://github.com/cchalmers/circuit-notation>.
-}

Expand All @@ -23,7 +23,6 @@ module Protocols

-- * Protocol types
, Df
, Dfs

-- * Basic circuits
, idC
Expand Down Expand Up @@ -54,4 +53,3 @@ module Protocols
import Data.Default (def)
import Protocols.Internal
import Protocols.Df (Df)
import Protocols.Df.Simple (Dfs)
Loading

0 comments on commit 9795f14

Please sign in to comment.