clash-prelude-0.8: src/CLaSH/Prelude/DataFlow.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Safe #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-|
Copyright : (C) 2013-2015, University of Twente
License : BSD2 (see the file LICENSE)
Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>
Self-synchronising circuits based on data-flow principles.
-}
module CLaSH.Prelude.DataFlow
( -- * Data types
DataFlow
, DataFlow'
, df
-- * Creating DataFlow circuits
, liftDF
, mealyDF
, mooreDF
-- * Composition combinators
, idDF
, seqDF
, firstDF
, swapDF
, secondDF
, parDF
, loopDF
-- * Lock-Step operation
, lockStep
, stepLock
)
where
import GHC.TypeLits (KnownNat, KnownSymbol)
import CLaSH.Signal ((.&&.), regEn, unbundle)
import CLaSH.Signal.Bundle (Bundle (..))
import CLaSH.Signal.Explicit (Clock (..), Signal', SystemClock, sclock)
{- | 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.
-}
newtype DataFlow' clk iEn oEn i o
= DF
{ -- | Create an ordinary circuit from a 'DataFlow' circuit
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.
)
}
-- | Dataflow circuit synchronised to the 'SystemClock'.
type DataFlow iEn oEn i o = DataFlow' SystemClock iEn oEn 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.
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
liftDF = DF
-- | Create a 'DataFlow' circuit from a Mealy machine description as those of
-- "CLaSH.Prelude.Mealy"
mealyDF :: (s -> i -> (s,o))
-> s
-> DataFlow Bool Bool i o
mealyDF f iS = DF (\i iV oR -> let en = iV .&&. oR
(s',o) = unbundle (f <$> s <*> i)
s = regEn iS en s'
in (o,iV,oR))
-- | Create a 'DataFlow' circuit from a Moore machine description as those of
-- "CLaSH.Prelude.Moore"
mooreDF :: (s -> i -> s)
-> (s -> o)
-> s
-> DataFlow Bool Bool i o
mooreDF ft fo iS = DF (\i iV oR -> let en = iV .&&. oR
s' = ft <$> s <*> i
s = regEn iS en s'
o = fo <$> s
in (o,iV,oR))
-- | Identity circuit
--
-- <<doc/idDF.svg>>
idDF :: DataFlow' clk en en a a
idDF = DF (\a val rdy -> (a,val,rdy))
-- | Sequential composition of two 'DataFlow' circuits.
--
-- <<doc/seqDF.svg>>
seqDF :: DataFlow' clk aEn bEn a b
-> DataFlow' clk bEn cEn b c
-> DataFlow' clk aEn cEn a c
(DF f) `seqDF` (DF g) = DF (\a aVal cRdy -> let (b,bVal,aRdy) = f a aVal bRdy
(c,cVal,bRdy) = g b bVal cRdy
in (c,cVal,aRdy))
-- | Apply the circuit to the first halve of the communication channels, leave
-- the second halve unchanged.
--
-- <<doc/firstDF.svg>>
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)
firstDF (DF f) = DF (\ac acV bcR -> let clk = sclock
(a,c) = unbundle' clk ac
(aV,cV) = unbundle' clk acV
(bR,cR) = unbundle' clk bcR
(b,bV,aR) = f a aV bR
bc = bundle' clk (b,c)
bcV = bundle' clk (bV,cV)
acR = bundle' clk (aR,cR)
in (bc,bcV,acR)
)
-- | Swap the two communication channels.
--
-- <<doc/swapDF.svg>>
swapDF :: DataFlow' ('Clk nm rate) (aEn,bEn) (bEn,aEn) (a,b) (b,a)
swapDF = DF (\ab abV baR -> (swap <$> ab, swap <$> abV, swap <$> baR))
where
swap ~(a,b) = (b,a)
-- | Apply the circuit to the second halve of the communication channels, leave
-- the first halve unchanged.
--
-- <<doc/secondDF.svg>>
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)
secondDF f = swapDF `seqDF` firstDF f `seqDF` swapDF
-- | Compose two 'DataFlow' circuits in parallel.
--
-- <<doc/parDF.svg>>
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)
f `parDF` g = firstDF f `seqDF` secondDF g
-- | 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.
--
-- <<doc/loopDF.svg>>
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
loopDF f = loopDF' h
where
h :: DataFlow' ('Clk nm rate) (Bool,Bool) (Bool,Bool) (a,d) (b,d)
h = lockStep `seqDF` f `seqDF` stepLock
loopDF' :: DataFlow' ('Clk nm rate) (Bool,Bool) (Bool,Bool) (a,d) (b,d)
-> DataFlow' ('Clk nm rate) Bool Bool a b
loopDF' (DF f') = DF (\a aV bR -> let clk = sclock
(bd,bdV,adR) = f' ad adV bdR
(b,d) = unbundle' clk bd
(bV,dV) = unbundle' clk bdV
(aR,dR) = unbundle' clk adR
ad = bundle' clk (a,d)
adV = bundle' clk (aV,dV)
bdR = bundle' clk (bR,dR)
in (b,bV,aR)
)
-- | Have parallel compositions operate in lock-step.
class LockStep a b where
-- | 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
-- @
--
-- <<doc/lockStep.svg>>
--
-- 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.
lockStep :: (KnownNat rate,KnownSymbol nm)
=> DataFlow' ('Clk nm rate) a Bool b b
-- | 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)
-- @
--
-- <<doc/stepLock.svg>>
--
-- 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.
stepLock :: (KnownNat rate,KnownSymbol nm)
=> DataFlow' ('Clk nm rate) Bool a b b
instance LockStep Bool c where
lockStep = idDF
stepLock = idDF
instance (LockStep a x, LockStep b y) => LockStep (a,b) (x,y) where
lockStep = (lockStep `parDF` lockStep) `seqDF`
(DF (\xy xyV rdy -> let clk = sclock
(xV,yV) = unbundle' clk xyV
val = xV .&&. yV
xR = yV .&&. rdy
yR = xV .&&. rdy
xyR = bundle' clk (xR,yR)
in (xy,val,xyR)))
stepLock = (DF (\xy val xyR -> let clk = sclock
(xR,yR) = unbundle' clk xyR
rdy = xR .&&. yR
xV = val .&&. yR
yV = val .&&. xR
xyV = bundle' clk (xV,yV)
in (xy,xyV,rdy))) `seqDF` (stepLock `parDF` stepLock)