clash-prelude-1.8.4: Clash: a functional hardware description language - Prelude library

Copyright | (C) 2013-2016 University of Twente 2017 Google Inc. 2019 Myrtle Software Ltd 2021 QBayLogic B.V.
License | BSD2 (see the file LICENSE)
Maintainer | QBayLogic B.V. <devops@qbaylogic.com>
Safe Haskell | Safe
Language | Haskell2010

Extensions

- MonoLocalBinds
- ScopedTypeVariables
- BangPatterns
- TypeFamilies
- ViewPatterns
- DataKinds
- InstanceSigs
- StandaloneDeriving
- DeriveDataTypeable
- DeriveFunctor
- DeriveTraversable
- DeriveFoldable
- DeriveGeneric
- DefaultSignatures
- DeriveLift
- DerivingStrategies
- TypeSynonymInstances
- FlexibleInstances
- ConstrainedClassMethods
- MultiParamTypeClasses
- MagicHash
- KindSignatures
- PostfixOperators
- TupleSections
- TypeOperators
- ExplicitNamespaces
- ExplicitForAll
- BinaryLiterals
- TypeApplications

Clash.Prelude.DataFlow

Contents

- Data types
- Creating DataFlow circuits
- Composition combinators
- Lock-Step operation

Description

Deprecated: Module will be removed in Clash 1.10 in favor of clash-protocols. See: https://github.com/clash-lang/clash-protocols/.

Self-synchronizing circuits based on data-flow principles.

Synopsis

- newtype DataFlow (dom :: Domain) iEn oEn i o = DF {
  - df :: Signal dom i -> Signal dom iEn -> Signal dom oEn -> (Signal dom o, Signal dom oEn, Signal dom iEn)
  }
- liftDF :: forall (dom :: Domain) i o. (Signal dom i -> Signal dom Bool -> Signal dom Bool -> (Signal dom o, Signal dom Bool, Signal dom Bool)) -> DataFlow dom Bool Bool i o
- pureDF :: forall i o (dom :: Domain). (i -> o) -> DataFlow dom Bool Bool i o
- mealyDF :: forall (dom :: Domain) s i o. (KnownDomain dom, NFDataX s) => Clock dom -> Reset dom -> Enable dom -> (s -> i -> (s, o)) -> s -> DataFlow dom Bool Bool i o
- mooreDF :: forall (dom :: Domain) s i o. (KnownDomain dom, NFDataX s) => Clock dom -> Reset dom -> Enable dom -> (s -> i -> s) -> (s -> o) -> s -> DataFlow dom Bool Bool i o
- fifoDF :: forall (addrSize :: Nat) (m :: Nat) (n :: Nat) a (dom :: Domain). (KnownDomain dom, NFDataX a, KnownNat addrSize, KnownNat n, KnownNat m, (m + n) ~ (2 ^ addrSize)) => Clock dom -> Reset dom -> Enable dom -> SNat (m + n) -> Vec m a -> DataFlow dom Bool Bool a a
- idDF :: forall (dom :: Domain) en a. DataFlow dom en en a a
- seqDF :: forall (dom :: Domain) aEn bEn a b cEn c. DataFlow dom aEn bEn a b -> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c
- firstDF :: forall (dom :: Domain) aEn bEn a b cEn c. DataFlow dom aEn bEn a b -> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)
- swapDF :: forall (dom :: Domain) aEn bEn a b. DataFlow dom (aEn, bEn) (bEn, aEn) (a, b) (b, a)
- secondDF :: forall (dom :: Domain) aEn bEn a b cEn c. DataFlow dom aEn bEn a b -> DataFlow dom (cEn, aEn) (cEn, bEn) (c, a) (c, b)
- parDF :: forall (dom :: Domain) aEn bEn a b cEn dEn c d. DataFlow dom aEn bEn a b -> DataFlow dom cEn dEn c d -> DataFlow dom (aEn, cEn) (bEn, dEn) (a, c) (b, d)
- parNDF :: forall (n :: Nat) (dom :: Domain) aEn bEn a b. KnownNat n => Vec n (DataFlow dom aEn bEn a b) -> DataFlow dom (Vec n aEn) (Vec n bEn) (Vec n a) (Vec n b)
- loopDF :: forall (dom :: Domain) d (m :: Nat) (n :: Nat) (addrSize :: Nat) a b. (KnownDomain dom, NFDataX d, KnownNat m, KnownNat n, KnownNat addrSize, (m + n) ~ (2 ^ addrSize)) => Clock dom -> Reset dom -> Enable dom -> SNat (m + n) -> Vec m d -> DataFlow dom (Bool, Bool) (Bool, Bool) (a, d) (b, d) -> DataFlow dom Bool Bool a b
- loopDF_nobuf :: forall (dom :: Domain) a d b. DataFlow dom (Bool, Bool) (Bool, Bool) (a, d) (b, d) -> DataFlow dom Bool Bool a b
- class LockStep a b where
  - lockStep :: forall (dom :: Domain). DataFlow dom a Bool b b
  - stepLock :: forall (dom :: Domain). DataFlow dom Bool a b b

# Data types

newtype DataFlow (dom :: Domain) iEn oEn i o Source #

Dataflow circuit with bidirectional synchronization channels.

In the forward direction we assert validity of the data. In the backward direction we assert that the circuit is ready to receive new data. A circuit adhering to the `DataFlow` type should:

- Not consume data when validity is deasserted.
- Only update its output when readiness is asserted.

The `DataFlow` type is defined as:

    newtype DataFlow' dom iEn oEn i o
      = DF
      { df :: Signal dom i     -- Incoming data
           -> Signal dom iEn   -- Flagged with /valid/ bits @iEn@.
           -> Signal dom oEn   -- Incoming back-pressure, /ready/ edge.
           -> ( Signal dom o   -- Outgoing data.
              , Signal dom oEn -- Flagged with /valid/ bits @oEn@.
              , Signal dom iEn -- Outgoing back-pressure, /ready/ edge.
              )
      }

where:

- `dom` is the domain to which the circuit is synchronized.
- `iEn` is the type of the bidirectional incoming synchronization channel.
- `oEn` is the type of the bidirectional outgoing synchronization channel.
- `i` is the incoming data type.
- `o` is the outgoing data type.

We define several composition operators for our `DataFlow` circuits:

- `seqDF` sequential composition.
- `parDF` parallel composition.
- `loopDF` add a feedback arc.
- `lockStep` proceed in lock-step.

When you look at the types of the above operators it becomes clear why we parametrize in the types of the synchronization channels.

Constructors

DF |

Fields

- df :: Signal dom i -> Signal dom iEn -> Signal dom oEn -> (Signal dom o, Signal dom oEn, Signal dom iEn)

  Create an ordinary circuit from a `DataFlow` circuit

# Creating DataFlow circuits

liftDF :: forall (dom :: Domain) i o. (Signal dom i -> Signal dom Bool -> Signal dom Bool -> (Signal dom o, Signal dom Bool, Signal dom Bool)) -> DataFlow dom Bool Bool i o Source #

Dataflow circuit synchronized to the `systemClockGen`. type DataFlow iEn oEn i o = DataFlow' systemClockGen iEn oEn i o

Create a `DataFlow` circuit from a circuit description with the appropriate type:

    Signal dom i        -- Incoming data.
    -> Signal dom Bool  -- Flagged with a single /valid/ bit.
    -> Signal dom Bool  -- Incoming back-pressure, /ready/ bit.
    -> ( Signal dom o   -- Outgoing data.
       , Signal dom oEn -- Flagged with a single /valid/ bit.
       , Signal dom iEn -- Outgoing back-pressure, /ready/ bit.
       )

A circuit adhering to the `DataFlow` type should:

- Not consume data when validity is deasserted.
- Only update its output when readiness is asserted.

pureDF :: forall i o (dom :: Domain). (i -> o) -> DataFlow dom Bool Bool i o Source #

Create a `DataFlow` circuit where the given function `f` operates on the data, and the synchronization channels are passed unaltered.

mealyDF :: forall (dom :: Domain) s i o. (KnownDomain dom, NFDataX s) => Clock dom -> Reset dom -> Enable dom -> (s -> i -> (s, o)) -> s -> DataFlow dom Bool Bool i o Source #

Create a `DataFlow` circuit from a Mealy machine description as those of Clash.Prelude.Mealy

mooreDF :: forall (dom :: Domain) s i o. (KnownDomain dom, NFDataX s) => Clock dom -> Reset dom -> Enable dom -> (s -> i -> s) -> (s -> o) -> s -> DataFlow dom Bool Bool i o Source #

Create a `DataFlow` circuit from a Moore machine description as those of Clash.Prelude.Moore

fifoDF Source #

Arguments

:: forall (addrSize :: Nat) (m :: Nat) (n :: Nat) a (dom :: Domain). (KnownDomain dom, NFDataX a, KnownNat addrSize, KnownNat n, KnownNat m, (m + n) ~ (2 ^ addrSize)) |
=> Clock dom |
-> Reset dom |
-> Enable dom |
-> SNat (m + n) | Depth of the FIFO buffer. Must be a power of two.
-> Vec m a | Initial content. Can be smaller than the size of the FIFO. Empty spaces are initialized with `undefined`.
-> DataFlow dom Bool Bool a a |

Create a FIFO buffer adhering to the `DataFlow` protocol. Can be filled with initial content.

To create a FIFO of size 4, with two initial values 2 and 3 you would write:

    fifo4 = fifoDF d4 (2 :> 3 :> Nil)

# Composition combinators

idDF :: forall (dom :: Domain) en a. DataFlow dom en en a a Source #

Identity circuit

seqDF :: forall (dom :: Domain) aEn bEn a b cEn c. DataFlow dom aEn bEn a b -> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c Source #

Sequential composition of two `DataFlow` circuits.

firstDF :: forall (dom :: Domain) aEn bEn a b cEn c. DataFlow dom aEn bEn a b -> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c) Source #

Apply the circuit to the first halve of the communication channels, leave the second halve unchanged.

swapDF :: forall (dom :: Domain) aEn bEn a b. DataFlow dom (aEn, bEn) (bEn, aEn) (a, b) (b, a) Source #

Swap the two communication channels.

secondDF :: forall (dom :: Domain) aEn bEn a b cEn c. DataFlow dom aEn bEn a b -> DataFlow dom (cEn, aEn) (cEn, bEn) (c, a) (c, b) Source #

Apply the circuit to the second halve of the communication channels, leave the first halve unchanged.

parDF :: forall (dom :: Domain) aEn bEn a b cEn dEn c d. DataFlow dom aEn bEn a b -> DataFlow dom cEn dEn c d -> DataFlow dom (aEn, cEn) (bEn, dEn) (a, c) (b, d) Source #

Compose two `DataFlow` circuits in parallel.

parNDF :: forall (n :: Nat) (dom :: Domain) aEn bEn a b. KnownNat n => Vec n (DataFlow dom aEn bEn a b) -> DataFlow dom (Vec n aEn) (Vec n bEn) (Vec n a) (Vec n b) Source #

Compose n `DataFlow` circuits in parallel.

loopDF Source #

Arguments

:: forall (dom :: Domain) d (m :: Nat) (n :: Nat) (addrSize :: Nat) a b. (KnownDomain dom, NFDataX d, KnownNat m, KnownNat n, KnownNat addrSize, (m + n) ~ (2 ^ addrSize)) |
=> Clock dom |
-> Reset dom |
-> Enable dom |
-> SNat (m + n) | Depth of the FIFO buffer. Must be a power of two
-> Vec m d | Initial content of the FIFO buffer. Can be smaller than the size of the FIFO. Empty spaces are initialized with `undefined`.
-> DataFlow dom (Bool, Bool) (Bool, Bool) (a, d) (b, d) |
-> DataFlow dom Bool Bool a b |

Feed back the second halve of the communication channel. The feedback loop is buffered by a `fifoDF` circuit.

So given a circuit h with two synchronization channels:

    h :: DataFlow (Bool,Bool) (Bool,Bool) (a,d) (b,d)

Feeding back the d part (including its synchronization channels) results in:

    loopDF d4 Nil h

When you have a circuit `h'`, with only a single synchronization channel:

    h' :: DataFlow Bool Bool (a,d) (b,d)

and you want to compose h' in a feedback loop, the following will not work:

    f `seqDF` (loopDF d4 Nil h') `seqDF` g

The circuits `f`, `h`, and `g`, must operate in lock-step because the h' circuit only has a single synchronization channel. Consequently, there should only be progress when all three circuits are producing valid data and all three circuits are ready to receive new data. We need to compose h' with the `lockStep` and `stepLock` functions to achieve the lock-step operation.

    f `seqDF` (lockStep `seqDF` loopDF d4 Nil h' `seqDF` stepLock) `seqDF` g

loopDF_nobuf :: forall (dom :: Domain) a d b. DataFlow dom (Bool, Bool) (Bool, Bool) (a, d) (b, d) -> DataFlow dom Bool Bool a b Source #

Feed back the second halve of the communication channel. Unlike `loopDF`, the feedback loop is not buffered.

# Lock-Step operation

class LockStep a b where Source #

Reduce or extend the synchronization granularity of parallel compositions.

Methods

lockStep :: forall (dom :: Domain). DataFlow dom a Bool b b Source #

Reduce the synchronization granularity to a single `Bool`ean value.

Given:

    f :: DataFlow Bool Bool a b
    g :: DataFlow Bool Bool c d
    h :: DataFlow Bool Bool (b,d) (p,q)

We cannot simply write:

    (f `parDF` g) `seqDF` h

because, `f `parDF` g`, has type, ``DataFlow` (Bool,Bool) (Bool,Bool) (a,c) (b,d)`, which does not match the expected synchronization granularity of `h`. We need a circuit in between that has the type:

    DataFlow (Bool,Bool) Bool (b,d) (b,d)

Simply `&&`-ing the valid signals in the forward direction, and duplicating the ready signal in the backward direction is however not enough. We also need to make sure that `f` does not update its output when `g`'s output is invalid and visa versa, as `h` can only consume its input when both `f` and `g` are producing valid data. `g`'s ready port is hence only asserted when `h` is ready and `f` is producing valid data. And `f`'s ready port is only asserted when `h` is ready and `g` is producing valid data. `f` and `g` will hence be proceeding in lock-step.

The `lockStep` function ensures that all synchronization signals are properly connected:

    (f `parDF` g) `seqDF` lockStep `seqDF` h

Note 1: ensure that the components that you are synchronizing have buffered/delayed `ready` and `valid` signals, or `lockStep` has the potential to introduce combinational loops. You can do this by placing `fifoDF`s on the parallel channels. Extending the above example, you would write:

    ((f `seqDF` fifoDF d4 Nil) `parDF` (g `seqDF` fifoDF d4 Nil)) `seqDF` lockStep `seqDF` h

Note 2: `lockStep` works for arbitrarily nested tuples. That is:

    p :: DataFlow Bool Bool ((b,d),d) z

    q :: DataFlow ((Bool,Bool),Bool) ((Bool,Bool),Bool) ((a,c),c) ((b,d),d)
    q = f `parDF` g `parDF` g

    r = q `seqDF` lockStep `seqDF` p

Does the right thing.

stepLock :: forall (dom :: Domain). DataFlow dom Bool a b b Source #

Extend the synchronization granularity from a single `Bool`ean value.

Given:

    f :: DataFlow Bool Bool a b
    g :: DataFlow Bool Bool c d
    h :: DataFlow Bool Bool (p,q) (a,c)

We cannot simply write:

    h `seqDF` (f `parDF` g)

because, `f `parDF` g`, has type, ``DataFlow` (Bool,Bool) (Bool,Bool) (a,c) (b,d)`, which does not match the expected synchronization granularity of `h`. We need a circuit in between that has the type:

    DataFlow Bool (Bool,Bool) (a,c) (a,c)

Simply `&&`-ing the ready signals in the backward direction, and duplicating the valid signal in the forward direction is however not enough. We need to make sure that `f` does not consume values when `g` is not ready and visa versa, because `h` cannot update the values of its output tuple independently. `f`'s valid port is hence only asserted when `h` is valid and `g` is ready to receive new values. `g`'s valid port is only asserted when `h` is valid and `f` is ready to receive new values. `f` and `g` will hence be proceeding in lock-step.

The `stepLock` function ensures that all synchronization signals are properly connected:

    h `seqDF` stepLock `seqDF` (f `parDF` g)

Note 1: ensure that the components that you are synchronizing have buffered/delayed `ready` and `valid` signals, or `stepLock` has the potential to introduce combinational loops. You can do this by placing `fifoDF`s on the parallel channels. Extending the above example, you would write:

    h `seqDF` stepLock `seqDF` ((fifoDF d4 Nil `seqDF` f) `parDF` (fifoDF d4 Nil `seqDF` g))

Note 2: `stepLock` works for arbitrarily nested tuples. That is:

    p :: DataFlow Bool Bool z ((a,c),c)

    q :: DataFlow ((Bool,Bool),Bool) ((Bool,Bool),Bool) ((a,c),c) ((b,d),d)
    q = f `parDF` g `parDF` g

    r = p `seqDF` stepLock `seqDF` q

Does the right thing.

#### Instances

Instances details

LockStep Bool c Source # |
Instance details Defined in Clash.Prelude.DataFlow Methods lockStep :: forall (dom :: Domain). DataFlow dom Bool Bool c c Source # stepLock :: forall (dom :: Domain). DataFlow dom Bool Bool c c Source #
(LockStep en a, KnownNat n) => LockStep (Vec n en) (Vec n a) Source # |
Instance details Defined in Clash.Prelude.DataFlow Methods lockStep :: forall (dom :: Domain). DataFlow dom (Vec n en) Bool (Vec n a) (Vec n a) Source # stepLock :: forall (dom :: Domain). DataFlow dom Bool (Vec n en) (Vec n a) (Vec n a) Source #
(LockStep a x, LockStep b y) => LockStep (a, b) (x, y) Source # |
Instance details Defined in Clash.Prelude.DataFlow Methods lockStep :: forall (dom :: Domain). DataFlow dom (a, b) Bool (x, y) (x, y) Source # stepLock :: forall (dom :: Domain). DataFlow dom Bool (a, b) (x, y) (x, y) Source #