module CLaSH.Prelude.Synchronizer
(
dualFlipFlopSynchronizer
, asyncFIFOSynchronizer
)
where
import Control.Applicative (liftA2)
import Data.Bits (complement, shiftR, xor)
import Data.Constraint ((:-)(..), Dict (..))
#if MIN_VERSION_constraints(0,9,0)
import Data.Constraint.Nat (leTrans)
#else
import Unsafe.Coerce
#endif
import Data.Maybe (isJust)
import GHC.TypeLits (type (+), type (), type (<=))
import CLaSH.Class.BitPack (boolToBV)
import CLaSH.Class.Resize (truncateB)
import CLaSH.Prelude.BitIndex (slice)
import CLaSH.Prelude.Mealy (mealyB')
import CLaSH.Prelude.RAM (asyncRam')
import CLaSH.Promoted.Nat (SNat (..), pow2SNat)
import CLaSH.Promoted.Nat.Literals (d0)
import CLaSH.Signal (mux)
import CLaSH.Signal.Explicit (Signal', SClock, register',
unsafeSynchronizer)
import CLaSH.Sized.BitVector (BitVector, (++#))
dualFlipFlopSynchronizer :: SClock clk1
-> SClock clk2
-> a
-> Signal' clk1 a
-> Signal' clk2 a
dualFlipFlopSynchronizer clk1 clk2 i = register' clk2 i
. register' clk2 i
. unsafeSynchronizer clk1 clk2
fifoMem ::
SClock wclk
-> SClock rclk
-> SNat addrSize
-> Signal' wclk Bool
-> Signal' rclk (BitVector addrSize)
-> Signal' wclk (Maybe (BitVector addrSize, a))
-> Signal' rclk a
fifoMem wclk rclk addrSize@SNat full raddr writeM =
asyncRam' wclk rclk
(pow2SNat addrSize)
raddr
(mux full (pure Nothing) writeM)
ptrCompareT :: SNat addrSize
-> (BitVector (addrSize + 1) -> BitVector (addrSize + 1) -> Bool)
-> (BitVector (addrSize + 1), BitVector (addrSize + 1), Bool)
-> (BitVector (addrSize + 1), Bool)
-> ((BitVector (addrSize + 1), BitVector (addrSize + 1), Bool)
,(Bool, BitVector addrSize, BitVector (addrSize + 1)))
ptrCompareT SNat flagGen (bin,ptr,flag) (s_ptr,inc) = ((bin',ptr',flag')
,(flag,addr,ptr))
where
bin' = bin + boolToBV (inc && not flag)
ptr' = (bin' `shiftR` 1) `xor` bin'
addr = truncateB bin
flag' = flagGen ptr' s_ptr
isFull :: forall addrSize .
(2 <= addrSize)
=> SNat addrSize
-> BitVector (addrSize + 1)
-> BitVector (addrSize + 1)
-> Bool
isFull addrSize@SNat ptr s_ptr = case leTrans @1 @2 @addrSize of
Sub Dict ->
let a1 = SNat @(addrSize 1)
a2 = SNat @(addrSize 2)
in ptr == (complement (slice addrSize a1 s_ptr) ++# slice a2 d0 s_ptr)
asyncFIFOSynchronizer
:: (2 <= addrSize)
=> SNat addrSize
-> SClock wclk
-> SClock rclk
-> Signal' rclk Bool
-> Signal' wclk (Maybe a)
-> (Signal' rclk a, Signal' rclk Bool, Signal' wclk Bool)
asyncFIFOSynchronizer addrSize@SNat wclk rclk rinc wdataM = (rdata,rempty,wfull)
where
s_rptr = dualFlipFlopSynchronizer rclk wclk 0 rptr
s_wptr = dualFlipFlopSynchronizer wclk rclk 0 wptr
rdata = fifoMem wclk rclk addrSize wfull raddr
(liftA2 (,) <$> (pure <$> waddr) <*> wdataM)
(rempty,raddr,rptr) = mealyB' rclk (ptrCompareT addrSize (==)) (0,0,True)
(s_wptr,rinc)
(wfull,waddr,wptr) = mealyB' wclk (ptrCompareT addrSize (isFull addrSize))
(0,0,False) (s_rptr,isJust <$> wdataM)
#if !MIN_VERSION_constraints(0,9,0)
axiom :: forall a b . Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
axiomLe :: forall a b. Dict (a <= b)
axiomLe = axiom
leTrans :: forall a b c. (b <= c, a <= b) :- (a <= c)
leTrans = Sub (axiomLe @a @c)
#endif