    {-|
    Copyright   :  (C) 2015-2016, University of Twente,
                       2016-2019, Myrtle Software Ltd,
                       2017     , Google Inc.,
                       2021-2022, QBayLogic B.V.
    License     :  BSD2 (see the file LICENSE)
    Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>

    Synchronizer circuits for safe clock domain crossings
    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE NoGeneralizedNewtypeDeriving #-}
    {-# LANGUAGE TypeFamilies #-}

    {-# LANGUAGE Safe #-}

    {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-}
    {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
    {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver    #-}

    {-# OPTIONS_HADDOCK show-extensions #-}

    module Clash.Explicit.Synchronizer
      ( -- * Bit-synchronizers
        dualFlipFlopSynchronizer
        -- * Word-synchronizers
      , asyncFIFOSynchronizer
      )
    where

    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 (<=), type (^), KnownNat)

    import Clash.Class.BitPack         (boolToBV, unpack)
    import Clash.Class.Resize          (truncateB)
    import Clash.Class.BitPack.BitIndex (slice)
    import Clash.Explicit.Mealy        (mealyB)
    import Clash.Explicit.BlockRam     (RamOp (..), trueDualPortBlockRam)
    import Clash.Explicit.Signal
      (Clock, Reset, Signal, Enable, register, unsafeSynchronizer, fromEnable,
      (.&&.), mux, KnownDomain)
    import Clash.Promoted.Nat          (SNat (..))
    import Clash.Promoted.Nat.Literals (d0)
    import Clash.Sized.BitVector       (BitVector, (++#))
    import Clash.XException            (NFDataX, fromJustX)

    -- * Dual flip-flop synchronizer

    -- | Synchronizer based on two sequentially connected flip-flops.
    --
    --  * __NB__: This synchronizer can be used for __bit__-synchronization.
    --
    --  * __NB__: Although this synchronizer does reduce metastability, it does
    --  not guarantee the proper synchronization of a whole __word__. For
    --  example, given that the output is sampled twice as fast as the input is
    --  running, and we have two samples in the input stream that look like:
    --
    --      @[0111,1000]@
    --
    --      But the circuit driving the input stream has a longer propagation delay
    --      on __msb__ compared to the __lsb__s. What can happen is an output stream
    --      that looks like this:
    --
    --      @[0111,0111,0000,1000]@
    --
    --      Where the level-change of the __msb__ was not captured, but the level
    --      change of the __lsb__s were.
    --
    --      If you want to have /safe/ __word__-synchronization use
    --      'asyncFIFOSynchronizer'.
    dualFlipFlopSynchronizer
      :: ( NFDataX a
         , KnownDomain dom1
         , KnownDomain dom2 )
      => Clock dom1
      -- ^ 'Clock' to which the incoming  data is synchronized
      -> Clock dom2
      -- ^ 'Clock' to which the outgoing data is synchronized
      -> Reset dom2
      -- ^ 'Reset' for registers on the outgoing domain
      -> Enable dom2
      -- ^ 'Enable' for registers on the outgoing domain
      -> a
      -- ^ Initial value of the two synchronization registers
      -> Signal dom1 a
      -- ^ Incoming data
      -> Signal dom2 a
      -- ^ Outgoing, synchronized, data
    dualFlipFlopSynchronizer :: 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 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

    -- * Asynchronous FIFO synchronizer

    fifoMem
      :: forall wdom rdom a addrSize
       . ( KnownDomain wdom
         , KnownDomain rdom
         , NFDataX a
         , KnownNat addrSize
         , 1 <= addrSize )
      => Clock wdom
      -> Clock rdom
      -> Enable wdom
      -> Enable rdom
      -> Signal wdom Bool
      -> Signal rdom (BitVector addrSize)
      -> Signal wdom (BitVector addrSize)
      -> Signal wdom (Maybe a)
      -> Signal rdom a
    fifoMem :: forall (wdom :: Domain) (rdom :: Domain) a (addrSize :: Nat).
    (KnownDomain wdom, KnownDomain rdom, NFDataX a, KnownNat addrSize,
     1 <= addrSize) =>
    Clock wdom
    -> Clock rdom
    -> Enable wdom
    -> Enable rdom
    -> Signal wdom Bool
    -> Signal rdom (BitVector addrSize)
    -> Signal wdom (BitVector addrSize)
    -> Signal wdom (Maybe a)
    -> Signal rdom a
    fifoMem Clock wdom
    wclk Clock rdom
    rclk Enable wdom
    wen Enable rdom
    ren Signal wdom Bool
    full Signal rdom (BitVector addrSize)
    raddr Signal wdom (BitVector addrSize)
    waddr Signal wdom (Maybe a)
    wdataM =
      (Signal rdom a, Signal wdom a) -> Signal rdom a
    forall a b. (a, b) -> a
    fst ((Signal rdom a, Signal wdom a) -> Signal rdom a)
    -> (Signal rdom a, Signal wdom a) -> Signal rdom a
    forall a b. (a -> b) -> a -> b
    $ Clock rdom
    -> Clock wdom
    -> Signal rdom (RamOp (2 ^ addrSize) a)
    -> Signal wdom (RamOp (2 ^ addrSize) a)
    -> (Signal rdom a, Signal wdom a)
    forall (nAddrs :: Nat) (domA :: Domain) (domB :: Domain) a.
    (HasCallStack, KnownNat nAddrs, KnownDomain domA, KnownDomain domB,
     NFDataX a) =>
    Clock domA
    -> Clock domB
    -> Signal domA (RamOp nAddrs a)
    -> Signal domB (RamOp nAddrs a)
    -> (Signal domA a, Signal domB a)
    trueDualPortBlockRam
        Clock rdom
    rclk Clock wdom
    wclk Signal rdom (RamOp (2 ^ addrSize) a)
    portA Signal wdom (RamOp (2 ^ addrSize) a)
    portB
     where
       portA :: Signal rdom (RamOp (2 ^ addrSize) a)
       portA :: Signal rdom (RamOp (2 ^ addrSize) a)
    portA = Signal rdom Bool
    -> Signal rdom (RamOp (2 ^ addrSize) a)
    -> Signal rdom (RamOp (2 ^ addrSize) a)
    -> Signal rdom (RamOp (2 ^ addrSize) a)
    forall (f :: Type -> Type) a.
    Applicative f =>
    f Bool -> f a -> f a -> f a
    mux (Enable rdom -> Signal rdom Bool
    forall (dom :: Domain). Enable dom -> Signal dom Bool
    fromEnable Enable rdom
    ren)
                   (Index (2 ^ addrSize) -> RamOp (2 ^ addrSize) a
    forall (n :: Nat) a. Index n -> RamOp n a
    RamRead (Index (2 ^ addrSize) -> RamOp (2 ^ addrSize) a)
    -> (BitVector addrSize -> Index (2 ^ addrSize))
    -> BitVector addrSize
    -> RamOp (2 ^ addrSize) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BitVector addrSize -> Index (2 ^ addrSize)
    BitVector (BitSize (Index (2 ^ addrSize))) -> Index (2 ^ addrSize)
    forall a. BitPack a => BitVector (BitSize a) -> a
    unpack (BitVector addrSize -> RamOp (2 ^ addrSize) a)
    -> Signal rdom (BitVector addrSize)
    -> Signal rdom (RamOp (2 ^ addrSize) a)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Signal rdom (BitVector addrSize)
    raddr)
                   (RamOp (2 ^ addrSize) a -> Signal rdom (RamOp (2 ^ addrSize) a)
    forall a. a -> Signal rdom a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure RamOp (2 ^ addrSize) a
    forall (n :: Nat) a. RamOp n a
    RamNoOp)
       portB :: Signal wdom (RamOp (2 ^ addrSize) a)
       portB :: Signal wdom (RamOp (2 ^ addrSize) a)
    portB = Signal wdom Bool
    -> Signal wdom (RamOp (2 ^ addrSize) a)
    -> Signal wdom (RamOp (2 ^ addrSize) a)
    -> Signal wdom (RamOp (2 ^ addrSize) a)
    forall (f :: Type -> Type) a.
    Applicative f =>
    f Bool -> f a -> f a -> f a
    mux (Enable wdom -> Signal wdom Bool
    forall (dom :: Domain). Enable dom -> Signal dom Bool
    fromEnable Enable wdom
    wen Signal wdom Bool -> Signal wdom Bool -> Signal wdom Bool
    forall (f :: Type -> Type).
    Applicative f =>
    f Bool -> f Bool -> f Bool
    .&&. (Bool -> Bool) -> Signal wdom Bool -> Signal wdom Bool
    forall a b. (a -> b) -> Signal wdom a -> Signal wdom b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap Bool -> Bool
    not Signal wdom Bool
    full Signal wdom Bool -> Signal wdom Bool -> Signal wdom Bool
    forall (f :: Type -> Type).
    Applicative f =>
    f Bool -> f Bool -> f Bool
    .&&. (Maybe a -> Bool) -> Signal wdom (Maybe a) -> Signal wdom Bool
    forall a b. (a -> b) -> Signal wdom a -> Signal wdom b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap Maybe a -> Bool
    forall a. Maybe a -> Bool
    isJust Signal wdom (Maybe a)
    wdataM)
                   (Index (2 ^ addrSize) -> a -> RamOp (2 ^ addrSize) a
    forall (n :: Nat) a. Index n -> a -> RamOp n a
    RamWrite (Index (2 ^ addrSize) -> a -> RamOp (2 ^ addrSize) a)
    -> Signal wdom (Index (2 ^ addrSize))
    -> Signal wdom (a -> RamOp (2 ^ addrSize) a)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (BitVector addrSize -> Index (2 ^ addrSize))
    -> Signal wdom (BitVector addrSize)
    -> Signal wdom (Index (2 ^ addrSize))
    forall a b. (a -> b) -> Signal wdom a -> Signal wdom b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap BitVector addrSize -> Index (2 ^ addrSize)
    BitVector (BitSize (Index (2 ^ addrSize))) -> Index (2 ^ addrSize)
    forall a. BitPack a => BitVector (BitSize a) -> a
    unpack Signal wdom (BitVector addrSize)
    waddr Signal wdom (a -> RamOp (2 ^ addrSize) a)
    -> Signal wdom a -> Signal wdom (RamOp (2 ^ addrSize) a)
    forall a b. Signal wdom (a -> b) -> Signal wdom a -> Signal wdom b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> (Maybe a -> a) -> Signal wdom (Maybe a) -> Signal wdom a
    forall a b. (a -> b) -> Signal wdom a -> Signal wdom b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap Maybe a -> a
    forall a. (HasCallStack, NFDataX a) => Maybe a -> a
    fromJustX Signal wdom (Maybe a)
    wdataM)
                   (RamOp (2 ^ addrSize) a -> Signal wdom (RamOp (2 ^ addrSize) a)
    forall a. a -> Signal wdom a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure RamOp (2 ^ addrSize) a
    forall (n :: Nat) a. RamOp n a
    RamNoOp)

    readPtrCompareT
      :: KnownNat addrSize
      => ( BitVector (addrSize + 1)
         , BitVector (addrSize + 1)
         , Bool )
      -> ( BitVector (addrSize + 1)
         , Bool )
      -> ( ( BitVector (addrSize + 1)
           , BitVector (addrSize + 1)
           , Bool )
         , ( Bool
           , BitVector addrSize
           , BitVector (addrSize + 1)
           )
         )
    readPtrCompareT :: forall (addrSize :: Nat).
    KnownNat addrSize =>
    (BitVector (addrSize + 1), BitVector (addrSize + 1), Bool)
    -> (BitVector (addrSize + 1), Bool)
    -> ((BitVector (addrSize + 1), BitVector (addrSize + 1), Bool),
        (Bool, BitVector addrSize, BitVector (addrSize + 1)))
    readPtrCompareT (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
      -- GRAYSTYLE2 pointer
      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 (a :: Nat) (b :: Nat).
    KnownNat a =>
    BitVector (a + b) -> BitVector a
    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)
    ptr' BitVector (addrSize + 1) -> BitVector (addrSize + 1) -> Bool
    forall a. Eq a => a -> a -> Bool
    == BitVector (addrSize + 1)
    s_ptr

    writePtrCompareT
      :: (2 <= addrSize)
      => SNat addrSize
      -> ( BitVector (addrSize + 1)
         , BitVector (addrSize + 1)
         , Bool )
      -> ( BitVector (addrSize + 1)
         , Bool )
      -> ( ( BitVector (addrSize + 1)
           , BitVector (addrSize + 1)
           , Bool )
         , ( Bool
           , BitVector addrSize
           , BitVector (addrSize + 1)
           )
         )
    writePtrCompareT :: forall (addrSize :: Nat).
    (2 <= addrSize) =>
    SNat addrSize
    -> (BitVector (addrSize + 1), BitVector (addrSize + 1), Bool)
    -> (BitVector (addrSize + 1), Bool)
    -> ((BitVector (addrSize + 1), BitVector (addrSize + 1), Bool),
        (Bool, BitVector addrSize, BitVector (addrSize + 1)))
    writePtrCompareT addrSize :: SNat addrSize
    addrSize@SNat addrSize
    SNat (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
      -- GRAYSTYLE2 pointer
      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 (a :: Nat) (b :: Nat).
    KnownNat a =>
    BitVector (a + b) -> BitVector a
    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' = 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)
    ptr' BitVector (addrSize + 1)
    s_ptr

    -- FIFO full: when next pntr == synchronized {~wptr[addrSize:addrSize-1],wptr[addrSize-2:0]}
    isFull
      :: forall addrSize
       . (2 <= addrSize)
      => SNat addrSize
      -> BitVector (addrSize + 1)
      -> BitVector (addrSize + 1)
      -> Bool
    isFull :: forall (addrSize :: Nat).
    (2 <= addrSize) =>
    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 forall (a :: Nat) (b :: Nat) (c :: Nat).
    (b <= c, a <= b) :- (a <= c)
    leTrans @1 @2 @addrSize of
        Sub Dict (1 <= addrSize)
    (2 <= addrSize, 1 <= 2) => Dict (1 <= addrSize)
    Dict ->
          let a1 :: SNat (addrSize - 1)
    a1 = forall (n :: Nat). KnownNat n => SNat n
    SNat @(addrSize - 1)
              a2 :: SNat (addrSize - 2)
    a2 = 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)

    -- | Synchronizer implemented as a FIFO around a synchronous RAM. Based on the
    -- design described in "Clash.Tutorial#multiclock", which is itself based on the
    -- design described in <http://www.sunburst-design.com/papers/CummingsSNUG2002SJ_FIFO1.pdf>.
    -- However, this FIFO uses a synchronous dual-ported RAM which, unlike those
    -- designs using RAM with an asynchronous read port, is nearly guaranteed to
    -- actually synthesize into one of the dual-ported RAMs found on most FPGAs.
    --
    -- __NB__: This synchronizer can be used for __word__-synchronization.
    -- __NB__: This synchronizer will only work safely when you set up the proper
    -- bus skew and maximum delay constraints inside your synthesis tool for the
    -- clock domain crossings of the gray pointers.
    asyncFIFOSynchronizer
      :: ( KnownDomain wdom
         , KnownDomain rdom
         , 2 <= addrSize
         , NFDataX a )
      => SNat addrSize
      -- ^ Size of the internally used addresses, the  FIFO contains @2^addrSize@
      -- elements.
      -> Clock wdom
      -- ^ 'Clock' to which the write port is synchronized
      -> Clock rdom
      -- ^ 'Clock' to which the read port is synchronized
      -> Reset wdom
      -> Reset rdom
      -> Enable wdom
      -> Enable rdom
      -> Signal rdom Bool
      -- ^ Read request
      -> Signal wdom (Maybe a)
      -- ^ Element to insert
      -> (Signal rdom a, Signal rdom Bool, Signal wdom Bool)
      -- ^ (Oldest element in the FIFO, @empty@ flag, @full@ flag)
    asyncFIFOSynchronizer :: forall (wdom :: Domain) (rdom :: Domain) (addrSize :: Nat) a.
    (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 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
    -> Enable rdom
    -> Signal wdom Bool
    -> Signal rdom (BitVector addrSize)
    -> Signal wdom (BitVector addrSize)
    -> Signal wdom (Maybe a)
    -> Signal rdom a
    forall (wdom :: Domain) (rdom :: Domain) a (addrSize :: Nat).
    (KnownDomain wdom, KnownDomain rdom, NFDataX a, KnownNat addrSize,
     1 <= addrSize) =>
    Clock wdom
    -> Clock rdom
    -> Enable wdom
    -> Enable rdom
    -> Signal wdom Bool
    -> Signal rdom (BitVector addrSize)
    -> Signal wdom (BitVector addrSize)
    -> Signal wdom (Maybe a)
    -> Signal rdom a
    fifoMem
          Clock wdom
    wclk Clock rdom
    rclk Enable wdom
    wen Enable rdom
    ren
          Signal wdom Bool
    wfull Signal rdom (BitVector addrSize)
    raddr
          Signal wdom (BitVector addrSize)
    waddr 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
          (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).
    KnownNat addrSize =>
    (BitVector (addrSize + 1), BitVector (addrSize + 1), Bool)
    -> (BitVector (addrSize + 1), Bool)
    -> ((BitVector (addrSize + 1), BitVector (addrSize + 1), Bool),
        (Bool, BitVector addrSize, BitVector (addrSize + 1)))
    readPtrCompareT
          (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), Bool)
    -> ((BitVector (addrSize + 1), BitVector (addrSize + 1), Bool),
        (Bool, BitVector addrSize, BitVector (addrSize + 1)))
    forall (addrSize :: Nat).
    (2 <= addrSize) =>
    SNat addrSize
    -> (BitVector (addrSize + 1), BitVector (addrSize + 1), Bool)
    -> (BitVector (addrSize + 1), Bool)
    -> ((BitVector (addrSize + 1), BitVector (addrSize + 1), Bool),
        (Bool, BitVector addrSize, BitVector (addrSize + 1)))
    writePtrCompareT 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)