CLaSH.Prelude.DataFlow

Self-synchronising circuits based on data-flow principles.

Data types

type DataFlow iEn oEn i o = DataFlow' SystemClock iEn oEn i o

Dataflow circuit synchronised to the SystemClock.

data DataFlow' clk 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' clk iEn oEn i o
  = DF
  { df :: Signal' clk i     -- Incoming data
       -> Signal' clk iEn   -- Flagged with valid bits iEn.
       -> Signal' clk oEn   -- Incoming back-pressure, ready edge.
       -> ( Signal' clk o   -- Outgoing data.
          , Signal' clk oEn -- Flagged with valid bits oEn.
          , Signal' clk iEn -- Outgoing back-pressure, ready edge.
          )
  }

where:

• clk 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.

df :: DataFlow' clk iEn oEn i o -> Signal' clk i -> Signal' clk iEn -> Signal' clk oEn -> (Signal' clk o, Signal' clk oEn, Signal' clk iEn)

Create an ordinary circuit from a DataFlow circuit

Creating DataFlow circuits

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

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

Signal' clk i        -- Incoming data.
-> Signal' clk Bool  -- Flagged with a single valid bit.
-> Signal' clk Bool  -- Incoming back-pressure, ready bit.
-> ( Signal' clk o   -- Outgoing data.
   , Signal' clk oEn -- Flagged with a single valid bit.
   , Signal' clk 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.

mealyDF :: (s -> i -> (s, o)) -> s -> DataFlow Bool Bool i o

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

mooreDF :: (s -> i -> s) -> (s -> o) -> s -> DataFlow Bool Bool i o

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

Composition combinators

idDF :: DataFlow' clk en en a a

Identity circuit

seqDF :: DataFlow' clk aEn bEn a b -> DataFlow' clk bEn cEn b c -> DataFlow' clk aEn cEn a c

Sequential composition of two DataFlow circuits.

firstDF :: (KnownSymbol nm, KnownNat rate) => DataFlow' (Clk nm rate) aEn bEn a b -> DataFlow' (Clk nm rate) (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' (Clk nm rate) (aEn, bEn) (bEn, aEn) (a, b) (b, a)

Swap the two communication channels.

secondDF :: (KnownSymbol nm, KnownNat rate) => DataFlow' (Clk nm rate) aEn bEn a b -> DataFlow' (Clk nm rate) (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 :: (KnownSymbol nm, KnownNat rate) => DataFlow' (Clk nm rate) aEn bEn a b -> DataFlow' (Clk nm rate) cEn dEn c d -> DataFlow' (Clk nm rate) (aEn, cEn) (bEn, dEn) (a, c) (b, d)

Compose two DataFlow circuits in parallel.

loopDF :: forall nm rate a b d. (KnownSymbol nm, KnownNat rate) => DataFlow' (Clk nm rate) Bool Bool (a, d) (b, d) -> DataFlow' (Clk nm rate) Bool Bool a b

Feed back the second halve of the communication channel.

Given:

f `seqDF` (loopDF h) `seqDF` g

The circuits f, h, and g, will operate in lock-step. Which means that there it only progress when all three circuits are producing valid data and all three circuits are ready to receive new data. The loopDF function uses the lockStep and stepLock functions to achieve the lock-step operation.

Lock-Step operation

lockStep :: (LockStep a b, KnownNat rate, KnownSymbol nm) => DataFlow' (Clk nm rate) 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 that 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 :: (LockStep a b, KnownNat rate, KnownSymbol nm) => DataFlow' (Clk nm rate) 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 that 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` lockStep `seqDF` q

Does the right thing.