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

Utilities to deal with resets.
-}

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# 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
  , holdReset
  , convertReset

    -- Reexports
  , Reset
  , resetGen
  , resetGenN
  , resetKind
  , systemResetGen
  , unsafeToReset
  , unsafeFromReset
  , unsafeToHighPolarity
  , unsafeToLowPolarity
  , unsafeFromHighPolarity
  , unsafeFromLowPolarity
  ) where

import           Data.Bits (testBit, shiftL, (.|.))
import           Data.Type.Equality ((:~:)(Refl))
import           GHC.Generics (Generic)

import           Clash.Class.BitPack (pack)
import           Clash.Class.Resize (resize)
import           Clash.Class.Num (satSucc, SaturationMode(SatBound))
import           Clash.Explicit.Mealy
import           Clash.Explicit.Signal
import           Clash.Promoted.Nat
import           Clash.Signal.Internal
import           Clash.Sized.BitVector (BitVector)
import           Clash.Sized.Index (Index)
import           Clash.XException (NFDataX, ShowX)

import           GHC.TypeLits (type (+), KnownNat)

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

-- | 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 singal that is not synchronized to any other signals. It stabalizes
-- the clock and then synchronizes the reset signal.
--
-- @
-- topEntity
--   :: Clock  System
--   -> Reset  System
--   -> Signal System Bit
--   -> Signal System (BitVector 8)
-- topEntity clk rst key1 =
--     let  (pllOut,pllStable) = altpll (SSymbol @"altpll50") clk rst
--          rstSync            = 'resetSynchronizer' pllOut (unsafeToHighPolarity 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). 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). 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
{-# NOINLINE resetSynchronizer #-} -- Give reset synchronizer its own HDL file

data GlitchFilterState = Idle | InReset
  deriving ((forall x. GlitchFilterState -> Rep GlitchFilterState x)
-> (forall x. Rep GlitchFilterState x -> GlitchFilterState)
-> Generic GlitchFilterState
forall x. Rep GlitchFilterState x -> GlitchFilterState
forall x. GlitchFilterState -> Rep GlitchFilterState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep GlitchFilterState x -> GlitchFilterState
$cfrom :: forall x. GlitchFilterState -> Rep GlitchFilterState x
Generic, HasCallStack => String -> GlitchFilterState
GlitchFilterState -> Bool
GlitchFilterState -> ()
GlitchFilterState -> GlitchFilterState
(HasCallStack => String -> GlitchFilterState)
-> (GlitchFilterState -> Bool)
-> (GlitchFilterState -> GlitchFilterState)
-> (GlitchFilterState -> ())
-> NFDataX GlitchFilterState
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: GlitchFilterState -> ()
$crnfX :: GlitchFilterState -> ()
ensureSpine :: GlitchFilterState -> GlitchFilterState
$censureSpine :: GlitchFilterState -> GlitchFilterState
hasUndefined :: GlitchFilterState -> Bool
$chasUndefined :: GlitchFilterState -> Bool
deepErrorX :: String -> GlitchFilterState
$cdeepErrorX :: HasCallStack => String -> GlitchFilterState
NFDataX, Int -> GlitchFilterState -> ShowS
[GlitchFilterState] -> ShowS
GlitchFilterState -> String
(Int -> GlitchFilterState -> ShowS)
-> (GlitchFilterState -> String)
-> ([GlitchFilterState] -> ShowS)
-> Show GlitchFilterState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GlitchFilterState] -> ShowS
$cshowList :: [GlitchFilterState] -> ShowS
show :: GlitchFilterState -> String
$cshow :: GlitchFilterState -> String
showsPrec :: Int -> GlitchFilterState -> ShowS
$cshowsPrec :: Int -> GlitchFilterState -> ShowS
Show, Int -> GlitchFilterState -> ShowS
[GlitchFilterState] -> ShowS
GlitchFilterState -> String
(Int -> GlitchFilterState -> ShowS)
-> (GlitchFilterState -> String)
-> ([GlitchFilterState] -> ShowS)
-> ShowX GlitchFilterState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> ShowX a
showListX :: [GlitchFilterState] -> ShowS
$cshowListX :: [GlitchFilterState] -> ShowS
showX :: GlitchFilterState -> String
$cshowX :: GlitchFilterState -> String
showsPrecX :: Int -> GlitchFilterState -> ShowS
$cshowsPrecX :: Int -> GlitchFilterState -> ShowS
ShowX)

-- | Filter glitches from reset signals by only triggering a reset after it has
-- been asserted for /glitchlessPeriod/ cycles. It will then stay asserted for
-- as long as the given reset was asserted consecutively.
--
-- If synthesized on a domain with initial values, 'resetGlitchFilter' will
-- output an asserted reset for /glitchlessPeriod/ cycles (plus any cycles added
-- by the given reset). If initial values can't be used, it will only output
-- defined reset values after /glitchlessPeriod/ cycles.
--
-- === __Example 1__
-- >>> let sampleResetN n = sampleN n . unsafeToHighPolarity
-- >>> let resetFromList = unsafeFromHighPolarity . fromList
-- >>> let rst = resetFromList [True, True, False, False, True, False, False, True, True, False, True]
-- >>> sampleResetN 12 (resetGlitchFilter d2 systemClockGen rst)
-- [True,True,True,True,False,False,False,False,False,True,True,False]
resetGlitchFilter
  :: forall dom glitchlessPeriod n
   . ( KnownDomain dom
     , glitchlessPeriod ~ (n + 1) )
  => 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
SNat Clock dom
clk Reset dom
rst =
  Signal dom Bool -> Reset dom
forall (dom :: Domain). Signal dom Bool -> Reset dom
unsafeToReset (Clock dom
-> Reset dom
-> Enable dom
-> (GlitchFilterState
    -> BitVector glitchlessPeriod -> (GlitchFilterState, Bool))
-> GlitchFilterState
-> Signal dom (BitVector glitchlessPeriod)
-> Signal dom Bool
forall (dom :: Domain) s i o.
(KnownDomain dom, NFDataX s) =>
Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> (s, o))
-> s
-> Signal dom i
-> Signal dom o
mealy Clock dom
clk Reset dom
noReset Enable dom
forall (dom :: Domain). Enable dom
enableGen GlitchFilterState
-> BitVector glitchlessPeriod -> (GlitchFilterState, Bool)
go GlitchFilterState
Idle Signal dom (BitVector glitchlessPeriod)
shiftReg)
 where
  shiftReg :: Signal dom (BitVector glitchlessPeriod)
shiftReg =
    Clock dom
-> Enable dom
-> BitVector glitchlessPeriod
-> Signal dom (BitVector glitchlessPeriod)
-> Signal dom (BitVector 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 BitVector glitchlessPeriod
noGlitch (BitVector glitchlessPeriod -> Bool -> BitVector glitchlessPeriod
forall (m :: Nat).
KnownNat m =>
BitVector (m + 1) -> Bool -> BitVector (m + 1)
shiftInLsb (BitVector glitchlessPeriod -> Bool -> BitVector glitchlessPeriod)
-> Signal dom (BitVector glitchlessPeriod)
-> Signal dom (Bool -> BitVector glitchlessPeriod)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (BitVector glitchlessPeriod)
shiftReg Signal dom (Bool -> BitVector glitchlessPeriod)
-> Signal dom Bool -> Signal dom (BitVector glitchlessPeriod)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Reset dom -> Signal dom Bool
forall (dom :: Domain). Reset dom -> Signal dom Bool
unsafeFromReset Reset dom
rst)

  go :: GlitchFilterState
-> BitVector glitchlessPeriod -> (GlitchFilterState, Bool)
go GlitchFilterState
gfs BitVector glitchlessPeriod
sreg
    | BitVector glitchlessPeriod
sreg BitVector glitchlessPeriod -> BitVector glitchlessPeriod -> Bool
forall a. Eq a => a -> a -> Bool
== BitVector glitchlessPeriod
noGlitch = (GlitchFilterState
InReset, Bool
asserted)
    | GlitchFilterState
Idle <- GlitchFilterState
gfs = (GlitchFilterState
Idle, Bool -> Bool
not Bool
asserted)
    | Bool
otherwise = (if Bool
msb Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
asserted then GlitchFilterState
InReset else GlitchFilterState
Idle, Bool
msb)
   where
    msb :: Bool
msb = BitVector glitchlessPeriod -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BitVector glitchlessPeriod
sreg (forall a. (Num a, KnownNat n) => a
forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @n)

  noGlitch :: BitVector glitchlessPeriod
  noGlitch :: BitVector glitchlessPeriod
noGlitch = if Bool
asserted then BitVector glitchlessPeriod
forall a. Bounded a => a
maxBound else BitVector glitchlessPeriod
forall a. Bounded a => a
minBound

  noReset :: Reset dom
  noReset :: Reset dom
noReset = Signal dom Bool -> Reset dom
forall (dom :: Domain). Signal dom Bool -> Reset dom
unsafeToReset (Bool -> Signal dom Bool
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> Bool
not Bool
asserted))

  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

  shiftInLsb :: forall m. KnownNat m => BitVector (m + 1) -> Bool -> BitVector (m + 1)
  shiftInLsb :: BitVector (m + 1) -> Bool -> BitVector (m + 1)
shiftInLsb BitVector (m + 1)
bv Bool
s = BitVector (m + 1) -> Int -> BitVector (m + 1)
forall a. Bits a => a -> Int -> a
shiftL BitVector (m + 1)
bv Int
1 BitVector (m + 1) -> BitVector (m + 1) -> BitVector (m + 1)
forall a. Bits a => a -> a -> a
.|. BitVector 1 -> BitVector (m + 1)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (Bool -> BitVector (BitSize Bool)
forall a. BitPack a => a -> BitVector (BitSize a)
pack Bool
s)
{-# NOINLINE resetGlitchFilter #-} -- Give reset glitch filter its own HDL file

-- | Hold reset for a number of cycles relative to an incoming reset signal.
--
-- Example:
--
-- >>> let sampleWithReset = sampleN 8 . unsafeToHighPolarity
-- >>> 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) (unsafeFromHighPolarity 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
unsafeFromHighPolarity ((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.
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
rstA2
 where
  rstA1 :: Reset domB
rstA1 = Signal domB Bool -> Reset domB
forall (dom :: Domain). Signal dom Bool -> Reset dom
unsafeToReset (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 (Reset domA -> Signal domA Bool
forall (dom :: Domain). Reset dom -> Signal dom Bool
unsafeFromReset Reset domA
rstA0))
  rstA2 :: Reset domB
rstA2 =
    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
rstA1