术语级访问时钟速率

Question

我想访问时钟速率（以 Hz 为单位）作为术语级值，以便我可以在计数器中使用它。

到目前为止，我能想到的一种方法是将类型级 Domain 解包到它的时钟周期（在 ps 中），然后将其转换为时钟速度。然而，这需要一个额外的 KnownNat ps 约束，然后会感染所有试图使用它的东西，一直到 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

另一种避免引入额外 KnownNat 约束的方法是在 Clock 上导入 Clash.Signal.Internal 和模式匹配，因为它包含 SNat 见证期间：

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

但这会使合成器崩溃（我猜我不应该导入 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

这是一个完整的模块，展示了这个问题（我尝试用 :vhdl 合成它以得到上述错误）：

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

我的问题是，有没有办法在不引入任何额外 KnownNat 约束或导入任何 Internal 模块的情况下，在术语级别具体化 clkRate？

Answer 1

看起来这已被 Clash 主要开发人员 Christiaan Baaij 确认为 Issue #348 中的 Clash 编译器错误。引用他在该问题报告中的评论：

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.

Answer 2

使用 Clash 1.0.0，这可以在没有爬行 KnownNat 约束或不导入任何 Internal 模块的情况下完成。诀窍是使用 knownDomain 获得给定时钟域的 SDomainConfiguration，它将包含单个时钟周期长度（以皮秒为单位）的 SNat period。通过 SNat 构造函数上的模式匹配，KnownNat witness 被引入范围。

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

这是更新后的顶层定义：

{-# 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

我已经测试过这适用于综合，将周期长度转换为时钟速率的除法是在编译时完成的。

术语级访问时钟速率

Term-level access to clock rate

haskell

type-level-computation

singleton-type

clash