Safe Haskell | None |
---|---|
Language | Haskell2010 |
Self-synchronising circuits based on data-flow principles.
- data DataFlow clk iEn oEn i o
- type DataFlow' iEn oEn i o = DataFlow SystemClock iEn oEn i o
- df :: DataFlow clk iEn oEn i o -> CSignal clk i -> CSignal clk iEn -> CSignal clk oEn -> (CSignal clk o, CSignal clk oEn, CSignal clk iEn)
- liftDF :: (CSignal clk i -> CSignal clk Bool -> CSignal clk Bool -> (CSignal clk o, CSignal clk Bool, CSignal clk Bool)) -> DataFlow clk Bool Bool i o
- mealyDF :: (s -> i -> (s, o)) -> s -> DataFlow' Bool Bool i o
- idDF :: DataFlow clk en en a a
- seqDF :: DataFlow clk aEn bEn a b -> DataFlow clk bEn cEn b c -> DataFlow clk aEn cEn a c
- 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)
- swapDF :: (KnownSymbol nm, KnownNat rate) => DataFlow (Clk nm rate) (aEn, bEn) (bEn, aEn) (a, b) (b, a)
- 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)
- 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)
- 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
- lockStep :: (LockStep a b, KnownNat rate, KnownSymbol nm) => DataFlow (Clk nm rate) a Bool b b
- stepLock :: (LockStep a b, KnownNat rate, KnownSymbol nm) => DataFlow (Clk nm rate) Bool a b b
Data types
data DataFlow clk iEn oEn i o Source
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 :: CSignal clk i -- Incoming data -> CSignal clk iEn -- Flagged with valid bitsiEn
. -> CSignal clk oEn -- Incoming back-pressure, ready edge. -> ( CSignal clk o -- Outgoing data. , CSignal clk oEn -- Flagged with valid bitsoEn
. , CSignal 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.
type DataFlow' iEn oEn i o = DataFlow SystemClock iEn oEn i o Source
Dataflow circuit synchronised to the SystemClock
.
df :: DataFlow clk iEn oEn i o -> CSignal clk i -> CSignal clk iEn -> CSignal clk oEn -> (CSignal clk o, CSignal clk oEn, CSignal clk iEn) Source
Create an ordinary circuit from a DataFlow
circuit
Creating DataFlow circuits
liftDF :: (CSignal clk i -> CSignal clk Bool -> CSignal clk Bool -> (CSignal clk o, CSignal clk Bool, CSignal clk Bool)) -> DataFlow clk Bool Bool i o Source
Create a DataFlow
circuit from a circuit description with the appropriate
type:
CSignal clk i -- Incoming data. -> CSignal clk Bool -- Flagged with a single /valid/ bit. -> CSignal clk Bool -- Incoming back-pressure, /ready/ bit. -> ( CSignal clk o -- Outgoing data. , CSignal clk oEn -- Flagged with a single /valid/ bit. , CSignal 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 Source
Create a DataFlow
circuit from a Mealy machine description as those of
CLaSH.Prelude.Mealy
Composition combinators
seqDF :: DataFlow clk aEn bEn a b -> DataFlow clk bEn cEn b c -> DataFlow clk aEn cEn a c Source
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) Source
Apply the circuit to the first halve of the communication channels, leave the second halve unchanged.
swapDF :: (KnownSymbol nm, KnownNat rate) => DataFlow (Clk nm rate) (aEn, bEn) (bEn, aEn) (a, b) (b, a) Source
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) Source
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) Source
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 Source
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 Source
Reduce the synchronisation 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 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 Source
Extend the synchronisation 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 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.