Clash.Prelude.DataFlow

Self-synchronising circuits based on data-flow principles.

Data types

newtype DataFlow domain iEn oEn i o

Dataflow circuit with bidirectional synchronisation 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 clock to which the circuit is synchronised.
• iEn is the type of the bidirectional incoming synchronisation channel.
• oEn is the type of the bidirectional outgoing synchronisation 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 parametrise in the types of the synchronisation channels.

Constructors

DF

Fields

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

  Create an ordinary circuit from a DataFlow circuit

Creating DataFlow circuits

liftDF :: (Signal dom i -> Signal dom Bool -> Signal dom Bool -> (Signal dom o, Signal dom Bool, Signal dom Bool)) -> DataFlow dom Bool Bool i o

Dataflow circuit synchronised 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 :: (i -> o) -> DataFlow dom Bool Bool i o

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

mealyDF :: Clock domain gated -> Reset domain synchronous -> (s -> i -> (s, o)) -> s -> DataFlow domain Bool Bool i o

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

mooreDF :: Clock domain gated -> Reset domain synchronous -> (s -> i -> s) -> (s -> o) -> s -> DataFlow domain Bool Bool i o

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

fifoDF

Arguments

:: (KnownNat addrSize, KnownNat n, KnownNat m, (m + n) ~ (2 ^ addrSize))

=> Clock domain gated

-> Reset domain synchronous

-> 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 initialised with undefined.

-> DataFlow domain 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 :: DataFlow dom en en a a

Identity circuit

seqDF :: DataFlow dom aEn bEn a b -> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c

Sequential composition of two DataFlow circuits.

firstDF :: DataFlow dom aEn bEn a b -> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)

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

swapDF :: DataFlow dom (aEn, bEn) (bEn, aEn) (a, b) (b, a)

Swap the two communication channels.

secondDF :: DataFlow dom aEn bEn a b -> DataFlow dom (cEn, aEn) (cEn, bEn) (c, a) (c, b)

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

parDF :: DataFlow dom aEn bEn a b -> DataFlow dom cEn dEn c d -> DataFlow dom (aEn, cEn) (bEn, dEn) (a, c) (b, d)

Compose two DataFlow circuits in parallel.

parNDF :: KnownNat n => Vec n (DataFlow dom aEn bEn a b) -> DataFlow dom (Vec n aEn) (Vec n bEn) (Vec n a) (Vec n b)

Compose n DataFlow circuits in parallel.

loopDF

Arguments

:: (KnownNat m, KnownNat n, KnownNat addrSize, (m + n) ~ (2 ^ addrSize))

=> Clock dom gated

-> Reset dom synchronous

-> 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 initialised 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 synchronisation channels:

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

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

loopDF d4 Nil h

When you have a circuit h', with only a single synchronisation 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 synchronisation 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 :: 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. Unlike loopDF, the feedback loop is not buffered.

Lock-Step operation

class LockStep a b where

Reduce or extend the synchronisation granularity of parallel compositions.

Minimal complete definition

lockStep, stepLock

Methods

lockStep :: DataFlow dom a Bool b b

Reduce the synchronisation granularity to a single Boolean 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 synchronisation 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 synchronisation signals are properly connected:

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

Note 1: ensure that the components that you are synchronising have buffered/delayed ready and valid signals, or lockStep has the potential to introduce combinational loops. You can do this by placing fifoDFs 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 :: DataFlow dom Bool a b b

Extend the synchronisation granularity from a single Boolean 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 synchronisation 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 synchronisation signals are properly connected:

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

Note 1: ensure that the components that you are synchronising have buffered/delayed ready and valid signals, or stepLock has the potential to introduce combinational loops. You can do this by placing fifoDFs 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

LockStep Bool c

Methods

lockStep :: DataFlow dom Bool Bool c c

stepLock :: DataFlow dom Bool Bool c c

(LockStep a x, LockStep b y) => LockStep (a, b) (x, y)

Methods

lockStep :: DataFlow dom (a, b) Bool (x, y) (x, y)

stepLock :: DataFlow dom Bool (a, b) (x, y) (x, y)

(LockStep en a, KnownNat n) => LockStep (Vec n en) (Vec n a)

Methods

lockStep :: DataFlow dom (Vec n en) Bool (Vec n a) (Vec n a)

stepLock :: DataFlow dom Bool (Vec n en) (Vec n a) (Vec n a)