content: {-|
  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 = unsafeFromActiveHigh (pure 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 = 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 (unsafeFromReset -> rst0) (unsafeFromReset -> rst1) =
    unsafeToReset $
      case resetPolarity @dom of
        SActiveHigh -> rst0 .||. rst1
        SActiveLow  -> rst0 .&&. rst1
  
  -- | Output reset will be asserted when both input resets are asserted
  andReset ::
    forall dom .
    HasSynchronousReset dom =>
    Reset dom ->
    Reset dom ->
    Reset dom
  andReset = 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 (unsafeFromReset -> rst0) (unsafeFromReset -> rst1) =
    unsafeToReset $
      case resetPolarity @dom of
        SActiveHigh -> rst0 .&&. rst1
        SActiveLow  -> rst0 .||. 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 clk rst = rstOut
   where
    isActiveHigh = case resetPolarity @dom of { SActiveHigh -> True; _ -> False }
    rstOut =
      case (resetKind @dom) of
        SAsynchronous -> unsafeToReset
                           $ register clk rst enableGen isActiveHigh
                           $ register clk rst enableGen isActiveHigh
                           $ pure (not isActiveHigh)
        SSynchronous  -> unsafeToReset
                           $ delay clk enableGen isActiveHigh
                           $ delay clk enableGen isActiveHigh
                           $ unsafeFromReset 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 = 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 glitchlessPeriod clk =
    resetGlitchFilter# glitchlessPeriod reg dffSync
   where
    reg = delay clk enableGen
    dffSync = dualFlipFlopSynchronizer clk clk noReset 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 glitchlessPeriod clk ownRst =
    resetGlitchFilter# glitchlessPeriod reg dffSync
   where
    reg = register clk ownRst enableGen
    dffSync = dualFlipFlopSynchronizer clk clk ownRst 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# SNat reg dffSync rstIn0 =
    let s' = go <$> s <*> rstIn2
        s  = reg (asserted, 0) s'
    in unsafeToReset $ fst <$> s
   where
    rstIn1 = unsafeFromReset rstIn0
    rstIn2 =
      case resetKind @dom of
        SAsynchronous -> dffSync asserted rstIn1
        SSynchronous -> rstIn1
  
    go :: state -> Bool -> state
    go (state, count) reset
      | reset == state    = (state,     0)
      | count == maxBound = (not state, 0)
      | otherwise         = (state,     count + 1)
  
    asserted :: Bool
    asserted =
      case resetPolarity @dom of
        SActiveHigh -> True
        SActiveLow -> 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 clk en SNat rst =
    unsafeFromActiveHigh ((/=maxBound) <$> counter)
   where
    counter :: Signal dom (Index (n+1))
    counter = register clk rst en 0 (satSucc SatBound <$> 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 clkA clkB rstA0 = rstB1
   where
    rstA1 = unsafeFromReset rstA0
    rstA2 =
      case (resetPolarity @domA, resetPolarity @domB) of
        (SActiveLow, SActiveLow)   -> rstA1
        (SActiveHigh, SActiveHigh) -> rstA1
        _                          -> not <$> rstA1
    rstA3 =
      case resetKind @domA of
        SSynchronous -> delay clkA enableGen assertedA rstA2
        _            -> rstA2
    rstB0 = unsafeToReset $ unsafeSynchronizer clkA clkB rstA3
    rstB1 =
      case (sameDomain @domA @domB) of
        Just Refl -> rstA0
        Nothing   -> resetSynchronizer clkB rstB0
    assertedA :: Bool
    assertedA =
      case resetPolarity @domA of
        SActiveHigh -> True
        SActiveLow  -> False
  