Term-level access to clock rate

Question

I'd like to access the clock rate (in Hz) as a term-level value, so that I can use it in counters.

One way I've been able to come up with so far involves unpacking the type-level Domain into its clock period (in ps), and then converting it into a clock rate. However, this requires an extra KnownNat ps constraint that will then infest everything that tries to use it, all the way up to topLevel:

clkPeriod :: forall dom gated name ps. (dom ~ Dom name ps, KnownNat ps) => Clock dom gated -> Integer
clkPeriod clk = natVal (Proxy :: Proxy ps)

clkRate :: (dom ~ Dom name ps, KnownNat ps) => Clock dom gated -> Integer
clkRate clk = 10^12 `div` clkPeriod clk

Another way, that avoids introducing the extra KnownNat constraint, is to import Clash.Signal.Internal and pattern-match on the Clock, since it contains an SNat witness of the period:

import Clash.Signal.Internal (Clock(..))

clkPeriod :: Clock dom gated -> Integer
clkPeriod (Clock _ period) = snatToInteger period
clkPeriod (GatedClock _ period _) = snatToInteger period

clkRate :: Clock dom gated -> Integer
clkRate clk = 10^12 `div` clkPeriod clk

but this crashes the synthesizer (guess I shouldn't be importing Clash.Signal.Internal):

*** Exception: Clash.Rewrite.Util(566): 
Can't create selector ("Clash.Normalize.Transformations(1136):doPatBndr",1,0) for:
($dKnownNat23000 :: GHC.Natural.Natural)

Additional info: TyCon has no DataCons: 
Name {nameSort = User, nameOcc = GHC.Natural.Natural3674937295934324782, nameLoc = UnhelpfulSpan "<no location info>"} GHC.Natural.Natural3674937295934324782

Here is a full module exhibiting this problem (I tried synthesizing it with :vhdl to get the above error):

module Test where

import Clash.Prelude hiding (clkPeriod)
import Data.Word
import Clash.Signal.Internal (Clock(..))

type FromHz rate = 1000000000000 `Div` rate
type Dom25 = Dom "CLK_25MHZ" (FromHz 25175000)

topEntity
    :: Clock Dom25 Source
    -> Reset Dom25 Asynchronous
    -> Signal Dom25 Bit
topEntity = exposeClockReset board
  where
    board = boolToBit <$> r

    r = regEn False (counter .==. 0) (not <$> r)
    counter = register clkrt $ mux (counter .==. 0) (pure clkrt) (pred <$> counter)
    clkrt = fromIntegral $ hideClock clkRate

clkPeriod :: Clock dom gated -> Integer
clkPeriod (Clock _ period) = snatToInteger period
clkPeriod (GatedClock _ period _) = snatToInteger period

clkRate :: Clock dom gated -> Integer
clkRate clk = 10^12 `div` clkPeriod clk

My question is, is there a way to reify clkRate in the term level without introducing any extra KnownNat constraints, or importing any Internal modules?

Answer 1

With Clash 1.0.0, this can be done without the creeping KnownNat constraints OR without importing any Internal module. The trick is to use knownDomain to get the SDomainConfiguration for a given clock domain, which will contain an SNat period for the length of a single clock cycle (in picoseconds). By pattern matching on the SNat constructor, the KnownNat witness is brought in scope.

clkPeriod :: forall dom. (KnownDomain dom) => Clock dom -> Integer
clkPeriod clk = case knownDomain @dom of
    SDomainConfiguration _ rate@SNat{} _ _ _ _ -> natVal rate

clkRate :: (KnownDomain dom) => Clock dom -> Integer
clkRate clk = 1_000_000_000_000 `div` clkPeriod clk

Here's the updated toplevel definition:

{-# LANGUAGE NumericUnderscores #-}
module Test where

import Clash.Prelude hiding (clkPeriod)
import Data.Word

createDomain vSystem{vName="Dom25", vPeriod = hzToPeriod 25_000_000}

topEntity
    :: Clock Dom25
    -> Reset Dom25
    -> Enable Dom25
    -> Signal Dom25 Bit
topEntity = exposeClockResetEnable board
  where
    board = boolToBit <$> r

    r = regEn False (counter .==. 0) (not <$> r)
    counter = register clkrt $ mux (counter .==. 0) (pure clkrt) (pred <$> counter)
    clkrt = fromInteger @Word32 $ hideClock clkRate

I've tested that this works with synthesis, and the division to convert period length to clock rate is done at compile time.