{-|
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 :: Reset dom
noReset = Signal dom Bool -> Reset dom
forall (dom :: Domain).
KnownDomain dom =>
Signal dom Bool -> Reset dom
unsafeFromActiveHigh (Bool -> Signal dom Bool
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 :: 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 :: 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
forall (polarity :: ResetPolarity).
(KnownDomain dom,
 DomainConfigurationResetPolarity (KnownConf 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 :: 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 :: 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
forall (polarity :: ResetPolarity).
(KnownDomain dom,
 DomainConfigurationResetPolarity (KnownConf 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 :: 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
forall (polarity :: ResetPolarity).
(KnownDomain dom,
 DomainConfigurationResetPolarity (KnownConf 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
forall (sync :: ResetKind).
(KnownDomain dom,
 DomainConfigurationResetKind (KnownConf 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 (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 :: SNat glitchlessPeriod -> Clock dom -> Reset dom -> Reset dom
resetGlitchFilter = SNat glitchlessPeriod -> Clock dom -> Reset dom -> Reset dom
forall (dom :: Domain) (glitchlessPeriod :: Nat).
(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 :: 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 :: Nat) 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 :: 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 :: Nat) 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# :: 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 (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
forall (sync :: ResetKind).
(KnownDomain dom,
 DomainConfigurationResetKind (KnownConf 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 (state, 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
forall (polarity :: ResetPolarity).
(KnownDomain dom,
 DomainConfigurationResetPolarity (KnownConf 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 :: 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 :: 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
forall (polarity :: ResetPolarity).
(KnownDomain domA,
 DomainConfigurationResetPolarity (KnownConf domA) ~ polarity) =>
SResetPolarity polarity
resetPolarity @domA, forall (dom :: Domain) (polarity :: ResetPolarity).
(KnownDomain dom, DomainResetPolarity dom ~ polarity) =>
SResetPolarity polarity
forall (polarity :: ResetPolarity).
(KnownDomain domB,
 DomainConfigurationResetPolarity (KnownConf domB) ~ 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
forall (sync :: ResetKind).
(KnownDomain domA,
 DomainConfigurationResetKind (KnownConf domA) ~ 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 ((KnownDomain domA, KnownDomain domB) => Maybe (domA :~: domB)
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
forall (polarity :: ResetPolarity).
(KnownDomain domA,
 DomainConfigurationResetPolarity (KnownConf domA) ~ polarity) =>
SResetPolarity polarity
resetPolarity @domA of
      SResetPolarity (DomainConfigurationResetPolarity (KnownConf domA))
SActiveHigh -> Bool
True
      SResetPolarity (DomainConfigurationResetPolarity (KnownConf domA))
SActiveLow  -> Bool
False