Clock and reset modelling

1. The situation in CLaSH 0.6 (and earlier)

In CLaSH 0.6 and earlier, synchronous signals in CLaSH are modelled as streams of values, one value for every cycle of the clock. Additionally, a signal is annotated with the clock domain to which it is synchronised:

data Clock = Clk Symbol Nat

data Signal (clk :: Clock) a = a :- Signal clk a

instance Functor (Signal clk) where ...
instance Applicative (Signal clk) where ...
instance Show a => Show (Signal clk a) where ...

The most basic memory primitive is register, which gets a singleton clock, and a reset value:

data SSymbol :: Symbol -> * where ...
data SNat :: Nat -> * where ...
data SClock (clk :: Clock) where
   SClock :: SSymbol name -> SNat rate -> SClock ('Clk name rate)

register :: SClock clk -> a -> Signal clk a -> Signal clk a
register _ i s = i :- s

As you can see, the singleton clock, SClock clk, is only used to annotate the register with its clock domain clk, and nothing else. Also note that the specification does not indicate what reset behaviour the synthesized register should have: synchronous or asynchronous reset, or whether it is active-high, or active-low/negated. At the moment, the CLaSH compiler opts to implement registers with active-low/negated, asynchronous resets.

So how does clock routing work if the register primitive does not use its singleton clock argument? Well, the CLaSH compiler implicitly routes clock and reset signal based on whether:

A primitive definition indicates it needed a clock or reset signal, using the special ~CLK[...] and ~RES[...] holes.
And underlying component needs clocks and or resets.

Lastly, for the purpose of synthesis, we use TopEntity annotation pragmas, specifically, the ClockSource, to tell the CLaSH compiler, whether, and if so, what component it should use to generate a clock signal. Additionally, if we use a ClockSource, we expect this clock-source to have a port indicating whether generated clock is stable, and attach the reset-signal corresponding to clock to this lock/stable output-port.

1.1 Improving the CLaSH 0.6 clock/reset situation

The CLaSH 0.6 situation with regards to clocks and resets has grown somewhat organically, without too much planning. This has led to some deficiencies, and "missing" features, which are given below in random order:

Clock signals and reset pins cannot be mapped to specifically named pins using TopEntity annotations (See https://github.com/clash-lang/clash-compiler/issues/145).
- Related: reset signals cannot be separately connected from clock signals.
There is no support for gated clocks.
PLLs, and other clock sources, cannot be specified as normal primitives, which lead to the need to update the TopEntity to support things like PLLs with differential inputs: https://github.com/clash-lang/clash-prelude/commit/4ba0d55912429ac2f95367c8710dad082985f4ff#diff-bd030b0acb573174890730e856b38bb4
- Related: reset synchronisers cannot be defined at all (they are currently derived by the CLaSH compiler).
There is no way to specify the reset behaviour of the memory primitives (active-high vs active-low, synchronous vs asynchronous, etc.)
- Related: Memory elements cannot be reset within CLaSH using their reset ports, i.e., in order to have a memory component with a synchronous reset, a user would have to write something like:
```
regReset :: SClock clk -> a -> Signal clk Bool -> Signal clk a -> Signal clk a
regReset clk i r d = register clk i (mux r (pure i) d)
```
  Thus creating extra logic in terms of mux, instead of being able to use the reset logic already available in the register primitive.
Memory primitives with no reset, such as blockRam, have their memory content initialised to undefined. The problem with undefined is that evaluating it leads to Error: undefined. I would be nice to have an explicit undefined, i.e.:
```
newtype X a = X {unX :: Maybe a}
  deriving (Num,Functor,etc.)
```
where the CLaSH compiler, considers X as a "transparant" type-constructor: the resulting HDL does not get the extra tag-bit for the Maybe.

The output of these reset-less memory primitives would then be Signal clk (X a) to indicate that the output is potentially undefined.
In simulation, all clock domains appear to exit reset at the same time. However, when TopEntity annotations and ClockSources are used, CLaSH adds reset-synchronisers for every domain. This means that components in a fast clock domain exit their reset state faster that components in a slow clock domain. Hence there is a simulation/synthesis mismatch for the reset behaviour of multiple clock domains.

Also, every clock domain get completely separate reset synchronisers, where in some situations chained reset synchronisers might be preferable.
feel free to add more problems with the clock/reset situation here

2. Ideas for CLaSH 0.7/1.0 (and later)

For version 0.7/1.0 of CLaSH, we will keep using the 0.6 stream-of-values definition for signals, however, instead of annotating the signal with its "clock", we annotate it with its "domain":

data Domain = Domain { domainName :: Symbol, clockRate :: Nat }

data Signal (domain :: Domain) a = a :- Signal domain a
infixr 5 :-

instance Foldable (Signal domain) where
  foldr f z (a :- s) = a `f` (foldr f z s)

instance Show a => Show (Signal domain a) where
  showsPrec _ = showList . toList

instance Functor (Signal domain) where
  fmap f (s :- ss) = f s :- fmap f ss

instance Applicative (Signal domain) where
  pure x = let s = x :- s in s
  (f :- fs) <*> ~(a :- as) = f a :- (fs <*> as)

Next follow some potential ideas to solve some of the problems that exist in CLaSH 0.6 (and earlier).

2.1 Dealing with `undefined`

So, initially, I thought it would be a good idea to explicitly model undefined using the code below:

2.1.1 Explicit modeling of `undefined` (a not so good idea)

newtype X a = X' { unX :: Maybe a }
  deriving (Functor,Applicative,Monad)

toX :: a -> X a
toX = X' . Just
{-# NOINLINE toX #-}

fromX :: X a -> a
fromX = fromJust . unX
{-# NOINLINE toX #-}

-- | Explicit undefined
pattern X :: X a
pattern X <- X' Nothing
  where
    X = X' Nothing

instance Show a => Show (X a) where
  show X = "X"
  show a = show . fromX

class Bundle a where
  type Unbundled (domain :: Domain) a  = res | res -> domain
  type Unbundled domain a = Signal domain a

  type UnbundledX (domain :: Domain) a = res | res -> domain
  type UnbundledX domain a = Signal domain (X a)

  bundle :: Unbundled domain a -> Signal domain a
  default bundle :: Signal domain a -> Signal domain a
  bundle s = s

  unbundle :: Signal domain a -> Unbundled domain a
  default unbundle :: Signal domain a -> Signal domain a
  unbundle s = s

  bundleX :: UnbundledX domain a -> Signal domain (X a)
  default bundleX :: Signal domain (X a) -> Signal domain (X a)
  bundleX s = s

  unbundleX :: Signal domain (X a) -> UnbundledX domain a
  default unbundleX :: Signal domain (X a) -> Signal domain (X a)
  unbundleX s = s

instance Bundle (a,b) where
  type Unbundled  domain (a,b) = (Signal domain a, Signal domain b)
  type UnbundledX domain (a,b) = (Signal domain (X a), Signal domain (X b))
  bundle (x,y)  = liftA2 (,) x y
  unbundle xy   = (fst <$> xy, snd <$> xy)
  bundleX (x,y) = liftA2 (liftA2 (,)) x y
  unbundleX xy  = ((fst <$>) <$> xy, (snd <$>) <$> xy)

We can then model a dflipflop (without reset) like so:

delay :: Signal domain a -> Signal domain (X a)
delay s = X :- (toX <$> s)

While working on explicit reset lines (described later), I noticed that working with an explicitly modeled undefined works out pretty terribly as it starts to creep up everywhere once it is introduced. As such, this approach was abandoned.

2.1.2 Catching `undefined`

So let's go back to the original problem definition (+extra emphasis):

Memory primitives with no reset, such as blockRam, have their memory content initialised to undefined. The problem with undefined is that evaluating it leads to Error: undefined

Haskell/CLaSH, is a lazy language, so when are we actually evaluating undefined in such a way that it lead to Error: undefined? This usually happens when we try to display the output of our circuits! (printing values in the interactive interpreter, writing to file, etc.)

So what we can do is make a new Exception type, X, and a special ShowX type-class that prints "X" when it catches an X exception:

{-# LANGUAGE DefaultSignatures   #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE MagicHash           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

module ShowX where

import Control.Exception
import GHC.Exts
import GHC.Generics
import GHC.Show
import GHC.Stack
import System.IO.Unsafe

newtype X = X String

instance Show X where
  show = coerce

instance Exception X

throwX :: HasCallStack => String -> a
throwX msg = throw (X ("X: " ++ msg ++ "\n" ++ prettyCallStack callStack))

showXWith :: (a -> ShowS) -> a -> ShowS
showXWith f x =
  \s -> unsafePerformIO (catch (f <$> evaluate x <*> pure s)
                               (\(X _) -> return ('X': s)))

showsPrecXWith :: (Int -> a -> ShowS) -> Int -> a -> ShowS
showsPrecXWith f n = showXWith (f n)

showsX :: ShowX a => a -> ShowS
showsX = showsPrecX 0

class ShowX a where
  showsPrecX :: Int -> a -> ShowS

  showX :: a -> String
  showX x = showsX x ""

  showListX :: [a] -> ShowS
  showListX ls s = showListX__ showsX ls s

  default showsPrecX :: (Generic a, GShowX (Rep a)) => Int -> a -> ShowS
  showsPrecX = genericShowsPrecX

showListX__ :: (a -> ShowS) -> [a] -> ShowS
showListX__ showx = showXWith go
  where
    go []     s = "[]" ++ s
    go (x:xs) s = '[' : showx x (showl xs)
      where
        showl []     = ']':s
        showl (y:ys) = ',' : showx y (showl ys)

data ShowType = Rec        -- Record
              | Tup        -- Tuple
              | Pref       -- Prefix
              | Inf String -- Infix

genericShowsPrecX :: (Generic a, GShowX (Rep a)) => Int -> a -> ShowS
genericShowsPrecX n = gshowsPrecX Pref n . from

instance ShowX ()
instance (ShowX a, ShowX b) => ShowX (a,b)
instance (ShowX a, ShowX b, ShowX c) => ShowX (a,b,c)

instance {-# OVERLAPPABLE #-} ShowX a => ShowX [a] where
  showsPrecX _ = showListX

instance ShowX Bool

instance ShowX Double where
  showsPrecX = showsPrecXWith showsPrec

instance (ShowX a, ShowX b) => ShowX (Either a b)

instance ShowX Float where
  showsPrecX = showsPrecXWith showsPrec

instance ShowX Int where
  showsPrecX = showsPrecXWith showsPrec

instance ShowX Integer where
  showsPrecX = showsPrecXWith showsPrec

instance ShowX a => ShowX (Maybe a)

instance {-# OVERLAPPING #-} ShowX String where
  showsPrecX = showsPrecXWith showsPrec

class GShowX f where
  gshowsPrecX :: ShowType -> Int -> f a -> ShowS
  isNullary   :: f a -> Bool
  isNullary = error "generic showX (isNullary): unnecessary case"

instance GShowX U1 where
  gshowsPrecX _ _ U1 = id
  isNullary _ = True

instance (ShowX c) => GShowX (K1 i c) where
  gshowsPrecX _ n (K1 a) = showsPrecX n a
  isNullary _ = False

instance (GShowX a, Constructor c) => GShowX (M1 C c a) where
  gshowsPrecX _ n c@(M1 x) =
    case fixity of
      Prefix ->
        showParen (n > appPrec && not (isNullary x))
          ( (if conIsTuple c then id else showString (conName c))
          . (if isNullary x || conIsTuple c then id else showString " ")
          . showBraces t (gshowsPrecX t appPrec x))
      Infix _ m -> showParen (n > m) (showBraces t (gshowsPrecX t m x))
      where fixity = conFixity c
            t = if conIsRecord c then Rec else
                  case conIsTuple c of
                    True -> Tup
                    False -> case fixity of
                                Prefix    -> Pref
                                Infix _ _ -> Inf (show (conName c))
            showBraces :: ShowType -> ShowS -> ShowS
            showBraces Rec     p = showChar '{' . p . showChar '}'
            showBraces Tup     p = showChar '(' . p . showChar ')'
            showBraces Pref    p = p
            showBraces (Inf _) p = p

            conIsTuple :: C1 c f p -> Bool
            conIsTuple y = tupleName (conName y) where
              tupleName ('(':',':_) = True
              tupleName _           = False

instance (Selector s, GShowX a) => GShowX (M1 S s a) where
  gshowsPrecX t n s@(M1 x) | selName s == "" =   gshowsPrecX t n x
                           | otherwise       =   showString (selName s)
                                               . showString " = "
                                               . gshowsPrecX t 0 x
  isNullary (M1 x) = isNullary x

instance (GShowX a) => GShowX (M1 D d a) where
  gshowsPrecX t = showsPrecXWith go
    where go n (M1 x) = gshowsPrecX t n x

instance (GShowX a, GShowX b) => GShowX (a :+: b) where
  gshowsPrecX t n (L1 x) = gshowsPrecX t n x
  gshowsPrecX t n (R1 x) = gshowsPrecX t n x

instance (GShowX a, GShowX b) => GShowX (a :*: b) where
  gshowsPrecX t@Rec     n (a :*: b) =
    gshowsPrecX t n     a . showString ", " . gshowsPrecX t n     b
  gshowsPrecX t@(Inf s) n (a :*: b) =
    gshowsPrecX t n     a . showString s    . gshowsPrecX t n     b
  gshowsPrecX t@Tup     n (a :*: b) =
    gshowsPrecX t n     a . showChar ','    . gshowsPrecX t n     b
  gshowsPrecX t@Pref    n (a :*: b) =
    gshowsPrecX t (n+1) a . showChar ' '    . gshowsPrecX t (n+1) b

  -- If we have a product then it is not a nullary constructor
  isNullary _ = False

-- Unboxed types
instance GShowX UChar where
  gshowsPrecX _ _ (UChar c)   = showsPrec 0 (C# c) . showChar '#'
instance GShowX UDouble where
  gshowsPrecX _ _ (UDouble d) = showsPrec 0 (D# d) . showString "##"
instance GShowX UFloat where
  gshowsPrecX _ _ (UFloat f)  = showsPrec 0 (F# f) . showChar '#'
instance GShowX UInt where
  gshowsPrecX _ _ (UInt i)    = showsPrec 0 (I# i) . showChar '#'
instance GShowX UWord where
  gshowsPrecX _ _ (UWord w)   = showsPrec 0 (W# w) . showString "##"

printX :: ShowX a => a -> IO ()
printX x = putStrLn $ showX x

The way this works is that we use throwX "message", instead of error "undefined" or undefined, at places where a value it undefined, but is not really a failure/error state of the circuit.

So we can now define delay as:

delay :: Signal domain a -> Signal domain a
delay s = withFrozenCallStack (throwX "delay': initial value undefined") :- s

Now, when we use the normal show function we get:

*Signal> show (delay (pure True))
"[*** Exception: delay: initial value undefined
CallStack (from HasCallStack):
  delay, called at <interactive>:10:7 in interactive:Ghci1

But when we use showX, we see:

*Signal> take 20 $ showX (delay (pure True))
"[X,True,True,True,Tr"

Also, by starting the interactive interpreter with the -interactive-print=ShowX.printX flag, the default printing behaviour is to use showX instead of show:

*Signal> take 5 $ toList $ delay (pure True)
[X,True,True,True,True]

2.2 Explicit clock lines

As proposed in https://github.com/clash-lang/clash-prelude/pull/36, in order for things like PLLs to be "normal" primitives we can model clock lines explicitly. When we do this, we can also model clock gating at the same time.

We can do this by embedding a signal of type Bool in the clock line, which indicates whether the clock line is active or inactive/gated:

data ClockKind = Original | Derived

data Clock (clockKind :: ClockKind) (domain :: Domain) where
  Clock' :: { clkEn :: Signal domain Bool } -> Clock clockKind domain
  -- ^ Will not be exported

-- | Only the Clock pattern will be exported
pattern Clock :: Signal domain Bool -> Clock Original domain
pattern Clock en <- Clock' en
  where
    Clock en = Clock' en

See Section 3. why we make the ClockKind distinction, and why we have the Clock pattern synonym.

The register function then only update its state when the clock is active:

import Control.Applicative

mux :: Applicative f => f Bool -> f a -> f a -> f a
mux = liftA3 (\b t f -> if b then t else f)

register' :: Clock clk domain -> a -> Signal domain a -> Signal domain a
register' (Clock' en) i d =
  let q  = reg q'
      q' = mux en d q
  in  q
  where reg s = i :- s

With the above definition of register', the reset logic must be asynchronous as the memory primitive is initially set to the reset value i regardless of whether the clock is active or not.

2.2.1 `unsafeSynchronizer` primitive:

Now that clock lines are explicitly explicitly modelled, we must also redefine the unsafeSynchronizer primitive, which in CLaSH 0.6 used to be defined as:

unsafeSynchronizer :: SClock clk1
                   -> SClock clk2
                   -> Signal' clk1 a
                   -> Signal' clk2 a

Now that Clocks are actual clock lines (and no longer just proxies for clock domains), it becomes weird that unsafeSynchronizer gets actual clock lines. So instead I propose

unsafeSynchronizer :: forall (dom1 :: Domain) (dom2 :: Domain) a nm1 r1 nm2 r2 .
                      ( dom1 ~ ('Domain nm1 r1), dom2 ~ ('Domain nm2 r2)
                      , KnownNat r1, KnownNat r2)
                   => Signal dom1 a
                   -> Signal dom2 a
unsafeSynchronizer = undefined -- no need to implement it right now

Now, the reason we use explicit forall, is so that we have full control in which order types can be applied using visible type applications. So we can then simply write (using -XTypeApplications):

*Signal> type System = 'Domain "System" 1000
*Signal> type VGA = 'Domain "VGA" 200
*Signal> :t unsafeSynchronizer @System @VGA
unsafeSynchronizer @System @VGA :: Signal System a -> Signal VGA a

2.2.2 Clock gating

Using this new definition for Clock and register, clock gating can now simply be implemented as:

clockGate :: Clock clk domain -> Signal domain Bool -> Clock Derived domain
clockGate (Clock' en) en' = Clock' ((&&) <$> en <*> en'))

2.2.3 Clock primitives

We can now define a PLL primitive by:

data SNat :: Nat -> * where
  SNat :: KnownNat n => SNat n

pll :: forall numerator denominator x y nm .
       ((x * numerator) ~ (y * denominator), KnownNat x, KnownNat y)
    => SNat numerator
    -> SNat denominator
    -> Clock Original ('Domain nm x)
    -> Clock Original ('Domain nm y)
pll num denom _ = Clock (pure True)

2.2.4 Implicit routing of clock signals

Using implicit parameters, we can implicitly (at the term-level) route clock signals:

register :: (?clk :: Clock Original domain) 
         => a -> Signal domain a -> Signal domain a
register = register' ?clk

And use register without having to provide the Clock argument:

*Signal> :t register True
register True
  :: (?clk::Clock 'Original domain) =>
     Signal domain Bool -> Signal domain Bool

2.3 Explicit reset lines

The deficiencies of 0.6 that haven't been dealt with so far are all related to explicit reset signals:

Reset signals cannot be separately connected from clock signals.
Reset synchronisers cannot be defined at all (they are currently derived by the CLaSH compiler).
There is no way to specify the reset behaviour of the memory primitives (active-high vs active-low, synchronous vs asynchronous, etc.)
Memory elements cannot be reset within CLaSH using their reset ports.
In simulation, all clock domains appear to exit reset at the same time. However, when TopEntity annotations and ClockSources are used, CLaSH adds reset-synchronisers for every domain. This means that components in a fast clock domain exit their reset state faster that components in a slow clock domain. Hence there is a simulation/synthesis mismatch for the reset behaviour of multiple clock domains. Also, every clock domain get completely separate reset synchronisers, where in some situations chained reset synchronisers might be preferable.

2.3.1 Pitfalls

The following are just some random thoughts/concerns with regards to reset lines

Until now, time step 0 (zero), has always been defined as the clock cycle on which the component comes out of reset. However, with user-controllable resets, it is not like we are "resetting time", whenever the reset is asserted. Consequently, there are two options:

Time step 0 (zero) is the clock cycle on which the component comes out of reset for "the first time"
Time step 0 (zero) is simply the first clock cycle, and reset might not have been asserted/desasserted yet.

This could mean that even memory elements with reset lines might start in an undefined state. Luckily, we have already covered how to handle undefined values.

While signals are annotated with their clock domain (to enforce explicit clock domain crossing, which in turn reduces the chance for accidental meta-stability), they are not annotated with their reset domain. This becomes a problem when we are using asynchronous resets, and two communicating components are in different reset domains, as this can induce meta-stability. There are several half/non-solutions:

Annotate signals with their reset domain, and only allow synchronous resets. This would mean that components in the same clock-domain, but different reset domains, can never induce meta-stability as the resets are synchronised to the clock. Components on different clock domains must by definition then also have different reset domains (synchronous resets only), and so the clock domain crossing logic will take care of the reset domain crossing.

The problem with synchronous resets are:
- They introduce propagation delays in the data-paths
- They need an active flank of the clock to bring a memory element in a known reset state, and so do not play well with clock gating.

I would like to find a solution where we can use asynchronous resets, and completely avoid accidental meta-stability, i.e. reset domains must be explicitly crossed using something similar to unsafeSynchronise.

CONCLUSION

A synchronous reset is linked to a certain clock (domain), meaning a synchronous reset domain and a clock domain are the same thing. So this means that reset domain crossing is already handled by unsafeSynchronise. The problem is asynchronous resets, as they operate independently from any clock. So we must be able to distinguish two asynchronous reset lines from each other, and this is a problem because no matter how we annotate reset lines at the type level, two reset lines with equal reset types can have different values and hence introduce meta-stability.

2.3.2 Best solution (so far)

The presented solution annotates both synchronous and asynchronous resets with their (clock) domain. Then, using the no-shadowing policy described in Section 3., we ensure that there can only ever be one asynchronous reset-line belonging to a certain clock domain, ensuring that reset assertion can never accidentally introduce meta-stability.

So we define reset lines by:

data ResetKind = Synchronous | Asynchronous

data Reset (resetKind :: ResetKind) (domain :: Domain) where
  Sync  :: Signal domain Bool -> Reset Synchronous  domain
  Async :: Signal domain Bool -> Reset Asynchronous domain

Where we can distinguish asynchronous from synchronous reset lines at the type level. We can subsequently define the register' primitive as:

register' :: HasCallStack => Reset reset domain -> Clock clk domain 
          -> a -> Signal domain a -> Signal domain a
register' (Sync r) (Clock' en) i d =
  let q  = reg q'
      q' = mux en d' q
      d' = mux r d (pure i) -- negated reset
  in  q
  where reg s = withFrozenCallStack (throwX msg) :- s
        msg   = "register': initial value undefined"

register' (Async r) (Clock' en) i d =
  let q  = reg q'
      q' = mux en d q
  in  mux r q (pure i) -- negated reset
  where reg s = withFrozenCallStack (throwX msg) :- s
        msg   = "register': initial value undefined"

register :: (?reset :: Reset Asynchronous domain, ?clk :: Clock Original domain)
         => a -> Signal domain a -> Signal domain a
register = register' ?reset ?clk

With register', the developer can now specify whether she wants an asynchronous reset or a synchronous reset. There is however no choice between negated and "normal" reset: the reset line is currently negated by default. An option would be to have two register primitives, one with a "normal" reset line, and another with a negated reset.

One of the reasons to have explicit reset lines is so that a developer can define her own reset synchroniser. To do this, we need to be able to treat reset lines as "normal" Boolean values; there are however some caveats:

-- It is HIGHLY unsafe to treat Asynchronous resets as Bool signals due to:
-- * meta-stability
-- * combinational loops

-- | ´unsafeFromAsyncReset' is HIGHLY unsafe
unsafeFromAsyncReset :: Reset Asynchronous domain -> Signal domain Bool
unsafeFromAsyncReset (Async r) = r

-- | 'unsafeToAsyncReset' is HIGHLY unsafe
unsafeToAsyncReset :: Signal domain Bool -> Reset Asynchronous domain
unsafeToAsyncReset r = Async r

-- It is safe to treat Synchronous resets as Bool signals
fromSyncReset :: Reset Synchronous domain -> Signal domain Bool
fromSyncReset (Sync r) = r

toSyncReset :: Signal domain Bool -> Reset Synchronous domain
toSyncReset r = Sync r

Prefixing the conversion functions for asynchronous resets with the word unsafe is hopefully a good enough measure to prevent accidental meta-stability by misuse of asynchronous reset lines.

We can now finally define a reset synchroniser using the "unsafe" methods:

resetSynchroniser :: Reset Asynchronous domain -> Clock clk domain
                  -> Reset Asynchronous domain
resetSynchroniser r c =
  let r1 = register' r c False (pure True)
      r2 = register' r c False r1
  in  unsafeToAsyncReset r2

And here are more prelude functions using the new clock/reset lines:

class Bundle a where
  type Unbundled (domain :: Domain) a  = res | res -> domain
  type Unbundled domain a = Signal domain a

  bundle :: Unbundled domain a -> Signal domain a
  default bundle :: Signal domain a -> Signal domain a
  bundle s = s

  unbundle :: Signal domain a -> Unbundled domain a
  default unbundle :: Signal domain a -> Signal domain a
  unbundle s = s

instance Bundle (a,b) where
  type Unbundled  domain (a,b) = (Signal domain a, Signal domain b)
  bundle (x,y)  = liftA2 (,) x y
  unbundle xy   = (fst <$> xy, snd <$> xy)

mealy' :: Reset reset domain -> Clock clk domain 
       -> (s -> i -> (s,o)) -> s -> Signal domain i -> Signal domain o
mealy' res clk f iS = \i -> let (s',o) = unbundle $ f <$> s <*> i
                                s      = register' res clk iS s'
                            in  o

mealy :: (?res :: Reset Asynchronous domain, ?clk :: Clock Original domain)
      => (s -> i -> (s,o))
      -> s
      -> Signal domain i
      -> Signal domain o
mealy = mealy' ?res ?clk

type System = 'Domain "system" 1000
systemClock = Clock @System (pure True)
systemReset = Async @System (False :- pure True)

simulate :: ((?res :: Reset Asynchronous System, ?clk :: Clock Original System) 
                   => Signal System a -> Signal System b)
         -> [a] -> [b]
simulate f xs = let ?clk = systemClock in
                let ?res = systemReset
                in  toList (f (fromList xs))

Which we can use like:

macT s (x,y) = (s',s)
  where
    s' = s + (x * y)

mac = mealy macT 0

testMac = simulate mac [(1,1),(2,2),(3,3),(4,4)]

where evaluation testMac gives:

*Signal> testMac 
[0,1,5,14,*** Exception: finite list
CallStack (from HasCallStack):
  error, called at Signal.hs:51:32 in main:Signal

3. No shadowing policy for clocks and resets

When clock and reset lines were implicitly routed by the CLaSH compiler, there was an implicit uniqueness constraint on the clock and reset lines. Meta-stability-safety "guarantees" of CLaSH's type-system were based on the uniqueness of clock and reset lines. But with explicit clock and reset lines, a user can (accidentally) circumvent these safety checks.

That is, it is now possible to have two clock lines with the same type, but with different values, meaning that it would be possible to connect two components to separate clock lines without the type system complaining, and thus making it possible to introduce accidental meta-stability.

So there are 4 different reset and clock lines:

Reset Asynchronous domain
Reset Synchronous domain
Clock Original domain
Clock Derived domain

We will go over each of them, and determine whether having two variables of their type in scope is potentially dangerous.

Reset sitiation 1.
```
f :: Reset Asynchronous domain -> Reset Asynchronous domain -> ... 
f x y = ...
```
This is potentially dangerous, because although x and y belong to the same domain according to their type, there is no guarantee that they actually have the same source. This means that one component can enter its reset state asynchronously with respect to the other, thus potentially introducing meta-stability.
Reset situation 2.
```
f :: Reset Synchronous domain -> Reset Asynchronous domain -> ... 
f x y = ...
```
This is potentially dangerous, because although x and y belong to the same domain according to their type, there is no guarantee that they actually have the same source. This means that if a component g connected to reset line y, which feeds data to component h (connect to reset x), asynchronously enters a reset state; then component h might go into a meta-stable state.
Reset situation 3.
```
f :: Reset Synchronous domain -> Reset Synchronous domain -> ... 
f x y = ...
```
There is no problem with f, because even though x and y can have different values, components connected to these reset lines are reset synchronously, and there is no chance of meta-stability.
We need to add some no-shadowing checks to the CLaSH compiler, so that during synthesis we get errors/warnings if there are two variables that represent the same clock/reset line.
Clock situation 1.
```
f :: Clock Original domain -> Clock Original domain -> ... 
f x y = ...
```
This is potentially dangerous, because although x and y belong to the same domain according to their type, there is no guarantee that they actually have the same source. We can thus have components operating at two different clock rates without the compiler warning us that we have place a clock domain synchroniser between the components. This is clearly a dangerous potential source of meta-stability.
Clock situation 2.
```
f :: Clock Derived domain -> Clock Original domain -> ... 
f x y = ...
```
There is no danger here, because the derived clock, x, is a gated version of y, and thus both lines are operating at the same frequency.
Clock situation 3.
```
f :: Clock Derived domain -> Clock Derived domain -> ... 
f x y = ...
```
There is no danger here, because x and y are both gated version of a master clock, meaning both are operating at the same frequency.

The no-shadowing rules are hence as follows:

If there is an Asychronous reset line in scope for a certain domain, it must be the only reset line in scope for that domain.
If there is an Original clock line in scope for a certain domain, there can be no other Original clock lines in scope for that domain.

Also, all the Clock arguments of the topEntity must be of kind Original so as not to "trick" the above no-shadowing rules.

Finally, the no-shadowing error can be turned into a no-shadowing warning using a command-line flag; just in case a developer really wants to have more than 1 asynchronous reset line per clock domain.

Appendix A: complete definitions

The complete ShowX.hs file:

{-# LANGUAGE DefaultSignatures   #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE MagicHash           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

module ShowX where

import Control.Exception
import GHC.Exts
import GHC.Generics
import GHC.Show
import GHC.Stack
import System.IO.Unsafe

newtype X = X String

instance Show X where
  show = coerce

instance Exception X

throwX :: HasCallStack => String -> a
throwX msg = throw (X ("X: " ++ msg ++ "\n" ++ prettyCallStack callStack))

showXWith :: (a -> ShowS) -> a -> ShowS
showXWith f x =
  \s -> unsafePerformIO (catch (f <$> evaluate x <*> pure s)
                               (\(X _) -> return ('X': s)))

showsPrecXWith :: (Int -> a -> ShowS) -> Int -> a -> ShowS
showsPrecXWith f n = showXWith (f n)

showsX :: ShowX a => a -> ShowS
showsX = showsPrecX 0

class ShowX a where
  showsPrecX :: Int -> a -> ShowS

  showX :: a -> String
  showX x = showsX x ""

  showListX :: [a] -> ShowS
  showListX ls s = showListX__ showsX ls s

  default showsPrecX :: (Generic a, GShowX (Rep a)) => Int -> a -> ShowS
  showsPrecX = genericShowsPrecX

showListX__ :: (a -> ShowS) -> [a] -> ShowS
showListX__ showx = showXWith go
  where
    go []     s = "[]" ++ s
    go (x:xs) s = '[' : showx x (showl xs)
      where
        showl []     = ']':s
        showl (y:ys) = ',' : showx y (showl ys)

data ShowType = Rec        -- Record
              | Tup        -- Tuple
              | Pref       -- Prefix
              | Inf String -- Infix

genericShowsPrecX :: (Generic a, GShowX (Rep a)) => Int -> a -> ShowS
genericShowsPrecX n = gshowsPrecX Pref n . from

instance ShowX ()
instance (ShowX a, ShowX b) => ShowX (a,b)
instance (ShowX a, ShowX b, ShowX c) => ShowX (a,b,c)

instance {-# OVERLAPPABLE #-} ShowX a => ShowX [a] where
  showsPrecX _ = showListX

instance ShowX Bool

instance ShowX Double where
  showsPrecX = showsPrecXWith showsPrec

instance (ShowX a, ShowX b) => ShowX (Either a b)

instance ShowX Float where
  showsPrecX = showsPrecXWith showsPrec

instance ShowX Int where
  showsPrecX = showsPrecXWith showsPrec

instance ShowX Integer where
  showsPrecX = showsPrecXWith showsPrec

instance ShowX a => ShowX (Maybe a)

instance {-# OVERLAPPING #-} ShowX String where
  showsPrecX = showsPrecXWith showsPrec

class GShowX f where
  gshowsPrecX :: ShowType -> Int -> f a -> ShowS
  isNullary   :: f a -> Bool
  isNullary = error "generic showX (isNullary): unnecessary case"

instance GShowX U1 where
  gshowsPrecX _ _ U1 = id
  isNullary _ = True

instance (ShowX c) => GShowX (K1 i c) where
  gshowsPrecX _ n (K1 a) = showsPrecX n a
  isNullary _ = False

instance (GShowX a, Constructor c) => GShowX (M1 C c a) where
  gshowsPrecX _ n c@(M1 x) =
    case fixity of
      Prefix ->
        showParen (n > appPrec && not (isNullary x))
          ( (if conIsTuple c then id else showString (conName c))
          . (if isNullary x || conIsTuple c then id else showString " ")
          . showBraces t (gshowsPrecX t appPrec x))
      Infix _ m -> showParen (n > m) (showBraces t (gshowsPrecX t m x))
      where fixity = conFixity c
            t = if conIsRecord c then Rec else
                  case conIsTuple c of
                    True -> Tup
                    False -> case fixity of
                                Prefix    -> Pref
                                Infix _ _ -> Inf (show (conName c))
            showBraces :: ShowType -> ShowS -> ShowS
            showBraces Rec     p = showChar '{' . p . showChar '}'
            showBraces Tup     p = showChar '(' . p . showChar ')'
            showBraces Pref    p = p
            showBraces (Inf _) p = p

            conIsTuple :: C1 c f p -> Bool
            conIsTuple y = tupleName (conName y) where
              tupleName ('(':',':_) = True
              tupleName _           = False

instance (Selector s, GShowX a) => GShowX (M1 S s a) where
  gshowsPrecX t n s@(M1 x) | selName s == "" =   gshowsPrecX t n x
                           | otherwise       =   showString (selName s)
                                               . showString " = "
                                               . gshowsPrecX t 0 x
  isNullary (M1 x) = isNullary x

instance (GShowX a) => GShowX (M1 D d a) where
  gshowsPrecX t = showsPrecXWith go
    where go n (M1 x) = gshowsPrecX t n x

instance (GShowX a, GShowX b) => GShowX (a :+: b) where
  gshowsPrecX t n (L1 x) = gshowsPrecX t n x
  gshowsPrecX t n (R1 x) = gshowsPrecX t n x

instance (GShowX a, GShowX b) => GShowX (a :*: b) where
  gshowsPrecX t@Rec     n (a :*: b) =
    gshowsPrecX t n     a . showString ", " . gshowsPrecX t n     b
  gshowsPrecX t@(Inf s) n (a :*: b) =
    gshowsPrecX t n     a . showString s    . gshowsPrecX t n     b
  gshowsPrecX t@Tup     n (a :*: b) =
    gshowsPrecX t n     a . showChar ','    . gshowsPrecX t n     b
  gshowsPrecX t@Pref    n (a :*: b) =
    gshowsPrecX t (n+1) a . showChar ' '    . gshowsPrecX t (n+1) b

  -- If we have a product then it is not a nullary constructor
  isNullary _ = False

-- Unboxed types
instance GShowX UChar where
  gshowsPrecX _ _ (UChar c)   = showsPrec 0 (C# c) . showChar '#'
instance GShowX UDouble where
  gshowsPrecX _ _ (UDouble d) = showsPrec 0 (D# d) . showString "##"
instance GShowX UFloat where
  gshowsPrecX _ _ (UFloat f)  = showsPrec 0 (F# f) . showChar '#'
instance GShowX UInt where
  gshowsPrecX _ _ (UInt i)    = showsPrec 0 (I# i) . showChar '#'
instance GShowX UWord where
  gshowsPrecX _ _ (UWord w)   = showsPrec 0 (W# w) . showString "##"

printX :: ShowX a => a -> IO ()
printX x = putStrLn $ showX x

The complete Signal.hs file:

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE DefaultSignatures      #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE ImplicitParams         #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE PatternSynonyms        #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators          #-}

module Signal where

import Control.Applicative
import Data.Coerce
import Data.Foldable
import GHC.Stack
import GHC.TypeLits

import ShowX

data Domain = Domain { domainName :: Symbol, clockRate :: Nat }

data Signal (domain :: Domain) a = a :- Signal domain a
infixr 5 :-

data ClockKind = Original | Derived

data Clock (clockKind :: ClockKind) (domain :: Domain) where
  Clock' :: { clkEn :: Signal domain Bool } -> Clock clockKind domain
  -- ^ Will not be exported

-- | Only the Clock pattern will be exported
pattern Clock :: Signal domain Bool -> Clock Original domain
pattern Clock en <- Clock' en
  where
    Clock en = Clock' en

data ResetKind = Synchronous | Asynchronous

data Reset (resetKind :: ResetKind) (domain :: Domain) where
  Sync  :: Signal domain Bool -> Reset Synchronous  domain
  Async :: Signal domain Bool -> Reset Asynchronous domain

instance Foldable (Signal domain) where
  foldr f z (a :- s) = a `f` (foldr f z s)

instance Show a => Show (Signal domain a) where
  showsPrec _ = showList . toList

instance ShowX a => ShowX (Signal clk a) where
  showsPrecX _ = showListX . toList

instance Functor (Signal domain) where
  fmap f (s :- ss) = f s :- fmap f ss

instance Applicative (Signal domain) where
  pure x = let s = x :- s in s
  (f :- fs) <*> ~(a :- as) = f a :- (fs <*> as)

fromList :: HasCallStack => [a] -> Signal domain a
fromList = foldr (:-) (withFrozenCallStack (error "finite list"))

mux :: Applicative f => f Bool -> f a -> f a -> f a
mux = liftA3 (\b t f -> if b then t else f)

register' :: HasCallStack => Reset reset domain -> Clock clk domain
          -> a -> Signal domain a -> Signal domain a
register' (Sync r) (Clock' en) i d =
  let q  = reg q'
      q' = mux en d' q
      d' = mux r d (pure i) -- negated reset
  in  q
  where reg s = withFrozenCallStack (throwX msg) :- s
        msg   = "register': initial value undefined"

register' (Async r) (Clock' en) i d =
  let q  = reg q'
      q' = mux en d q
  in  mux r q (pure i) -- negated reset
  where reg s = withFrozenCallStack (throwX msg) :- s
        msg   = "register': initial value undefined"

register :: (?reset :: Reset Asynchronous domain, ?clk :: Clock Original domain)
         => a -> Signal domain a -> Signal domain a
register = register' ?reset ?clk

delay' :: HasCallStack => Clock clk domain -> Signal domain a -> Signal domain a
delay' (Clock' en) d =
  let q  = reg q'
      q' = mux en d q
  in  q
  where reg s = withFrozenCallStack (throwX msg) :- s
        msg   = "delay': initial value undefined"

delay :: (?clk :: Clock Original domain) => Signal domain a -> Signal domain a
delay = delay' ?clk

unsafeSynchronizer :: forall (dom1 :: Domain) (dom2 :: Domain) a nm1 r1 nm2 r2 .
                      ( dom1 ~ ('Domain nm1 r1), dom2 ~ ('Domain nm2 r2)
                      , KnownNat r1, KnownNat r2)
                   => Signal dom1 a
                   -> Signal dom2 a
unsafeSynchronizer = undefined -- no need to implement it right now

clockGate :: Clock clk domain -> Signal domain Bool -> Clock Derived domain
clockGate (Clock' en) en' = (Clock' ((&&) <$> en <*> en'))

data SNat :: Nat -> * where
  SNat :: KnownNat n => SNat n

pll :: forall numerator denominator x y nm .
       ((x * numerator) ~ (y * denominator), KnownNat x, KnownNat y)
    => SNat numerator
    -> SNat denominator
    -> Clock Original ('Domain nm x)
    -> Clock Original ('Domain nm y)
pll num denom _ = Clock (pure True)

-- It is HIGHLY unsafe to treat Asynchronous resets as Bool signals due to:
-- * meta-stability
-- * combinational loops

-- | ´unsafeFromAsyncReset' is HIGHLY unsafe
unsafeFromAsyncReset :: Reset Asynchronous domain -> Signal domain Bool
unsafeFromAsyncReset (Async r) = r

-- | 'unsafeToAsyncReset' is HIGHLY unsafe
unsafeToAsyncReset :: Signal domain Bool -> Reset Asynchronous domain
unsafeToAsyncReset r = Async r

-- It is safe to treat Synchronous resets as Bool signals
fromSyncReset :: Reset Synchronous domain -> Signal domain Bool
fromSyncReset (Sync r) = r

toSyncReset :: Signal domain Bool -> Reset Synchronous domain
toSyncReset r = Sync r

resetSynchroniser :: Reset Asynchronous domain -> Clock clk domain
                  -> Reset Asynchronous domain
resetSynchroniser r c =
  let r1 = register' r c False (pure True)
      r2 = register' r c False r1
  in  unsafeToAsyncReset r2

class Bundle a where
  type Unbundled (domain :: Domain) a  = res | res -> domain
  type Unbundled domain a = Signal domain a

  bundle :: Unbundled domain a -> Signal domain a
  default bundle :: Signal domain a -> Signal domain a
  bundle s = s

  unbundle :: Signal domain a -> Unbundled domain a
  default unbundle :: Signal domain a -> Signal domain a
  unbundle s = s

instance Bundle (a,b) where
  type Unbundled  domain (a,b) = (Signal domain a, Signal domain b)
  bundle (x,y)  = liftA2 (,) x y
  unbundle xy   = (fst <$> xy, snd <$> xy)

mealy' :: Reset reset domain -> Clock clk domain 
       -> (s -> i -> (s,o)) -> s -> Signal domain i -> Signal domain o
mealy' res clk f iS = \i -> let (s',o) = unbundle $ f <$> s <*> i
                                s      = register' res clk iS s'
                            in  o

mealy :: (?res :: Reset Asynchronous domain, ?clk :: Clock Original domain)
      => (s -> i -> (s,o))
      -> s
      -> Signal domain i
      -> Signal domain o
mealy = mealy' ?res ?clk

type System = 'Domain "system" 1000
systemClock = Clock @System (pure True)
systemReset = Async @System (False :- pure True)

simulate :: ((?res :: Reset Asynchronous System, ?clk :: Clock Original System) 
                   => Signal System a -> Signal System b)
         -> [a] -> [b]
simulate f xs = let ?clk = systemClock in
                let ?res = systemReset
                in  toList (f (fromList xs))

macT s (x,y) = (s',s)
  where
    s' = s + (x * y)

mac :: (?res :: Reset Asynchronous System, ?clk :: Clock Original System) 
    => Signal System (Int,Int) -> Signal System Int
mac = mealy macT 0

testMac = simulate mac [(1,1),(2,2),(3,3),(4,4)]

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Clock and reset modelling

1. The situation in CLaSH 0.6 (and earlier)

1.1 Improving the CLaSH 0.6 clock/reset situation

2. Ideas for CLaSH 0.7/1.0 (and later)

2.1 Dealing with `undefined`

2.1.1 Explicit modeling of `undefined` (a not so good idea)

2.1.2 Catching `undefined`

2.2 Explicit clock lines

2.2.1 `unsafeSynchronizer` primitive:

2.2.2 Clock gating

2.2.3 Clock primitives

2.2.4 Implicit routing of clock signals

2.3 Explicit reset lines

2.3.1 Pitfalls

2.3.2 Best solution (so far)

3. No shadowing policy for clocks and resets

Appendix A: complete definitions

Clone this wiki locally

Clock and reset modelling

1. The situation in CLaSH 0.6 (and earlier)

1.1 Improving the CLaSH 0.6 clock/reset situation

2. Ideas for CLaSH 0.7/1.0 (and later)

2.1 Dealing with undefined

2.1.1 Explicit modeling of undefined (a not so good idea)

2.1.2 Catching undefined

2.2 Explicit clock lines

2.2.1 unsafeSynchronizer primitive:

2.2.2 Clock gating

2.2.3 Clock primitives

2.2.4 Implicit routing of clock signals

2.3 Explicit reset lines

2.3.1 Pitfalls

2.3.2 Best solution (so far)

3. No shadowing policy for clocks and resets

Appendix A: complete definitions

Clone this wiki locally

2.1 Dealing with `undefined`

2.1.1 Explicit modeling of `undefined` (a not so good idea)

2.1.2 Catching `undefined`

2.2.1 `unsafeSynchronizer` primitive: