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

…ns are equal. Fixed `resetConvert` not correctly converting between synchronous domains.
clash-lang · Nov 4, 2020 · 0661388 · 0661388
1 parent d45b4ba
commit 0661388
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 11 deletions.
diff --git a/changelog/2020-11-04T14_50_10+01_00_convertReset b/changelog/2020-11-04T14_50_10+01_00_convertReset
@@ -0,0 +1,2 @@
+ADDED: Added 'Clash.Signal.sameDomain': Allows user obtain evidence whether two domains are equal.
+FIXED: Fixed 'Clash.Explicit.Reset.convertReset': Reset conversion was never performed when converting between synchronous resets.
diff --git a/clash-prelude/src/Clash/Explicit/Reset.hs b/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)
@@ -243,15 +244,14 @@ 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 = unsafeSynchronizer clkA clkB $ unsafeToHighPolarity 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, resetKind @domA, resetKind @domB) of
+      (Just Refl, _, _)       -> rstA0
+      (_, _,  SAsynchronous)  -> unsafeFromHighPolarity rstA1
+      (_, _, _)               ->
+        unsafeFromHighPolarity
+          $ delay clkB enableGen True
+          $ delay clkB enableGen True rstA1
diff --git a/clash-prelude/src/Clash/Signal.hs b/clash-prelude/src/Clash/Signal.hs
@@ -90,6 +90,7 @@ module Clash.Signal
   , BiSignalDefault(..)
     -- * Domain
   , Domain
+  , sameDomain
   , KnownDomain(..)
   , KnownConfiguration
   , ActiveEdge(..)

diff --git a/clash-prelude/src/Clash/Signal/Internal.hs b/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,16 @@ 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: