Added a way for users to be able to get evidence of whether two domai…

…ns are equal.

Fixed `resetSynchronizer` not synchronizing the reset correctly for synchronous domains.
Fixed `resetConvert` not correctly converting between synchronous and asynchronous domains.

changelog/2020-11-04T14_50_10+01_00_convertReset

@@ -0,0 +1,3 @@
+ADDED: Added 'Clash.Signal.sameDomain': Allows user obtain evidence whether two domains are equal.
+FIXED: Fixed 'Clash.Explicit.Reset.resetSynchronizer': The synchronizer was not synchronizing reset for synchronous domains correctly.
+FIXED: Fixed 'Clash.Explicit.Reset.convertReset': Reset conversion was never performed when converting between synchronous resets.

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

@@ -35,6 +35,7 @@ module Clash.Explicit.Reset
   ) where
 
 import           Data.Bits (testBit, shiftL, (.|.))
+import           Data.Type.Equality ((:~:)(Refl))
 import           GHC.Generics (Generic)
 
 import           Clash.Class.BitPack (pack)
@@ -51,7 +52,15 @@ import           Clash.XException (NFDataX, ShowX)
 import           GHC.TypeLits (type (+), KnownNat)
 
 
--- | Normally, asynchronous resets can be both asynchronously asserted and
+-- | 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
@@ -65,6 +74,10 @@ import           GHC.TypeLits (type (+), KnownNat)
 -- 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
@@ -107,7 +120,7 @@ import           GHC.TypeLits (type (+), KnownNat)
 -- @
 --
 -- === __Implementation details__
--- 'resetSynchronizer' implements the following circuit:
+-- 'resetSynchronizer' implements the following circuit for asynchronous domains:
 --
 -- @
 --                                   rst
@@ -126,6 +139,20 @@ import           GHC.TypeLits (type (+), KnownNat)
 --
 -- 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
@@ -134,11 +161,19 @@ resetSynchronizer
   -> Enable dom
   -- ^ Warning: this argument will be removed in future versions of Clash.
   -> Reset dom
-resetSynchronizer clk rst ena =
-  unsafeToReset (asyncReg (asyncReg (pure (not isActiveHigh))))
+resetSynchronizer clk rst _ = rstOut
  where
   isActiveHigh = case resetPolarity @dom of { SActiveHigh -> True; _ -> False }
-  asyncReg = asyncRegister# clk rst ena isActiveHigh isActiveHigh
+  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
 {-# NOINLINE resetSynchronizer #-} -- Give reset synchronizer its own HDL file
 
 data GlitchFilterState = Idle | InReset
@@ -232,8 +267,9 @@ holdReset clk en SNat rst =
   counter :: Signal dom (Index (n+1))
   counter = register clk rst en 0 (satSucc SatBound <$> counter)
 
--- | Convert between different types of reset, adding a synchronizer in case
--- it needs to convert from an asynchronous to a synchronous reset.
+-- | 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
@@ -243,15 +279,10 @@ convertReset
   -> Clock domB
   -> Reset domA
   -> Reset domB
-convertReset clkA clkB (unsafeToHighPolarity -> rstA0) =
-  unsafeFromHighPolarity rstA2
+convertReset clkA clkB rstA0 = rstA2
  where
-  rstA1 = unsafeSynchronizer clkA clkB rstA0
+  rstA1 = unsafeToReset (unsafeSynchronizer clkA clkB (unsafeFromReset rstA0))
   rstA2 =
-    case (resetKind @domA, resetKind @domB) of
-      (SSynchronous,  SSynchronous)  -> rstA1
-      (SAsynchronous, SAsynchronous) -> rstA1
-      (SSynchronous,  SAsynchronous) -> rstA1
-      (SAsynchronous, SSynchronous) ->
-        delay clkB enableGen True $
-          delay clkB enableGen True rstA1
+    case (sameDomain @domA @domB) of
+      Just Refl -> rstA0
+      Nothing   -> resetSynchronizer clkB rstA1 enableGen

clash-prelude/src/Clash/Signal.hs

@@ -90,6 +90,7 @@ module Clash.Signal
   , BiSignalDefault(..)
     -- * Domain
   , Domain
+  , sameDomain
   , KnownDomain(..)
   , KnownConfiguration
   , ActiveEdge(..)

clash-prelude/src/Clash/Signal/Internal.hs

@@ -39,6 +39,7 @@ module Clash.Signal.Internal
   , tail#
     -- * Domains
   , Domain
+  , sameDomain
   , KnownDomain(..)
   , KnownConfiguration
   , knownDomainByName
@@ -144,9 +145,10 @@ import Data.Data                  (Data)
 import Data.Default.Class         (Default (..))
 import Data.Hashable              (Hashable)
 import Data.Proxy                 (Proxy(..))
+import Data.Type.Equality         ((:~:))
 import GHC.Generics               (Generic)
 import GHC.Stack                  (HasCallStack)
-import GHC.TypeLits               (KnownSymbol, Nat, Symbol, type (<=))
+import GHC.TypeLits               (KnownSymbol, Nat, Symbol, type (<=), sameSymbol)
 import Language.Haskell.TH.Syntax -- (Lift (..), Q, Dec)
 import Language.Haskell.TH.Compat
 import Numeric.Natural            (Natural)
@@ -606,6 +608,14 @@ createDomain (VDomainConfiguration name period edge reset init_ polarity) =
 
 type Domain = Symbol
 
+-- | We either get evidence that this function was instantiated with the same
+-- domains, or Nothing.
+sameDomain
+  :: forall (domA :: Domain) (domB :: Domain)
+   . (KnownDomain domA, KnownDomain domB)
+  => Maybe (domA :~: domB)
+sameDomain = sameSymbol (Proxy @domA) (Proxy @domB)
+
 infixr 5 :-
 {- | Clash has synchronous 'Signal's in the form of:
 

tests/shouldwork/Signal/ResetSynchronizer.hs

@@ -28,23 +28,24 @@ testReset tbClk tbRst cClk =
   $ stimuliGenerator tbClk tbRst
     ( True
 
-      -- Reset synchronizer introduces a delay of two, but lets asynchronous
-      -- asserts through untouched. This means that for 'topEntity' we'll see
-      -- [R, R, R, R] for these cycles. Where the first two zeroes are caused by
-      -- 'resetSynchronizer's induced latency, the next zero by the first cycle
-      -- not in reset, and the last zero because we're in reset again (async
-      -- behavior).
+      -- Asynchronous resets:
+      --
+      --   Resets are asserted asynchronously and deasserted synchronously with
+      --   a delay of two cycles. This means that for 'topEntity' we'll see
+      --   [R, R, R, R] for the first batch of reset cycles. The first two Rs
+      --   are caused by  'resetSynchronizer's induced latency, the next zero
+      --   by the first cycle not in reset, and the last zero because we're in
+      --   reset again (async assertion behavior).
+      --
+      --   The second batch of resets is similar to ^, but the reset is held
+      --   a cycle longer so we should be able to see a count output.
+      --
+      -- Synchronous resets:
+      --
+      --   Synchronous resets are simply delayed for two cycles. Hence, we
+      --   should count up to the number of deasserted cycles.
       --
-      -- We should be able to see a difference between asynchronous and synchronous
-      -- resets here: the counter is driven by a register whose synchronicity
-      -- is imposed by the 'KnownDomain' constraint. Synchronous counters will
-      -- only see the reset asserted on the /next/ cycle, hence outputting
-      -- [R, R, R, 0] instead.
    :> False :> False :> False :> True
-
-      -- Similar to ^, but now we're out of of reset one cycle longer so we should
-      -- start seeing [R, R, R, 0, R] for asynchronous counters, and
-      -- [R, R, R, 0, 1] for synchronous ones.
    :> False :> False :> False :>  False :> True
    :> replicate d20 False )
 
@@ -75,11 +76,11 @@ polyTestBench ::
   (Signal System Bool, [ResetCount])
 polyTestBench Proxy = (done, sampleN 20 (polyTopEntity cClk cRst))
  where
-  rKind = resetKind @circuitDom
+  ror' = flip ror (resetKind @circuitDom)
   expectedOutput = outputVerifier tbClk tbRst
-    ( RRRRRRR :> RRRRRRR :> RRRRRRR :> RRRRRRR :> rOr 0 rKind
-   :> RRRRRRR :> RRRRRRR :> RRRRRRR :> Count 0 :> rOr 1 rKind
-   :> RRRRRRR :> RRRRRRR :> RRRRRRR :> Count 0 :> Count 1 :> Count 2
+    ( RRRRRRR :> RRRRRRR :> RRRRRRR :> RRRRRRR :> rOr' 0
+   :> rOr' 1  :> rOr' 2  :> RRRRRRR :> Count 0 :> rOr' 1
+   :> rOr' 2  :> rOr' 3  :> RRRRRRR :> Count 0 :> Count 1 :> Count 2
    :> Nil )
   done = expectedOutput (polyTopEntity cClk cRst)
   (tbClk, cClk) = biTbClockGen @System @circuitDom (not <$> done)