{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Safe #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module Clash.Explicit.Synchronizer
(
dualFlipFlopSynchronizer
, asyncFIFOSynchronizer
)
where
import Control.Applicative (liftA2)
import Data.Bits (complement, shiftR, xor)
import Data.Constraint ((:-)(..), Dict (..))
import Data.Constraint.Nat (leTrans)
import Data.Maybe (isJust)
import GHC.TypeLits (type (+), type (-), type (<=))
import Clash.Class.BitPack (boolToBV)
import Clash.Class.Resize (truncateB)
import Clash.Class.BitPack.BitIndex (slice)
import Clash.Explicit.Mealy (mealyB)
import Clash.Explicit.RAM (asyncRam)
import Clash.Explicit.Signal
(Clock, Reset, Signal, Enable, register, unsafeSynchronizer)
import Clash.Promoted.Nat (SNat (..), pow2SNat)
import Clash.Promoted.Nat.Literals (d0)
import Clash.Signal (mux, KnownDomain)
import Clash.Sized.BitVector (BitVector, (++#))
import Clash.XException (NFDataX)
dualFlipFlopSynchronizer
:: ( NFDataX a
, KnownDomain dom1
, KnownDomain dom2 )
=> Clock dom1
-> Clock dom2
-> Reset dom2
-> Enable dom2
-> a
-> Signal dom1 a
-> Signal dom2 a
dualFlipFlopSynchronizer :: Clock dom1
-> Clock dom2
-> Reset dom2
-> Enable dom2
-> a
-> Signal dom1 a
-> Signal dom2 a
dualFlipFlopSynchronizer Clock dom1
clk1 Clock dom2
clk2 Reset dom2
rst Enable dom2
en a
i =
Clock dom2
-> Reset dom2 -> Enable dom2 -> a -> Signal dom2 a -> Signal dom2 a
forall (dom :: Domain) a.
(KnownDomain dom, NFDataX a) =>
Clock dom
-> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
register Clock dom2
clk2 Reset dom2
rst Enable dom2
en a
i
(Signal dom2 a -> Signal dom2 a)
-> (Signal dom1 a -> Signal dom2 a)
-> Signal dom1 a
-> Signal dom2 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clock dom2
-> Reset dom2 -> Enable dom2 -> a -> Signal dom2 a -> Signal dom2 a
forall (dom :: Domain) a.
(KnownDomain dom, NFDataX a) =>
Clock dom
-> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
register Clock dom2
clk2 Reset dom2
rst Enable dom2
en a
i
(Signal dom2 a -> Signal dom2 a)
-> (Signal dom1 a -> Signal dom2 a)
-> Signal dom1 a
-> Signal dom2 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clock dom1 -> Clock dom2 -> Signal dom1 a -> Signal dom2 a
forall (dom1 :: Domain) (dom2 :: Domain) a.
(KnownDomain dom1, KnownDomain dom2) =>
Clock dom1 -> Clock dom2 -> Signal dom1 a -> Signal dom2 a
unsafeSynchronizer Clock dom1
clk1 Clock dom2
clk2
fifoMem
:: ( KnownDomain wdom
, KnownDomain rdom
, NFDataX a )
=> Clock wdom
-> Clock rdom
-> Enable wdom
-> SNat addrSize
-> Signal wdom Bool
-> Signal rdom (BitVector addrSize)
-> Signal wdom (Maybe (BitVector addrSize, a))
-> Signal rdom a
fifoMem :: Clock wdom
-> Clock rdom
-> Enable wdom
-> SNat addrSize
-> Signal wdom Bool
-> Signal rdom (BitVector addrSize)
-> Signal wdom (Maybe (BitVector addrSize, a))
-> Signal rdom a
fifoMem Clock wdom
wclk Clock rdom
rclk Enable wdom
en addrSize :: SNat addrSize
addrSize@SNat addrSize
SNat Signal wdom Bool
full Signal rdom (BitVector addrSize)
raddr Signal wdom (Maybe (BitVector addrSize, a))
writeM =
Clock wdom
-> Clock rdom
-> Enable wdom
-> SNat (2 ^ addrSize)
-> Signal rdom (BitVector addrSize)
-> Signal wdom (Maybe (BitVector addrSize, a))
-> Signal rdom a
forall addr (wdom :: Domain) (rdom :: Domain) a (n :: Nat).
(Enum addr, HasCallStack, KnownDomain wdom, KnownDomain rdom,
NFDataX a) =>
Clock wdom
-> Clock rdom
-> Enable wdom
-> SNat n
-> Signal rdom addr
-> Signal wdom (Maybe (addr, a))
-> Signal rdom a
asyncRam
Clock wdom
wclk Clock rdom
rclk Enable wdom
en
(SNat addrSize -> SNat (2 ^ addrSize)
forall (a :: Nat). SNat a -> SNat (2 ^ a)
pow2SNat SNat addrSize
addrSize)
Signal rdom (BitVector addrSize)
raddr
(Signal wdom Bool
-> Signal wdom (Maybe (BitVector addrSize, a))
-> Signal wdom (Maybe (BitVector addrSize, a))
-> Signal wdom (Maybe (BitVector addrSize, a))
forall (f :: Type -> Type) a.
Applicative f =>
f Bool -> f a -> f a -> f a
mux Signal wdom Bool
full (Maybe (BitVector addrSize, a)
-> Signal wdom (Maybe (BitVector addrSize, a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (BitVector addrSize, a)
forall a. Maybe a
Nothing) Signal wdom (Maybe (BitVector addrSize, a))
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 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 addrSize
SNat BitVector (addrSize + 1) -> BitVector (addrSize + 1) -> Bool
flagGen (BitVector (addrSize + 1)
bin, BitVector (addrSize + 1)
ptr, Bool
flag) (BitVector (addrSize + 1)
s_ptr, Bool
inc) =
((BitVector (addrSize + 1)
bin', BitVector (addrSize + 1)
ptr', Bool
flag'), (Bool
flag, BitVector addrSize
addr, BitVector (addrSize + 1)
ptr))
where
bin' :: BitVector (addrSize + 1)
bin' = BitVector (addrSize + 1)
bin BitVector (addrSize + 1)
-> BitVector (addrSize + 1) -> BitVector (addrSize + 1)
forall a. Num a => a -> a -> a
+ Bool -> BitVector (addrSize + 1)
forall (n :: Nat). KnownNat n => Bool -> BitVector (n + 1)
boolToBV (Bool
inc Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
flag)
ptr' :: BitVector (addrSize + 1)
ptr' = (BitVector (addrSize + 1)
bin' BitVector (addrSize + 1) -> Int -> BitVector (addrSize + 1)
forall a. Bits a => a -> Int -> a
`shiftR` Int
1) BitVector (addrSize + 1)
-> BitVector (addrSize + 1) -> BitVector (addrSize + 1)
forall a. Bits a => a -> a -> a
`xor` BitVector (addrSize + 1)
bin'
addr :: BitVector addrSize
addr = BitVector (addrSize + 1) -> BitVector addrSize
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a) =>
f (a + b) -> f a
truncateB BitVector (addrSize + 1)
bin
flag' :: Bool
flag' = BitVector (addrSize + 1) -> BitVector (addrSize + 1) -> Bool
flagGen BitVector (addrSize + 1)
ptr' BitVector (addrSize + 1)
s_ptr
isFull
:: forall addrSize
. (2 <= addrSize)
=> SNat addrSize
-> BitVector (addrSize + 1)
-> BitVector (addrSize + 1)
-> Bool
isFull :: SNat addrSize
-> BitVector (addrSize + 1) -> BitVector (addrSize + 1) -> Bool
isFull addrSize :: SNat addrSize
addrSize@SNat addrSize
SNat BitVector (addrSize + 1)
ptr BitVector (addrSize + 1)
s_ptr =
case (2 <= addrSize, 1 <= 2) :- (1 <= addrSize)
forall (a :: Nat) (b :: Nat) (c :: Nat).
(b <= c, a <= b) :- (a <= c)
leTrans @1 @2 @addrSize of
Sub (2 <= addrSize, 1 <= 2) => Dict (1 <= addrSize)
Dict ->
let a1 :: SNat (addrSize - 1)
a1 = KnownNat (addrSize - 1) => SNat (addrSize - 1)
forall (n :: Nat). KnownNat n => SNat n
SNat @(addrSize - 1)
a2 :: SNat (addrSize - 2)
a2 = KnownNat (addrSize - 2) => SNat (addrSize - 2)
forall (n :: Nat). KnownNat n => SNat n
SNat @(addrSize - 2)
in BitVector (addrSize + 1)
ptr BitVector (addrSize + 1) -> BitVector (addrSize + 1) -> Bool
forall a. Eq a => a -> a -> Bool
== (BitVector ((addrSize + 1) - (addrSize - 1))
-> BitVector ((addrSize + 1) - (addrSize - 1))
forall a. Bits a => a -> a
complement (SNat addrSize
-> SNat (addrSize - 1)
-> BitVector (addrSize + 1)
-> BitVector ((addrSize + 1) - (addrSize - 1))
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat addrSize
addrSize SNat (addrSize - 1)
a1 BitVector (addrSize + 1)
s_ptr) BitVector ((addrSize + 1) - (addrSize - 1))
-> BitVector ((addrSize - 2) + 1)
-> BitVector
(((addrSize + 1) - (addrSize - 1)) + ((addrSize - 2) + 1))
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# SNat (addrSize - 2)
-> SNat 0
-> BitVector (addrSize + 1)
-> BitVector (((addrSize - 2) + 1) - 0)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat (addrSize - 2)
a2 SNat 0
d0 BitVector (addrSize + 1)
s_ptr)
asyncFIFOSynchronizer
:: ( KnownDomain wdom
, KnownDomain rdom
, 2 <= addrSize
, NFDataX a )
=> SNat addrSize
-> Clock wdom
-> Clock rdom
-> Reset wdom
-> Reset rdom
-> Enable wdom
-> Enable rdom
-> Signal rdom Bool
-> Signal wdom (Maybe a)
-> (Signal rdom a, Signal rdom Bool, Signal wdom Bool)
asyncFIFOSynchronizer :: SNat addrSize
-> Clock wdom
-> Clock rdom
-> Reset wdom
-> Reset rdom
-> Enable wdom
-> Enable rdom
-> Signal rdom Bool
-> Signal wdom (Maybe a)
-> (Signal rdom a, Signal rdom Bool, Signal wdom Bool)
asyncFIFOSynchronizer addrSize :: SNat addrSize
addrSize@SNat addrSize
SNat Clock wdom
wclk Clock rdom
rclk Reset wdom
wrst Reset rdom
rrst Enable wdom
wen Enable rdom
ren Signal rdom Bool
rinc Signal wdom (Maybe a)
wdataM =
(Signal rdom a
rdata, Signal rdom Bool
rempty, Signal wdom Bool
wfull)
where
s_rptr :: Signal wdom (BitVector (addrSize + 1))
s_rptr = Clock rdom
-> Clock wdom
-> Reset wdom
-> Enable wdom
-> BitVector (addrSize + 1)
-> Signal rdom (BitVector (addrSize + 1))
-> Signal wdom (BitVector (addrSize + 1))
forall a (dom1 :: Domain) (dom2 :: Domain).
(NFDataX a, KnownDomain dom1, KnownDomain dom2) =>
Clock dom1
-> Clock dom2
-> Reset dom2
-> Enable dom2
-> a
-> Signal dom1 a
-> Signal dom2 a
dualFlipFlopSynchronizer Clock rdom
rclk Clock wdom
wclk Reset wdom
wrst Enable wdom
wen BitVector (addrSize + 1)
0 Signal rdom (BitVector (addrSize + 1))
rptr
s_wptr :: Signal rdom (BitVector (addrSize + 1))
s_wptr = Clock wdom
-> Clock rdom
-> Reset rdom
-> Enable rdom
-> BitVector (addrSize + 1)
-> Signal wdom (BitVector (addrSize + 1))
-> Signal rdom (BitVector (addrSize + 1))
forall a (dom1 :: Domain) (dom2 :: Domain).
(NFDataX a, KnownDomain dom1, KnownDomain dom2) =>
Clock dom1
-> Clock dom2
-> Reset dom2
-> Enable dom2
-> a
-> Signal dom1 a
-> Signal dom2 a
dualFlipFlopSynchronizer Clock wdom
wclk Clock rdom
rclk Reset rdom
rrst Enable rdom
ren BitVector (addrSize + 1)
0 Signal wdom (BitVector (addrSize + 1))
wptr
rdata :: Signal rdom a
rdata =
Clock wdom
-> Clock rdom
-> Enable wdom
-> SNat addrSize
-> Signal wdom Bool
-> Signal rdom (BitVector addrSize)
-> Signal wdom (Maybe (BitVector addrSize, a))
-> Signal rdom a
forall (wdom :: Domain) (rdom :: Domain) a (addrSize :: Nat).
(KnownDomain wdom, KnownDomain rdom, NFDataX a) =>
Clock wdom
-> Clock rdom
-> Enable wdom
-> SNat addrSize
-> Signal wdom Bool
-> Signal rdom (BitVector addrSize)
-> Signal wdom (Maybe (BitVector addrSize, a))
-> Signal rdom a
fifoMem
Clock wdom
wclk Clock rdom
rclk Enable wdom
wen
SNat addrSize
addrSize Signal wdom Bool
wfull Signal rdom (BitVector addrSize)
raddr
((BitVector addrSize -> a -> (BitVector addrSize, a))
-> Maybe (BitVector addrSize)
-> Maybe a
-> Maybe (BitVector addrSize, a)
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) (Maybe (BitVector addrSize)
-> Maybe a -> Maybe (BitVector addrSize, a))
-> Signal wdom (Maybe (BitVector addrSize))
-> Signal wdom (Maybe a -> Maybe (BitVector addrSize, a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BitVector addrSize -> Maybe (BitVector addrSize)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BitVector addrSize -> Maybe (BitVector addrSize))
-> Signal wdom (BitVector addrSize)
-> Signal wdom (Maybe (BitVector addrSize))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal wdom (BitVector addrSize)
waddr) Signal wdom (Maybe a -> Maybe (BitVector addrSize, a))
-> Signal wdom (Maybe a)
-> Signal wdom (Maybe (BitVector addrSize, a))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Signal wdom (Maybe a)
wdataM)
(Signal rdom Bool
rempty, Signal rdom (BitVector addrSize)
raddr, Signal rdom (BitVector (addrSize + 1))
rptr) =
Clock rdom
-> Reset rdom
-> Enable rdom
-> ((BitVector (addrSize + 1), BitVector (addrSize + 1), Bool)
-> (BitVector (addrSize + 1), Bool)
-> ((BitVector (addrSize + 1), BitVector (addrSize + 1), Bool),
(Bool, BitVector addrSize, BitVector (addrSize + 1))))
-> (BitVector (addrSize + 1), BitVector (addrSize + 1), Bool)
-> Unbundled rdom (BitVector (addrSize + 1), Bool)
-> Unbundled
rdom (Bool, BitVector addrSize, BitVector (addrSize + 1))
forall (dom :: Domain) s i o.
(KnownDomain dom, NFDataX s, Bundle i, Bundle o) =>
Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> (s, o))
-> s
-> Unbundled dom i
-> Unbundled dom o
mealyB
Clock rdom
rclk Reset rdom
rrst Enable rdom
ren
(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)))
forall (addrSize :: Nat).
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 addrSize
addrSize BitVector (addrSize + 1) -> BitVector (addrSize + 1) -> Bool
forall a. Eq a => a -> a -> Bool
(==))
(BitVector (addrSize + 1)
0, BitVector (addrSize + 1)
0, Bool
True)
(Signal rdom (BitVector (addrSize + 1))
s_wptr, Signal rdom Bool
rinc)
(Signal wdom Bool
wfull, Signal wdom (BitVector addrSize)
waddr, Signal wdom (BitVector (addrSize + 1))
wptr) =
Clock wdom
-> Reset wdom
-> Enable wdom
-> ((BitVector (addrSize + 1), BitVector (addrSize + 1), Bool)
-> (BitVector (addrSize + 1), Bool)
-> ((BitVector (addrSize + 1), BitVector (addrSize + 1), Bool),
(Bool, BitVector addrSize, BitVector (addrSize + 1))))
-> (BitVector (addrSize + 1), BitVector (addrSize + 1), Bool)
-> Unbundled wdom (BitVector (addrSize + 1), Bool)
-> Unbundled
wdom (Bool, BitVector addrSize, BitVector (addrSize + 1))
forall (dom :: Domain) s i o.
(KnownDomain dom, NFDataX s, Bundle i, Bundle o) =>
Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> (s, o))
-> s
-> Unbundled dom i
-> Unbundled dom o
mealyB
Clock wdom
wclk Reset wdom
wrst Enable wdom
wen
(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)))
forall (addrSize :: Nat).
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 addrSize
addrSize (SNat addrSize
-> BitVector (addrSize + 1) -> BitVector (addrSize + 1) -> Bool
forall (addrSize :: Nat).
(2 <= addrSize) =>
SNat addrSize
-> BitVector (addrSize + 1) -> BitVector (addrSize + 1) -> Bool
isFull SNat addrSize
addrSize))
(BitVector (addrSize + 1)
0, BitVector (addrSize + 1)
0, Bool
False)
(Signal wdom (BitVector (addrSize + 1))
s_rptr, Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (Maybe a -> Bool) -> Signal wdom (Maybe a) -> Signal wdom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal wdom (Maybe a)
wdataM)