Я хотел бы получить доступ к тактовой частоте (в Гц) в качестве значения уровня термина, чтобы я мог использовать ее в счетчиках.
Один из способов, который мне удалось найти, заключается в распаковке уровня типа Dom ain в его тактовый период (в пс), а затем преобразовании его в тактовую частоту. Однако для этого требуется дополнительное ограничение 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 состоит в том, чтобы импортировать Clash.Signal.Internal и сопоставление с шаблоном в Clock, поскольку он содержит 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
У меня вопрос: есть ли способ повысить clkRate на уровне терминов без введения каких-либо дополнительных ограничений KnownNat или импорта каких-либо модулей Internal?