{-|
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 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, (.&&.))
import Clash.Promoted.Nat          (SNat (..))
import Clash.Promoted.Nat.Literals (d0)
import Clash.Signal                (mux, KnownDomain)
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 :: 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 :: 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)
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 (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 (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 (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 (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap BitVector 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 (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 (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJustX Signal wdom (Maybe a)
wdataM)
               (RamOp (2 ^ addrSize) a -> Signal wdom (RamOp (2 ^ addrSize) 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 :: (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 (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 :: 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 (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 :: 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)

-- | 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 :: 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)