clash-prelude: Add warning to holdReset and implement correct stretchReset

Author: rowanG077

changelog/2026-01-08T16_58_32+01_00_add_stretchreset

@@ -0,0 +1,2 @@
+FIXED: Added warnings to `holdReset` [#3115](https://github.com/clash-lang/clash-compiler/issues/3115)
+FIXED: Added `stretchReset` as safe replacement for `holdReset` [#3115](https://github.com/clash-lang/clash-compiler/issues/3115)

clash-prelude/src/Clash/Explicit/Reset.hs

@@ -16,6 +16,7 @@ Utilities to deal with resets.
 
 {-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}
 {-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}
+{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Extra.Solver #-}
 
 module Clash.Explicit.Reset
   ( -- Defined in this module
@@ -24,6 +25,7 @@ module Clash.Explicit.Reset
   , resetGlitchFilterWithReset
   , unsafeResetGlitchFilter
   , holdReset
+  , stretchReset
   , convertReset
   , noReset
   , andReset, unsafeAndReset
@@ -55,11 +57,15 @@ import           Clash.Class.Num (satSucc, SaturationMode(SatBound))
 import           Clash.Explicit.Signal
 import           Clash.Explicit.Synchronizer (dualFlipFlopSynchronizer)
 import           Clash.Promoted.Nat
+import           Clash.Promoted.Nat.Literals
 import           Clash.Signal.Internal
 import           Clash.Sized.Index (Index)
+import           Clash.Magic (clashCompileError)
 
 import           GHC.Stack (HasCallStack)
-import           GHC.TypeLits (type (+), type (<=))
+import           GHC.TypeLits (type (+), type (-), type (<=))
+
+import GHC.TypeLits.Extra (Max)
 
 {- $setup
 >>> import Clash.Explicit.Prelude
@@ -399,7 +405,15 @@ resetGlitchFilter# SNat reg dffSync rstIn0 =
       SActiveHigh -> True
       SActiveLow -> False
 
--- | Hold reset for a number of cycles relative to an incoming reset signal.
+-- | Hold/stretch reset for a number of cycles relative to an incoming reset
+-- signal.
+--
+-- __NB__: 'holdReset' is unsafe for asynchronous resets. It can cause
+-- spurious resets.
+-- For synchronous the output is pessimistic since it is driven by combinational
+-- logic.
+-- You probably want to use 'stretchReset' which is safe but has slightly
+-- different timing behaviour.
 --
 -- Example:
 --
@@ -433,6 +447,135 @@ holdReset clk en SNat rst =
   counter :: Signal dom (Index (n+1))
   counter = register clk rst en 0 (satSucc SatBound <$> counter)
 
+-- | Hold/stretch reset for a number of cycles relative to an incoming reset
+-- signal. This is a safe replacement for `holdReset`. There are some
+-- differences in behaviour for synchronous resets and asynchronous resets.
+--
+-- Synchronous resets
+--
+-- If used with a synchronous reset the assertion of the reset is delayed by 1
+-- cycle. If your domain can support initial values the first clock cycle
+-- after boot the reset will be asserted. Afterwards the reset keeps being
+-- asserted for (n + 1) cycles.
+--
+-- Examples on a domain with synchronous reset and supporting initial values:
+--
+-- >>> let sampleWithReset = sampleN 8 . unsafeToActiveHigh
+-- >>> let stretchResetBy2 = stretchReset @XilinxSystem clockGen enableGen (SNat @2)
+-- >>> sampleWithReset (stretchResetBy2 (resetGenN (SNat @3)))
+-- [True,True,True,True,True,True,False,False]
+--
+-- The first 3 cycles the input reset is asserted and `stretchReset` should
+-- stretch it by 2 cycles. That results in a reset that is asserted for 6
+-- cycles. This additional cycle is due to the first cycle always being reset if
+-- initial values are supported.  'stretchReset' also works on intermediate
+-- assertions of the reset signal:
+--
+-- >>> let rst = fromList [False, False, False, True, False, False, False, False]
+-- >>> sampleWithReset (stretchResetBy2 (unsafeFromActiveHigh rst))
+-- [True,True,True,False,False,True,True,False]
+--
+-- Here it again shows that on boot the reset is asserted for (n + 1) cycles
+-- And then after 4 cycles the input reset is asserted. Notice the delay on
+-- the output reset.
+--
+-- Asynchronous resets
+--
+-- If used with an asynchronous reset the minimum stretch period is always three
+-- cycles. This is due to an additional reset synchronizer that is inserted.
+-- The synchronizer itself consumes two cycles and the stretch adds at least
+-- one cycle, hence the minimum of three. There is no delay between assertion
+-- of the input and the assertion of the output.
+--
+-- Example with asynchronous reset:
+--
+-- >>> let sampleWithReset = sampleN 9 . unsafeToActiveHigh
+-- >>> let stretchResetBy3 = stretchReset @System clockGen enableGen (SNat @3)
+-- >>> sampleWithReset (stretchResetBy3 (resetGenN (SNat @3)))
+-- [True,True,True,True,True,True,False,False,False]
+--
+-- 'stretchReset' holds the reset for an additional 3 clock cycles for a total
+-- of 6 clock cycles where the reset is asserted. 'stretchReset' also works on
+-- intermediate assertions of the reset signal:
+--
+-- >>> let rst = fromList [False, False, False, False, True, False, False, False, False]
+-- >>> sampleWithReset (stretchResetBy3 (unsafeFromActiveHigh rst))
+-- [True,True,True,False,True,True,True,True, False]
+--
+-- Notice here that on startup it always resets for exactly the specified amount
+-- of cycles. In addition it appears to reset for (n + 1) cycles on a trigger.
+-- However the first asserted cycle is the asynchronous assertion so we don't
+-- count it as a full cycle.
+--
+stretchReset
+  :: forall dom n
+   . KnownDomain dom
+  => Clock dom
+  -> Enable dom
+  -- ^ Global enable
+  -> SNat n
+  -- ^ Hold for /n/ cycles
+  -> Reset dom
+  -- ^ Reset to extend
+  -> Reset dom
+stretchReset clk en n@SNat rst = case (resetKind @dom, compareSNat d1 (SNat @(Max 2 (Max 1 n - 1)))) of
+  (SSynchronous, _) -> stretchResetSync clk en n rst
+  (SAsynchronous, SNatGT) -> clashCompileError "stretchReset: Impossible 1 <= Max 2 (Max 1 n - 1) does not hold. Contact clash developers at: https://github.com/clash-lang/clash-compiler/issues"
+  (SAsynchronous, SNatLE) -> stretchResetAsync clk en n rst
+
+stretchResetSync
+  :: forall dom n
+   . KnownDomain dom
+  => DomainResetKind dom ~ 'Synchronous
+  => Clock dom
+  -> Enable dom
+  -- ^ Global enable
+  -> SNat n
+  -- ^ Hold for /n/ cycles
+  -> Reset dom
+  -- ^ Reset to extend
+  -> Reset dom
+stretchResetSync clk en SNat rst = unsafeToReset (delay clk en isActiveHigh rawRst)
+ where
+  counter :: Signal dom (Index (n + 1))
+  counter = register clk rst en 0 (satSucc SatBound <$> counter)
+  rawRst :: Signal dom Bool
+  rawRst = case resetPolarity @dom of
+    SActiveHigh -> (/=maxBound) <$> counter
+    SActiveLow -> (==maxBound) <$> counter
+
+  isActiveHigh = case resetPolarity @dom of { SActiveHigh -> True; _ -> False }
+
+stretchResetAsync
+  :: forall dom n
+   . KnownDomain dom
+  => DomainResetKind dom ~ 'Asynchronous
+  => 1 <= Max 2 (Max 1 n - 1)
+  => 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
+stretchResetAsync clk en SNat rst = rstOut
+ where
+  -- This ensures the index at least has one cycle for counting.
+  counter :: Signal dom (Index ((Max 2 ((Max 1 n) - 1))))
+  counter = register clk rst en 0 (satSucc SatBound <$> counter)
+  rawRst :: Signal dom Bool
+  rawRst = case resetPolarity @dom of
+    SActiveHigh -> (/=maxBound) <$> counter
+    SActiveLow -> (==maxBound) <$> counter
+
+  isActiveHigh = case resetPolarity @dom of { SActiveHigh -> True; _ -> False }
+  rstOut = unsafeToReset
+              $ register clk (unsafeToReset rawRst) en isActiveHigh
+              $ register clk (unsafeToReset rawRst) en isActiveHigh
+              $ pure (not isActiveHigh)
+
 -- | Convert between different types of reset, adding a synchronizer when
 -- the domains are not the same. See 'resetSynchronizer' for further details
 -- about reset synchronization.

clash-prelude/src/Clash/Signal.hs

@@ -157,6 +157,7 @@ module Clash.Signal
   , resetSynchronizer
   , resetGlitchFilter
   , holdReset
+  , stretchReset
     -- * Enabling
   , Enable
   , toEnable
@@ -1635,26 +1636,104 @@ testFor
   -> Property
 testFor n s = property (and (Clash.Signal.sampleN n s))
 
--- | Hold reset for a number of cycles relative to an implicit reset signal.
+-- __NB__: 'holdReset' is unsafe for asynchronous resets. It can cause
+-- spurious resets.
+-- For synchronous the output is pessimistic since it is driven by combinational
+-- logic.
+-- You probably want to use 'stretchReset' which is safe but has slightly
+-- different timing behaviour.
 --
 -- Example:
 --
--- >>> sampleN @System 8 (unsafeToActiveHigh (holdReset (SNat @2)))
--- [True,True,True,False,False,False,False,False]
+-- >>> holdResetBool = unsafeToActiveHigh . (holdReset @System)
+-- >>> sampleN 8 (exposeReset (holdResetBool (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 3 clock cycles where the reset is asserted.
+-- 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]
+-- >>> sampleN 8 (exposeReset (holdResetBool (SNat @2)) (unsafeFromActiveHigh rst))
+-- [True,True,True,False,True,True,True,False]
 --
 holdReset
   :: forall dom m
    . HiddenClockResetEnable dom
   => SNat m
-  -- ^ Hold for /m/ cycles, counting from the moment the incoming reset
-  -- signal becomes deasserted.
+  -- ^ Hold for /m/ cycles
   -> Reset dom
 holdReset m =
   hideClockResetEnable (\clk rst en -> E.holdReset clk en m rst)
 
+
+-- | Hold/stretch reset for a number of cycles relative to an incoming reset
+-- signal. This is a safe replacement for `holdReset`. There are some
+-- differences in behaviour for synchronous resets and asynchronous resets.
+--
+-- Synchronous resets
+--
+-- If used with a synchronous reset the assertion of the reset is delayed by 1
+-- cycle. If your domain can support initial values the first clock cycle
+-- after boot the reset will be asserted. Afterwards the reset keeps being
+-- asserted for (n + 1) cycles.
+--
+-- Examples on a domain with synchronous reset and supporting initial values:
+--
+-- >>> stretchResetBool = unsafeToActiveHigh . (stretchReset @System)
+-- >>> sampleN 8 (exposeReset (stretchResetBool (SNat @2)) (resetGenN (SNat @3)))
+-- [True,True,True,True,True,True,False,False]
+--
+-- The first 3 cycles the input reset is asserted and `stretchReset` should
+-- stretch it by 2 cycles. That results in a reset that is asserted for 6
+-- cycles. This additional cycle is due to the first cycle always being reset if
+-- initial values are supported.  'stretchReset' also works on intermediate
+-- assertions of the reset signal:
+--
+-- >>> let rst = fromList [False, False, False, True, False, False, False, False]
+-- >>> sampleN 8 (exposeReset (stretchResetBool (SNat @2)) (unsafeFromActiveHigh rst)))
+-- [True,True,True,False,False,True,True,False]
+--
+-- Here it again shows that on boot the reset is asserted for (n + 1) cycles
+-- And then after 4 cycles the input reset is asserted. Notice the delay on
+-- the output reset.
+--
+-- Asynchronous resets
+--
+-- If used with an asynchronous reset the minimum stretch period is always three
+-- cycles. This is due to an additional reset synchronizer that is inserted.
+-- The synchronizer itself consumes two cycles and the stretch adds at least
+-- one cycle, hence the minimum of three. There is no delay between assertion
+-- of the input and the assertion of the output.
+--
+-- Example with asynchronous reset:
+--
+-- >>> stretchResetBool = unsafeToActiveHigh . (stretchReset @XilinxSystem)
+-- >>> sampleN 8 (exposeReset (stretchResetBool (SNat @2)) (resetGenN (SNat @3)))
+-- [True,True,True,True,True,True,False,False,False]
+--
+-- 'stretchReset' holds the reset for an additional 3 clock cycles for a total
+-- of 6 clock cycles where the reset is asserted. 'stretchReset' also works on
+-- intermediate assertions of the reset signal:
+--
+-- >>> let rst = fromList [False, False, False, False, True, False, False, False, False]
+-- >>> sampleN 8 (exposeReset (stretchResetBool (SNat @2)) (unsafeFromActiveHigh rst)))
+-- [True,True,True,False,True,True,True,True, False]
+--
+-- Notice here that on startup it always resets for exactly the specified amount
+-- of cycles. In addition it appears to reset for (n + 1) cycles on a trigger.
+-- However the first asserted cycle is the asynchronous assertion so we don't
+-- count it as a full cycle.
+--
+stretchReset
+  :: forall dom m
+   . HiddenClockResetEnable dom
+  => SNat m
+  -- ^ Hold for /m/ cycles
+  -> Reset dom
+stretchReset m =
+  hideClockResetEnable (\clk rst en -> E.stretchReset clk en m rst)
+
 -- | Like 'fromList', but resets on reset and has a defined reset value.
 --
 -- >>> let rst = unsafeFromActiveHigh (fromList [True, True, False, False, True, False])