    {-|
    Copyright  :  (C) 2020-2023, QBayLogic B.V.,
                      2022-2023, Google LLC
    License    :  BSD2 (see the file LICENSE)
    Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>

    Utilities to deal with resets.
    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE MagicHash #-}
    {-# LANGUAGE QuasiQuotes #-}
    {-# LANGUAGE TypeFamilies #-}

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

    module Clash.Explicit.Reset
      ( -- Defined in this module
        resetSynchronizer
      , resetGlitchFilter
      , resetGlitchFilterWithReset
      , unsafeResetGlitchFilter
      , holdReset
      , convertReset
      , noReset
      , andReset, unsafeAndReset
      , orReset, unsafeOrReset

        -- Re-exports
      , Reset
      , resetGen
      , resetGenN
      , resetKind
      , systemResetGen
      , unsafeToReset
      , unsafeFromReset
      , unsafeToActiveHigh
      , unsafeToActiveLow
      , unsafeFromActiveHigh
      , unsafeFromActiveLow

      -- * Deprecated
      , unsafeFromHighPolarity
      , unsafeFromLowPolarity
      , unsafeToHighPolarity
      , unsafeToLowPolarity
      ) where

    import           Data.Type.Equality ((:~:)(Refl))

    import           Clash.Class.Num (satSucc, SaturationMode(SatBound))
    import           Clash.Explicit.Signal
    import           Clash.Explicit.Synchronizer (dualFlipFlopSynchronizer)
    import           Clash.Promoted.Nat
    import           Clash.Signal.Internal
    import           Clash.Sized.Index (Index)

    import           GHC.Stack (HasCallStack)
    import           GHC.TypeLits (type (+), type (<=))

    {- $setup
    >>> import Clash.Explicit.Prelude
    -}

    -- | A reset that is never asserted
    noReset :: KnownDomain dom => Reset dom
    noReset :: forall (dom :: Domain). KnownDomain dom => Reset dom
    noReset = Signal dom Bool -> Reset dom
    forall (dom :: Domain).
    KnownDomain dom =>
    Signal dom Bool -> Reset dom
    unsafeFromActiveHigh (Bool -> Signal dom Bool
    forall a. a -> Signal dom a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    False)

    -- | Output reset will be asserted when either one of the input resets is
    -- asserted
    orReset ::
      forall dom .
      HasSynchronousReset dom =>
      Reset dom ->
      Reset dom ->
      Reset dom
    orReset :: forall (dom :: Domain).
    HasSynchronousReset dom =>
    Reset dom -> Reset dom -> Reset dom
    orReset = Reset dom -> Reset dom -> Reset dom
    forall (dom :: Domain).
    KnownDomain dom =>
    Reset dom -> Reset dom -> Reset dom
    unsafeOrReset

    -- | Output reset will be asserted when either one of the input resets is
    -- asserted. This function is considered unsafe because it can be used on
    -- domains with components with asynchronous resets, where use of this function
    -- can introduce glitches triggering a reset.
    unsafeOrReset :: forall dom. KnownDomain dom => Reset dom -> Reset dom -> Reset dom
    unsafeOrReset :: forall (dom :: Domain).
    KnownDomain dom =>
    Reset dom -> Reset dom -> Reset dom
    unsafeOrReset (Reset dom -> Signal dom Bool
    forall (dom :: Domain). Reset dom -> Signal dom Bool
    unsafeFromReset -> Signal dom Bool
    rst0) (Reset dom -> Signal dom Bool
    forall (dom :: Domain). Reset dom -> Signal dom Bool
    unsafeFromReset -> Signal dom Bool
    rst1) =
      Signal dom Bool -> Reset dom
    forall (dom :: Domain).
    KnownDomain dom =>
    Signal dom Bool -> Reset dom
    unsafeToReset (Signal dom Bool -> Reset dom) -> Signal dom Bool -> Reset dom
    forall a b. (a -> b) -> a -> b
    $
        case forall (dom :: Domain) (polarity :: ResetPolarity).
    (KnownDomain dom, DomainResetPolarity dom ~ polarity) =>
    SResetPolarity polarity
    resetPolarity @dom of
          SResetPolarity (DomainConfigurationResetPolarity (KnownConf dom))
    SActiveHigh -> Signal dom Bool
    rst0 Signal dom Bool -> Signal dom Bool -> Signal dom Bool
    forall (f :: Type -> Type).
    Applicative f =>
    f Bool -> f Bool -> f Bool
    .||. Signal dom Bool
    rst1
          SResetPolarity (DomainConfigurationResetPolarity (KnownConf dom))
    SActiveLow  -> Signal dom Bool
    rst0 Signal dom Bool -> Signal dom Bool -> Signal dom Bool
    forall (f :: Type -> Type).
    Applicative f =>
    f Bool -> f Bool -> f Bool
    .&&. Signal dom Bool
    rst1

    -- | Output reset will be asserted when both input resets are asserted
    andReset ::
      forall dom .
      HasSynchronousReset dom =>
      Reset dom ->
      Reset dom ->
      Reset dom
    andReset :: forall (dom :: Domain).
    HasSynchronousReset dom =>
    Reset dom -> Reset dom -> Reset dom
    andReset = Reset dom -> Reset dom -> Reset dom
    forall (dom :: Domain).
    KnownDomain dom =>
    Reset dom -> Reset dom -> Reset dom
    unsafeAndReset

    -- | Output reset will be asserted when both input resets are asserted. This
    -- function is considered unsafe because it can be used on domains with
    -- components with asynchronous resets, where use of this function can introduce
    -- glitches triggering a reset.
    unsafeAndReset :: forall dom. KnownDomain dom => Reset dom -> Reset dom -> Reset dom
    unsafeAndReset :: forall (dom :: Domain).
    KnownDomain dom =>
    Reset dom -> Reset dom -> Reset dom
    unsafeAndReset (Reset dom -> Signal dom Bool
    forall (dom :: Domain). Reset dom -> Signal dom Bool
    unsafeFromReset -> Signal dom Bool
    rst0) (Reset dom -> Signal dom Bool
    forall (dom :: Domain). Reset dom -> Signal dom Bool
    unsafeFromReset -> Signal dom Bool
    rst1) =
      Signal dom Bool -> Reset dom
    forall (dom :: Domain).
    KnownDomain dom =>
    Signal dom Bool -> Reset dom
    unsafeToReset (Signal dom Bool -> Reset dom) -> Signal dom Bool -> Reset dom
    forall a b. (a -> b) -> a -> b
    $
        case forall (dom :: Domain) (polarity :: ResetPolarity).
    (KnownDomain dom, DomainResetPolarity dom ~ polarity) =>
    SResetPolarity polarity
    resetPolarity @dom of
          SResetPolarity (DomainConfigurationResetPolarity (KnownConf dom))
    SActiveHigh -> Signal dom Bool
    rst0 Signal dom Bool -> Signal dom Bool -> Signal dom Bool
    forall (f :: Type -> Type).
    Applicative f =>
    f Bool -> f Bool -> f Bool
    .&&. Signal dom Bool
    rst1
          SResetPolarity (DomainConfigurationResetPolarity (KnownConf dom))
    SActiveLow  -> Signal dom Bool
    rst0 Signal dom Bool -> Signal dom Bool -> Signal dom Bool
    forall (f :: Type -> Type).
    Applicative f =>
    f Bool -> f Bool -> f Bool
    .||. Signal dom Bool
    rst1

    -- | The resetSynchronizer will synchronize an incoming reset according to
    -- whether the domain is synchronous or asynchronous.
    --
    -- For asynchronous resets this synchronizer ensures the reset will only
    -- be de-asserted synchronously but it can still be asserted asynchronously.
    -- The reset assert is immediate, but reset de-assertion is delayed by two
    -- cycles.
    --
    -- Normally, asynchronous resets can be both asynchronously asserted and
    -- de-asserted. Asynchronous de-assertion can induce meta-stability in the
    -- component which is being reset. To ensure this doesn't happen,
    -- 'resetSynchronizer' ensures that de-assertion of a reset happens
    -- synchronously. Assertion of the reset remains asynchronous.
    --
    -- Note that asynchronous assertion does not induce meta-stability in the
    -- component whose reset is asserted. However, when a component \"A\" in another
    -- clock or reset domain depends on the value of a component \"B\" being
    -- reset, then asynchronous assertion of the reset of component \"B"\ can induce
    -- meta-stability in component \"A\". To prevent this from happening you need
    -- to use a proper synchronizer, for example one of the synchronizers in
    -- "Clash.Explicit.Synchronizer".
    --
    -- For synchronous resets this function ensures that the reset is asserted and
    -- de-asserted synchronously. Both the assertion and de-assertion of the reset
    -- are delayed by two cycles.
    --
    -- === __Example 1__
    -- The circuit below detects a rising bit (i.e., a transition from 0 to 1) in a
    -- given argument. It takes a reset that is not synchronized to any of the other
    -- incoming signals and synchronizes it using 'resetSynchronizer'.
    --
    -- @
    -- topEntity
    --   :: Clock  System
    --   -> Reset  System
    --   -> Signal System Bit
    --   -> Signal System (BitVector 8)
    -- topEntity clk asyncRst key1 =
    --   withClockResetEnable clk rst enableGen leds
    --  where
    --   rst   = 'resetSynchronizer' clk asyncRst
    --   key1R = isRising 1 key1
    --   leds  = mealy blinkerT (1, False, 0) key1R
    -- @
    --
    -- === __Example 2__
    -- Similar to /Example 1/ this circuit detects a rising bit (i.e., a transition
    -- from 0 to 1) in a given argument. It takes a clock that is not stable yet and
    -- a reset signal that is not synchronized to any other signals. It stabilizes
    -- the clock and then synchronizes the reset signal.
    --
    --
    -- Note that the function 'Clash.Intel.ClockGen.altpllSync' provides this
    -- functionality in a convenient form, obviating the need for
    -- @resetSynchronizer@ for this use case.
    --
    -- @
    -- topEntity
    --   :: Clock  System
    --   -> Reset  System
    --   -> Signal System Bit
    --   -> Signal System (BitVector 8)
    -- topEntity clk rst key1 =
    --     let  (pllOut,pllStable) = unsafeAltpll clk rst
    --          rstSync            = 'resetSynchronizer' pllOut (unsafeFromActiveLow pllStable)
    --     in   exposeClockResetEnable leds pllOut rstSync enableGen
    --   where
    --     key1R  = isRising 1 key1
    --     leds   = mealy blinkerT (1, False, 0) key1R
    -- @
    --
    -- === __Implementation details__
    -- 'resetSynchronizer' implements the following circuit for asynchronous domains:
    --
    -- >                                   rst
    -- >   --------------------------------------+
    -- >                       |                 |
    -- >                  +----v----+       +----v----+
    -- >     deasserted   |         |       |         |
    -- >   --------------->         +------->         +-------->
    -- >                  |         |       |         |
    -- >              +---|>        |   +---|>        |
    -- >              |   |         |   |   |         |
    -- >              |   +---------+   |   +---------+
    -- >      clk     |                 |
    -- >   -----------------------------+
    --
    -- This corresponds to figure 3d at <https://www.embedded.com/asynchronous-reset-synchronization-and-distribution-challenges-and-solutions/>
    --
    -- For synchronous domains two sequential dflipflops are used:
    --
    -- >                  +---------+       +---------+
    -- >     rst          |         |       |         |
    -- >   --------------->         +------->         +-------->
    -- >                  |         |       |         |
    -- >              +---|>        |   +---|>        |
    -- >              |   |         |   |   |         |
    -- >              |   +---------+   |   +---------+
    -- >      clk     |                 |
    -- >   -----------------------------+
    --
    resetSynchronizer
      :: forall dom
       . KnownDomain dom
      => Clock dom
      -> Reset dom
      -> Reset dom
    resetSynchronizer :: forall (dom :: Domain).
    KnownDomain dom =>
    Clock dom -> Reset dom -> Reset dom
    resetSynchronizer Clock dom
    clk Reset dom
    rst = Reset dom
    rstOut
     where
      isActiveHigh :: Bool
    isActiveHigh = case forall (dom :: Domain) (polarity :: ResetPolarity).
    (KnownDomain dom, DomainResetPolarity dom ~ polarity) =>
    SResetPolarity polarity
    resetPolarity @dom of { SResetPolarity (DomainConfigurationResetPolarity (KnownConf dom))
    SActiveHigh -> Bool
    True; SResetPolarity (DomainConfigurationResetPolarity (KnownConf dom))
    _ -> Bool
    False }
      rstOut :: Reset dom
    rstOut =
        case (forall (dom :: Domain) (sync :: ResetKind).
    (KnownDomain dom, DomainResetKind dom ~ sync) =>
    SResetKind sync
    resetKind @dom) of
          SResetKind (DomainConfigurationResetKind (KnownConf dom))
    SAsynchronous -> Signal dom Bool -> Reset dom
    forall (dom :: Domain).
    KnownDomain dom =>
    Signal dom Bool -> Reset dom
    unsafeToReset
                             (Signal dom Bool -> Reset dom) -> Signal dom Bool -> Reset dom
    forall a b. (a -> b) -> a -> b
    $ Clock dom
    -> Reset dom
    -> Enable dom
    -> Bool
    -> Signal dom Bool
    -> Signal dom Bool
    forall (dom :: Domain) a.
    (KnownDomain dom, NFDataX a) =>
    Clock dom
    -> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
    register Clock dom
    clk Reset dom
    rst Enable dom
    forall (dom :: Domain). Enable dom
    enableGen Bool
    isActiveHigh
                             (Signal dom Bool -> Signal dom Bool)
    -> Signal dom Bool -> Signal dom Bool
    forall a b. (a -> b) -> a -> b
    $ Clock dom
    -> Reset dom
    -> Enable dom
    -> Bool
    -> Signal dom Bool
    -> Signal dom Bool
    forall (dom :: Domain) a.
    (KnownDomain dom, NFDataX a) =>
    Clock dom
    -> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
    register Clock dom
    clk Reset dom
    rst Enable dom
    forall (dom :: Domain). Enable dom
    enableGen Bool
    isActiveHigh
                             (Signal dom Bool -> Signal dom Bool)
    -> Signal dom Bool -> Signal dom Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Signal dom Bool
    forall a. a -> Signal dom a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Bool -> Bool
    not Bool
    isActiveHigh)
          SResetKind (DomainConfigurationResetKind (KnownConf dom))
    SSynchronous  -> Signal dom Bool -> Reset dom
    forall (dom :: Domain).
    KnownDomain dom =>
    Signal dom Bool -> Reset dom
    unsafeToReset
                             (Signal dom Bool -> Reset dom) -> Signal dom Bool -> Reset dom
    forall a b. (a -> b) -> a -> b
    $ Clock dom
    -> Enable dom -> Bool -> Signal dom Bool -> Signal dom Bool
    forall (dom :: Domain) a.
    (KnownDomain dom, NFDataX a) =>
    Clock dom -> Enable dom -> a -> Signal dom a -> Signal dom a
    delay Clock dom
    clk Enable dom
    forall (dom :: Domain). Enable dom
    enableGen Bool
    isActiveHigh
                             (Signal dom Bool -> Signal dom Bool)
    -> Signal dom Bool -> Signal dom Bool
    forall a b. (a -> b) -> a -> b
    $ Clock dom
    -> Enable dom -> Bool -> Signal dom Bool -> Signal dom Bool
    forall (dom :: Domain) a.
    (KnownDomain dom, NFDataX a) =>
    Clock dom -> Enable dom -> a -> Signal dom a -> Signal dom a
    delay Clock dom
    clk Enable dom
    forall (dom :: Domain). Enable dom
    enableGen Bool
    isActiveHigh
                             (Signal dom Bool -> Signal dom Bool)
    -> Signal dom Bool -> Signal dom Bool
    forall a b. (a -> b) -> a -> b
    $ Reset dom -> Signal dom Bool
    forall (dom :: Domain). Reset dom -> Signal dom Bool
    unsafeFromReset Reset dom
    rst

    -- | Filter glitches from reset signals by only triggering a reset after it has
    -- been asserted for /glitchlessPeriod/ cycles. Similarly, it will stay
    -- asserted until a /glitchlessPeriod/ number of deasserted cycles have been
    -- observed.
    --
    -- This circuit can only be used on platforms supporting initial values. This
    -- restriction can be worked around by using 'unsafeResetGlitchFilter' but this
    -- is not recommended.
    --
    -- On platforms without initial values, you should instead use
    -- 'resetGlitchFilterWithReset' with an additional power-on reset, or
    -- 'holdReset' if filtering is only needed on deassertion.
    --
    -- At power-on, the reset will be asserted. If the filtered reset input remains
    -- unasserted, the output reset will deassert after /glitchlessPeriod/ clock
    -- cycles.
    --
    -- If @resetGlitchFilter@ is used in a domain with asynchronous resets
    -- ('Asynchronous'), @resetGlitchFilter@ will first synchronize the reset input
    -- with 'dualFlipFlopSynchronizer'.
    --
    -- === __Example 1__
    -- >>> let sampleResetN n = sampleN n . unsafeToActiveHigh
    -- >>> let resetFromList = unsafeFromActiveHigh . fromList
    -- >>> let rst = resetFromList [True, True, False, False, True, False, False, True, True, False, True, True]
    -- >>> sampleResetN 12 (resetGlitchFilter d2 (clockGen @XilinxSystem) rst)
    -- [True,True,True,True,False,False,False,False,False,True,True,True]
    resetGlitchFilter
      :: forall dom glitchlessPeriod
       . ( HasCallStack
         , HasDefinedInitialValues dom
         , 1 <= glitchlessPeriod
         )
      => SNat glitchlessPeriod
      -- ^ Consider a reset signal to be properly asserted after having seen the
      -- reset asserted for /glitchlessPeriod/ cycles straight.
      -> Clock dom
      -> Reset dom
      -> Reset dom
    resetGlitchFilter :: forall (dom :: Domain) (glitchlessPeriod :: Natural).
    (HasCallStack, HasDefinedInitialValues dom,
     1 <= glitchlessPeriod) =>
    SNat glitchlessPeriod -> Clock dom -> Reset dom -> Reset dom
    resetGlitchFilter = SNat glitchlessPeriod -> Clock dom -> Reset dom -> Reset dom
    forall (dom :: Domain) (glitchlessPeriod :: Natural).
    (HasCallStack, KnownDomain dom, 1 <= glitchlessPeriod) =>
    SNat glitchlessPeriod -> Clock dom -> Reset dom -> Reset dom
    unsafeResetGlitchFilter
    {-# INLINE resetGlitchFilter #-}

    -- | Filter glitches from reset signals by only triggering a reset after it has
    -- been asserted for /glitchlessPeriod/ cycles. Similarly, it will stay
    -- asserted until a /glitchlessPeriod/ number of deasserted cycles have been
    -- observed.
    --
    -- On platforms without initial values ('Unknown'), 'resetGlitchFilter' cannot
    -- be used and you should use 'resetGlitchFilterWithReset' with an additional
    -- power-on reset, or 'holdReset' if filtering is only needed on deassertion.
    --
    -- @unsafeResetGlitchFilter@ allows breaking the requirement of initial values,
    -- but by doing so it is possible that the design starts up with a period of up
    -- to /2 * glitchlessPeriod/ clock cycles where the reset output is unasserted
    -- (or longer in the case of glitches on the filtered reset input). This can
    -- cause a number of problems. The outputs\/tri-states of the design might
    -- output random things, including coherent but incorrect streams of data. This
    -- might have grave repercussions in the design's environment (sending network
    -- packets, overwriting non-volatile memory, in extreme cases destroying
    -- controlled equipment or causing harm to living beings, ...).
    --
    -- Without initial values, the synthesized result of @unsafeResetGlitchFilter@
    -- eventually correctly outputs a filtered version of the reset input. However,
    -- in simulation, it will indefinitely output an undefined value. This happens
    -- both in Clash simulation and in HDL simulation. Therefore, simulation should
    -- not include the @unsafeResetGlitchFilter@.
    --
    -- If @unsafeResetGlitchFilter@ is used in a domain with asynchronous resets
    -- ('Asynchronous'), @unsafeResetGlitchFilter@ will first synchronize the reset
    -- input with 'dualFlipFlopSynchronizer'.
    unsafeResetGlitchFilter
      :: forall dom glitchlessPeriod
       . ( HasCallStack
         , KnownDomain dom
         , 1 <= glitchlessPeriod
         )
      => SNat glitchlessPeriod
      -- ^ Consider a reset signal to be properly asserted after having seen the
      -- reset asserted for /glitchlessPeriod/ cycles straight.
      -> Clock dom
      -> Reset dom
      -> Reset dom
    unsafeResetGlitchFilter :: forall (dom :: Domain) (glitchlessPeriod :: Natural).
    (HasCallStack, KnownDomain dom, 1 <= glitchlessPeriod) =>
    SNat glitchlessPeriod -> Clock dom -> Reset dom -> Reset dom
    unsafeResetGlitchFilter SNat glitchlessPeriod
    glitchlessPeriod Clock dom
    clk =
      SNat glitchlessPeriod
    -> ((Bool, Index glitchlessPeriod)
        -> Signal dom (Bool, Index glitchlessPeriod)
        -> Signal dom (Bool, Index glitchlessPeriod))
    -> (Bool -> Signal dom Bool -> Signal dom Bool)
    -> Reset dom
    -> Reset dom
    forall (dom :: Domain) (glitchlessPeriod :: Natural) state.
    (HasCallStack, KnownDomain dom, 1 <= glitchlessPeriod,
     state ~ (Bool, Index glitchlessPeriod)) =>
    SNat glitchlessPeriod
    -> (state -> Signal dom state -> Signal dom state)
    -> (Bool -> Signal dom Bool -> Signal dom Bool)
    -> Reset dom
    -> Reset dom
    resetGlitchFilter# SNat glitchlessPeriod
    glitchlessPeriod (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    reg Bool -> Signal dom Bool -> Signal dom Bool
    dffSync
     where
      reg :: (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    reg = Clock dom
    -> Enable dom
    -> (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    forall (dom :: Domain) a.
    (KnownDomain dom, NFDataX a) =>
    Clock dom -> Enable dom -> a -> Signal dom a -> Signal dom a
    delay Clock dom
    clk Enable dom
    forall (dom :: Domain). Enable dom
    enableGen
      dffSync :: Bool -> Signal dom Bool -> Signal dom Bool
    dffSync = Clock dom
    -> Clock dom
    -> Reset dom
    -> Enable dom
    -> Bool
    -> Signal dom Bool
    -> Signal dom Bool
    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 dom
    clk Clock dom
    clk Reset dom
    forall (dom :: Domain). KnownDomain dom => Reset dom
    noReset Enable dom
    forall (dom :: Domain). Enable dom
    enableGen
    {-# INLINE unsafeResetGlitchFilter #-}

    -- | Filter glitches from reset signals by only triggering a reset after it has
    -- been asserted for /glitchlessPeriod/ cycles. Similarly, it will stay
    -- asserted until a /glitchlessPeriod/ number of deasserted cycles have been
    -- observed.
    --
    -- Compared to 'resetGlitchFilter', this function adds an additional power-on
    -- reset input. As soon as the power-on reset asserts, the reset output will
    -- assert, and after the power-on reset deasserts, the reset output will stay
    -- asserted for another /glitchlessPeriod/ clock cycles. This is identical
    -- behavior to 'holdReset' where it concerns the power-on reset, and differs
    -- from the filtered reset, which will only cause an assertion after
    -- /glitchlessPeriod/ cycles.
    --
    -- If @resetGlitchFilterWithReset@ is used in a domain with asynchronous resets
    -- ('Asynchronous'), @resetGlitchFilterWithReset@ will first synchronize the
    -- reset input with 'dualFlipFlopSynchronizer'.
    resetGlitchFilterWithReset
      :: forall dom glitchlessPeriod
       . ( HasCallStack
         , KnownDomain dom
         , 1 <= glitchlessPeriod
         )
      => SNat glitchlessPeriod
      -- ^ Consider a reset signal to be properly asserted after having seen the
      -- reset asserted for /glitchlessPeriod/ cycles straight.
      -> Clock dom
      -> Reset dom
      -- ^ The power-on reset for the glitch filter itself
      -> Reset dom
      -- ^ The reset that will be filtered
      -> Reset dom
    resetGlitchFilterWithReset :: forall (dom :: Domain) (glitchlessPeriod :: Natural).
    (HasCallStack, KnownDomain dom, 1 <= glitchlessPeriod) =>
    SNat glitchlessPeriod
    -> Clock dom -> Reset dom -> Reset dom -> Reset dom
    resetGlitchFilterWithReset SNat glitchlessPeriod
    glitchlessPeriod Clock dom
    clk Reset dom
    ownRst =
      SNat glitchlessPeriod
    -> ((Bool, Index glitchlessPeriod)
        -> Signal dom (Bool, Index glitchlessPeriod)
        -> Signal dom (Bool, Index glitchlessPeriod))
    -> (Bool -> Signal dom Bool -> Signal dom Bool)
    -> Reset dom
    -> Reset dom
    forall (dom :: Domain) (glitchlessPeriod :: Natural) state.
    (HasCallStack, KnownDomain dom, 1 <= glitchlessPeriod,
     state ~ (Bool, Index glitchlessPeriod)) =>
    SNat glitchlessPeriod
    -> (state -> Signal dom state -> Signal dom state)
    -> (Bool -> Signal dom Bool -> Signal dom Bool)
    -> Reset dom
    -> Reset dom
    resetGlitchFilter# SNat glitchlessPeriod
    glitchlessPeriod (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    reg Bool -> Signal dom Bool -> Signal dom Bool
    dffSync
     where
      reg :: (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    reg = Clock dom
    -> Reset dom
    -> Enable dom
    -> (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    -> Signal dom (Bool, Index glitchlessPeriod)
    forall (dom :: Domain) a.
    (KnownDomain dom, NFDataX a) =>
    Clock dom
    -> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
    register Clock dom
    clk Reset dom
    ownRst Enable dom
    forall (dom :: Domain). Enable dom
    enableGen
      dffSync :: Bool -> Signal dom Bool -> Signal dom Bool
    dffSync = Clock dom
    -> Clock dom
    -> Reset dom
    -> Enable dom
    -> Bool
    -> Signal dom Bool
    -> Signal dom Bool
    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 dom
    clk Clock dom
    clk Reset dom
    ownRst Enable dom
    forall (dom :: Domain). Enable dom
    enableGen
    {-# INLINE resetGlitchFilterWithReset #-}

    resetGlitchFilter#
      :: forall dom glitchlessPeriod state
       . ( HasCallStack
         , KnownDomain dom
         , 1 <= glitchlessPeriod
         , state ~ (Bool, Index glitchlessPeriod)
         )
      => SNat glitchlessPeriod
      -> (   state
          -> Signal dom state
          -> Signal dom state
         )
      -> (   Bool
          -> Signal dom Bool
          -> Signal dom Bool
         )
      -> Reset dom
      -> Reset dom
    resetGlitchFilter# :: forall (dom :: Domain) (glitchlessPeriod :: Natural) state.
    (HasCallStack, KnownDomain dom, 1 <= glitchlessPeriod,
     state ~ (Bool, Index glitchlessPeriod)) =>
    SNat glitchlessPeriod
    -> (state -> Signal dom state -> Signal dom state)
    -> (Bool -> Signal dom Bool -> Signal dom Bool)
    -> Reset dom
    -> Reset dom
    resetGlitchFilter# SNat glitchlessPeriod
    SNat state -> Signal dom state -> Signal dom state
    reg Bool -> Signal dom Bool -> Signal dom Bool
    dffSync Reset dom
    rstIn0 =
      let s' :: Signal dom state
    s' = state -> Bool -> state
    go (state -> Bool -> state)
    -> Signal dom state -> Signal dom (Bool -> state)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Signal dom state
    s Signal dom (Bool -> state) -> Signal dom Bool -> Signal dom state
    forall a b. Signal dom (a -> b) -> Signal dom a -> Signal dom b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> Signal dom Bool
    rstIn2
          s :: Signal dom state
    s  = state -> Signal dom state -> Signal dom state
    reg (Bool
    asserted, Index glitchlessPeriod
    0) Signal dom state
    s'
      in Signal dom Bool -> Reset dom
    forall (dom :: Domain).
    KnownDomain dom =>
    Signal dom Bool -> Reset dom
    unsafeToReset (Signal dom Bool -> Reset dom) -> Signal dom Bool -> Reset dom
    forall a b. (a -> b) -> a -> b
    $ (Bool, Index glitchlessPeriod) -> Bool
    forall a b. (a, b) -> a
    fst ((Bool, Index glitchlessPeriod) -> Bool)
    -> Signal dom (Bool, Index glitchlessPeriod) -> Signal dom Bool
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Signal dom state
    Signal dom (Bool, Index glitchlessPeriod)
    s
     where
      rstIn1 :: Signal dom Bool
    rstIn1 = Reset dom -> Signal dom Bool
    forall (dom :: Domain). Reset dom -> Signal dom Bool
    unsafeFromReset Reset dom
    rstIn0
      rstIn2 :: Signal dom Bool
    rstIn2 =
        case forall (dom :: Domain) (sync :: ResetKind).
    (KnownDomain dom, DomainResetKind dom ~ sync) =>
    SResetKind sync
    resetKind @dom of
          SResetKind (DomainConfigurationResetKind (KnownConf dom))
    SAsynchronous -> Bool -> Signal dom Bool -> Signal dom Bool
    dffSync Bool
    asserted Signal dom Bool
    rstIn1
          SResetKind (DomainConfigurationResetKind (KnownConf dom))
    SSynchronous -> Signal dom Bool
    rstIn1

      go :: state -> Bool -> state
      go :: state -> Bool -> state
    go (Bool
    state, Index glitchlessPeriod
    count) Bool
    reset
        | Bool
    reset Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    state    = (Bool
    state,     Index glitchlessPeriod
    0)
        | Index glitchlessPeriod
    count Index glitchlessPeriod -> Index glitchlessPeriod -> Bool
    forall a. Eq a => a -> a -> Bool
    == Index glitchlessPeriod
    forall a. Bounded a => a
    maxBound = (Bool -> Bool
    not Bool
    state, Index glitchlessPeriod
    0)
        | Bool
    otherwise         = (Bool
    state,     Index glitchlessPeriod
    count Index glitchlessPeriod
    -> Index glitchlessPeriod -> Index glitchlessPeriod
    forall a. Num a => a -> a -> a
    + Index glitchlessPeriod
    1)

      asserted :: Bool
      asserted :: Bool
    asserted =
        case forall (dom :: Domain) (polarity :: ResetPolarity).
    (KnownDomain dom, DomainResetPolarity dom ~ polarity) =>
    SResetPolarity polarity
    resetPolarity @dom of
          SResetPolarity (DomainConfigurationResetPolarity (KnownConf dom))
    SActiveHigh -> Bool
    True
          SResetPolarity (DomainConfigurationResetPolarity (KnownConf dom))
    SActiveLow -> Bool
    False

    -- | Hold reset for a number of cycles relative to an incoming reset signal.
    --
    -- Example:
    --
    -- >>> let sampleWithReset = sampleN 8 . unsafeToActiveHigh
    -- >>> sampleWithReset (holdReset @System clockGen enableGen (SNat @2) (resetGenN (SNat @3)))
    -- [True,True,True,True,True,False,False,False]
    --
    -- 'holdReset' holds the reset for an additional 2 clock cycles for a total
    -- of 5 clock cycles where the reset is asserted. 'holdReset' also works on
    -- intermediate assertions of the reset signal:
    --
    -- >>> let rst = fromList [True, False, False, False, True, False, False, False]
    -- >>> sampleWithReset (holdReset @System clockGen enableGen (SNat @2) (unsafeFromActiveHigh rst))
    -- [True,True,True,False,True,True,True,False]
    --
    holdReset
      :: forall dom n
       . KnownDomain dom
      => Clock dom
      -> Enable dom
      -- ^ Global enable
      -> SNat n
      -- ^ Hold for /n/ cycles, counting from the moment the incoming reset
      -- signal becomes deasserted.
      -> Reset dom
      -- ^ Reset to extend
      -> Reset dom
    holdReset :: forall (dom :: Domain) (n :: Natural).
    KnownDomain dom =>
    Clock dom -> Enable dom -> SNat n -> Reset dom -> Reset dom
    holdReset Clock dom
    clk Enable dom
    en SNat n
    SNat Reset dom
    rst =
      Signal dom Bool -> Reset dom
    forall (dom :: Domain).
    KnownDomain dom =>
    Signal dom Bool -> Reset dom
    unsafeFromActiveHigh ((Index (n + 1) -> Index (n + 1) -> Bool
    forall a. Eq a => a -> a -> Bool
    /=Index (n + 1)
    forall a. Bounded a => a
    maxBound) (Index (n + 1) -> Bool)
    -> Signal dom (Index (n + 1)) -> Signal dom Bool
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Signal dom (Index (n + 1))
    counter)
     where
      counter :: Signal dom (Index (n+1))
      counter :: Signal dom (Index (n + 1))
    counter = Clock dom
    -> Reset dom
    -> Enable dom
    -> Index (n + 1)
    -> Signal dom (Index (n + 1))
    -> Signal dom (Index (n + 1))
    forall (dom :: Domain) a.
    (KnownDomain dom, NFDataX a) =>
    Clock dom
    -> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
    register Clock dom
    clk Reset dom
    rst Enable dom
    en Index (n + 1)
    0 (SaturationMode -> Index (n + 1) -> Index (n + 1)
    forall a. SaturatingNum a => SaturationMode -> a -> a
    satSucc SaturationMode
    SatBound (Index (n + 1) -> Index (n + 1))
    -> Signal dom (Index (n + 1)) -> Signal dom (Index (n + 1))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Signal dom (Index (n + 1))
    counter)

    -- | Convert between different types of reset, adding a synchronizer when
    -- the domains are not the same. See 'resetSynchronizer' for further details
    -- about reset synchronization.
    --
    -- If @domA@ has 'Synchronous' resets, a flip-flop is inserted in @domA@ to
    -- filter glitches. This adds one @domA@ clock cycle delay.
    convertReset
      :: forall domA domB
       . ( KnownDomain domA
         , KnownDomain domB
         )
      => Clock domA
      -> Clock domB
      -> Reset domA
      -> Reset domB
    convertReset :: forall (domA :: Domain) (domB :: Domain).
    (KnownDomain domA, KnownDomain domB) =>
    Clock domA -> Clock domB -> Reset domA -> Reset domB
    convertReset Clock domA
    clkA Clock domB
    clkB Reset domA
    rstA0 = Reset domB
    rstB1
     where
      rstA1 :: Signal domA Bool
    rstA1 = Reset domA -> Signal domA Bool
    forall (dom :: Domain). Reset dom -> Signal dom Bool
    unsafeFromReset Reset domA
    rstA0
      rstA2 :: Signal domA Bool
    rstA2 =
        case (forall (dom :: Domain) (polarity :: ResetPolarity).
    (KnownDomain dom, DomainResetPolarity dom ~ polarity) =>
    SResetPolarity polarity
    resetPolarity @domA, forall (dom :: Domain) (polarity :: ResetPolarity).
    (KnownDomain dom, DomainResetPolarity dom ~ polarity) =>
    SResetPolarity polarity
    resetPolarity @domB) of
          (SResetPolarity (DomainConfigurationResetPolarity (KnownConf domA))
    SActiveLow, SResetPolarity (DomainConfigurationResetPolarity (KnownConf domB))
    SActiveLow)   -> Signal domA Bool
    rstA1
          (SResetPolarity (DomainConfigurationResetPolarity (KnownConf domA))
    SActiveHigh, SResetPolarity (DomainConfigurationResetPolarity (KnownConf domB))
    SActiveHigh) -> Signal domA Bool
    rstA1
          (SResetPolarity
       (DomainConfigurationResetPolarity (KnownConf domA)),
     SResetPolarity (DomainConfigurationResetPolarity (KnownConf domB)))
    _                          -> Bool -> Bool
    not (Bool -> Bool) -> Signal domA Bool -> Signal domA Bool
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Signal domA Bool
    rstA1
      rstA3 :: Signal domA Bool
    rstA3 =
        case forall (dom :: Domain) (sync :: ResetKind).
    (KnownDomain dom, DomainResetKind dom ~ sync) =>
    SResetKind sync
    resetKind @domA of
          SResetKind (DomainConfigurationResetKind (KnownConf domA))
    SSynchronous -> Clock domA
    -> Enable domA -> Bool -> Signal domA Bool -> Signal domA Bool
    forall (dom :: Domain) a.
    (KnownDomain dom, NFDataX a) =>
    Clock dom -> Enable dom -> a -> Signal dom a -> Signal dom a
    delay Clock domA
    clkA Enable domA
    forall (dom :: Domain). Enable dom
    enableGen Bool
    assertedA Signal domA Bool
    rstA2
          SResetKind (DomainConfigurationResetKind (KnownConf domA))
    _            -> Signal domA Bool
    rstA2
      rstB0 :: Reset domB
    rstB0 = Signal domB Bool -> Reset domB
    forall (dom :: Domain).
    KnownDomain dom =>
    Signal dom Bool -> Reset dom
    unsafeToReset (Signal domB Bool -> Reset domB) -> Signal domB Bool -> Reset domB
    forall a b. (a -> b) -> a -> b
    $ Clock domA -> Clock domB -> Signal domA Bool -> Signal domB Bool
    forall (dom1 :: Domain) (dom2 :: Domain) a.
    (KnownDomain dom1, KnownDomain dom2) =>
    Clock dom1 -> Clock dom2 -> Signal dom1 a -> Signal dom2 a
    unsafeSynchronizer Clock domA
    clkA Clock domB
    clkB Signal domA Bool
    rstA3
      rstB1 :: Reset domB
    rstB1 =
        case (forall (domA :: Domain) (domB :: Domain).
    (KnownDomain domA, KnownDomain domB) =>
    Maybe (domA :~: domB)
    sameDomain @domA @domB) of
          Just domA :~: domB
    Refl -> Reset domA
    Reset domB
    rstA0
          Maybe (domA :~: domB)
    Nothing   -> Clock domB -> Reset domB -> Reset domB
    forall (dom :: Domain).
    KnownDomain dom =>
    Clock dom -> Reset dom -> Reset dom
    resetSynchronizer Clock domB
    clkB Reset domB
    rstB0
      assertedA :: Bool
      assertedA :: Bool
    assertedA =
        case forall (dom :: Domain) (polarity :: ResetPolarity).
    (KnownDomain dom, DomainResetPolarity dom ~ polarity) =>
    SResetPolarity polarity
    resetPolarity @domA of
          SResetPolarity (DomainConfigurationResetPolarity (KnownConf domA))
    SActiveHigh -> Bool
    True
          SResetPolarity (DomainConfigurationResetPolarity (KnownConf domA))
    SActiveLow  -> Bool
    False