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?

Do you have a self-contained minimal example that generates the exception? Otherwise, it's hard to know if a potential solution will be any better than what you've already tried. — K. A. Buhr, Sep 08 '18 at 14:27
@K.A.Buhr: I don't have a minimal example yet; the real-life self-contained example would be the one at https://github.com/gergoerdi/chip8-clash. However, I think there is something fundamentally broken about the `Clock` argument you can access via `hideClock`: https://github.com/clash-lang/clash-compiler/issues/348#issuecomment-419611322 — Cactus, Sep 09 '18 at 03:18
@K.A.Buhr I've edited my question to contain a minimal example. — Cactus, Sep 11 '18 at 13:23

score 1 · Answer 1 · answered Sep 22 '18 at 21:30

It looks like this has been acknowledged by the Clash primary developer Christiaan Baaij as a Clash compiler bug in Issue #348. To quote from his comment in that issue report:

So the issue is that the Core we're getting is pattern-matching on something of type Integer and exposing the internals of its representation; something the compiler obviously doesn't handle. I'll create a work-around/hack to always pick the branch where the Integer fits inside the [-2^63 .. 2^63-1] range, since Clash currently "erroneously" translates Integer to 64-bit numbers anyways.

score 0 · Accepted Answer · answered Oct 29 '19 at 11:25

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.

Term-level access to clock rate

2 Answers2