From 01169c4d215a9153ebb980474a23cd7d3c21a978 Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Fri, 26 Apr 2019 16:31:28 +0200 Subject: [PATCH] tmp --- clash-prelude/src/Clash/Clocks.hs | 4 +- clash-prelude/src/Clash/Clocks/Deriving.hs | 6 +- clash-prelude/src/Clash/Examples.hs | 98 +-- clash-prelude/src/Clash/Explicit/BlockRam.hs | 106 +-- .../src/Clash/Explicit/BlockRam/File.hs | 4 +- clash-prelude/src/Clash/Explicit/DDR.hs | 166 +++-- clash-prelude/src/Clash/Explicit/Mealy.hs | 20 +- clash-prelude/src/Clash/Explicit/Moore.hs | 50 +- clash-prelude/src/Clash/Explicit/Prelude.hs | 43 +- .../src/Clash/Explicit/Prelude/Safe.hs | 64 +- clash-prelude/src/Clash/Explicit/RAM.hs | 66 +- clash-prelude/src/Clash/Explicit/ROM.hs | 51 +- clash-prelude/src/Clash/Explicit/ROM/File.hs | 2 +- clash-prelude/src/Clash/Explicit/Signal.hs | 274 ++++--- .../src/Clash/Explicit/Signal/Delayed.hs | 66 +- .../src/Clash/Explicit/Synchronizer.hs | 74 +- clash-prelude/src/Clash/Explicit/Testbench.hs | 132 ++-- clash-prelude/src/Clash/Intel/ClockGen.hs | 22 +- clash-prelude/src/Clash/Intel/DDR.hs | 26 +- clash-prelude/src/Clash/Prelude.hs | 38 +- clash-prelude/src/Clash/Prelude/BlockRam.hs | 93 +-- .../src/Clash/Prelude/BlockRam/File.hs | 24 +- clash-prelude/src/Clash/Prelude/DataFlow.hs | 187 ++--- clash-prelude/src/Clash/Prelude/Mealy.hs | 38 +- clash-prelude/src/Clash/Prelude/Moore.hs | 28 +- clash-prelude/src/Clash/Prelude/RAM.hs | 23 +- clash-prelude/src/Clash/Prelude/ROM.hs | 79 +- clash-prelude/src/Clash/Prelude/ROM/File.hs | 20 +- clash-prelude/src/Clash/Prelude/Safe.hs | 45 +- clash-prelude/src/Clash/Prelude/Testbench.hs | 49 +- clash-prelude/src/Clash/Promoted/Nat.hs | 40 +- clash-prelude/src/Clash/Signal.hs | 474 ++++++------ clash-prelude/src/Clash/Signal/BiSignal.hs | 45 +- clash-prelude/src/Clash/Signal/Bundle.hs | 36 +- clash-prelude/src/Clash/Signal/Delayed.hs | 106 +-- .../src/Clash/Signal/Delayed/Bundle.hs | 29 +- .../src/Clash/Signal/Delayed/Internal.hs | 46 +- clash-prelude/src/Clash/Signal/Internal.hs | 678 +++++++++--------- clash-prelude/src/Clash/Signal/Trace.hs | 76 +- clash-prelude/src/Clash/Sized/Fixed.hs | 8 +- .../src/Clash/Sized/Internal/BitVector.hs | 10 +- .../src/Clash/Sized/Internal/Index.hs | 8 +- .../src/Clash/Sized/Internal/Signed.hs | 8 +- .../src/Clash/Sized/Internal/Unsigned.hs | 8 +- clash-prelude/src/Clash/Tutorial.hs | 133 ++-- clash-prelude/src/Clash/Xilinx/ClockGen.hs | 41 +- clash-prelude/src/Clash/Xilinx/DDR.hs | 35 +- 47 files changed, 2003 insertions(+), 1676 deletions(-) diff --git a/clash-prelude/src/Clash/Clocks.hs b/clash-prelude/src/Clash/Clocks.hs index afee3a909d..ebcbb10762 100644 --- a/clash-prelude/src/Clash/Clocks.hs +++ b/clash-prelude/src/Clash/Clocks.hs @@ -21,8 +21,8 @@ import Clash.Clocks.Deriving (deriveClocksInstances) class Clocks t where clocks - :: Clock pplIn 'Source - -> Reset pplIn 'Asynchronous + :: Clock tagIn 'Regular + -> Reset tagIn 'ActiveHigh -> t deriveClocksInstances 16 diff --git a/clash-prelude/src/Clash/Clocks/Deriving.hs b/clash-prelude/src/Clash/Clocks/Deriving.hs index e9f7c2004b..1d120211c5 100644 --- a/clash-prelude/src/Clash/Clocks/Deriving.hs +++ b/clash-prelude/src/Clash/Clocks/Deriving.hs @@ -32,7 +32,7 @@ derive' n = do let clkImpls = replicate n (clkImpl clk rst) let instTuple = TupE $ clkImpls ++ [AppE (VarE 'unsafeCoerce) (VarE rst)] let funcBody = NormalB instTuple - let rstPat = ConP 'Async [VarP rst] + let rstPat = ConP 'ActiveHighReset [VarP rst] let instFunc = FunD (mkName "clocks") [Clause [VarP clk, rstPat] funcBody []] return $ InstanceD Nothing [] instType' [instFunc, noInline] @@ -41,7 +41,7 @@ derive' n = do -- | Generate type @Clock dom 'Source@ with fresh @dom@ variable clkType n' = let c = varT $ mkName ("c" ++ show n') in - [t| Clock $c 'Source |] + [t| Clock $c 'Regular |] -- | Generate type @Signal dom 'Bool@ with fresh @dom@ variable lockType = @@ -49,7 +49,7 @@ derive' n = do [t| Signal $c Bool |] clkImpl (VarE -> clk) (VarE -> rst) = - AppE (VarE 'unsafeCoerce) (AppE (AppE (VarE 'clockGate) clk) rst) + AppE (VarE 'unsafeCoerce) (AppE (AppE (VarE 'toEnabledClock) clk) rst) -- Derive instances for up to and including to /n/ clocks deriveClocksInstances :: Int -> Q [Dec] diff --git a/clash-prelude/src/Clash/Examples.hs b/clash-prelude/src/Clash/Examples.hs index d411f19fb1..9a078cb86d 100644 --- a/clash-prelude/src/Clash/Examples.hs +++ b/clash-prelude/src/Clash/Examples.hs @@ -81,8 +81,10 @@ encoderCase enable binaryIn | enable = 0x8000 -> 0xF encoderCase _ _ = 0 -upCounter :: HiddenClockReset domain gated synchronous - => Signal domain Bool -> Signal domain (Unsigned 8) +upCounter + :: HiddenClockReset tag enabled polarity dom + => Signal tag Bool + -> Signal tag (Unsigned 8) upCounter enable = s where s = register 0 (mux enable (s + 1) s) @@ -95,12 +97,16 @@ upCounterLdT s (ld,en,dIn) = (s',s) | en = s + 1 | otherwise = s -upCounterLd :: HiddenClockReset domain gated synchronous - => Signal domain (Bool,Bool,Unsigned 8) -> Signal domain (Unsigned 8) +upCounterLd + :: HiddenClockReset tag enabled polarity dom + => Signal tag (Bool, Bool, Unsigned 8) + -> Signal tag (Unsigned 8) upCounterLd = mealy upCounterLdT 0 -upDownCounter :: HiddenClockReset domain gated synchronous - => Signal domain Bool -> Signal domain (Unsigned 8) +upDownCounter + :: HiddenClockReset tag enabled polarity dom + => Signal tag Bool + -> Signal tag (Unsigned 8) upDownCounter upDown = s where s = register 0 (mux upDown (s + 1) (s - 1)) @@ -110,8 +116,9 @@ lfsrF' s = pack feedback ++# slice d15 d1 s where feedback = s!5 `xor` s!3 `xor` s!2 `xor` s!0 -lfsrF :: HiddenClockReset domain gated synchronous - => BitVector 16 -> Signal domain Bit +lfsrF + :: HiddenClockReset tag enabled polarity dom + => BitVector 16 -> Signal tag Bit lfsrF seed = msb <$> r where r = register seed (lfsrF' <$> r) @@ -126,17 +133,24 @@ lfsrGP taps regs = zipWith xorM taps (fb +>> regs) xorM i x | i = x `xor` fb | otherwise = x -lfsrG :: HiddenClockReset domain gated synchronous => BitVector 16 -> Signal domain Bit +lfsrG + :: HiddenClockReset tag enabled polarity dom + => BitVector 16 + -> Signal tag Bit lfsrG seed = last (unbundle r) where r = register (unpack seed) (lfsrGP (unpack 0b0011010000000000) <$> r) -grayCounter :: HiddenClockReset domain gated synchronous - => Signal domain Bool -> Signal domain (BitVector 8) +grayCounter + :: HiddenClockReset tag enabled polarity dom + => Signal tag Bool + -> Signal tag (BitVector 8) grayCounter en = gray <$> upCounter en where gray xs = pack (msb xs) ++# xor (slice d7 d1 xs) (slice d6 d0 xs) -oneHotCounter :: HiddenClockReset domain gated synchronous - => Signal domain Bool -> Signal domain (BitVector 8) +oneHotCounter + :: HiddenClockReset tag enabled polarity dom + => Signal tag Bool + -> Signal tag (BitVector 8) oneHotCounter enable = s where s = register 1 (mux enable (rotateL <$> s <*> 1) s) @@ -153,8 +167,12 @@ crcT bv dIn = replaceBit 0 dInXor rotated = rotateL bv 1 fb = msb bv -crc :: HiddenClockReset domain gated synchronous - => Signal domain Bool -> Signal domain Bool -> Signal domain Bit -> Signal domain (BitVector 16) +crc + :: HiddenClockReset tag enabled polarity dom + => Signal tag Bool + -> Signal tag Bool + -> Signal tag Bit + -> Signal tag (BitVector 16) crc enable ld dIn = s where s = register 0xFFFF (mux enable (mux ld 0xFFFF (crcT <$> s <*> dIn)) s) @@ -370,9 +388,9 @@ Using `register`: @ upCounter - :: HiddenClockReset domain gated synchronous - => Signal domain Bool - -> Signal domain (Unsigned 8) + :: HiddenClockReset tag enabled polarity dom + => Signal tag Bool + -> Signal tag (Unsigned 8) upCounter enable = s where s = `register` 0 (`mux` enable (s + 1) s) @@ -384,9 +402,9 @@ Using `mealy`: @ upCounterLd - :: HiddenClockReset domain gated synchronous - => Signal domain (Bool,Bool,Unsigned 8) - -> Signal domain (Unsigned 8) + :: HiddenClockReset tag enabled polarity dom + => Signal tag (Bool,Bool,Unsigned 8) + -> Signal tag (Unsigned 8) upCounterLd = `mealy` upCounterLdT 0 upCounterLdT s (ld,en,dIn) = (s',s) @@ -402,9 +420,9 @@ Using `register` and `mux`: @ upDownCounter - :: HiddenClockReset domain gated synchronous - => Signal domain Bool - -> Signal domain (Unsigned 8) + :: HiddenClockReset tag enabled polarity dom + => Signal tag Bool + -> Signal tag (Unsigned 8) upDownCounter upDown = s where s = `register` 0 (`mux` upDown (s + 1) (s - 1)) @@ -412,7 +430,7 @@ upDownCounter upDown = s The following property holds: -prop> \en -> en ==> testFor 1000 (upCounter (pure en) .==. upDownCounter (pure en)) +prop> \en -> en ==> testFor 1000 (upCounter (pure en) .==. upDownCounter (pure en) :: Signal "System" Bool) = LFSR @@ -425,9 +443,9 @@ lfsrF' s = 'pack' feedback '++#' 'slice' d15 d1 s feedback = s'!'5 ``xor`` s'!'3 ``xor`` s'!'2 ``xor`` s'!'0 lfsrF - :: HiddenClockReset domain gated synchronous + :: HiddenClockReset tag enabled polarity dom => BitVector 16 - -> Signal domain Bit + -> Signal tag Bit lfsrF seed = 'msb' '<$>' r where r = 'register' seed (lfsrF' '<$>' r) @ @@ -446,14 +464,14 @@ lfsrGP taps regs = 'zipWith' xorM taps (fb '+>>' regs) Then we can instantiate a 16-bit LFSR as follows: @ -lfsrG :: HiddenClockReset domain gated synchronous => BitVector 16 -> Signal domain Bit +lfsrG :: HiddenClockReset tag enabled polarity dom => BitVector 16 -> Signal tag Bit lfsrG seed = 'last' ('unbundle' r) where r = 'register' ('unpack' seed) (lfsrGP ('unpack' 0b0011010000000000) '<$>' r) @ The following property holds: -prop> testFor 100 (lfsrF 0xACE1 .==. lfsrG 0x4645) +prop> testFor 100 (lfsrF 0xACE1 .==. lfsrG 0x4645 :: Signal "System" Bool) = Gray counter @@ -461,9 +479,9 @@ Using the previously defined @upCounter@: @ grayCounter - :: HiddenClockReset domain gated synchronous - => Signal domain Bool - -> Signal domain (BitVector 8) + :: HiddenClockReset tag enabled polarity dom + => Signal tag Bool + -> Signal tag (BitVector 8) grayCounter en = gray '<$>' upCounter en where gray xs = 'pack' ('msb' xs) '++#' 'xor' ('slice' d7 d1 xs) ('slice' d6 d0 xs) @ @@ -474,9 +492,9 @@ Basically a barrel-shifter: @ oneHotCounter - :: HiddenClockReset domain gated synchronous - => Signal domain Bool - -> Signal domain (BitVector 8) + :: HiddenClockReset tag enabled polarity dom + => Signal tag Bool + -> Signal tag (BitVector 8) oneHotCounter enable = s where s = 'register' 1 ('mux' enable ('rotateL' '<$>' s '<*>' 1) s) @@ -513,11 +531,11 @@ crcT bv dIn = 'replaceBit' 0 dInXor fb = 'msb' bv crc - :: HiddenClockReset domain gated synchronous - => Signal domain Bool - -> Signal domain Bool - -> Signal domain Bit - -> Signal domain (BitVector 16) + :: HiddenClockReset tag enabled polarity dom + => Signal tag Bool + -> Signal tag Bool + -> Signal tag Bit + -> Signal tag (BitVector 16) crc enable ld dIn = s where s = 'register' 0xFFFF ('mux' enable ('mux' ld 0xFFFF (crcT '<$>' s '<*>' dIn)) s) diff --git a/clash-prelude/src/Clash/Explicit/BlockRam.hs b/clash-prelude/src/Clash/Explicit/BlockRam.hs index 681bbb8c1a..df378a76e9 100644 --- a/clash-prelude/src/Clash/Explicit/BlockRam.hs +++ b/clash-prelude/src/Clash/Explicit/BlockRam.hs @@ -120,13 +120,13 @@ We initially create a memory out of simple registers: @ dataMem - :: Clock domain gated - -> Reset domain synchronous - -> Signal domain MemAddr + :: Clock tag gated + -> Reset tag polarity + -> Signal tag MemAddr -- ^ Read address - -> Signal domain (Maybe (MemAddr,Value)) + -> Signal tag (Maybe (MemAddr,Value)) -- ^ (write address, data in) - -> Signal domain Value + -> Signal tag Value -- ^ data out dataMem clk rst rd wrM = 'Clash.Explicit.Mealy.mealy' clk rst dataMemT ('Clash.Sized.Vector.replicate' d32 0) (bundle (rd,wrM)) where @@ -144,9 +144,9 @@ And then connect everything: system :: KnownNat n => Vec n Instruction - -> Clock domain gated - -> Reset domain synchronous - -> Signal domain Value + -> Clock tag gated + -> Reset tag polarity + -> Signal tag Value system instrs clk rst = memOut where memOut = dataMem clk rst rdAddr dout @@ -191,7 +191,7 @@ prog = -- 0 := 4 And test our system: @ ->>> sampleN 32 $ system prog systemClockGen asyncResetGen +>>> sampleN 32 $ system prog systemClockGen resetGen [0,0,0,0,0,0,4,4,4,4,4,4,4,4,6,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,2] @ @@ -211,9 +211,9 @@ has the potential to be translated to a more efficient structure: system2 :: KnownNat n => Vec n Instruction - -> Clock domain gated - -> Reset domain synchronous - -> Signal domain Value + -> Clock tag gated + -> Reset tag polarity + -> Signal tag Value system2 instrs clk rst = memOut where memOut = 'Clash.Explicit.RAM.asyncRam' clk clk d32 rdAddr dout @@ -228,7 +228,7 @@ output samples are also 'undefined'. We use the utility function 'printX' to con filter out the undefinedness and replace it with the string "X" in the few leading outputs. @ ->>> printX $ sampleN 32 $ system2 prog systemClockGen asyncResetGen +>>> printX $ sampleN 32 $ system2 prog systemClockGen resetGen [X,X,X,X,X,X,4,4,4,4,4,4,4,4,6,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,2] @ @@ -301,9 +301,9 @@ We can now finally instantiate our system with a 'blockRam': system3 :: KnownNat n => Vec n Instruction - -> Clock domain gated - -> Reset domain synchronous - -> Signal domain Value + -> Clock tag gated + -> Reset tag polarity + -> Signal tag Value system3 instrs clk rst = memOut where memOut = 'blockRam' clk (replicate d32 0) rdAddr dout @@ -356,7 +356,7 @@ we need to disregard the first sample, because the initial output of a filter out the undefinedness and replace it with the string "X". @ ->>> printX $ sampleN 34 $ system3 prog2 systemClockGen asyncResetGen +>>> printX $ sampleN 34 $ system3 prog2 systemClockGen resetGen [X,0,0,0,0,0,0,4,4,4,4,4,4,4,4,6,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,2] @ @@ -382,7 +382,7 @@ This concludes the short introduction to using 'blockRam'. {-# OPTIONS_GHC -fno-cpr-anal #-} module Clash.Explicit.BlockRam - ( -- * BlockRAM synchronised to the system clock + ( -- * BlockRAM synchronized to the system clock blockRam , blockRamPow2 -- * Read/Write conflict resolution @@ -398,7 +398,7 @@ import GHC.Stack (HasCallStack, withFrozenCallStack) import GHC.TypeLits (KnownNat, type (^)) import Prelude hiding (length) -import Clash.Explicit.Signal (register) +import Clash.Explicit.Signal (KnownDomain, register) import Clash.Signal.Internal (Clock, Reset, Signal (..), (.&&.), clockEnable, mux) import Clash.Signal.Bundle (unbundle) @@ -507,11 +507,12 @@ cpu regbank (memOut,instr) = (regbank',(rdAddr,(,aluOut) <$> wrAddrM,fromIntegra >>> :{ dataMem - :: Clock domain gated - -> Reset domain synchronous - -> Signal domain MemAddr - -> Signal domain (Maybe (MemAddr,Value)) - -> Signal domain Value + :: KnownDomain tag dom + => Clock tag gated + -> Reset tag polarity + -> Signal tag MemAddr + -> Signal tag (Maybe (MemAddr,Value)) + -> Signal tag Value dataMem clk rst rd wrM = mealy clk rst dataMemT (C.replicate d32 0) (bundle (rd,wrM)) where dataMemT mem (rd,wrM) = (mem',dout) @@ -524,11 +525,12 @@ dataMem clk rst rd wrM = mealy clk rst dataMemT (C.replicate d32 0) (bundle (rd, >>> :{ system - :: KnownNat n + :: ( KnownDomain tag dom + , KnownNat n ) => Vec n Instruction - -> Clock domain gated - -> Reset domain synchronous - -> Signal domain Value + -> Clock tag gated + -> Reset tag polarity + -> Signal tag Value system instrs clk rst = memOut where memOut = dataMem clk rst rdAddr dout @@ -570,11 +572,12 @@ prog = -- 0 := 4 >>> :{ system2 - :: KnownNat n + :: ( KnownDomain tag dom + , KnownNat n ) => Vec n Instruction - -> Clock domain gated - -> Reset domain synchronous - -> Signal domain Value + -> Clock tag gated + -> Reset tag polarity + -> Signal tag Value system2 instrs clk rst = memOut where memOut = asyncRam clk clk d32 rdAddr dout @@ -619,11 +622,12 @@ cpu2 (regbank,ldRegD) (memOut,instr) = ((regbank',ldRegD'),(rdAddr,(,aluOut) <$> >>> :{ system3 - :: KnownNat n + :: ( KnownDomain tag dom + , KnownNat n ) => Vec n Instruction - -> Clock domain gated - -> Reset domain synchronous - -> Signal domain Value + -> Clock tag gated + -> Reset tag polarity + -> Signal tag Value system3 instrs clk rst = memOut where memOut = blockRam clk (C.replicate d32 0) rdAddr dout @@ -671,10 +675,10 @@ prog2 = -- 0 := 4 -- * __NB__: Initial output value is 'undefined' -- -- @ --- bram40 :: 'Clock' domain gated --- -> 'Signal' domain ('Unsigned' 6) --- -> 'Signal' domain (Maybe ('Unsigned' 6, 'Clash.Sized.BitVector.Bit')) --- -> 'Signal' domain 'Clash.Sized.BitVector.Bit' +-- bram40 :: 'Clock' tag gated +-- -> 'Signal' tag ('Unsigned' 6) +-- -> 'Signal' tag (Maybe ('Unsigned' 6, 'Clash.Sized.BitVector.Bit')) +-- -> 'Signal' tag 'Clash.Sized.BitVector.Bit' -- bram40 clk = 'blockRam' clk ('Clash.Sized.Vector.replicate' d40 1) -- @ -- @@ -715,9 +719,9 @@ blockRam = \clk content rd wrM -> -- * __NB__: Initial output value is 'undefined' -- -- @ --- bram32 :: 'Signal' domain ('Unsigned' 5) --- -> 'Signal' domain (Maybe ('Unsigned' 5, 'Clash.Sized.BitVector.Bit')) --- -> 'Signal' domain 'Clash.Sized.BitVector.Bit' +-- bram32 :: 'Signal' tag ('Unsigned' 5) +-- -> 'Signal' tag (Maybe ('Unsigned' 5, 'Clash.Sized.BitVector.Bit')) +-- -> 'Signal' tag 'Clash.Sized.BitVector.Bit' -- bram32 clk = 'blockRamPow2' clk ('Clash.Sized.Vector.replicate' d32 1) -- @ -- @@ -795,16 +799,18 @@ blockRam# clk content rd wen = case clockEnable clk of -- | Create read-after-write blockRAM from a read-before-write one readNew - :: (Undefined a, Eq addr) - => Reset domain synchronous - -> Clock domain gated - -> (Signal domain addr -> Signal domain (Maybe (addr, a)) -> Signal domain a) + :: ( KnownDomain tag dom + , Undefined a + , Eq addr ) + => Reset tag polarity + -> Clock tag gated + -> (Signal tag addr -> Signal tag (Maybe (addr, a)) -> Signal tag a) -- ^ The @ram@ component - -> Signal domain addr + -> Signal tag addr -- ^ Read address @r@ - -> Signal domain (Maybe (addr, a)) + -> Signal tag (Maybe (addr, a)) -- ^ (Write address @w@, value to write) - -> Signal domain a + -> Signal tag a -- ^ Value of the @ram@ at address @r@ from the previous clock cycle readNew rst clk ram rdAddr wrM = mux wasSame wasWritten $ ram rdAddr wrM where readNewT rd (Just (wr, wrdata)) = (wr == rd, wrdata) diff --git a/clash-prelude/src/Clash/Explicit/BlockRam/File.hs b/clash-prelude/src/Clash/Explicit/BlockRam/File.hs index 8de8c073fe..76c9bdd955 100644 --- a/clash-prelude/src/Clash/Explicit/BlockRam/File.hs +++ b/clash-prelude/src/Clash/Explicit/BlockRam/File.hs @@ -88,7 +88,7 @@ __>>> L.tail $ sampleN 4 $ g systemClockGen (fromList [3..5])__ {-# OPTIONS_GHC -fno-cpr-anal #-} module Clash.Explicit.BlockRam.File - ( -- * BlockRAM synchronised to an arbitrary clock + ( -- * BlockRAM synchronized to an arbitrary clock blockRamFile , blockRamFilePow2 -- * Internal @@ -256,7 +256,7 @@ blockRamFile# clk _sz file rd wen = case clockEnable clk of ramI = V.fromList content {-# NOINLINE blockRamFile# #-} --- | __NB:__ Not synthesisable +-- | __NB:__ Not synthesizable initMem :: KnownNat n => FilePath -> IO [BitVector n] initMem = fmap (map parseBV . lines) . readFile where diff --git a/clash-prelude/src/Clash/Explicit/DDR.hs b/clash-prelude/src/Clash/Explicit/DDR.hs index df7be66f1f..236dded1ce 100644 --- a/clash-prelude/src/Clash/Explicit/DDR.hs +++ b/clash-prelude/src/Clash/Explicit/DDR.hs @@ -6,23 +6,25 @@ Maintainer : Christiaan Baaij We simulate DDR signal by using 'Signal's which have exactly half the period (or double the speed) of our normal 'Signal's. -The primives in this module can be used to produce of consume DDR signals. +The primitives in this module can be used to produce of consume DDR signals. DDR signals are not meant to be used internally in a design, but only to communicate with the outside world. -In some cases hardware specific DDR IN registers can be infered by synthesis tools -from these generic primitives. But to be sure your design will synthesize to -dedicated hardware resources use the functions from "Clash.Intel.DDR" +In some cases hardware specific DDR IN registers can be inferred by synthesis +tools from these generic primitives. But to be sure your design will synthesize +to dedicated hardware resources use the functions from "Clash.Intel.DDR" or "Clash.Xilinx.DDR". -} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} #if __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE NoStarIsType #-} #endif @@ -46,19 +48,20 @@ import Clash.Signal.Internal -- -- Consumes a DDR input signal and produces a regular signal containing a pair -- of values. +-- TODO: Check edge/reset/init ddrIn :: ( HasCallStack - , fast ~ 'Dom n pFast - , slow ~ 'Dom n (2*pFast)) - => Clock slow gated + , KnownDomain fast ('Domain fast fPeriod edge reset init) + , KnownDomain slow ('Domain slow (2*fPeriod) edge reset init) ) + => Clock slow enabled -- ^ clock - -> Reset slow synchronous + -> Reset slow polarity -- ^ reset -> (a, a, a) -- ^ reset values -> Signal fast a -- ^ DDR input signal - -> Signal slow (a,a) + -> Signal slow (a, a) -- ^ normal speed output pairs ddrIn clk rst (i0,i1,i2) = withFrozenCallStack $ ddrIn# clk rst i0 i1 i2 @@ -66,66 +69,92 @@ ddrIn clk rst (i0,i1,i2) = withFrozenCallStack $ ddrIn# clk rst i0 i1 i2 -- For details about all the seq's en seqX's -- see the [Note: register strictness annotations] in Clash.Signal.Internal ddrIn# - :: forall a slow fast n pFast gated synchronous + :: forall a slow fast fPeriod enabled polarity edge reset init . ( HasCallStack - , fast ~ 'Dom n pFast - , slow ~ 'Dom n (2*pFast)) - => Clock slow gated - -> Reset slow synchronous + , KnownDomain fast ('Domain fast fPeriod edge reset init) + , KnownDomain slow ('Domain slow (2*fPeriod) edge reset init) ) + => Clock slow enabled + -> Reset slow polarity -> a -> a -> a -> Signal fast a -> Signal slow (a,a) -ddrIn# (Clock {}) (Sync rst) i0 i1 i2 = - go ((errorX "ddrIn: initial value 0 undefined") - ,(errorX "ddrIn: initial value 1 undefined") - ,(errorX "ddrIn: initial value 2 undefined")) - rst +ddrIn# (Clock tag Nothing) (toHighPolarity -> hRst) i0 i1 i2 = + case knownDomain tag of + SDomain _tag _period _edge SSynchronous _init -> + goSync + ( errorX "ddrIn: initial value 0 undefined" + , errorX "ddrIn: initial value 1 undefined" + , errorX "ddrIn: initial value 2 undefined" ) + (fromSyncReset hRst) + SDomain _tag _period _edge SAsynchronous _init -> + goAsync + ( errorX "ddrIn: initial value 0 undefined" + , errorX "ddrIn: initial value 1 undefined" + , errorX "ddrIn: initial value 2 undefined" ) + (unsafeFromReset hRst) where - go :: (a,a,a) -> Signal slow Bool -> Signal fast a -> Signal slow (a,a) - go (o0,o1,o2) rt@(~(r :- rs)) as@(~(x0 :- x1 :- xs)) = - let (o0',o1',o2') = if r then (i0,i1,i2) else (o2,x0,x1) - in o0 `seqX` o1 `seqX` (o0,o1) :- (rt `seq` as `seq` go (o0',o1',o2') rs xs) - -ddrIn# (Clock {}) (Async rst) i0 i1 i2 = - go ((errorX "ddrIn: initial value 0 undefined") - ,(errorX "ddrIn: initial value 1 undefined") - ,(errorX "ddrIn: initial value 2 undefined")) - rst - where - go :: (a,a,a) -> Signal slow Bool -> Signal fast a -> Signal slow (a,a) - go (o0,o1,o2) ~(r :- rs) as@(~(x0 :- x1 :- xs)) = + goAsync + :: (a,a,a) + -> Signal slow Bool + -> Signal fast a + -> Signal slow (a,a) + goAsync (o0,o1,o2) ~(r :- rs) as@(~(x0 :- x1 :- xs)) = let (o0',o1',o2') = if r then (i0,i1,i2) else (o0,o1,o2) - in o0' `seqX` o1' `seqX`(o0',o1') :- (as `seq` go (o2',x0,x1) rs xs) - -ddrIn# (GatedClock _ _ ena) (Sync rst) i0 i1 i2 = - go ((errorX "ddrIn: initial value 0 undefined") - ,(errorX "ddrIn: initial value 1 undefined") - ,(errorX "ddrIn: initial value 2 undefined")) - rst - ena + in o0' `seqX` o1' `seqX`(o0',o1') :- (as `seq` goAsync (o2',x0,x1) rs xs) + + goSync + :: (a, a, a) + -> Signal slow Bool + -> Signal fast a + -> Signal slow (a,a) + goSync (o0,o1,o2) rt@(~(r :- rs)) as@(~(x0 :- x1 :- xs)) = + let (o0',o1',o2') = if r then (i0,i1,i2) else (o2,x0,x1) + in o0 `seqX` o1 `seqX` (o0,o1) :- (rt `seq` as `seq` goSync (o0',o1',o2') rs xs) + + +ddrIn# (Clock tag (Just ena)) (toHighPolarity -> hRst) i0 i1 i2 = + case knownDomain tag of + SDomain _tag _period _edge SSynchronous _init -> + goSync + ( errorX "ddrIn: initial value 0 undefined" + , errorX "ddrIn: initial value 1 undefined" + , errorX "ddrIn: initial value 2 undefined" ) + (fromSyncReset hRst) + ena + SDomain _tag _period _edge SAsynchronous _init -> + goAsync + ( errorX "ddrIn: initial value 0 undefined" + , errorX "ddrIn: initial value 1 undefined" + , errorX "ddrIn: initial value 2 undefined" ) + (unsafeFromReset hRst) + ena where - go :: (a,a,a) -> Signal slow Bool -> Signal slow Bool -> Signal fast a -> Signal slow (a,a) - go (o0,o1,o2) rt@(~(r :- rs)) ~(e :- es) as@(~(x0 :- x1 :- xs)) = + goSync + :: (a, a, a) + -> Signal slow Bool + -> Signal slow Bool + -> Signal fast a + -> Signal slow (a,a) + goSync (o0,o1,o2) rt@(~(r :- rs)) ~(e :- es) as@(~(x0 :- x1 :- xs)) = let (o0',o1',o2') = if r then (i0,i1,i2) else (o2,x0,x1) in o0 `seqX` o1 `seqX` (o0,o1) - :- (rt `seq` as `seq` if e then go (o0',o1',o2') rs es xs - else go (o0 ,o1 ,o2) rs es xs) - -ddrIn# (GatedClock _ _ ena) (Async rst) i0 i1 i2 = - go ((errorX "ddrIn: initial value 0 undefined") - ,(errorX "ddrIn: initial value 1 undefined") - ,(errorX "ddrIn: initial value 2 undefined")) - rst - ena - where - go :: (a,a,a) -> Signal slow Bool -> Signal slow Bool -> Signal fast a -> Signal slow (a,a) - go (o0,o1,o2) ~(r :- rs) ~(e :- es) as@(~(x0 :- x1 :- xs)) = + :- (rt `seq` as `seq` if e then goSync (o0',o1',o2') rs es xs + else goSync (o0 ,o1 ,o2) rs es xs) + + goAsync + :: (a, a, a) + -> Signal slow Bool + -> Signal slow Bool + -> Signal fast a + -> Signal slow (a, a) + goAsync (o0,o1,o2) ~(r :- rs) ~(e :- es) as@(~(x0 :- x1 :- xs)) = let (o0',o1',o2') = if r then (i0,i1,i2) else (o0,o1,o2) in o0' `seqX` o1' `seqX` (o0',o1') - :- (as `seq` if e then go (o2',x0 ,x1) rs es xs - else go (o0',o1',o2') rs es xs) + :- (as `seq` if e then goAsync (o2',x0 ,x1) rs es xs + else goAsync (o0',o1',o2') rs es xs) + {-# NOINLINE ddrIn# #-} -- | DDR output primitive @@ -134,23 +163,26 @@ ddrIn# (GatedClock _ _ ena) (Async rst) i0 i1 i2 = ddrOut :: ( HasCallStack , Undefined a - , fast ~ 'Dom n pFast - , slow ~ 'Dom n (2*pFast)) - => Clock slow gated -- ^ clock - -> Reset slow synchronous -- ^ reset - -> a -- ^ reset value - -> Signal slow (a,a) -- ^ normal speed input pairs - -> Signal fast a -- ^ DDR output signal + , KnownDomain fast ('Domain fast fPeriod edge reset init) + , KnownDomain slow ('Domain slow (2*fPeriod) edge reset init) ) + => Clock slow enabled + -> Reset slow polarity + -> a + -- ^ reset value + -> Signal slow (a, a) + -- ^ Normal speed input pairs + -> Signal fast a + -- ^ DDR output signal ddrOut clk rst i0 = uncurry (withFrozenCallStack $ ddrOut# clk rst i0) . unbundle ddrOut# :: ( HasCallStack , Undefined a - , fast ~ 'Dom n pFast - , slow ~ 'Dom n (2*pFast)) - => Clock slow gated - -> Reset slow synchronous + , KnownDomain fast ('Domain fast fPeriod edge reset init) + , KnownDomain slow ('Domain slow (2*fPeriod) edge reset init) ) + => Clock slow enabled + -> Reset slow polarity -> a -> Signal slow a -> Signal slow a diff --git a/clash-prelude/src/Clash/Explicit/Mealy.hs b/clash-prelude/src/Clash/Explicit/Mealy.hs index 14a1586e08..477556a545 100644 --- a/clash-prelude/src/Clash/Explicit/Mealy.hs +++ b/clash-prelude/src/Clash/Explicit/Mealy.hs @@ -21,7 +21,7 @@ module Clash.Explicit.Mealy where import Clash.Explicit.Signal - (Bundle (..), Clock, Reset, Signal, register) + (KnownDomain, Bundle (..), Clock, Reset, Signal, register) import Clash.XException (Undefined) {- $setup @@ -78,15 +78,16 @@ let macT s (x,y) = (s',s) -- s2 = 'mealy' clk rst mac 0 ('bundle' (b,y)) -- @ mealy - :: Undefined s - => Clock dom gated + :: ( KnownDomain tag dom + , Undefined s ) + => Clock tag gated -- ^ 'Clock' to synchronize to - -> Reset dom synchronous + -> Reset tag synchronous -> (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@ -> s -- ^ Initial state - -> (Signal dom i -> Signal dom o) + -> (Signal tag i -> Signal tag o) -- ^ Synchronous sequential function with input and output matching that -- of the mealy machine mealy clk rst f iS = @@ -122,16 +123,17 @@ mealy clk rst f iS = -- (i2,b2) = 'mealyB' clk rst f 3 (i1,c) -- @ mealyB - :: ( Undefined s + :: ( KnownDomain tag dom + , Undefined s , Bundle i , Bundle o ) - => Clock dom gated - -> Reset dom synchronous + => Clock tag gated + -> Reset tag synchronous -> (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@ -> s -- ^ Initial state - -> (Unbundled dom i -> Unbundled dom o) + -> (Unbundled tag i -> Unbundled tag o) -- ^ Synchronous sequential function with input and output matching that -- of the mealy machine mealyB clk rst f iS i = unbundle (mealy clk rst f iS (bundle i)) diff --git a/clash-prelude/src/Clash/Explicit/Moore.hs b/clash-prelude/src/Clash/Explicit/Moore.hs index 208302f1ad..fa97d8f56f 100644 --- a/clash-prelude/src/Clash/Explicit/Moore.hs +++ b/clash-prelude/src/Clash/Explicit/Moore.hs @@ -23,7 +23,7 @@ module Clash.Explicit.Moore where import Clash.Explicit.Signal - (Bundle (..), Clock, Reset, Signal, register) + (KnownDomain, Bundle (..), Clock, Reset, Signal, register) import Clash.XException (Undefined) {- $setup @@ -56,32 +56,33 @@ import Clash.XException (Undefined) -- ... -- -- Synchronous sequential functions can be composed just like their --- combinational counterpart: +-- combinatorial counterpart: -- -- @ -- dualMac --- :: Clock domain gated --- -> Reset domain synchronous --- -> ('Signal' domain Int, 'Signal' domain Int) --- -> ('Signal' domain Int, 'Signal' domain Int) --- -> 'Signal' domain Int +-- :: Clock tag gated +-- -> Reset tag synchronous +-- -> ('Signal' tag Int, 'Signal' tag Int) +-- -> ('Signal' tag Int, 'Signal' tag Int) +-- -> 'Signal' tag Int -- dualMac clk rst (a,b) (x,y) = s1 + s2 -- where -- s1 = 'moore' clk rst mac id 0 ('bundle' (a,x)) -- s2 = 'moore' clk rst mac id 0 ('bundle' (b,y)) -- @ moore - :: Undefined s - => Clock domain gated + :: ( KnownDomain tag dom + , Undefined s ) + => Clock tag gated -- ^ 'Clock' to synchronize to - -> Reset domain synchronous + -> Reset tag synchronous -> (s -> i -> s) -- ^ Transfer function in moore machine form: @state -> input -> newstate@ -> (s -> o) -- ^ Output function in moore machine form: @state -> output@ -> s -- ^ Initial state - -> (Signal domain i -> Signal domain o) + -> (Signal tag i -> Signal tag o) -- ^ Synchronous sequential function with input and output matching that -- of the moore machine moore clk rst ft fo iS = @@ -93,12 +94,13 @@ moore clk rst ft fo iS = -- | Create a synchronous function from a combinational function describing -- a moore machine without any output logic medvedev - :: Undefined s - => Clock domain gated - -> Reset domain synchronous + :: ( KnownDomain tag dom + , Undefined s ) + => Clock tag gated + -> Reset tag synchronous -> (s -> i -> s) -> s - -> (Signal domain i -> Signal domain s) + -> (Signal tag i -> Signal tag s) medvedev clk rst tr st = moore clk rst tr id st {-# INLINE medvedev #-} @@ -130,17 +132,18 @@ medvedev clk rst tr st = moore clk rst tr id st -- (i2,b2) = 'mooreB' clk rst t o 3 (i1,c) -- @ mooreB - :: ( Undefined s + :: ( KnownDomain tag dom + , Undefined s , Bundle i , Bundle o ) - => Clock domain gated - -> Reset domain synchronous + => Clock tag gated + -> Reset tag synchronous -> (s -> i -> s) -- ^ Transfer function in moore machine form: -- @state -> input -> newstate@ -> (s -> o) -- ^ Output function in moore machine form: -- @state -> output@ -> s -- ^ Initial state - -> (Unbundled domain i -> Unbundled domain o) + -> (Unbundled tag i -> Unbundled tag o) -- ^ Synchronous sequential function with input and output matching that -- of the moore machine mooreB clk rst ft fo iS i = unbundle (moore clk rst ft fo iS (bundle i)) @@ -148,13 +151,14 @@ mooreB clk rst ft fo iS i = unbundle (moore clk rst ft fo iS (bundle i)) -- | A version of 'medvedev' that does automatic 'Bundle'ing medvedevB - :: ( Undefined s + :: ( KnownDomain tag dom + , Undefined s , Bundle i , Bundle s ) - => Clock domain gated - -> Reset domain synchronous + => Clock tag gated + -> Reset tag synchronous -> (s -> i -> s) -> s - -> (Unbundled domain i -> Unbundled domain s) + -> (Unbundled tag i -> Unbundled tag s) medvedevB clk rst tr st = mooreB clk rst tr id st {-# INLINE medvedevB #-} diff --git a/clash-prelude/src/Clash/Explicit/Prelude.hs b/clash-prelude/src/Clash/Explicit/Prelude.hs index 8e2956f881..431c0bf6fe 100644 --- a/clash-prelude/src/Clash/Explicit/Prelude.hs +++ b/clash-prelude/src/Clash/Explicit/Prelude.hs @@ -19,13 +19,13 @@ you can make multi-clock designs. {-# OPTIONS_HADDOCK show-extensions #-} module Clash.Explicit.Prelude - ( -- * Creating synchronous sequential circuits + ( -- * Creating polarity sequential circuits mealy , mealyB , moore , mooreB , registerB - -- * Synchronizer circuits for safe clock domain crossings + -- * Synchronizer circuits for safe clock tag crossings , dualFlipFlopSynchronizer , asyncFIFOSynchronizer -- * ROMs @@ -183,8 +183,8 @@ import Clash.XException -- -- @ -- window4 ---- :: Clock domain gated -> Reset domain synchronous --- -> 'Signal' domain Int -> 'Vec' 4 ('Signal' domain Int) +--- :: Clock tag enabled -> Reset tag polarity +-- -> 'Signal' tag Int -> 'Vec' 4 ('Signal' tag Int) -- window4 = 'window' -- @ -- @@ -192,12 +192,16 @@ import Clash.XException -- [<1,0,0,0>,<2,1,0,0>,<3,2,1,0>,<4,3,2,1>,<5,4,3,2>... -- ... window - :: (KnownNat n, Undefined a, Default a) - => Clock domain gated + :: ( KnownNat n + , KnownDomain tag dom + , Undefined a + , Default a + ) + => Clock tag enabled -- ^ Clock to which the incoming signal is synchronized - -> Reset domain synchronous - -> Signal domain a -- ^ Signal to create a window over - -> Vec (n + 1) (Signal domain a) -- ^ Window of at least size 1 + -> Reset tag polarity + -> Signal tag a -- ^ Signal to create a window over + -> Vec (n + 1) (Signal tag a) -- ^ Window of at least size 1 window clk rst x = res where res = x :> prev @@ -210,21 +214,26 @@ window clk rst x = res -- | Give a delayed window over a 'Signal' -- -- @ --- windowD3 :: Clock domain gated -> Reset domain synchronous --- -> 'Signal' domain Int -> 'Vec' 3 ('Signal' domain Int) +-- windowD3 :: Clock tag enabled -> Reset tag polarity +-- -> 'Signal' tag Int -> 'Vec' 3 ('Signal' tag Int) -- windowD3 = 'windowD' -- @ -- --- >>> simulateB (windowD3 systemClockGen asyncResetGen) [1::Int,1,2,3,4] :: [Vec 3 Int] +-- >>> simulateB (windowD3 systemClockGen resetGen) [1::Int,1,2,3,4] :: [Vec 3 Int] -- [<0,0,0>,<0,0,0>,<1,0,0>,<2,1,0>,<3,2,1>,<4,3,2>... -- ... windowD - :: (KnownNat n, Undefined a, Default a) - => Clock domain gated + :: ( KnownNat n + , Undefined a + , Default a + , KnownDomain tag dom ) + => Clock tag enabled -- ^ Clock to which the incoming signal is synchronized - -> Reset domain synchronous - -> Signal domain a -- ^ Signal to create a window over - -> Vec (n + 1) (Signal domain a) -- ^ Window of at least size 1 + -> Reset tag polarity + -> Signal tag a + -- ^ Signal to create a window over + -> Vec (n + 1) (Signal tag a) + -- ^ Window of at least size 1 windowD clk rst x = let prev = registerB clk rst (repeat def) next next = x +>> prev diff --git a/clash-prelude/src/Clash/Explicit/Prelude/Safe.hs b/clash-prelude/src/Clash/Explicit/Prelude/Safe.hs index a84ff6c876..12feda8f22 100644 --- a/clash-prelude/src/Clash/Explicit/Prelude/Safe.hs +++ b/clash-prelude/src/Clash/Explicit/Prelude/Safe.hs @@ -27,7 +27,7 @@ module Clash.Explicit.Prelude.Safe , moore , mooreB , registerB - -- * Synchronizer circuits for safe clock domain crossing + -- * Synchronizer circuits for safe clock tag crossing , dualFlipFlopSynchronizer , asyncFIFOSynchronizer -- * ROMs @@ -155,9 +155,9 @@ import Clash.XException -- @('Signal' a, 'Signal' b)@) -- -- @ --- rP :: Clock domain gated -> Reset domain synchronous --- -> ('Signal' domain Int, 'Signal' domain Int) --- -> ('Signal' domain Int, 'Signal' domain Int) +-- rP :: Clock tag enabled -> Reset tag synchronous +-- -> ('Signal' tag Int, 'Signal' tag Int) +-- -> ('Signal' tag Int, 'Signal' tag Int) -- rP clk rst = 'registerB' clk rst (8,8) -- @ -- @@ -165,23 +165,28 @@ import Clash.XException -- [(8,8),(8,8),(1,1),(2,2),(3,3)... -- ... registerB - :: (Undefined a, Bundle a) - => Clock domain gated - -> Reset domain synchronous + :: ( KnownDomain tag dom + , Undefined a + , Bundle a ) + => Clock tag enabled + -> Reset tag synchronous -> a - -> Unbundled domain a - -> Unbundled domain a + -> Unbundled tag a + -> Unbundled tag a registerB clk rst i = unbundle Prelude.. register clk rst i Prelude.. bundle {-# INLINE registerB #-} -- | Give a pulse when the 'Signal' goes from 'minBound' to 'maxBound' isRising - :: (Undefined a, Bounded a, Eq a) - => Clock domain gated - -> Reset domain synchronous + :: ( KnownDomain tag dom + , Undefined a + , Bounded a + , Eq a ) + => Clock tag enabled + -> Reset tag synchronous -> a -- ^ Starting value - -> Signal domain a - -> Signal domain Bool + -> Signal tag a + -> Signal tag Bool isRising clk rst is s = liftA2 edgeDetect prev s where prev = register clk rst is s @@ -190,12 +195,15 @@ isRising clk rst is s = liftA2 edgeDetect prev s -- | Give a pulse when the 'Signal' goes from 'maxBound' to 'minBound' isFalling - :: (Undefined a, Bounded a, Eq a) - => Clock domain gated - -> Reset domain synchronous + :: ( KnownDomain tag dom + , Undefined a + , Bounded a + , Eq a ) + => Clock tag enabled + -> Reset tag synchronous -> a -- ^ Starting value - -> Signal domain a - -> Signal domain Bool + -> Signal tag a + -> Signal tag Bool isFalling clk rst is s = liftA2 edgeDetect prev s where prev = register clk rst is s @@ -206,11 +214,12 @@ isFalling clk rst is s = liftA2 edgeDetect prev s -- combined with functions like @'Clash.Explicit.Signal.regEn'@ or -- @'Clash.Explicit.Signal.mux'@, in order to delay a register by a known amount. riseEvery - :: forall domain gated synchronous n - . Clock domain gated - -> Reset domain synchronous + :: forall tag dom enabled synchronous n + . KnownDomain tag dom + => Clock tag enabled + -> Reset tag synchronous -> SNat n - -> Signal domain Bool + -> Signal tag Bool riseEvery clk rst SNat = moore clk rst transfer output 0 (pure ()) where output :: Index n -> Bool @@ -222,12 +231,13 @@ riseEvery clk rst SNat = moore clk rst transfer output 0 (pure ()) -- | Oscillate a @'Bool'@ for a given number of cycles, given the starting state. oscillate - :: forall domain gated synchronous n - . Clock domain gated - -> Reset domain synchronous + :: forall tag dom enabled synchronous n + . KnownDomain tag dom + => Clock tag enabled + -> Reset tag synchronous -> Bool -> SNat n - -> Signal domain Bool + -> Signal tag Bool oscillate clk rst begin SNat = moore clk rst transfer snd (0, begin) (pure ()) where transfer :: (Index n, Bool) -> () -> (Index n, Bool) diff --git a/clash-prelude/src/Clash/Explicit/RAM.hs b/clash-prelude/src/Clash/Explicit/RAM.hs index 341781dfc6..f15b7c6fc2 100644 --- a/clash-prelude/src/Clash/Explicit/RAM.hs +++ b/clash-prelude/src/Clash/Explicit/RAM.hs @@ -26,7 +26,7 @@ RAM primitives with a combinational read port. {-# OPTIONS_HADDOCK show-extensions #-} module Clash.Explicit.RAM - ( -- * RAM synchronised to an arbitrary clock + ( -- * RAM synchronized to an arbitrary clock asyncRam , asyncRamPow2 -- * Internal @@ -39,7 +39,7 @@ import GHC.Stack (HasCallStack, withFrozenCallStack) import GHC.TypeLits (KnownNat) import qualified Data.Vector as V -import Clash.Explicit.Signal ((.&&.), unbundle, unsafeSynchronizer) +import Clash.Explicit.Signal ((.&&.), unbundle, unsafeSynchronizer, KnownDomain) import Clash.Promoted.Nat (SNat (..), snatToNum, pow2SNat) import Clash.Signal.Internal (Clock (..), Signal (..), clockEnable) import Clash.Sized.Unsigned (Unsigned) @@ -54,17 +54,21 @@ import Clash.XException (errorX, maybeIsX) -- * See "Clash.Prelude.BlockRam#usingrams" for more information on how to use a -- RAM. asyncRamPow2 - :: forall wdom rdom wgated rgated n a - . (KnownNat n, HasCallStack) - => Clock wdom wgated + :: forall wtag rtag wenabled renabled wconf rconf n a + . ( KnownNat n + , HasCallStack + , KnownDomain wtag wconf + , KnownDomain rtag rconf + ) + => Clock wtag wenabled -- ^ 'Clock' to which to synchronise the write port of the RAM - -> Clock rdom rgated - -- ^ 'Clock' to which the read address signal, @r@, is synchronised - -> Signal rdom (Unsigned n) + -> Clock rtag renabled + -- ^ 'Clock' to which the read address signal, @r@, is synchronized + -> Signal rtag (Unsigned n) -- ^ Read address @r@ - -> Signal wdom (Maybe (Unsigned n, a)) + -> Signal wtag (Maybe (Unsigned n, a)) -- ^ (write address @w@, value to write) - -> Signal rdom a + -> Signal rtag a -- ^ Value of the @RAM@ at address @r@ asyncRamPow2 = \wclk rclk rd wrM -> withFrozenCallStack (asyncRam wclk rclk (pow2SNat (SNat @ n)) rd wrM) @@ -80,18 +84,22 @@ asyncRamPow2 = \wclk rclk rd wrM -> withFrozenCallStack -- * See "Clash.Explicit.BlockRam#usingrams" for more information on how to use a -- RAM. asyncRam - :: (Enum addr, HasCallStack) - => Clock wdom wgated + :: ( Enum addr + , HasCallStack + , KnownDomain wtag wconf + , KnownDomain rtag rconf + ) + => Clock wtag wenabled -- ^ 'Clock' to which to synchronise the write port of the RAM - -> Clock rdom rgated - -- ^ 'Clock' to which the read address signal, @r@, is synchronised + -> Clock rtag renabled + -- ^ 'Clock' to which the read address signal, @r@, is synchronized -> SNat n -- ^ Size @n@ of the RAM - -> Signal rdom addr + -> Signal rtag addr -- ^ Read address @r@ - -> Signal wdom (Maybe (addr, a)) + -> Signal wtag (Maybe (addr, a)) -- ^ (write address @w@, value to write) - -> Signal rdom a + -> Signal rtag a -- ^ Value of the @RAM@ at address @r@ asyncRam = \wclk rclk sz rd wrM -> let en = isJust <$> wrM @@ -102,17 +110,19 @@ asyncRam = \wclk rclk sz rd wrM -> -- | RAM primitive asyncRam# - :: HasCallStack - => Clock wdom wgated + :: ( HasCallStack + , KnownDomain wtag wconf + , KnownDomain rtag rconf ) + => Clock wtag wenabled -- ^ 'Clock' to which to synchronise the write port of the RAM - -> Clock rdom rgated - -- ^ 'Clock' to which the read address signal, @r@, is synchronised + -> Clock rtag renabled + -- ^ 'Clock' to which the read address signal, @r@, is synchronized -> SNat n -- ^ Size @n@ of the RAM - -> Signal rdom Int -- ^ Read address @r@ - -> Signal wdom Bool -- ^ Write enable - -> Signal wdom Int -- ^ Write address @w@ - -> Signal wdom a -- ^ Value to write (at address @w@) - -> Signal rdom a -- ^ Value of the @RAM@ at address @r@ + -> Signal rtag Int -- ^ Read address @r@ + -> Signal wtag Bool -- ^ Write enable + -> Signal wtag Int -- ^ Write address @w@ + -> Signal wtag a -- ^ Value to write (at address @w@) + -> Signal rtag a -- ^ Value of the @RAM@ at address @r@ asyncRam# wclk rclk sz rd en wr din = unsafeSynchronizer wclk rclk dout where @@ -125,8 +135,8 @@ asyncRam# wclk rclk sz rd en wr din = Just wgt -> wgt .&&. en dout = go ramI rd' en' wr din - go :: V.Vector a -> Signal wdom Int -> Signal wdom Bool - -> Signal wdom Int -> Signal wdom a -> Signal wdom a + go :: V.Vector a -> Signal wtag Int -> Signal wtag Bool + -> Signal wtag Int -> Signal wtag a -> Signal wtag a go !ram (r :- rs) (e :- es) (w :- ws) (d :- ds) = let ram' = upd ram e (fromEnum w) d o = ram V.! r diff --git a/clash-prelude/src/Clash/Explicit/ROM.hs b/clash-prelude/src/Clash/Explicit/ROM.hs index 5cb793680f..97b45b2141 100644 --- a/clash-prelude/src/Clash/Explicit/ROM.hs +++ b/clash-prelude/src/Clash/Explicit/ROM.hs @@ -18,7 +18,7 @@ ROMs {-# OPTIONS_HADDOCK show-extensions #-} module Clash.Explicit.ROM - ( -- * Synchronous ROM synchronised to an arbitrary clock + ( -- * Synchronous ROM synchronized to an arbitrary clock rom , romPow2 -- * Internal @@ -47,12 +47,16 @@ import Clash.XException (errorX, seqX) -- for ideas on how to use ROMs and RAMs romPow2 :: KnownNat n - => Clock domain gated -- ^ 'Clock' to synchronize to - -> Vec (2^n) a -- ^ ROM content - -- - -- __NB:__ must be a constant - -> Signal domain (Unsigned n) -- ^ Read address @rd@ - -> Signal domain a -- ^ The value of the ROM at address @rd@ + => Clock tag enabled + -- ^ 'Clock' to synchronize to + -> Vec (2^n) a + -- ^ ROM content + -- + -- __NB:__ must be a constant + -> Signal tag (Unsigned n) + -- ^ Read address @rd@ + -> Signal tag a + -- ^ The value of the ROM at address @rd@ romPow2 = rom {-# INLINE romPow2 #-} @@ -66,13 +70,13 @@ romPow2 = rom -- * See "Clash.Sized.Fixed#creatingdatafiles" and "Clash.Explicit.BlockRam#usingrams" -- for ideas on how to use ROMs and RAMs rom - :: (KnownNat n, Enum addr) - => Clock domain gated -- ^ 'Clock' to synchronize to + :: ( KnownNat n, Enum addr) + => Clock tag enabled -- ^ 'Clock' to synchronize to -> Vec n a -- ^ ROM content -- -- __NB:__ must be a constant - -> Signal domain addr -- ^ Read address @rd@ - -> Signal domain a + -> Signal tag addr -- ^ Read address @rd@ + -> Signal tag a -- ^ The value of the ROM at address @rd@ from the previous clock cycle rom = \clk content rd -> rom# clk content (fromEnum <$> rd) {-# INLINE rom #-} @@ -80,25 +84,28 @@ rom = \clk content rd -> rom# clk content (fromEnum <$> rd) -- | ROM primitive rom# :: KnownNat n - => Clock domain gated -- ^ 'Clock' to synchronize to - -> Vec n a -- ^ ROM content - -- - -- __NB:__ must be a constant - -> Signal domain Int -- ^ Read address @rd@ - -> Signal domain a + => Clock tag enabled + -- ^ 'Clock' to synchronize to + -> Vec n a + -- ^ ROM content + -- + -- __NB:__ must be a constant + -> Signal tag Int + -- ^ Read address @rd@ + -> Signal tag a -- ^ The value of the ROM at address @rd@ from the previous clock cycle rom# clk content rd = go clk ((arr !) <$> rd) where szI = length content arr = listArray (0,szI-1) (toList content) - go :: Clock domain gated - -> Signal domain a - -> Signal domain a - go Clock {} = + go :: Clock tag enabled + -> Signal tag a + -> Signal tag a + go (Clock _ Nothing) = \s -> withFrozenCallStack (errorX "rom: initial value undefined") :- s - go (GatedClock _ _ en) = + go (Clock _ (Just en)) = go' (withFrozenCallStack (errorX "rom: initial value undefined")) en go' o (e :- es) as@(~(x :- xs)) = diff --git a/clash-prelude/src/Clash/Explicit/ROM/File.hs b/clash-prelude/src/Clash/Explicit/ROM/File.hs index 6cce5c8b5f..8262fa0fd8 100644 --- a/clash-prelude/src/Clash/Explicit/ROM/File.hs +++ b/clash-prelude/src/Clash/Explicit/ROM/File.hs @@ -80,7 +80,7 @@ __>>> L.tail $ sampleN 4 $ g systemClockGen (fromList [3..5])__ {-# OPTIONS_HADDOCK show-extensions #-} module Clash.Explicit.ROM.File - ( -- * Synchronous ROM synchronised to an arbitrary clock + ( -- * Synchronous ROM synchronized to an arbitrary clock romFile , romFilePow2 -- * Internal diff --git a/clash-prelude/src/Clash/Explicit/Signal.hs b/clash-prelude/src/Clash/Explicit/Signal.hs index 07f719926c..e96e26388b 100644 --- a/clash-prelude/src/Clash/Explicit/Signal.hs +++ b/clash-prelude/src/Clash/Explicit/Signal.hs @@ -1,31 +1,31 @@ {-| Copyright : (C) 2013-2016, University of Twente, - 2016 , Myrtle Software, + 2016-2019, Myrtle Software, 2017 , Google Inc. License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij -Clash has synchronous 'Signal's in the form of: +Clash has polarity 'Signal's in the form of: @ -'Signal' (domain :: 'Domain') a +'Signal' (tag :: 'Domain') a @ Where /a/ is the type of the value of the 'Signal', for example /Int/ or /Bool/, -and /domain/ is the /clock-/ (and /reset-/) domain to which the memory elements +and /tag/ is the /clock-/ (and /reset-/) tag to which the memory elements manipulating these 'Signal's belong. -The type-parameter, /domain/, is of the kind 'Domain' which has types of the +The type-parameter, /tag/, is of the kind 'Domain' which has types of the following shape: @ -data Domain = Dom { domainName :: 'GHC.TypeLits.Symbol', clkPeriod :: 'GHC.TypeLits.Nat' } +data tag = Dom { domainName :: 'GHC.TypeLits.Symbol', clkPeriod :: 'GHC.TypeLits.Nat' } @ Where /domainName/ is a type-level string ('GHC.TypeLits.Symbol') representing -the name of the /clock-/ (and /reset-/) domain, and /clkPeriod/ is a type-level +the name of the /clock-/ (and /reset-/) tag, and /clkPeriod/ is a type-level natural number ('GHC.TypeLits.Nat') representing the clock period (in __ps__) -of the clock lines in the /clock-domain/. +of the clock lines in the /clock-tag/. * __NB__: \"Bad things\"™ happen when you actually use a clock period of @0@, so do __not__ do that! @@ -40,17 +40,17 @@ are also implicitly unique. The protection against accidental -offered by Clash's /domain/ annotation on 'Signal's is based on the uniqueness +offered by Clash's /tag/ annotation on 'Signal's is based on the uniqueness of clocks and resets. But with explicit clock and reset lines, there are ways to (accidentally) introduce situations that are prone to metastability. There are four different clock and reset lines: @ -'Reset' domain 'Synchronous' -'Reset' domain 'Asynchronous' -'Clock' domain 'Source' -'Clock' domain 'Gated' +'Reset' tag 'polarity' +'Reset' tag 'Asynchronous' +'Clock' tag 'Regular' +'Clock' tag 'Enabled' @ We now go over the combinations over these clock and reset line combinations @@ -60,7 +60,7 @@ meta-stability: * /Reset situation 1/: @ - f :: Reset domain Synchronous -> Reset domain Synchronous -> .. + f :: Reset tag polarity -> Reset tag polarity -> .. f x y = .. @ @@ -71,12 +71,12 @@ meta-stability: * /Reset situation 2/: @ - g :: Reset domain Asynchronous -> Reset domain Asynchronous -> .. + g :: Reset tag Asynchronous -> Reset tag Asynchronous -> .. g x y = .. @ This situation can be prone to metastability, because although /x/ and - /y/ belong to the same /domain/ according to their type, there is no + /y/ belong to the same /tag/ according to their type, there is no guarantee that they actually originate from the same source. This means that one component can enter its reset state asynchronously to another component, inducing metastability in the other component. @@ -89,7 +89,7 @@ meta-stability: * /Reset situation 3/: @ - h :: Reset domain Asynchronous -> Reset domain Synchronous -> .. + h :: Reset tag Asynchronous -> Reset tag polarity -> .. h x y = .. @ @@ -99,8 +99,8 @@ meta-stability: * The Clash compiler will give a warning whenever a function has a type-signature similar to the one above. - * Although in a standalone context, converting between @'Reset' domain - 'Synchronous'@ and @'Signal' domain 'Bool'@ would be safe from a + * Although in a standalone context, converting between @'Reset' tag + 'polarity'@ and @'Signal' tag 'Bool'@ would be safe from a metastability point of view, it is not when we're in a context where there are also asynchronous resets. That is why 'unsafeToSyncReset' is prefixed with the word /unsafe/. @@ -108,18 +108,18 @@ meta-stability: * /Clock situations 1, 2, and 3/: @ - k :: Clock domain Source -> Clock domain Source -> .. + k :: Clock tag Regular -> Clock tag Regular -> .. k x y = .. - l :: Clock domain Source -> Clock domain Gated -> .. + l :: Clock tag Regular -> Clock tag Enabled -> .. l x y = .. - m :: Clock domain Gated -> Clock domain Gated -> .. + m :: Clock tag Enabled -> Clock tag Enabled -> .. m x y = .. @ All the above situations are potentially prone to metastability, because - even though /x/ and /y/ belong to the same /domain/ according to their + even though /x/ and /y/ belong to the same /tag/ according to their type, there is no guarantee that they actually originate from the same source. They could hence be connected to completely unrelated clock sources, and components can then induce metastable states in others. @@ -128,30 +128,48 @@ meta-stability: type-signature similar to one of the above three situations. -} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE MagicHash #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE Trustworthy #-} {-# OPTIONS_HADDOCK show-extensions #-} module Clash.Explicit.Signal - ( -- * Synchronous signal - Signal, Domain (..), System + ( -- * polarity signal + Signal + -- * tag + , KnownDomain(..) + , ActiveEdge(..) + , SActiveEdge(..) + , InitBehavior(..) + , SInitBehavior(..) + , ResetKind(..) + , SResetKind(..) + , Domain(..) + , SDomain(..) + , System -- * Clock , Clock, ClockKind (..) , freqCalc -- ** Synchronisation primitive , unsafeSynchronizer -- ** Clock gating - , clockGate + , toEnabledClock -- * Reset - , Reset, ResetKind (..) - , unsafeFromAsyncReset - , unsafeToAsyncReset + , Reset(..) + , ResetPolarity(..) , fromSyncReset - , unsafeToSyncReset + , syncPolarity + , toHighPolarity + , toLowPolarity + , unsafeFromReset + , unsafeToActiveHighReset + , unsafeToActiveLowReset , resetSynchronizer -- * Basic circuit functions , delay @@ -163,8 +181,7 @@ module Clash.Explicit.Signal -- * Simulation and testbench functions , clockGen , tbClockGen - , asyncResetGen - , syncResetGen + , resetGen , systemClockGen , tbSystemClockGen , systemResetGen @@ -172,13 +189,13 @@ module Clash.Explicit.Signal , (.&&.), (.||.) -- * Product/Signal isomorphism , Bundle(..) - -- * Simulation functions (not synthesisable) + -- * Simulation functions (not synthesizable) , simulate , simulateB -- ** lazy versions , simulate_lazy , simulateB_lazy - -- * List \<-\> Signal conversion (not synthesisable) + -- * List \<-\> Signal conversion (not synthesizable) , sample , sampleN , fromList @@ -198,16 +215,26 @@ where import Data.Maybe (isJust, fromJust) -import Clash.Signal.Internal import Clash.Signal.Bundle (Bundle (..)) +import Clash.Signal.Internal import Clash.XException (Undefined) {- $setup ->>> :set -XDataKinds -XTypeApplications +>>> :set -XDataKinds -XTypeApplications -XFlexibleInstances -XMultiParamTypeClasses >>> import Clash.Explicit.Prelude >>> import qualified Data.List as L ->>> type Dom2 = Dom "dom" 2 ->>> type Dom7 = Dom "dom" 7 +>>> :{ +instance KnownDomain "Dom2" ('Domain "Dom2" 2 'Rising 'Asynchronous 'Defined) where + knownDomain tag = SDomain tag SNat SRising SAsynchronous SDefined +:} + +>>> :{ +instance KnownDomain "Dom7" ('Domain "Dom7" 7 'Rising 'Asynchronous 'Defined) where + knownDomain tag = SDomain tag SNat SRising SAsynchronous SDefined +:} + +>>> type Dom2 = "Dom2" +>>> type Dom7 = "Dom7" >>> let clk2 = clockGen @Dom2 >>> let clk7 = clockGen @Dom7 >>> let oversampling clkA clkB dflt = delay clkB dflt . unsafeSynchronizer clkA clkB . delay clkA dflt @@ -230,19 +257,15 @@ countSometimes clk rst = s where -} -- **Clock - --- | A /clock/ (and /reset/) domain with clocks running at 100 MHz -type System = 'Dom "system" 10000 - --- | Clock generator for the 'System' clock domain. +-- | Clock generator for the 'System' clock tag. -- -- __NB__: should only be used for simulation, and __not__ for the /testBench/ -- function. For the /testBench/ function, used 'tbSystemClockGen' systemClockGen - :: Clock System 'Source + :: Clock System 'Regular systemClockGen = clockGen --- | Clock generator for the 'System' clock domain. +-- | Clock generator for the 'System' clock tag. -- -- __NB__: can be used in the /testBench/ function -- @@ -263,10 +286,10 @@ systemClockGen = clockGen -- @ tbSystemClockGen :: Signal System Bool - -> Clock System 'Source + -> Clock System 'Regular tbSystemClockGen = tbClockGen --- | Reset generator for the 'System' clock domain. +-- | Reset generator for the 'System' clock tag. -- -- __NB__: should only be used for simulation or the \testBench\ function. -- @@ -285,8 +308,8 @@ tbSystemClockGen = tbClockGen -- clk = tbSystemClockGen (not <\$\> done) -- rst = 'systemResetGen' -- @ -systemResetGen :: Reset System 'Asynchronous -systemResetGen = asyncResetGen +systemResetGen :: Reset System 'ActiveHigh +systemResetGen = resetGen -- | Normally, asynchronous resets can be both asynchronously asserted and -- de-asserted. Asynchronous de-assertion can induce meta-stability in the @@ -296,20 +319,17 @@ systemResetGen = asyncResetGen -- -- Note that asynchronous assertion does not induce meta-stability in the -- component whose reset is asserted. However, when a component \"A\" in another --- clock or reset domain depends on the value of a component \"B\" being +-- clock or reset tag depends on the value of a component \"B\" being -- reset, then asynchronous assertion of the reset of component \"B"\ can induce -- meta-stability in component \"A\". To prevent this from happening you need -- to use a proper synchronizer, for example one of the synchronizers in -- "Clash.Explicit.Synchronizer" -- --- __NB:__ Assumes the component(s) being reset have an /active-high/ reset port, --- which all components in __clash-prelude__ have. --- -- === __Example__ -- -- @ -- topEntity --- :: Clock System Source +-- :: Clock System Regular -- -> Reset System Asynchronous -- -> Signal System Bit -- -> Signal System (BitVector 8) @@ -321,14 +341,22 @@ systemResetGen = asyncResetGen -- key1R = isRising 1 key1 -- leds = mealy blinkerT (1,False,0) key1R -- @ +-- TODO: Docs resetSynchronizer - :: Clock domain gated - -> Reset domain 'Asynchronous - -> Reset domain 'Asynchronous -resetSynchronizer clk rst = - let r1 = register clk rst True (pure False) - r2 = register clk rst True r1 - in unsafeToAsyncReset r2 + :: KnownDomain tag dom + => Clock tag gated + -> Reset tag polarity + -> Reset tag polarity +resetSynchronizer clk@(Clock tag _) rst@(toHighPolarity -> hRst) = + case knownDomain tag of + SDomain _tag _period _edge SSynchronous _init -> + let r1 = register clk hRst True (pure False) + r2 = register clk hRst True r1 + in syncPolarity rst (unsafeToActiveHighReset r2) + _ -> + -- Reset is already polarity, nothing to do! + rst + -- | Calculate the period, in __ps__, given a frequency in __Hz__ -- @@ -337,16 +365,16 @@ resetSynchronizer clk rst = -- >>> freqCalc 240e6 -- 4167 -- --- __NB__: This function is /not/ synthesisable +-- __NB__: This function is /not/ synthesizable freqCalc :: Double -> Integer freqCalc freq = ceiling ((1.0 / freq) / 1.0e-12) -- ** Synchronisation primitive {-# NOINLINE unsafeSynchronizer #-} -- | The 'unsafeSynchronizer' function is a primitive that must be used to --- connect one clock domain to the other, and will be synthesised to a (bundle +-- connect one clock domain to the other, and will be synthesized to a (bundle -- of) wire(s) in the eventual circuit. This function should only be used as --- part of a proper synchronisation component, such as the following dual +-- part of a proper synchronization component, such as the following dual -- flip-flop synchronizer: -- -- @ @@ -365,7 +393,7 @@ freqCalc freq = ceiling ((1.0 / freq) / 1.0e-12) -- @ -- type Dom7 = 'Dom' \"dom\" 7 -- --- clk7 :: 'Clock' Dom7 Source +-- clk7 :: 'Clock' Dom7 Regular -- clk7 = 'clockGen' -- @ -- @@ -374,7 +402,7 @@ freqCalc freq = ceiling ((1.0 / freq) / 1.0e-12) -- @ -- type Dom2 = 'Dom' \"dom\" 2 -- --- clk2 :: 'Clock' Dom2 Source +-- clk2 :: 'Clock' Dom2 Regular -- clk2 = 'clockGen' -- @ -- @@ -411,10 +439,14 @@ freqCalc freq = ceiling ((1.0 / freq) / 1.0e-12) -- >>> sampleN 12 (almostId clk2 clk7 0 (fromList [(1::Int)..10])) -- [0,0,1,2,3,4,5,6,7,8,9,10] unsafeSynchronizer - :: Clock domain1 gated1 -- ^ 'Clock' of the incoming signal - -> Clock domain2 gated2 -- ^ 'Clock' of the outgoing signal - -> Signal domain1 a - -> Signal domain2 a + :: KnownDomain tag1 conf1 + => KnownDomain tag2 conf2 + => Clock tag1 gated1 + -- ^ 'Clock' of the incoming signal + -> Clock tag2 gated2 + -- ^ 'Clock' of the outgoing signal + -> Signal tag1 a + -> Signal tag2 a unsafeSynchronizer clk1 clk2 s = s' where t1 = clockPeriod clk1 @@ -423,13 +455,13 @@ unsafeSynchronizer clk1 clk2 s = s' | t1 > t2 = oversample t1 t2 s | otherwise = same s -same :: Signal domain1 a -> Signal domain2 a +same :: Signal tag1 a -> Signal tag2 a same (s :- ss) = s :- same ss -oversample :: Int -> Int -> Signal domain1 a -> Signal domain2 a +oversample :: Int -> Int -> Signal tag1 a -> Signal tag2 a oversample high low (s :- ss) = s :- oversampleS (reverse (repSchedule high low)) ss -oversampleS :: [Int] -> Signal domain1 a -> Signal domain2 a +oversampleS :: [Int] -> Signal tag1 a -> Signal tag2 a oversampleS sched = oversample' sched where oversample' [] s = oversampleS sched s @@ -438,10 +470,10 @@ oversampleS sched = oversample' sched prefixN 0 _ s = s prefixN n x s = x :- prefixN (n-1) x s -compress :: Int -> Int -> Signal domain1 a -> Signal domain2 a +compress :: Int -> Int -> Signal tag1 a -> Signal tag2 a compress high low s = compressS (repSchedule high low) s -compressS :: [Int] -> Signal domain1 a -> Signal domain2 a +compressS :: [Int] -> Signal tag1 a -> Signal tag2 a compressS sched = compress' sched where compress' [] s = compressS sched s @@ -466,12 +498,12 @@ repSchedule high low = take low $ repSchedule' low high 1 -- [0,1,2] delay :: Undefined a - => Clock domain gated + => Clock tag gated -- ^ Clock -> a -- ^ Default value - -> Signal domain a - -> Signal domain a + -> Signal tag a + -> Signal tag a delay = delay# {-# INLINE delay #-} @@ -483,12 +515,12 @@ delay = delay# -- [0,1,2,2,2,5,6] delayMaybe :: Undefined a - => Clock domain gated + => Clock tag gated -- ^ Clock -> a -- ^ Initial value - -> Signal domain (Maybe a) - -> Signal domain a + -> Signal tag (Maybe a) + -> Signal tag a delayMaybe clk dflt i = delayEn clk dflt (isJust <$> i) (fromJust <$> i) {-# INLINE delayMaybe #-} @@ -501,36 +533,37 @@ delayMaybe clk dflt i = -- [0,1,2,2,2,5,6] delayEn :: Undefined a - => Clock domain gated + => Clock tag gated -- ^ Clock -> a -- ^ Initial value - -> Signal domain Bool + -> Signal tag Bool -- ^ Enable - -> Signal domain a - -> Signal domain a + -> Signal tag a + -> Signal tag a delayEn clk dflt en i = - delay (clockGate clk en) dflt i + delay (toEnabledClock clk en) dflt i {-# INLINE delayEn #-} -- | \"@'register' clk rst i s@\" delays the values in 'Signal' /s/ for one -- cycle, and sets the value to @i@ the moment the reset becomes 'False'. -- --- >>> sampleN 5 (register systemClockGen asyncResetGen 8 (fromList [1,1,2,3,4])) +-- >>> sampleN 5 (register systemClockGen resetGen 8 (fromList [1,1,2,3,4])) -- [8,8,1,2,3] register - :: Undefined a - => Clock domain gated + :: ( KnownDomain tag dom + , Undefined a ) + => Clock tag gated -- ^ clock - -> Reset domain synchronous + -> Reset tag polarity -- ^ Reset (active-high), 'register' outputs the reset value when the -- reset value becomes 'True' -> a -- ^ Reset value - -> Signal domain a - -> Signal domain a + -> Signal tag a + -> Signal tag a register clk rst initial i = - register# clk rst initial initial i + register# clk (toHighPolarity rst) initial initial i {-# INLINE register #-} -- | Version of 'register' that only updates its content when its fourth @@ -550,23 +583,24 @@ register clk rst initial i = -- -- We get: -- --- >>> sampleN 9 (sometimes1 systemClockGen asyncResetGen) +-- >>> sampleN 9 (sometimes1 systemClockGen resetGen) -- [Nothing,Nothing,Just 1,Nothing,Just 1,Nothing,Just 1,Nothing,Just 1] --- >>> sampleN 9 (count systemClockGen asyncResetGen) +-- >>> sampleN 9 (count systemClockGen resetGen) -- [0,0,0,1,1,2,2,3,3] regMaybe - :: Undefined a - => Clock domain gated + :: ( KnownDomain tag dom + , Undefined a ) + => Clock tag gated -- ^ Clock - -> Reset domain synchronous + -> Reset tag polarity -- ^ Reset (active-high), 'regMaybe' outputs the reset value when the -- reset value becomes 'True' -> a -- ^ Reset value - -> Signal domain (Maybe a) - -> Signal domain a + -> Signal tag (Maybe a) + -> Signal tag a regMaybe clk rst initial iM = - register (clockGate clk (fmap isJust iM)) rst initial (fmap fromJust iM) + register (toEnabledClock clk (fmap isJust iM)) rst initial (fmap fromJust iM) {-# INLINE regMaybe #-} -- | Version of 'register' that only updates its content when its fourth @@ -579,25 +613,27 @@ regMaybe clk rst initial iM = -- -- We get: -- --- >>> sampleN 9 (oscillate systemClockGen asyncResetGen) +-- >>> sampleN 9 (oscillate systemClockGen resetGen) -- [False,False,True,False,True,False,True,False,True] --- >>> sampleN 9 (count systemClockGen asyncResetGen) +-- >>> sampleN 9 (count systemClockGen resetGen) -- [0,0,0,1,1,2,2,3,3] regEn - :: Undefined a - => Clock domain clk + :: ( KnownDomain tag dom + , Undefined a + ) + => Clock tag clk -- ^ Clock - -> Reset domain synchronous + -> Reset tag polarity -- ^ Reset (active-high), 'regEn' outputs the reset value when the -- reset value becomes 'True' -> a -- ^ Reset value - -> Signal domain Bool + -> Signal tag Bool -- ^ Enable signal - -> Signal domain a - -> Signal domain a + -> Signal tag a + -> Signal tag a regEn clk rst initial en i = - register (clockGate clk en) rst initial i + register (toEnabledClock clk en) rst initial i {-# INLINE regEn #-} -- * Product/Signal isomorphism @@ -605,14 +641,14 @@ regEn clk rst initial en i = -- | Simulate a (@'Unbundled' a -> 'Unbundled' b@) function given a list of -- samples of type /a/ -- --- >>> simulateB (unbundle . register systemClockGen asyncResetGen (8,8) . bundle) [(1,1), (1,1), (2,2), (3,3)] :: [(Int,Int)] +-- >>> simulateB (unbundle . register systemClockGen resetGen (8,8) . bundle) [(1,1), (1,1), (2,2), (3,3)] :: [(Int,Int)] -- [(8,8),(8,8),(1,1),(2,2),(3,3)... -- ... -- --- __NB__: This function is not synthesisable +-- __NB__: This function is not synthesizable simulateB :: (Bundle a, Bundle b, Undefined a, Undefined b) - => (Unbundled domain1 a -> Unbundled domain2 b) + => (Unbundled tag1 a -> Unbundled tag2 b) -- ^ The function we want to simulate -> [a] -- ^ Input samples @@ -622,14 +658,14 @@ simulateB f = simulate (bundle . f . unbundle) -- | /Lazily/ simulate a (@'Unbundled' a -> 'Unbundled' b@) function given a -- list of samples of type /a/ -- --- >>> simulateB (unbundle . register systemClockGen asyncResetGen (8,8) . bundle) [(1,1), (1,1), (2,2), (3,3)] :: [(Int,Int)] +-- >>> simulateB (unbundle . register systemClockGen resetGen (8,8) . bundle) [(1,1), (1,1), (2,2), (3,3)] :: [(Int,Int)] -- [(8,8),(8,8),(1,1),(2,2),(3,3)... -- ... -- --- __NB__: This function is not synthesisable +-- __NB__: This function is not synthesizable simulateB_lazy :: (Bundle a, Bundle b) - => (Unbundled domain1 a -> Unbundled domain2 b) + => (Unbundled tag1 a -> Unbundled tag2 b) -- ^ The function we want to simulate -> [a] -- ^ Input samples diff --git a/clash-prelude/src/Clash/Explicit/Signal/Delayed.hs b/clash-prelude/src/Clash/Explicit/Signal/Delayed.hs index 4c396a1b94..62b8f0d162 100644 --- a/clash-prelude/src/Clash/Explicit/Signal/Delayed.hs +++ b/clash-prelude/src/Clash/Explicit/Signal/Delayed.hs @@ -27,7 +27,7 @@ module Clash.Explicit.Signal.Delayed -- * Signal \<-\> DSignal conversion , fromSignal , toSignal - -- * List \<-\> DSignal conversion (not synthesisable) + -- * List \<-\> DSignal conversion (not synthesizable) , dfromList -- ** lazy versions , dfromList_lazy @@ -48,7 +48,7 @@ import Clash.Signal.Delayed.Internal unsafeFromSignal, antiDelay, feedback) import Clash.Explicit.Signal - (Clock, Reset, Signal, register, bundle, unbundle) + (KnownDomain, Clock, Reset, Signal, register, bundle, unbundle) import Clash.XException (Undefined) @@ -59,7 +59,7 @@ import Clash.XException (Undefined) >>> let delay3 clk rst = delayed clk rst (-1 :> -1 :> -1 :> Nil) >>> let delay2 clk rst = (delayedI clk rst :: Int -> DSignal System n Int -> DSignal System (n + 2) Int) >>> :{ -let mac :: Clock System gated +let mac :: Clock System enabled -> Reset System synchronous -> DSignal System 0 Int -> DSignal System 0 Int -> DSignal System 0 Int @@ -79,28 +79,29 @@ let mac :: Clock System gated -- -- @ -- delay3 --- :: Clock domain gated --- -> Reset domain synchronous --- -> 'DSignal' domain n Int --- -> 'DSignal' domain (n + 3) Int +-- :: Clock tag enabled +-- -> Reset tag polarity +-- -> 'DSignal' tag n Int +-- -> 'DSignal' tag (n + 3) Int -- delay3 clk rst = 'delayed' clk rst (-1 ':>' -1 ':>' -1 ':>' 'Nil') -- @ -- --- >>> sampleN 7 (delay3 systemClockGen asyncResetGen (dfromList [0..])) +-- >>> sampleN 7 (delay3 systemClockGen resetGen (dfromList [0..])) -- [-1,-1,-1,-1,1,2,3] delayed - :: forall domain gated synchronous a n d - . KnownNat d - => Undefined a - => Clock domain gated - -> Reset domain synchronous + :: forall tag dom enabled polarity a n d + . ( KnownDomain tag dom + , KnownNat d + , Undefined a ) + => Clock tag enabled + -> Reset tag polarity -> Vec d a -- ^ Default values - -> DSignal domain n a - -> DSignal domain (n + d) a + -> DSignal tag n a + -> DSignal tag (n + d) a delayed clk rst m ds = coerce (delaySignal (coerce ds)) where - delaySignal :: Signal domain a -> Signal domain a + delaySignal :: Signal tag a -> Signal tag a delaySignal s = case length m of 0 -> s _ -> let (r',o) = shiftInAt0 (unbundle r) (singleton s) @@ -112,34 +113,35 @@ delayed clk rst m ds = coerce (delaySignal (coerce ds)) -- -- @ -- delay2 --- :: Clock domain gated --- -> Reset domain synchronous +-- :: Clock tag enabled +-- -> Reset tag polarity -- -> Int --- -> 'DSignal' domain n Int --- -> 'DSignal' domain (n + 2) Int +-- -> 'DSignal' tag n Int +-- -> 'DSignal' tag (n + 2) Int -- delay2 = 'delayedI' -- @ -- --- >>> sampleN 7 (delay2 systemClockGen asyncResetGen (-1) (dfromList ([0..]))) +-- >>> sampleN 7 (delay2 systemClockGen resetGen (-1) (dfromList ([0..]))) -- [-1,-1,-1,1,2,3,4] -- -- @d@ can also be specified using type application: -- -- >>> :t delayedI @3 -- delayedI @3 --- :: Undefined a => --- Clock domain gated --- -> Reset domain synchronous +-- :: ... => +-- Clock tag enabled +-- -> Reset tag polarity -- -> a --- -> DSignal domain n a --- -> DSignal domain (n + 3) a +-- -> DSignal tag n a +-- -> DSignal tag (n + 3) a delayedI - :: KnownNat d - => Undefined a - => Clock domain gated - -> Reset domain synchronous + :: ( KnownNat d + , KnownDomain tag dom + , Undefined a ) + => Clock tag enabled + -> Reset tag polarity -> a -- ^ Default value - -> DSignal domain n a - -> DSignal domain (n + d) a + -> DSignal tag n a + -> DSignal tag (n + d) a delayedI clk rst dflt = delayed clk rst (repeat dflt) diff --git a/clash-prelude/src/Clash/Explicit/Synchronizer.hs b/clash-prelude/src/Clash/Explicit/Synchronizer.hs index 3ef3180730..018f104a45 100644 --- a/clash-prelude/src/Clash/Explicit/Synchronizer.hs +++ b/clash-prelude/src/Clash/Explicit/Synchronizer.hs @@ -5,7 +5,7 @@ Copyright : (C) 2015-2016, University of Twente, License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij -Synchronizer circuits for safe clock domain crossings +Synchronizer circuits for safe clock tag crossings -} {-# LANGUAGE CPP #-} @@ -45,18 +45,18 @@ import Clash.Explicit.Signal (Clock, Reset, Signal, register, unsafeSynchronizer) import Clash.Promoted.Nat (SNat (..), pow2SNat) import Clash.Promoted.Nat.Literals (d0) -import Clash.Signal (mux) +import Clash.Signal (mux, KnownDomain) import Clash.Sized.BitVector (BitVector, (++#)) import Clash.XException (Undefined) -- * Dual flip-flop synchronizer --- | Synchroniser based on two sequentially connected flip-flops. +-- | Synchronizer based on two sequentially connected flip-flops. -- --- * __NB__: This synchroniser can be used for __bit__-synchronization. +-- * __NB__: This synchronizer can be used for __bit__-synchronization. -- --- * __NB__: Although this synchroniser does reduce metastability, it does --- not guarantee the proper synchronisation of a whole __word__. For +-- * __NB__: Although this synchronizer does reduce metastability, it does +-- not guarantee the proper synchronization of a whole __word__. For -- example, given that the output is sampled twice as fast as the input is -- running, and we have two samples in the input stream that look like: -- @@ -71,33 +71,37 @@ import Clash.XException (Undefined) -- Where the level-change of the __msb__ was not captured, but the level -- change of the __lsb__s were. -- --- If you want to have /safe/ __word__-synchronisation use +-- If you want to have /safe/ __word__-synchronization use -- 'asyncFIFOSynchronizer'. dualFlipFlopSynchronizer - :: Undefined a - => Clock domain1 gated1 - -- ^ 'Clock' to which the incoming data is synchronised - -> Clock domain2 gated2 - -- ^ 'Clock' to which the outgoing data is synchronised - -> Reset domain2 synchronous + :: ( Undefined a + , KnownDomain tag1 conf1 + , KnownDomain tag2 conf2 ) + => Clock tag1 enabled1 + -- ^ 'Clock' to which the incoming data is synchronized + -> Clock tag2 enabled2 + -- ^ 'Clock' to which the outgoing data is synchronized + -> Reset tag2 polarity -- ^ 'Reset' for registers on the outgoing domain -> a - -- ^ Initial value of the two synchronisation registers - -> Signal domain1 a -- ^ Incoming data - -> Signal domain2 a -- ^ Outgoing, synchronised, data + -- ^ Initial value of the two synchronization registers + -> Signal tag1 a -- ^ Incoming data + -> Signal tag2 a -- ^ Outgoing, synchronized, data dualFlipFlopSynchronizer clk1 clk2 rst i = register clk2 rst i . register clk2 rst i . unsafeSynchronizer clk1 clk2 -- * Asynchronous FIFO synchronizer fifoMem - :: Clock wdomain wgated - -> Clock rdomain rgated + :: ( KnownDomain wtag conf1 + , KnownDomain rtag conf2 ) + => Clock wtag wenabled + -> Clock rtag renabled -> SNat addrSize - -> Signal wdomain Bool - -> Signal rdomain (BitVector addrSize) - -> Signal wdomain (Maybe (BitVector addrSize, a)) - -> Signal rdomain a + -> Signal wtag Bool + -> Signal rtag (BitVector addrSize) + -> Signal wtag (Maybe (BitVector addrSize, a)) + -> Signal rtag a fifoMem wclk rclk addrSize@SNat full raddr writeM = asyncRam wclk rclk (pow2SNat addrSize) @@ -133,27 +137,29 @@ isFull addrSize@SNat ptr s_ptr = case leTrans @1 @2 @addrSize of a2 = SNat @(addrSize - 2) in ptr == (complement (slice addrSize a1 s_ptr) ++# slice a2 d0 s_ptr) --- | Synchroniser implemented as a FIFO around an asynchronous RAM. Based on the +-- | Synchronizer implemented as a FIFO around an asynchronous RAM. Based on the -- design described in "Clash.Tutorial#multiclock", which is itself based on the -- design described in . -- --- __NB__: This synchroniser can be used for __word__-synchronization. +-- __NB__: This synchronizer can be used for __word__-synchronization. asyncFIFOSynchronizer - :: (2 <= addrSize) + :: ( KnownDomain wtag wconf + , KnownDomain rtag rconf + , 2 <= addrSize ) => SNat addrSize -- ^ Size of the internally used addresses, the FIFO contains @2^addrSize@ -- elements. - -> Clock wdomain wgated - -- ^ 'Clock' to which the write port is synchronised - -> Clock rdomain rgated - -- ^ 'Clock' to which the read port is synchronised - -> Reset wdomain synchronous - -> Reset rdomain synchronous - -> Signal rdomain Bool + -> Clock wtag wenabled + -- ^ 'Clock' to which the write port is synchronized + -> Clock rtag renabled + -- ^ 'Clock' to which the read port is synchronized + -> Reset wtag polarity + -> Reset rtag polarity + -> Signal rtag Bool -- ^ Read request - -> Signal wdomain (Maybe a) + -> Signal wtag (Maybe a) -- ^ Element to insert - -> (Signal rdomain a, Signal rdomain Bool, Signal wdomain Bool) + -> (Signal rtag a, Signal rtag Bool, Signal wtag Bool) -- ^ (Oldest element in the FIFO, @empty@ flag, @full@ flag) asyncFIFOSynchronizer addrSize@SNat wclk rclk wrst rrst rinc wdataM = (rdata,rempty,wfull) diff --git a/clash-prelude/src/Clash/Explicit/Testbench.hs b/clash-prelude/src/Clash/Explicit/Testbench.hs index 4a318f503f..19e2b5882f 100644 --- a/clash-prelude/src/Clash/Explicit/Testbench.hs +++ b/clash-prelude/src/Clash/Explicit/Testbench.hs @@ -28,7 +28,7 @@ import System.IO.Unsafe (unsafeDupablePerformIO) import Clash.Explicit.Signal (Clock, Reset, Signal, fromList, register, unbundle) -import Clash.Signal (mux) +import Clash.Signal (mux, KnownDomain) import Clash.Sized.Index (Index) import Clash.Sized.Internal.BitVector (BitVector, isLike) @@ -51,25 +51,21 @@ import Clash.XException (ShowX (..), XException) -- __NB__: This function /can/ be used in synthesizable designs. assert :: (Eq a,ShowX a) - => Clock domain gated - -> Reset domain synchronous + => Clock tag enabled + -> Reset tag polarity -> String -- ^ Additional message - -> Signal domain a -- ^ Checked value - -> Signal domain a -- ^ Expected value - -> Signal domain b -- ^ Return value - -> Signal domain b + -> Signal tag a -- ^ Checked value + -> Signal tag a -- ^ Expected value + -> Signal tag b -- ^ Return value + -> Signal tag b assert clk _rst msg checked expected returned = (\c e cnt r -> if eqX c e then r - else trace (concat [ "\ncycle(" ++ show clk ++ "): " - , show cnt - , ", " - , msg - , "\nexpected value: " - , showX e - , ", not equal to actual value: " - , showX c + else trace (concat [ "\nOn cycle ", show cnt, " of ", show clk, ", " + , msg, " encountered an unexpected value:\n" + , " Expected: ", showX e, "\n" + , " Actual: ", showX c ]) r) <$> checked <*> expected <*> fromList [(0::Integer)..] <*> returned where @@ -80,13 +76,13 @@ assert clk _rst msg checked expected returned = -- | The same as 'assert', but can handle don't care bits in it's expected value. assertBitVector :: (KnownNat n) - => Clock domain gated - -> Reset domain synchronous + => Clock tag enabled + -> Reset tag polarity -> String -- ^ Additional message - -> Signal domain (BitVector n) -- ^ Checked value - -> Signal domain (BitVector n) -- ^ Expected value - -> Signal domain b -- ^ Return value - -> Signal domain b + -> Signal tag (BitVector n) -- ^ Checked value + -> Signal tag (BitVector n) -- ^ Expected value + -> Signal tag b -- ^ Return value + -> Signal tag b assertBitVector clk _rst msg checked expected returned = (\c e cnt r -> if eqX c e @@ -116,21 +112,26 @@ assertBitVector clk _rst msg checked expected returned = -- -- @ -- testInput --- :: Clock domain gated -> Reset domain synchronous --- -> 'Signal' domain Int +-- :: KnownDomain tag dom +-- => Clock tag enabled +-- -> Reset tag polarity +-- -> 'Signal' tag Int -- testInput clk rst = 'stimuliGenerator' clk rst $('Clash.Sized.Vector.listToVecTH' [(1::Int),3..21]) -- @ -- --- >>> sampleN 14 (testInput systemClockGen asyncResetGen) +-- >>> sampleN 14 (testInput systemClockGen resetGen) -- [1,1,3,5,7,9,11,13,15,17,19,21,21,21] stimuliGenerator - :: forall l domain gated synchronous a - . KnownNat l - => Clock domain gated + :: forall l tag dom enabled polarity a + . ( KnownNat l + , KnownDomain tag dom ) + => Clock tag enabled -- ^ Clock to which to synchronize the output signal - -> Reset domain synchronous - -> Vec l a -- ^ Samples to generate - -> Signal domain a -- ^ Signal of given samples + -> Reset tag polarity + -> Vec l a + -- ^ Samples to generate + -> Signal tag a + -- ^ Signal of given samples stimuliGenerator clk rst samples = let (r,o) = unbundle (genT <$> register clk rst 0 r) in o @@ -153,46 +154,56 @@ stimuliGenerator clk rst samples = -- -- @ -- expectedOutput --- :: Clock domain gated -> Reset domain synchronous --- -> 'Signal' domain Int -> 'Signal' domain Bool +-- :: Clock tag enabled -> Reset tag polarity +-- -> 'Signal' tag Int -> 'Signal' tag Bool -- expectedOutput clk rst = 'outputVerifier' clk rst $('Clash.Sized.Vector.listToVecTH' ([70,99,2,3,4,5,7,8,9,10]::[Int])) -- @ -- -- >>> import qualified Data.List as List --- >>> sampleN 12 (expectedOutput systemClockGen asyncResetGen (fromList (0:[0..10] List.++ [10,10,10]))) +-- >>> sampleN 12 (expectedOutput systemClockGen resetGen (fromList (0:[0..10] List.++ [10,10,10]))) -- --- cycle(system10000): 0, outputVerifier --- expected value: 70, not equal to actual value: 0 +-- On cycle 0 of , outputVerifier encountered an unexpected value: +-- Expected: 70 +-- Actual: 0 -- [False --- cycle(system10000): 1, outputVerifier --- expected value: 70, not equal to actual value: 0 +-- On cycle 1 of , outputVerifier encountered an unexpected value: +-- Expected: 70 +-- Actual: 0 -- ,False --- cycle(system10000): 2, outputVerifier --- expected value: 99, not equal to actual value: 1 +-- On cycle 2 of , outputVerifier encountered an unexpected value: +-- Expected: 99 +-- Actual: 1 -- ,False,False,False,False,False --- cycle(system10000): 7, outputVerifier --- expected value: 7, not equal to actual value: 6 +-- On cycle 7 of , outputVerifier encountered an unexpected value: +-- Expected: 7 +-- Actual: 6 -- ,False --- cycle(system10000): 8, outputVerifier --- expected value: 8, not equal to actual value: 7 +-- On cycle 8 of , outputVerifier encountered an unexpected value: +-- Expected: 8 +-- Actual: 7 -- ,False --- cycle(system10000): 9, outputVerifier --- expected value: 9, not equal to actual value: 8 +-- On cycle 9 of , outputVerifier encountered an unexpected value: +-- Expected: 9 +-- Actual: 8 -- ,False --- cycle(system10000): 10, outputVerifier --- expected value: 10, not equal to actual value: 9 +-- On cycle 10 of , outputVerifier encountered an unexpected value: +-- Expected: 10 +-- Actual: 9 -- ,False,True] -- -- If your working with 'BitVector's containing don't care bit you should use 'outputVerifierBitVector'. outputVerifier - :: forall l domain gated synchronous a - . (KnownNat l, Eq a, ShowX a) - => Clock domain gated + :: forall l tag dom enabled polarity a + . ( KnownNat l + , KnownDomain tag dom + , Eq a + , ShowX a ) + => Clock tag enabled -- ^ Clock to which the input signal is synchronized to - -> Reset domain synchronous + -> Reset tag polarity -> Vec l a -- ^ Samples to compare with - -> Signal domain a -- ^ Signal to verify - -> Signal domain Bool -- ^ Indicator that all samples are verified + -> Signal tag a -- ^ Signal to verify + -> Signal tag Bool -- ^ Indicator that all samples are verified outputVerifier clk rst samples i = let (s,o) = unbundle (genT <$> register clk rst 0 s) (e,f) = unbundle o @@ -215,14 +226,17 @@ outputVerifier clk rst samples i = -- | Same as 'outputVerifier', -- but can handle don't care bits in it's expected values. outputVerifierBitVector - :: forall l n domain gated synchronous - . (KnownNat l, KnownNat n) - => Clock domain gated + :: forall l n tag dom enabled polarity + . ( KnownNat l + , KnownNat n + , KnownDomain tag dom + ) + => Clock tag enabled -- ^ Clock to which the input signal is synchronized to - -> Reset domain synchronous + -> Reset tag polarity -> Vec l (BitVector n) -- ^ Samples to compare with - -> Signal domain (BitVector n) -- ^ Signal to verify - -> Signal domain Bool -- ^ Indicator that all samples are verified + -> Signal tag (BitVector n) -- ^ Signal to verify + -> Signal tag Bool -- ^ Indicator that all samples are verified outputVerifierBitVector clk rst samples i = let (s,o) = unbundle (genT <$> register clk rst 0 s) (e,f) = unbundle o diff --git a/clash-prelude/src/Clash/Intel/ClockGen.hs b/clash-prelude/src/Clash/Intel/ClockGen.hs index 7e313cd4e5..a9d23f8253 100644 --- a/clash-prelude/src/Clash/Intel/ClockGen.hs +++ b/clash-prelude/src/Clash/Intel/ClockGen.hs @@ -7,6 +7,7 @@ PLL and other clock-related components for Intel (Altera) FPGAs -} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ExplicitForAll #-} module Clash.Intel.ClockGen @@ -17,7 +18,8 @@ module Clash.Intel.ClockGen import Clash.Clocks (clocks, Clocks) import Clash.Promoted.Symbol (SSymbol) import Clash.Signal.Internal - (Signal, ClockKind(..), Clock, Reset, ResetKind(..) ) + (Signal, ClockKind(..), Clock, Reset, ResetKind(..), + ResetPolarity(ActiveHigh), KnownDomain, Domain(..)) -- | A clock source that corresponds to the Intel/Quartus \"ALTPLL\" component @@ -38,20 +40,23 @@ import Clash.Signal.Internal -- -- outputs a clock running at 100 MHz -- altpll @@Dom100MHz (SSymbol @@"altpll50to100") clk50 rst -- @ +-- TODO: Docs altpll - :: forall pllOut pllIn name - . SSymbol name + :: forall tagIn tagOut periodIn periodOut edge init name + . ( KnownDomain tagIn ('Domain tagIn periodIn edge 'Asynchronous init) + , KnownDomain tagOut ('Domain tagOut periodOut edge 'Asynchronous init) ) + => SSymbol name -- ^ Name of the component, must correspond to the name entered in the QSys -- dialog. -- -- For example, when you entered \"altPLL50\", instantiate as follows: -- -- > SSymbol @ "altPLL50" - -> Clock pllIn 'Source + -> Clock tagIn 'Regular -- ^ Free running clock (i.e. a clock pin connected to a crystal) - -> Reset pllIn 'Asynchronous + -> Reset tagIn 'ActiveHigh -- ^ Reset for the PLL - -> (Clock pllOut 'Source, Signal pllOut Bool) + -> (Clock tagOut 'Regular, Signal tagOut Bool) -- ^ (Stable PLL clock, PLL lock) altpll _ = clocks {-# NOINLINE altpll #-} @@ -90,6 +95,7 @@ altpll _ = clocks -- @ -- -- respectively. +-- TODO: Docs alteraPll :: Clocks t => SSymbol name @@ -99,9 +105,9 @@ alteraPll -- For example, when you entered \"alteraPLL50\", instantiate as follows: -- -- > SSymbol @ "alteraPLL50" - -> Clock pllIn 'Source + -> Clock tagIn 'Regular -- ^ Free running clock (i.e. a clock pin connected to a crystal) - -> Reset pllIn 'Asynchronous + -> Reset tagIn 'ActiveHigh -- ^ Reset for the PLL -> t alteraPll _ = clocks diff --git a/clash-prelude/src/Clash/Intel/DDR.hs b/clash-prelude/src/Clash/Intel/DDR.hs index 5841a35167..98e8eead07 100644 --- a/clash-prelude/src/Clash/Intel/DDR.hs +++ b/clash-prelude/src/Clash/Intel/DDR.hs @@ -7,7 +7,7 @@ DDR primitives for Intel FPGAs using ALTDDIO primitives. For general information about DDR primitives see "Clash.Explicit.DDR". -Note that a synchronous reset is only available on certain devices, +Note that a polarity reset is only available on certain devices, see ALTDDIO userguide for the specifics: https://www.altera.com/content/dam/altera-www/global/en_US/pdfs/literature/ug/ug_altddio.pdf -} @@ -38,8 +38,8 @@ import Clash.Explicit.DDR -- Reset values are @0@ altddioIn :: ( HasCallStack - , fast ~ 'Dom n pFast - , slow ~ 'Dom n (2*pFast) + , KnownDomain fast ('Domain fast fPeriod edge reset init) + , KnownDomain slow ('Domain slow (2*fPeriod) edge reset init) , KnownNat m ) => SSymbol deviceFamily -- ^ The FPGA family @@ -47,9 +47,9 @@ altddioIn -- For example this can be instantiated as follows: -- -- > SSymbol @"Cyclone IV GX" - -> Clock slow gated + -> Clock slow enabled -- ^ clock - -> Reset slow synchronous + -> Reset slow polarity -- ^ reset -> Signal fast (BitVector m) -- ^ DDR input signal @@ -63,8 +63,8 @@ altddioIn _devFam clk rst = withFrozenCallStack ddrIn# clk rst 0 0 0 -- Reset value is @0@ altddioOut :: ( HasCallStack - , fast ~ 'Dom n pFast - , slow ~ 'Dom n (2*pFast) + , KnownDomain fast ('Domain fast fPeriod edge reset init) + , KnownDomain slow ('Domain slow (2*fPeriod) edge reset init) , KnownNat m ) => SSymbol deviceFamily -- ^ The FPGA family @@ -72,9 +72,9 @@ altddioOut -- For example this can be instantiated as follows: -- -- > SSymbol @"Cyclone IV E" - -> Clock slow gated + -> Clock slow enabled -- ^ clock - -> Reset slow synchronous + -> Reset slow polarity -- ^ reset -> Signal slow (BitVector m,BitVector m) -- ^ normal speed input pair @@ -85,12 +85,12 @@ altddioOut devFam clk rst = altddioOut# :: ( HasCallStack - , fast ~ 'Dom n pFast - , slow ~ 'Dom n (2*pFast) + , KnownDomain fast ('Domain fast fPeriod edge reset init) + , KnownDomain slow ('Domain slow (2*fPeriod) edge reset init) , KnownNat m ) => SSymbol deviceFamily - -> Clock slow gated - -> Reset slow synchronous + -> Clock slow enabled + -> Reset slow polarity -> Signal slow (BitVector m) -> Signal slow (BitVector m) -> Signal fast (BitVector m) diff --git a/clash-prelude/src/Clash/Prelude.hs b/clash-prelude/src/Clash/Prelude.hs index 8b56740ef9..79bbb164f2 100644 --- a/clash-prelude/src/Clash/Prelude.hs +++ b/clash-prelude/src/Clash/Prelude.hs @@ -7,7 +7,7 @@ Clash is a functional hardware description language that borrows both its syntax and semantics from the functional programming language Haskell. The merits of using a functional language to describe hardware comes from the fact - that combinational circuits can be directly modeled as mathematical functions + that combinatorial circuits can be directly modeled as mathematical functions and that functional languages lend themselves very well at describing and (de-)composing mathematical functions. @@ -41,7 +41,7 @@ {-# OPTIONS_HADDOCK show-extensions #-} module Clash.Prelude - ( -- * Creating synchronous sequential circuits + ( -- * Creating polarity sequential circuits mealy , mealyB , (<^>) @@ -185,9 +185,9 @@ import Clash.Signal.Trace import Clash.XException {- $setup ->>> :set -XDataKinds -XFlexibleContexts ->>> let window4 = window :: HiddenClockReset domain gated synchronous => Signal domain Int -> Vec 4 (Signal domain Int) ->>> let windowD3 = windowD :: HiddenClockReset domain gated synchronous => Signal domain Int -> Vec 3 (Signal domain Int) +>>> :set -XDataKinds -XFlexibleContexts -XTypeApplications +>>> let window4 = window :: HiddenClockReset tag enabled polarity dom => Signal tag Int -> Vec 4 (Signal tag Int) +>>> let windowD3 = windowD :: HiddenClockReset tag enabled polarity dom => Signal tag Int -> Vec 3 (Signal tag Int) -} {- $hiding @@ -203,38 +203,42 @@ It instead exports the identically named functions defined in terms of -- | Give a window over a 'Signal' -- --- > window4 :: HiddenClockReset domain gated synchronous --- > => Signal domain Int -> Vec 4 (Signal domain Int) +-- > window4 :: HiddenClockReset tag enabled polarity dom +-- > => Signal tag Int -> Vec 4 (Signal tag Int) -- > window4 = window -- --- >>> simulateB window4 [1::Int,2,3,4,5] :: [Vec 4 Int] +-- >>> simulateB @System window4 [1::Int,2,3,4,5] :: [Vec 4 Int] -- [<1,0,0,0>,<2,1,0,0>,<3,2,1,0>,<4,3,2,1>,<5,4,3,2>... -- ... window - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , KnownNat n , Default a , Undefined a ) - => Signal domain a -- ^ Signal to create a window over - -> Vec (n + 1) (Signal domain a) -- ^ Window of at least size 1 + => Signal tag a + -- ^ Signal to create a window over + -> Vec (n + 1) (Signal tag a) + -- ^ Window of at least size 1 window = hideClockReset E.window {-# INLINE window #-} -- | Give a delayed window over a 'Signal' -- --- > windowD3 :: HiddenClockReset domain gated synchronous --- > => Signal domain Int -> Vec 3 (Signal domain Int) +-- > windowD3 :: HiddenClockReset tag enabled polarity dom +-- > => Signal tag Int -> Vec 3 (Signal tag Int) -- > windowD3 = windowD -- --- >>> simulateB windowD3 [1::Int,2,3,4] :: [Vec 3 Int] +-- >>> simulateB @System windowD3 [1::Int,2,3,4] :: [Vec 3 Int] -- [<0,0,0>,<1,0,0>,<2,1,0>,<3,2,1>,<4,3,2>... -- ... windowD - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , KnownNat n , Default a , Undefined a ) - => Signal domain a -- ^ Signal to create a window over - -> Vec (n + 1) (Signal domain a) -- ^ Window of at least size 1 + => Signal tag a + -- ^ Signal to create a window over + -> Vec (n + 1) (Signal tag a) + -- ^ Window of at least size 1 windowD = hideClockReset E.windowD {-# INLINE windowD #-} diff --git a/clash-prelude/src/Clash/Prelude/BlockRam.hs b/clash-prelude/src/Clash/Prelude/BlockRam.hs index 9839a2f02b..caadcdf5a3 100644 --- a/clash-prelude/src/Clash/Prelude/BlockRam.hs +++ b/clash-prelude/src/Clash/Prelude/BlockRam.hs @@ -18,7 +18,7 @@ We start with the definition of the Instructions, Register names and machine codes: @ -{\-\# LANGUAGE RecordWildCards, TupleSections, DeriveAnyClass \#-\} +{\-\# LANGUAGE RecordWildCards, TupleSections, DeriveAnyClass, TypeApplications \#-\} module CPU where import Clash.Prelude @@ -116,10 +116,10 @@ alu CmpGt x y = if x > y then 1 else 0 We initially create a memory out of simple registers: @ -dataMem :: HiddenClockReset domain gated synchronous - => Signal domain MemAddr -- ^ Read address - -> Signal domain (Maybe (MemAddr,Value)) -- ^ (write address, data in) - -> Signal domain Value -- ^ data out +dataMem :: HiddenClockReset tag enabled polarity dom + => Signal tag MemAddr -- ^ Read address + -> Signal tag (Maybe (MemAddr,Value)) -- ^ (write address, data in) + -> Signal tag Value -- ^ data out dataMem rd wrM = 'Clash.Prelude.Mealy.mealy' dataMemT ('replicate' d32 0) (bundle (rd,wrM)) where dataMemT mem (rd,wrM) = (mem',dout) @@ -133,7 +133,7 @@ dataMem rd wrM = 'Clash.Prelude.Mealy.mealy' dataMemT ('replicate' d32 0) (bundl And then connect everything: @ -system :: (KnownNat n, HiddenClockReset domain gated synchronous) => Vec n Instruction -> Signal domain Value +system :: (KnownNat n, HiddenClockReset tag enabled polarity dom) => Vec n Instruction -> Signal tag Value system instrs = memOut where memOut = dataMem rdAddr dout @@ -178,7 +178,7 @@ prog = -- 0 := 4 And test our system: @ ->>> sampleN 32 (system prog) +>>> sampleN @System 32 (system prog) [0,0,0,0,0,0,4,4,4,4,4,4,4,4,6,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,2] @ @@ -195,7 +195,7 @@ Instead it is preferable to use the 'Clash.Prelude.RAM.asyncRam' function which has the potential to be translated to a more efficient structure: @ -system2 :: (KnownNat n, HiddenClockReset domain gated synchronous) => Vec n Instruction -> Signal domain Value +system2 :: (KnownNat n, HiddenClockReset tag enabled polarity dom) => Vec n Instruction -> Signal tag Value system2 instrs = memOut where memOut = 'Clash.Prelude.RAM.asyncRam' d32 rdAddr dout @@ -210,7 +210,7 @@ output samples are also 'undefined'. We use the utility function 'printX' to con filter out the undefinedness and replace it with the string "X" in the few leading outputs. @ ->>> printX $ sampleN 32 (system2 prog) +>>> printX $ sampleN @System 32 (system2 prog) [X,X,X,X,X,X,4,4,4,4,4,4,4,4,6,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,2] @ @@ -277,7 +277,7 @@ cpu2 (regbank,ldRegD) (memOut,instr) = ((regbank',ldRegD'),(rdAddr,(,aluOut) '<$ We can now finally instantiate our system with a 'blockRam': @ -system3 :: (KnownNat n, HiddenClockReset domain gated synchronous) => Vec n Instruction -> Signal domain Value +system3 :: (KnownNat n, HiddenClockReset tag enabled polarity dom) => Vec n Instruction -> Signal tag Value system3 instrs = memOut where memOut = 'blockRam' (replicate d32 0) rdAddr dout @@ -330,7 +330,7 @@ we need to disregard the first sample, because the initial output of a filter out the undefinedness and replace it with the string "X". @ ->>> printX $ sampleN 34 (system3 prog2) +>>> printX $ sampleN @System 34 (system3 prog2) [X,0,0,0,0,0,0,4,4,4,4,4,4,4,4,6,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,2] @ @@ -350,7 +350,7 @@ This concludes the short introduction to using 'blockRam'. {-# OPTIONS_HADDOCK show-extensions #-} module Clash.Prelude.BlockRam - ( -- * BlockRAM synchronised to the system clock + ( -- * BlockRAM synchronized to the system clock blockRam , blockRamPow2 -- * Read/Write conflict resolution @@ -468,10 +468,10 @@ cpu regbank (memOut,instr) = (regbank',(rdAddr,(,aluOut) <$> wrAddrM,fromIntegra >>> :{ dataMem - :: HiddenClockReset domain gated synchronous - => Signal domain MemAddr - -> Signal domain (Maybe (MemAddr,Value)) - -> Signal domain Value + :: HiddenClockReset tag enabled polarity dom + => Signal tag MemAddr + -> Signal tag (Maybe (MemAddr,Value)) + -> Signal tag Value dataMem rd wrM = mealy dataMemT (C.replicate d32 0) (bundle (rd,wrM)) where dataMemT mem (rd,wrM) = (mem',dout) @@ -484,9 +484,9 @@ dataMem rd wrM = mealy dataMemT (C.replicate d32 0) (bundle (rd,wrM)) >>> :{ system - :: (KnownNat n, HiddenClockReset domain gated synchronous) + :: (KnownNat n, HiddenClockReset tag enabled polarity dom) => Vec n Instruction - -> Signal domain Value + -> Signal tag Value system instrs = memOut where memOut = dataMem rdAddr dout @@ -528,9 +528,9 @@ prog = -- 0 := 4 >>> :{ system2 - :: (KnownNat n, HiddenClockReset domain gated synchronous) + :: (KnownNat n, HiddenClockReset tag enabled polarity dom) => Vec n Instruction - -> Signal domain Value + -> Signal tag Value system2 instrs = memOut where memOut = asyncRam d32 rdAddr dout @@ -575,9 +575,9 @@ cpu2 (regbank,ldRegD) (memOut,instr) = ((regbank',ldRegD'),(rdAddr,(,aluOut) <$> >>> :{ system3 - :: (KnownNat n, HiddenClockReset domain gated synchronous) + :: (KnownNat n, HiddenClockReset tag enabled polarity dom) => Vec n Instruction - -> Signal domain Value + -> Signal tag Value system3 instrs = memOut where memOut = blockRam (C.replicate d32 0) rdAddr dout @@ -626,10 +626,10 @@ prog2 = -- 0 := 4 -- -- @ -- bram40 --- :: 'HiddenClock' domain --- => 'Signal' domain ('Unsigned' 6) --- -> 'Signal' domain (Maybe ('Unsigned' 6, 'Clash.Sized.BitVector.Bit')) --- -> 'Signal' domain 'Clash.Sized.BitVector.Bit' +-- :: 'HiddenClock' tag +-- => 'Signal' tag ('Unsigned' 6) +-- -> 'Signal' tag (Maybe ('Unsigned' 6, 'Clash.Sized.BitVector.Bit')) +-- -> 'Signal' tag 'Clash.Sized.BitVector.Bit' -- bram40 = 'blockRam' ('Clash.Sized.Vector.replicate' d40 1) -- @ -- @@ -640,17 +640,17 @@ prog2 = -- 0 := 4 -- * Use the adapter 'readNew' for obtaining write-before-read semantics like this: @readNew (blockRam inits) rd wrM@. blockRam :: HasCallStack - => HiddenClock domain gated + => HiddenClock tag enabled dom => Undefined a => Enum addr => Vec n a -- ^ Initial content of the BRAM, also -- determines the size, @n@, of the BRAM. -- -- __NB__: __MUST__ be a constant. - -> Signal domain addr -- ^ Read address @r@ - -> Signal domain (Maybe (addr, a)) + -> Signal tag addr -- ^ Read address @r@ + -> Signal tag (Maybe (addr, a)) -- ^ (write address @w@, value to write) - -> Signal domain a + -> Signal tag a -- ^ Value of the @blockRAM@ at address @r@ from the previous clock -- cycle blockRam = \cnt rd wrM -> withFrozenCallStack @@ -664,10 +664,10 @@ blockRam = \cnt rd wrM -> withFrozenCallStack -- -- @ -- bram32 --- :: 'HiddenClock' domain --- => 'Signal' domain ('Unsigned' 5) --- -> 'Signal' domain (Maybe ('Unsigned' 5, 'Clash.Sized.BitVector.Bit')) --- -> 'Signal' domain 'Clash.Sized.BitVector.Bit' +-- :: 'HiddenClock' tag +-- => 'Signal' tag ('Unsigned' 5) +-- -> 'Signal' tag (Maybe ('Unsigned' 5, 'Clash.Sized.BitVector.Bit')) +-- -> 'Signal' tag 'Clash.Sized.BitVector.Bit' -- bram32 = 'blockRamPow2' ('Clash.Sized.Vector.replicate' d32 1) -- @ -- @@ -678,43 +678,44 @@ blockRam = \cnt rd wrM -> withFrozenCallStack -- * Use the adapter 'readNew' for obtaining write-before-read semantics like this: @readNew (blockRamPow2 inits) rd wrM@. blockRamPow2 :: HasCallStack - => HiddenClock domain gated + => HiddenClock tag enabled dom => Undefined a => KnownNat n => Vec (2^n) a -- ^ Initial content of the BRAM, also -- determines the size, @2^n@, of the BRAM. -- -- __NB__: __MUST__ be a constant. - -> Signal domain (Unsigned n) -- ^ Read address @r@ - -> Signal domain (Maybe (Unsigned n, a)) + -> Signal tag (Unsigned n) -- ^ Read address @r@ + -> Signal tag (Maybe (Unsigned n, a)) -- ^ (write address @w@, value to write) - -> Signal domain a + -> Signal tag a -- ^ Value of the @blockRAM@ at address @r@ from the previous clock -- cycle blockRamPow2 = \cnt rd wrM -> withFrozenCallStack (hideClock E.blockRamPow2 cnt rd wrM) {-# INLINE blockRamPow2 #-} --- | Create read-after-write blockRAM from a read-before-write one (synchronised to system clock) +-- | Create read-after-write blockRAM from a read-before-write one (synchronized to system clock) -- -- >>> import Clash.Prelude -- >>> :t readNew (blockRam (0 :> 1 :> Nil)) -- readNew (blockRam (0 :> 1 :> Nil)) -- :: ... +-- ... +-- ... -- ... => --- Signal domain addr --- -> Signal domain (Maybe (addr, a)) -> Signal domain a +-- Signal tag addr -> Signal tag (Maybe (addr, a)) -> Signal tag a readNew - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , Undefined a , Eq addr ) - => (Signal domain addr -> Signal domain (Maybe (addr, a)) -> Signal domain a) + => (Signal tag addr -> Signal tag (Maybe (addr, a)) -> Signal tag a) -- ^ The @ram@ component - -> Signal domain addr + -> Signal tag addr -- ^ Read address @r@ - -> Signal domain (Maybe (addr, a)) + -> Signal tag (Maybe (addr, a)) -- ^ (Write address @w@, value to write) - -> Signal domain a + -> Signal tag a -- ^ Value of the @ram@ at address @r@ from the previous clock cycle readNew = hideClockReset (\clk rst -> E.readNew rst clk) {-# INLINE readNew #-} diff --git a/clash-prelude/src/Clash/Prelude/BlockRam/File.hs b/clash-prelude/src/Clash/Prelude/BlockRam/File.hs index b1fc6a91da..ac19cf7f9b 100644 --- a/clash-prelude/src/Clash/Prelude/BlockRam/File.hs +++ b/clash-prelude/src/Clash/Prelude/BlockRam/File.hs @@ -33,7 +33,7 @@ For example, a data file @memory.bin@ containing the 9-bit unsigned number We can instantiate a BlockRAM using the content of the above file like so: @ -f :: HiddenClock domain -> Signal domain (Unsigned 3) -> Signal domain (Unsigned 9) +f :: HiddenClock tag -> Signal tag (Unsigned 3) -> Signal tag (Unsigned 9) f rd = 'Clash.Class.BitPack.unpack' '<$>' exposeClock 'blockRamFile' clk d7 \"memory.bin\" rd (signal Nothing) @ @@ -50,7 +50,7 @@ However, we can also interpret the same data as a tuple of a 6-bit unsigned number, and a 3-bit signed number: @ -g :: HiddenClock domain -> Signal domain (Unsigned 3) -> Signal domain (Unsigned 6,Signed 3) +g :: HiddenClock tag -> Signal tag (Unsigned 3) -> Signal tag (Unsigned 6,Signed 3) g clk rd = 'Clash.Class.BitPack.unpack' '<$>' exposeClock 'blockRamFile' clk d7 \"memory.bin\" rd (signal Nothing) @ @@ -78,7 +78,7 @@ __>>> L.tail $ sampleN 4 $ g (fromList [3..5])__ {-# OPTIONS_HADDOCK show-extensions #-} module Clash.Prelude.BlockRam.File - ( -- * BlockRAM synchronised to an arbitrary clock + ( -- * BlockRAM synchronized to an arbitrary clock blockRamFile , blockRamFilePow2 ) @@ -121,15 +121,15 @@ import Clash.Sized.Unsigned (Unsigned) -- * See "Clash.Sized.Fixed#creatingdatafiles" for ideas on how to create your -- own data files. blockRamFilePow2 - :: forall domain gated n m - . (KnownNat m, KnownNat n, HiddenClock domain gated, HasCallStack) + :: forall tag gated dom n m + . (KnownNat m, KnownNat n, HiddenClock tag gated dom, HasCallStack) => FilePath -- ^ File describing the initial content of the blockRAM - -> Signal domain (Unsigned n) + -> Signal tag (Unsigned n) -- ^ Read address @r@ - -> Signal domain (Maybe (Unsigned n, BitVector m)) + -> Signal tag (Maybe (Unsigned n, BitVector m)) -- ^ (write address @w@, value to write) - -> Signal domain (BitVector m) + -> Signal tag (BitVector m) -- ^ Value of the @blockRAM@ at address @r@ from the previous -- clock cycle blockRamFilePow2 = \fp rd wrM -> withFrozenCallStack @@ -163,16 +163,16 @@ blockRamFilePow2 = \fp rd wrM -> withFrozenCallStack -- * See "Clash.Sized.Fixed#creatingdatafiles" for ideas on how to create your -- own data files. blockRamFile - :: (KnownNat m, Enum addr, HiddenClock domain gated, HasCallStack) + :: (KnownNat m, Enum addr, HiddenClock tag gated dom, HasCallStack) => SNat n -- ^ Size of the blockRAM -> FilePath -- ^ File describing the initial content of the blockRAM - -> Signal domain addr + -> Signal tag addr -- ^ Read address @r@ - -> Signal domain (Maybe (addr, BitVector m)) + -> Signal tag (Maybe (addr, BitVector m)) -- ^ (write address @w@, value to write) - -> Signal domain (BitVector m) + -> Signal tag (BitVector m) -- ^ Value of the @blockRAM@ at address @r@ from the previous -- clock cycle blockRamFile = \sz fp rd wrM -> withFrozenCallStack diff --git a/clash-prelude/src/Clash/Prelude/DataFlow.hs b/clash-prelude/src/Clash/Prelude/DataFlow.hs index 4b47302aa5..33f392a64b 100644 --- a/clash-prelude/src/Clash/Prelude/DataFlow.hs +++ b/clash-prelude/src/Clash/Prelude/DataFlow.hs @@ -54,15 +54,15 @@ import Clash.Class.Resize (truncateB) import Clash.Prelude.BitIndex (msb) import Clash.Explicit.Mealy (mealyB) import Clash.Promoted.Nat (SNat) -import Clash.Signal ((.&&.), unbundle) +import Clash.Signal (KnownDomain, (.&&.), unbundle) import Clash.Signal.Bundle (Bundle (..)) -import Clash.Signal.Internal (clockGate) +import Clash.Signal.Internal (toEnabledClock) import Clash.Explicit.Signal (Clock, Reset, Signal, register) import Clash.Sized.BitVector (BitVector) import Clash.Sized.Vector import Clash.XException (errorX, Undefined) -{- | Dataflow circuit with bidirectional synchronisation channels. +{- | Dataflow circuit with bidirectional synchronization channels. In the /forward/ direction we assert /validity/ of the data. In the /backward/ direction we assert that the circuit is /ready/ to receive new data. A circuit @@ -74,23 +74,23 @@ adhering to the 'DataFlow' type should: The 'DataFlow'' type is defined as: @ -newtype DataFlow' dom iEn oEn i o +newtype DataFlow' tag iEn oEn i o = DF - { df :: 'Signal'' dom i -- Incoming data - -> 'Signal'' dom iEn -- Flagged with /valid/ bits @iEn@. - -> 'Signal'' dom oEn -- Incoming back-pressure, /ready/ edge. - -> ( 'Signal'' dom o -- Outgoing data. - , 'Signal'' dom oEn -- Flagged with /valid/ bits @oEn@. - , 'Signal'' dom iEn -- Outgoing back-pressure, /ready/ edge. + { df :: 'Signal'' tag i -- Incoming data + -> 'Signal'' tag iEn -- Flagged with /valid/ bits @iEn@. + -> 'Signal'' tag oEn -- Incoming back-pressure, /ready/ edge. + -> ( 'Signal'' tag o -- Outgoing data. + , 'Signal'' tag oEn -- Flagged with /valid/ bits @oEn@. + , 'Signal'' tag iEn -- Outgoing back-pressure, /ready/ edge. ) } @ where: - * @dom@ is the clock to which the circuit is synchronised. - * @iEn@ is the type of the bidirectional incoming synchronisation channel. - * @oEn@ is the type of the bidirectional outgoing synchronisation channel. + * @tag@ is the domain to which the circuit is synchronized. + * @iEn@ is the type of the bidirectional incoming synchronization channel. + * @oEn@ is the type of the bidirectional outgoing synchronization channel. * @i@ is the incoming data type. * @o@ is the outgoing data type. @@ -102,33 +102,33 @@ We define several composition operators for our 'DataFlow' circuits: * 'lockStep' proceed in lock-step. When you look at the types of the above operators it becomes clear why we -parametrise in the types of the synchronisation channels. +parametrise in the types of the synchronization channels. -} -newtype DataFlow domain iEn oEn i o +newtype DataFlow tag iEn oEn i o = DF { -- | Create an ordinary circuit from a 'DataFlow' circuit - df :: Signal domain i -- Incoming data - -> Signal domain iEn -- Flagged with /valid/ bits @iEn@. - -> Signal domain oEn -- Incoming back-pressure, /ready/ edge. - -> ( Signal domain o -- Outgoing data. - , Signal domain oEn -- Flagged with /valid/ bits @oEn@. - , Signal domain iEn -- Outgoing back-pressure, /ready/ edge. + df :: Signal tag i -- Incoming data + -> Signal tag iEn -- Flagged with /valid/ bits @iEn@. + -> Signal tag oEn -- Incoming back-pressure, /ready/ edge. + -> ( Signal tag o -- Outgoing data. + , Signal tag oEn -- Flagged with /valid/ bits @oEn@. + , Signal tag iEn -- Outgoing back-pressure, /ready/ edge. ) } --- | Dataflow circuit synchronised to the 'systemClockGen'. +-- | Dataflow circuit synchronized to the 'systemClockGen'. -- type DataFlow iEn oEn i o = DataFlow' systemClockGen iEn oEn i o -- | Create a 'DataFlow' circuit from a circuit description with the appropriate -- type: -- -- @ --- 'Signal'' dom i -- Incoming data. --- -> 'Signal'' dom Bool -- Flagged with a single /valid/ bit. --- -> 'Signal'' dom Bool -- Incoming back-pressure, /ready/ bit. --- -> ( 'Signal'' dom o -- Outgoing data. --- , 'Signal'' dom oEn -- Flagged with a single /valid/ bit. --- , 'Signal'' dom iEn -- Outgoing back-pressure, /ready/ bit. +-- 'Signal'' tag i -- Incoming data. +-- -> 'Signal'' tag Bool -- Flagged with a single /valid/ bit. +-- -> 'Signal'' tag Bool -- Incoming back-pressure, /ready/ bit. +-- -> ( 'Signal'' tag o -- Outgoing data. +-- , 'Signal'' tag oEn -- Flagged with a single /valid/ bit. +-- , 'Signal'' tag iEn -- Outgoing back-pressure, /ready/ bit. -- ) -- @ -- @@ -137,49 +137,51 @@ newtype DataFlow domain iEn oEn i o -- * Not consume data when validity is deasserted. -- * Only update its output when readiness is asserted. liftDF - :: ( Signal dom i - -> Signal dom Bool - -> Signal dom Bool - -> (Signal dom o, Signal dom Bool, Signal dom Bool)) - -> DataFlow dom Bool Bool i o + :: ( Signal tag i + -> Signal tag Bool + -> Signal tag Bool + -> (Signal tag o, Signal tag Bool, Signal tag Bool)) + -> DataFlow tag Bool Bool i o liftDF = DF -- | Create a 'DataFlow' circuit where the given function @f@ operates on the --- data, and the synchronisation channels are passed unaltered. +-- data, and the synchronization channels are passed unaltered. pureDF :: (i -> o) - -> DataFlow dom Bool Bool i o + -> DataFlow tag Bool Bool i o pureDF f = DF (\i iV oR -> (fmap f i,iV,oR)) -- | Create a 'DataFlow' circuit from a Mealy machine description as those of -- "Clash.Prelude.Mealy" mealyDF - :: Undefined s - => Clock domain gated - -> Reset domain synchronous + :: ( KnownDomain tag dom + , Undefined s ) + => Clock tag gated + -> Reset tag polarity -> (s -> i -> (s,o)) -> s - -> DataFlow domain Bool Bool i o + -> DataFlow tag Bool Bool i o mealyDF clk rst f iS = DF (\i iV oR -> let en = iV .&&. oR (s',o) = unbundle (f <$> s <*> i) - s = register (clockGate clk en) rst iS s' + s = register (toEnabledClock clk en) rst iS s' in (o,iV,oR)) -- | Create a 'DataFlow' circuit from a Moore machine description as those of -- "Clash.Prelude.Moore" mooreDF - :: Undefined s - => Clock domain gated - -> Reset domain synchronous + :: ( KnownDomain tag dom + , Undefined s ) + => Clock tag gated + -> Reset tag polarity -> (s -> i -> s) -> (s -> o) -> s - -> DataFlow domain Bool Bool i o + -> DataFlow tag Bool Bool i o mooreDF clk rst ft fo iS = DF (\i iV oR -> let en = iV .&&. oR s' = ft <$> s <*> i - s = register (clockGate clk en) rst iS s' + s = register (toEnabledClock clk en) rst iS s' o = fo <$> s in (o,iV,oR)) @@ -212,18 +214,19 @@ fifoDF_mealy (mem,rptr,wptr) (wdata,winc,rinc) = -- fifo4 = 'fifoDF' d4 (2 :> 3 :> Nil) -- @ fifoDF - :: forall addrSize m n a domain gated synchronous - . ( Undefined a + :: forall addrSize m n a tag dom polarity gated + . ( KnownDomain tag dom + , Undefined a , KnownNat addrSize , KnownNat n , KnownNat m , (m + n) ~ (2 ^ addrSize) ) - => Clock domain gated - -> Reset domain synchronous + => Clock tag gated + -> Reset tag polarity -> SNat (m + n) -- ^ Depth of the FIFO buffer. Must be a power of two. -> Vec m a -- ^ Initial content. Can be smaller than the size of the -- FIFO. Empty spaces are initialised with 'undefined'. - -> DataFlow domain Bool Bool a a + -> DataFlow tag Bool Bool a a fifoDF clk rst _ iS = DF $ \i iV oR -> let initRdPtr = 0 initWrPtr = fromIntegral (length iS) @@ -235,15 +238,16 @@ fifoDF clk rst _ iS = DF $ \i iV oR -> -- | Identity circuit -- -- <> -idDF :: DataFlow dom en en a a +idDF :: DataFlow tag en en a a idDF = DF (\a val rdy -> (a,val,rdy)) -- | Sequential composition of two 'DataFlow' circuits. -- -- <> -seqDF :: DataFlow dom aEn bEn a b - -> DataFlow dom bEn cEn b c - -> DataFlow dom aEn cEn a c +seqDF + :: DataFlow tag aEn bEn a b + -> DataFlow tag bEn cEn b c + -> DataFlow tag aEn cEn a c (DF f) `seqDF` (DF g) = DF (\a aVal cRdy -> let (b,bVal,aRdy) = f a aVal bRdy (c,cVal,bRdy) = g b bVal cRdy in (c,cVal,aRdy)) @@ -252,8 +256,9 @@ seqDF :: DataFlow dom aEn bEn a b -- the second halve unchanged. -- -- <> -firstDF :: DataFlow dom aEn bEn a b - -> DataFlow dom (aEn,cEn) (bEn,cEn) (a,c) (b,c) +firstDF + :: DataFlow tag aEn bEn a b + -> DataFlow tag (aEn, cEn) (bEn, cEn) (a, c) (b, c) firstDF (DF f) = DF (\ac acV bcR -> let (a,c) = unbundle ac (aV,cV) = unbundle acV (bR,cR) = unbundle bcR @@ -267,7 +272,7 @@ firstDF (DF f) = DF (\ac acV bcR -> let (a,c) = unbundle ac -- | Swap the two communication channels. -- -- <> -swapDF :: DataFlow dom (aEn,bEn) (bEn,aEn) (a,b) (b,a) +swapDF :: DataFlow tag (aEn, bEn) (bEn, aEn) (a, b) (b, a) swapDF = DF (\ab abV baR -> (swap <$> ab, swap <$> abV, swap <$> baR)) where swap ~(a,b) = (b,a) @@ -276,26 +281,25 @@ swapDF = DF (\ab abV baR -> (swap <$> ab, swap <$> abV, swap <$> baR)) -- the first halve unchanged. -- -- <> -secondDF :: DataFlow dom aEn bEn a b - -> DataFlow dom (cEn,aEn) (cEn,bEn) (c,a) (c,b) +secondDF + :: DataFlow tag aEn bEn a b + -> DataFlow tag (cEn, aEn) (cEn, bEn) (c, a) (c, b) secondDF f = swapDF `seqDF` firstDF f `seqDF` swapDF -- | Compose two 'DataFlow' circuits in parallel. -- -- <> -parDF :: DataFlow dom aEn bEn a b - -> DataFlow dom cEn dEn c d - -> DataFlow dom (aEn,cEn) (bEn,dEn) (a,c) (b,d) +parDF + :: DataFlow tag aEn bEn a b + -> DataFlow tag cEn dEn c d + -> DataFlow tag (aEn, cEn) (bEn, dEn) (a, c) (b, d) f `parDF` g = firstDF f `seqDF` secondDF g -- | Compose /n/ 'DataFlow' circuits in parallel. -parNDF :: KnownNat n - => Vec n (DataFlow dom aEn bEn a b) - -> DataFlow dom - (Vec n aEn) - (Vec n bEn) - (Vec n a) - (Vec n b) +parNDF + :: KnownNat n + => Vec n (DataFlow tag aEn bEn a b) + -> DataFlow tag (Vec n aEn) (Vec n bEn) (Vec n a) (Vec n b) parNDF fs = DF (\as aVs bRs -> let as' = unbundle as @@ -309,13 +313,13 @@ parNDF fs = -- | Feed back the second halve of the communication channel. The feedback loop -- is buffered by a 'fifoDF' circuit. -- --- So given a circuit /h/ with two synchronisation channels: +-- So given a circuit /h/ with two synchronization channels: -- -- @ -- __h__ :: 'DataFlow' (Bool,Bool) (Bool,Bool) (a,d) (b,d) -- @ -- --- Feeding back the /d/ part (including its synchronisation channels) results +-- Feeding back the /d/ part (including its synchronization channels) results -- in: -- -- @ @@ -324,7 +328,7 @@ parNDF fs = -- -- <> -- --- When you have a circuit @h'@, with only a single synchronisation channel: +-- When you have a circuit @h'@, with only a single synchronization channel: -- -- @ -- __h'__ :: 'DataFlow' Bool Bool (a,d) (b,d) @@ -337,7 +341,7 @@ parNDF fs = -- @ -- -- The circuits @f@, @h@, and @g@, must operate in /lock-step/ because the /h'/ --- circuit only has a single synchronisation channel. Consequently, there +-- circuit only has a single synchronization channel. Consequently, there -- should only be progress when all three circuits are producing /valid/ data -- and all three circuits are /ready/ to receive new data. We need to compose -- /h'/ with the 'lockStep' and 'stepLock' functions to achieve the /lock-step/ @@ -349,20 +353,21 @@ parNDF fs = -- -- <> loopDF - :: ( Undefined d + :: ( KnownDomain tag dom + , Undefined d , KnownNat m , KnownNat n , KnownNat addrSize , (m+n) ~ (2^addrSize) ) - => Clock dom gated - -> Reset dom synchronous + => Clock tag gated + -> Reset tag synchronous -> SNat (m + n) -- ^ Depth of the FIFO buffer. Must be a power of two -> Vec m d -- ^ Initial content of the FIFO buffer. Can be smaller than the size of the -- FIFO. Empty spaces are initialised with 'undefined'. - -> DataFlow dom (Bool,Bool) (Bool,Bool) (a,d) (b,d) - -> DataFlow dom Bool Bool a b + -> DataFlow tag (Bool,Bool) (Bool,Bool) (a,d) (b,d) + -> DataFlow tag Bool Bool a b loopDF clk rst sz is (DF f) = DF (\a aV bR -> let (bd,bdV,adR) = f ad adV bdR (b,d) = unbundle bd @@ -378,8 +383,8 @@ loopDF clk rst sz is (DF f) = -- | Feed back the second halve of the communication channel. Unlike 'loopDF', -- the feedback loop is /not/ buffered. -loopDF_nobuf :: DataFlow dom (Bool,Bool) (Bool,Bool) (a,d) (b,d) - -> DataFlow dom Bool Bool a b +loopDF_nobuf :: DataFlow tag (Bool,Bool) (Bool,Bool) (a,d) (b,d) + -> DataFlow tag Bool Bool a b loopDF_nobuf (DF f) = DF (\a aV bR -> let (bd,bdV,adR) = f ad adV bdR (b,d) = unbundle bd (bV,dV) = unbundle bdV @@ -390,9 +395,9 @@ loopDF_nobuf (DF f) = DF (\a aV bR -> let (bd,bdV,adR) = f ad adV bdR in (b,bV,aR) ) --- | Reduce or extend the synchronisation granularity of parallel compositions. +-- | Reduce or extend the synchronization granularity of parallel compositions. class LockStep a b where - -- | Reduce the synchronisation granularity to a single 'Bool'ean value. + -- | Reduce the synchronization granularity to a single 'Bool'ean value. -- -- Given: -- @@ -409,7 +414,7 @@ class LockStep a b where -- @ -- -- because, @f \`parDF\` g@, has type, @'DataFlow' (Bool,Bool) (Bool,Bool) (a,c) (b,d)@, - -- which does not match the expected synchronisation granularity of @h@. We + -- which does not match the expected synchronization granularity of @h@. We -- need a circuit in between that has the type: -- -- @ @@ -425,7 +430,7 @@ class LockStep a b where -- ready port is only asserted when @h@ is ready and @g@ is producing valid -- data. @f@ and @g@ will hence be proceeding in /lock-step/. -- - -- The 'lockStep' function ensures that all synchronisation signals are + -- The 'lockStep' function ensures that all synchronization signals are -- properly connected: -- -- @ @@ -436,7 +441,7 @@ class LockStep a b where -- -- __Note 1__: ensure that the components that you are synchronising have -- buffered/delayed @ready@ and @valid@ signals, or 'lockStep' has the - -- potential to introduce combinational loops. You can do this by placing + -- potential to introduce combinatorial loops. You can do this by placing -- 'fifoDF's on the parallel channels. Extending the above example, you would -- write: -- @@ -456,9 +461,9 @@ class LockStep a b where -- @ -- -- Does the right thing. - lockStep :: DataFlow dom a Bool b b + lockStep :: DataFlow tag a Bool b b - -- | Extend the synchronisation granularity from a single 'Bool'ean value. + -- | Extend the synchronization granularity from a single 'Bool'ean value. -- -- Given: -- @@ -475,7 +480,7 @@ class LockStep a b where -- @ -- -- because, @f \`parDF\` g@, has type, @'DataFlow' (Bool,Bool) (Bool,Bool) (a,c) (b,d)@, - -- which does not match the expected synchronisation granularity of @h@. We + -- which does not match the expected synchronization granularity of @h@. We -- need a circuit in between that has the type: -- -- @ @@ -491,7 +496,7 @@ class LockStep a b where -- only asserted when @h@ is valid and @f@ is ready to receive new values. -- @f@ and @g@ will hence be proceeding in /lock-step/. -- - -- The 'stepLock' function ensures that all synchronisation signals are + -- The 'stepLock' function ensures that all synchronization signals are -- properly connected: -- -- @ @@ -502,7 +507,7 @@ class LockStep a b where -- -- __Note 1__: ensure that the components that you are synchronising have -- buffered/delayed @ready@ and @valid@ signals, or 'stepLock' has the - -- potential to introduce combinational loops. You can do this by placing + -- potential to introduce combinatorial loops. You can do this by placing -- 'fifoDF's on the parallel channels. Extending the above example, you would -- write: -- @@ -522,7 +527,7 @@ class LockStep a b where -- @ -- -- Does the right thing. - stepLock :: DataFlow dom Bool a b b + stepLock :: DataFlow tag Bool a b b instance LockStep Bool c where lockStep = idDF diff --git a/clash-prelude/src/Clash/Prelude/Mealy.hs b/clash-prelude/src/Clash/Prelude/Mealy.hs index 8f913cbe86..7ce97c0a9f 100644 --- a/clash-prelude/src/Clash/Prelude/Mealy.hs +++ b/clash-prelude/src/Clash/Prelude/Mealy.hs @@ -16,7 +16,7 @@ {-# LANGUAGE Safe #-} module Clash.Prelude.Mealy - ( -- * Mealy machine synchronised to the system clock + ( -- * Mealy machine synchronized to the system clock mealy , mealyB , (<^>) @@ -39,7 +39,7 @@ let macT s (x,y) = (s',s) -} --- | Create a synchronous function from a combinational function describing +-- | Create a synchronous function from a combinatorial function describing -- a mealy machine -- -- @ @@ -51,36 +51,36 @@ let macT s (x,y) = (s',s) -- where -- s' = x * y + s -- --- mac :: HiddenClockReset domain gated synchronous => 'Signal' domain (Int, Int) -> 'Signal' domain Int +-- mac :: HiddenClockReset tag enabled polarity dom => 'Signal' tag (Int, Int) -> 'Signal' tag Int -- mac = 'mealy' macT 0 -- @ -- --- >>> simulate mac [(0,0),(1,1),(2,2),(3,3),(4,4)] +-- >>> simulate @System mac [(0,0),(1,1),(2,2),(3,3),(4,4)] -- [0,0,1,5,14... -- ... -- -- Synchronous sequential functions can be composed just like their --- combinational counterpart: +-- combinatorial counterpart: -- -- @ -- dualMac --- :: HiddenClockReset domain gated synchronous --- => ('Signal' domain Int, 'Signal' domain Int) --- -> ('Signal' domain Int, 'Signal' domain Int) --- -> 'Signal' domain Int +-- :: HiddenClockReset tag enabled polarity dom +-- => ('Signal' tag Int, 'Signal' tag Int) +-- -> ('Signal' tag Int, 'Signal' tag Int) +-- -> 'Signal' tag Int -- dualMac (a,b) (x,y) = s1 + s2 -- where -- s1 = 'mealy' mac 0 ('Clash.Signal.bundle' (a,x)) -- s2 = 'mealy' mac 0 ('Clash.Signal.bundle' (b,y)) -- @ mealy - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , Undefined s ) => (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@ -> s -- ^ Initial state - -> (Signal domain i -> Signal domain o) + -> (Signal tag i -> Signal tag o) -- ^ Synchronous sequential function with input and output matching that -- of the mealy machine mealy = hideClockReset E.mealy @@ -113,13 +113,15 @@ mealy = hideClockReset E.mealy -- (i2,b2) = 'mealyB' f 3 (i1,c) -- @ mealyB - :: ( HiddenClockReset domain gated synchronous - , Undefined s, Bundle i, Bundle o ) + :: ( HiddenClockReset tag enabled polarity dom + , Undefined s + , Bundle i + , Bundle o ) => (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@ -> s -- ^ Initial state - -> (Unbundled domain i -> Unbundled domain o) + -> (Unbundled tag i -> Unbundled tag o) -- ^ Synchronous sequential function with input and output matching that -- of the mealy machine mealyB = hideClockReset E.mealyB @@ -127,13 +129,15 @@ mealyB = hideClockReset E.mealyB -- | Infix version of 'mealyB' (<^>) - :: ( HiddenClockReset domain gated synchronous - , Undefined s, Bundle i, Bundle o ) + :: ( HiddenClockReset tag enabled polarity dom + , Undefined s + , Bundle i + , Bundle o ) => (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@ -> s -- ^ Initial state - -> (Unbundled domain i -> Unbundled domain o) + -> (Unbundled tag i -> Unbundled tag o) -- ^ Synchronous sequential function with input and output matching that -- of the mealy machine (<^>) = mealyB diff --git a/clash-prelude/src/Clash/Prelude/Moore.hs b/clash-prelude/src/Clash/Prelude/Moore.hs index 9999e3eb18..a7e68166e1 100644 --- a/clash-prelude/src/Clash/Prelude/Moore.hs +++ b/clash-prelude/src/Clash/Prelude/Moore.hs @@ -48,11 +48,11 @@ let macT s (x,y) = x * y + s -- -> Int -- Updated state -- macT s (x,y) = x * y + s -- --- mac :: HiddenClockReset domain gated synchronous => 'Signal' domain (Int, Int) -> 'Signal' domain Int +-- mac :: HiddenClockReset tag enabled polarity dom => 'Signal' tag (Int, Int) -> 'Signal' tag Int -- mac = 'moore' mac id 0 -- @ -- --- >>> simulate mac [(0,0),(1,1),(2,2),(3,3),(4,4)] +-- >>> simulate @System mac [(0,0),(1,1),(2,2),(3,3),(4,4)] -- [0,0,1,5,14,30,... -- ... -- @@ -61,24 +61,24 @@ let macT s (x,y) = x * y + s -- -- @ -- dualMac --- :: HiddenClockReset domain gated synchronous --- => ('Signal' domain Int, 'Signal' domain Int) --- -> ('Signal' domain Int, 'Signal' domain Int) --- -> 'Signal' domain Int +-- :: HiddenClockReset tag enabled polarity dom +-- => ('Signal' tag Int, 'Signal' tag Int) +-- -> ('Signal' tag Int, 'Signal' tag Int) +-- -> 'Signal' tag Int -- dualMac (a,b) (x,y) = s1 + s2 -- where -- s1 = 'moore' mac id 0 ('Clash.Signal.bundle' (a,x)) -- s2 = 'moore' mac id 0 ('Clash.Signal.bundle' (b,y)) -- @ moore - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , Undefined s ) => (s -> i -> s) -- ^ Transfer function in moore machine form: -- @state -> input -> newstate@ -> (s -> o) -- ^ Output function in moore machine form: -- @state -> output@ -> s -- ^ Initial state - -> (Signal domain i -> Signal domain o) + -> (Signal tag i -> Signal tag o) -- ^ Synchronous sequential function with input and output matching that -- of the moore machine moore = hideClockReset E.moore @@ -88,11 +88,11 @@ moore = hideClockReset E.moore -- | Create a synchronous function from a combinational function describing -- a moore machine without any output logic medvedev - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , Undefined s ) => (s -> i -> s) -> s - -> (Signal domain i -> Signal domain s) + -> (Signal tag i -> Signal tag s) medvedev tr st = moore tr id st {-# INLINE medvedev #-} @@ -124,7 +124,7 @@ medvedev tr st = moore tr id st -- (i2,b2) = 'mooreB' t o 3 (i1,c) -- @ mooreB - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , Undefined s , Bundle i , Bundle o ) @@ -133,7 +133,7 @@ mooreB -> (s -> o) -- ^ Output function in moore machine form: -- @state -> output@ -> s -- ^ Initial state - -> (Unbundled domain i -> Unbundled domain o) + -> (Unbundled tag i -> Unbundled tag o) -- ^ Synchronous sequential function with input and output matching that -- of the moore machine mooreB = hideClockReset E.mooreB @@ -141,12 +141,12 @@ mooreB = hideClockReset E.mooreB -- | A version of 'medvedev' that does automatic 'Bundle'ing medvedevB - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , Undefined s , Bundle i , Bundle s ) => (s -> i -> s) -> s - -> (Unbundled domain i -> Unbundled domain s) + -> (Unbundled tag i -> Unbundled tag s) medvedevB tr st = mooreB tr id st {-# INLINE medvedevB #-} diff --git a/clash-prelude/src/Clash/Prelude/RAM.hs b/clash-prelude/src/Clash/Prelude/RAM.hs index fd9169f07a..90db23b4f9 100644 --- a/clash-prelude/src/Clash/Prelude/RAM.hs +++ b/clash-prelude/src/Clash/Prelude/RAM.hs @@ -22,7 +22,7 @@ RAM primitives with a combinational read port. {-# OPTIONS_HADDOCK show-extensions #-} module Clash.Prelude.RAM - ( -- * RAM synchronised to an arbitrary clock + ( -- * RAM synchronized to an arbitrary clock asyncRam , asyncRamPow2 ) @@ -46,14 +46,17 @@ import Clash.Sized.Unsigned (Unsigned) -- * See "Clash.Prelude.BlockRam#usingrams" for more information on how to use a -- RAM. asyncRam - :: (Enum addr, HiddenClock domain gated, HasCallStack) + :: ( Enum addr + , HiddenClock tag enabled dom + , HasCallStack + ) => SNat n -- ^ Size @n@ of the RAM - -> Signal domain addr + -> Signal tag addr -- ^ Read address @r@ - -> Signal domain (Maybe (addr, a)) + -> Signal tag (Maybe (addr, a)) -- ^ (write address @w@, value to write) - -> Signal domain a + -> Signal tag a -- ^ Value of the @RAM@ at address @r@ asyncRam = \sz rd wrM -> withFrozenCallStack (hideClock (\clk -> E.asyncRam clk clk sz rd wrM)) @@ -68,12 +71,14 @@ asyncRam = \sz rd wrM -> withFrozenCallStack -- * See "Clash.Prelude.BlockRam#usingrams" for more information on how to use a -- RAM. asyncRamPow2 - :: (KnownNat n, HiddenClock domain gated, HasCallStack) - => Signal domain (Unsigned n) + :: ( KnownNat n + , HiddenClock tag enabled dom + , HasCallStack ) + => Signal tag (Unsigned n) -- ^ Read address @r@ - -> Signal domain (Maybe (Unsigned n, a)) + -> Signal tag (Maybe (Unsigned n, a)) -- ^ (write address @w@, value to write) - -> Signal domain a + -> Signal tag a -- ^ Value of the @RAM@ at address @r@ asyncRamPow2 = \rd wrM -> withFrozenCallStack (hideClock (\clk -> E.asyncRamPow2 clk clk rd wrM)) diff --git a/clash-prelude/src/Clash/Prelude/ROM.hs b/clash-prelude/src/Clash/Prelude/ROM.hs index b9cfab52ba..e521eda443 100644 --- a/clash-prelude/src/Clash/Prelude/ROM.hs +++ b/clash-prelude/src/Clash/Prelude/ROM.hs @@ -21,7 +21,7 @@ module Clash.Prelude.ROM ( -- * Asynchronous ROM asyncRom , asyncRomPow2 - -- * Synchronous ROM synchronised to an arbitrary clock + -- * Synchronous ROM synchronized to an arbitrary clock , rom , romPow2 -- * Internal @@ -44,12 +44,16 @@ import Clash.Sized.Vector (Vec, length, toList) -- -- * See "Clash.Sized.Fixed#creatingdatafiles" and "Clash.Prelude.BlockRam#usingrams" -- for ideas on how to use ROMs and RAMs -asyncRom :: (KnownNat n, Enum addr) - => Vec n a -- ^ ROM content - -- - -- __NB:__ must be a constant - -> addr -- ^ Read address @rd@ - -> a -- ^ The value of the ROM at address @rd@ +asyncRom + :: (KnownNat n, Enum addr) + => Vec n a + -- ^ ROM content + -- + -- __NB:__ must be a constant + -> addr + -- ^ Read address @rd@ + -> a + -- ^ The value of the ROM at address @rd@ asyncRom = \content rd -> asyncRom# content (fromEnum rd) {-# INLINE asyncRom #-} @@ -59,22 +63,28 @@ asyncRom = \content rd -> asyncRom# content (fromEnum rd) -- -- * See "Clash.Sized.Fixed#creatingdatafiles" and "Clash.Prelude.BlockRam#usingrams" -- for ideas on how to use ROMs and RAMs -asyncRomPow2 :: KnownNat n - => Vec (2^n) a -- ^ ROM content - -- - -- __NB:__ must be a constant - -> Unsigned n -- ^ Read address @rd@ - -> a -- ^ The value of the ROM at address @rd@ +asyncRomPow2 + :: KnownNat n + => Vec (2^n) a -- ^ ROM content + -- + -- __NB:__ must be a constant + -> Unsigned n + -- ^ Read address @rd@ + -> a + -- ^ The value of the ROM at address @rd@ asyncRomPow2 = asyncRom {-# INLINE asyncRomPow2 #-} -- | asyncROM primitive -asyncRom# :: KnownNat n - => Vec n a -- ^ ROM content - -- - -- __NB:__ must be a constant - -> Int -- ^ Read address @rd@ - -> a -- ^ The value of the ROM at address @rd@ +asyncRom# + :: KnownNat n + => Vec n a -- ^ ROM content + -- + -- __NB:__ must be a constant + -> Int + -- ^ Read address @rd@ + -> a + -- ^ The value of the ROM at address @rd@ asyncRom# content rd = arr ! rd where szI = length content @@ -91,12 +101,17 @@ asyncRom# content rd = arr ! rd -- * See "Clash.Sized.Fixed#creatingdatafiles" and "Clash.Prelude.BlockRam#usingrams" -- for ideas on how to use ROMs and RAMs rom - :: (KnownNat n, KnownNat m, HiddenClock domain gated) - => Vec n a -- ^ ROM content - -- - -- __NB:__ must be a constant - -> Signal domain (Unsigned m) -- ^ Read address @rd@ - -> Signal domain a -- ^ The value of the ROM at address @rd@ + :: ( KnownNat n + , KnownNat m + , HiddenClock tag gated dom ) + => Vec n a + -- ^ ROM content + -- + -- __NB:__ must be a constant + -> Signal tag (Unsigned m) + -- ^ Read address @rd@ + -> Signal tag a + -- ^ The value of the ROM at address @rd@ rom = hideClock E.rom {-# INLINE rom #-} @@ -110,11 +125,13 @@ rom = hideClock E.rom -- * See "Clash.Sized.Fixed#creatingdatafiles" and "Clash.Prelude.BlockRam#usingrams" -- for ideas on how to use ROMs and RAMs romPow2 - :: (KnownNat n, HiddenClock domain gated) - => Vec (2^n) a -- ^ ROM content - -- - -- __NB:__ must be a constant - -> Signal domain (Unsigned n) -- ^ Read address @rd@ - -> Signal domain a -- ^ The value of the ROM at address @rd@ + :: ( KnownNat n + , HiddenClock tag gated dom ) + => Vec (2^n) a + -- ^ ROM content + -- + -- __NB:__ must be a constant + -> Signal tag (Unsigned n) -- ^ Read address @rd@ + -> Signal tag a -- ^ The value of the ROM at address @rd@ romPow2 = hideClock E.romPow2 {-# INLINE romPow2 #-} diff --git a/clash-prelude/src/Clash/Prelude/ROM/File.hs b/clash-prelude/src/Clash/Prelude/ROM/File.hs index fb3857ccd1..9614e898a4 100644 --- a/clash-prelude/src/Clash/Prelude/ROM/File.hs +++ b/clash-prelude/src/Clash/Prelude/ROM/File.hs @@ -33,7 +33,7 @@ We can instantiate a synchronous ROM using the content of the above file like so: @ -f :: HiddenClock domain => Signal domain (Unsigned 3) -> Signal domain (Unsigned 9) +f :: HiddenClock tag => Signal tag (Unsigned 3) -> Signal tag (Unsigned 9) f rd = 'Clash.Class.BitPack.unpack' '<$>' 'romFile' d7 \"memory.bin\" rd @ @@ -49,7 +49,7 @@ However, we can also interpret the same data as a tuple of a 6-bit unsigned number, and a 3-bit signed number: @ -g :: HiddenClock domain => Signal domain (Unsigned 3) -> Signal domain (Unsigned 6,Signed 3) +g :: HiddenClock tag => Signal tag (Unsigned 3) -> Signal tag (Unsigned 6,Signed 3) g rd = 'Clash.Class.BitPack.unpack' '<$>' 'romFile' d7 \"memory.bin\" rd @ @@ -77,7 +77,7 @@ module Clash.Prelude.ROM.File ( -- * Asynchronous ROM asyncRomFile , asyncRomFilePow2 - -- * Synchronous ROM synchronised to an arbitrary clock + -- * Synchronous ROM synchronized to an arbitrary clock , romFile , romFilePow2 -- * Internal @@ -258,11 +258,11 @@ asyncRomFile# sz file = (content !) -- Leave "(content !)" eta-reduced, see -- * See "Clash.Sized.Fixed#creatingdatafiles" for ideas on how to create your -- own data files. romFile - :: (KnownNat m, KnownNat n, HiddenClock domain gated) + :: (KnownNat m, KnownNat n, HiddenClock tag gated dom) => SNat n -- ^ Size of the ROM -> FilePath -- ^ File describing the content of the ROM - -> Signal domain (Unsigned n) -- ^ Read address @rd@ - -> Signal domain (BitVector m) + -> Signal tag (Unsigned n) -- ^ Read address @rd@ + -> Signal tag (BitVector m) -- ^ The value of the ROM at address @rd@ from the previous clock cycle romFile = hideClock E.romFile {-# INLINE romFile #-} @@ -291,11 +291,11 @@ romFile = hideClock E.romFile -- * See "Clash.Sized.Fixed#creatingdatafiles" for ideas on how to create your -- own data files. romFilePow2 - :: forall n m domain gated - . (KnownNat m, KnownNat n, HiddenClock domain gated) + :: forall n m tag gated dom + . (KnownNat m, KnownNat n, HiddenClock tag gated dom) => FilePath -- ^ File describing the content of the ROM - -> Signal domain (Unsigned n) -- ^ Read address @rd@ - -> Signal domain (BitVector m) + -> Signal tag (Unsigned n) -- ^ Read address @rd@ + -> Signal tag (BitVector m) -- ^ The value of the ROM at address @rd@ from the previous clock cycle romFilePow2 = hideClock E.romFilePow2 {-# INLINE romFilePow2 #-} diff --git a/clash-prelude/src/Clash/Prelude/Safe.hs b/clash-prelude/src/Clash/Prelude/Safe.hs index f918e635b8..3177f48f8d 100644 --- a/clash-prelude/src/Clash/Prelude/Safe.hs +++ b/clash-prelude/src/Clash/Prelude/Safe.hs @@ -175,46 +175,46 @@ It instead exports the identically named functions defined in terms of -- | Create a 'register' function for product-type like signals (e.g. '(Signal a, Signal b)') -- --- > rP :: HiddenClockReset domain gated synchronous --- > => (Signal domain Int, Signal domain Int) --- > -> (Signal domain Int, Signal domain Int) +-- > rP :: HiddenClockReset tag enabled polarity dom +-- > => (Signal tag Int, Signal tag Int) +-- > -> (Signal tag Int, Signal tag Int) -- > rP = registerB (8,8) -- --- >>> simulateB rP [(1,1),(2,2),(3,3)] :: [(Int,Int)] +-- >>> simulateB @System rP [(1,1),(2,2),(3,3)] :: [(Int,Int)] -- [(8,8),(1,1),(2,2),(3,3)... -- ... registerB - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , Undefined a , Bundle a ) => a - -> Unbundled domain a - -> Unbundled domain a + -> Unbundled tag a + -> Unbundled tag a registerB = hideClockReset E.registerB infixr 3 `registerB` {-# INLINE registerB #-} -- | Give a pulse when the 'Signal' goes from 'minBound' to 'maxBound' isRising - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , Undefined a , Bounded a , Eq a ) => a -- ^ Starting value - -> Signal domain a - -> Signal domain Bool + -> Signal tag a + -> Signal tag Bool isRising = hideClockReset E.isRising {-# INLINE isRising #-} -- | Give a pulse when the 'Signal' goes from 'maxBound' to 'minBound' isFalling - :: ( HiddenClockReset domain gated synchronous + :: ( HiddenClockReset tag enabled polarity dom , Undefined a , Bounded a , Eq a ) => a -- ^ Starting value - -> Signal domain a - -> Signal domain Bool + -> Signal tag a + -> Signal tag Bool isFalling = hideClockReset E.isFalling {-# INLINE isFalling #-} @@ -225,9 +225,9 @@ isFalling = hideClockReset E.isFalling -- To be precise: the given signal will be @'False'@ for the next @n-1@ cycles, -- followed by a single @'True'@ value: -- --- >>> Prelude.last (sampleN 1025 (riseEvery d1024)) == True +-- >>> Prelude.last (sampleN @System 1025 (riseEvery d1024)) == True -- True --- >>> Prelude.or (sampleN 1024 (riseEvery d1024)) == False +-- >>> Prelude.or (sampleN @System 1024 (riseEvery d1024)) == False -- True -- -- For example, to update a counter once every 10 million cycles: @@ -236,9 +236,9 @@ isFalling = hideClockReset E.isFalling -- counter = 'Clash.Signal.regEn' 0 ('riseEvery' ('SNat' :: 'SNat' 10000000)) (counter + 1) -- @ riseEvery - :: HiddenClockReset domain gated synchronous + :: HiddenClockReset tag enabled polarity dom => SNat n - -> Signal domain Bool + -> Signal tag Bool riseEvery = hideClockReset E.riseEvery {-# INLINE riseEvery #-} @@ -249,24 +249,23 @@ riseEvery = hideClockReset E.riseEvery -- -- To oscillate on an interval of 5 cycles: -- --- >>> sampleN 11 (oscillate False d5) +-- >>> sampleN @System 11 (oscillate False d5) -- [False,False,False,False,False,False,True,True,True,True,True] -- -- To oscillate between @'True'@ and @'False'@: -- --- >>> sampleN 11 (oscillate False d1) +-- >>> sampleN @System 11 (oscillate False d1) -- [False,False,True,False,True,False,True,False,True,False,True] -- -- An alternative definition for the above could be: -- -- >>> let osc' = register False (not <$> osc') --- >>> let sample' = sampleN 200 --- >>> sample' (oscillate False d1) == sample' osc' +-- >>> sampleN @System 200 (oscillate False d1) == sampleN @System 200 osc' -- True oscillate - :: HiddenClockReset domain gated synchronous + :: HiddenClockReset tag enabled polarity dom => Bool -> SNat n - -> Signal domain Bool + -> Signal tag Bool oscillate = hideClockReset E.oscillate {-# INLINE oscillate #-} diff --git a/clash-prelude/src/Clash/Prelude/Testbench.hs b/clash-prelude/src/Clash/Prelude/Testbench.hs index a43d45aece..0de29a782d 100644 --- a/clash-prelude/src/Clash/Prelude/Testbench.hs +++ b/clash-prelude/src/Clash/Prelude/Testbench.hs @@ -25,7 +25,7 @@ import GHC.TypeLits (KnownNat) import qualified Clash.Explicit.Testbench as E import Clash.Signal - (HiddenClockReset, Signal, hideClockReset) + (KnownDomain, HiddenClockReset, Signal, hideClockReset) import Clash.Sized.BitVector (BitVector) import Clash.Sized.Vector (Vec) import Clash.XException (ShowX) @@ -45,12 +45,16 @@ import Clash.XException (ShowX) -- -- __NB__: This function /can/ be used in synthesizable designs. assert - :: (Eq a,ShowX a,HiddenClockReset domain gated synchronous) - => String -- ^ Additional message - -> Signal domain a -- ^ Checked value - -> Signal domain a -- ^ Expected value - -> Signal domain b -- ^ Return value - -> Signal domain b + :: (Eq a,ShowX a,HiddenClockReset tag enabled polarity dom) + => String + -- ^ Additional message + -> Signal tag a + -- ^ Checked value + -> Signal tag a + -- ^ Expected value + -> Signal tag b + -- ^ Return value + -> Signal tag b assert = hideClockReset E.assert {-# INLINE assert #-} @@ -62,17 +66,18 @@ assert = hideClockReset E.assert -- -- @ -- testInput --- :: HiddenClockReset domain gated synchronous --- => 'Signal' domain Int +-- :: HiddenClockReset tag enabled polarity dom +-- => 'Signal' tag Int -- testInput = 'stimuliGenerator' $('Clash.Sized.Vector.listToVecTH' [(1::Int),3..21]) -- @ -- -- >>> sampleN 13 testInput -- [1,3,5,7,9,11,13,15,17,19,21,21,21] stimuliGenerator - :: (KnownNat l, HiddenClockReset domain gated synchronous) + :: ( KnownNat l + , HiddenClockReset tag enabled polarity dom ) => Vec l a -- ^ Samples to generate - -> Signal domain a -- ^ Signal of given samples + -> Signal tag a -- ^ Signal of given samples stimuliGenerator = hideClockReset E.stimuliGenerator {-# INLINE stimuliGenerator #-} @@ -84,8 +89,8 @@ stimuliGenerator = hideClockReset E.stimuliGenerator -- -- @ -- expectedOutput --- :: HiddenClockReset domain gated synchronous --- -> 'Signal' domain Int -> 'Signal' domain Bool +-- :: HiddenClockReset tag enabled polarity dom +-- -> 'Signal' tag Int -> 'Signal' tag Bool -- expectedOutput = 'outputVerifier' $('Clash.Sized.Vector.listToVecTH' ([70,99,2,3,4,5,7,8,9,10]::[Int])) -- @ -- @@ -113,10 +118,14 @@ stimuliGenerator = hideClockReset E.stimuliGenerator -- -- If your working with 'BitVector's containing don't care bit you should use 'outputVerifierBitVector'. outputVerifier - :: (KnownNat l, Eq a, ShowX a, HiddenClockReset domain gated synchronous) + :: ( KnownNat l + , Eq a + , ShowX a + , KnownDomain tag dom + , HiddenClockReset tag enabled polarity dom ) => Vec l a -- ^ Samples to compare with - -> Signal domain a -- ^ Signal to verify - -> Signal domain Bool -- ^ Indicator that all samples are verified + -> Signal tag a -- ^ Signal to verify + -> Signal tag Bool -- ^ Indicator that all samples are verified outputVerifier = hideClockReset E.outputVerifier {-# INLINE outputVerifier #-} @@ -124,9 +133,11 @@ outputVerifier = hideClockReset E.outputVerifier -- | Same as 'outputVerifier', -- but can handle don't care bits in it's expected values. outputVerifierBitVector - :: (KnownNat l, KnownNat n, HiddenClockReset domain gated synchronous) + :: ( KnownNat l + , KnownNat n + , HiddenClockReset tag enabled polarity dom ) => Vec l (BitVector n) -- ^ Samples to compare with - -> Signal domain (BitVector n) -- ^ Signal to verify - -> Signal domain Bool -- ^ Indicator that all samples are verified + -> Signal tag (BitVector n) -- ^ Signal to verify + -> Signal tag Bool -- ^ Indicator that all samples are verified outputVerifierBitVector = hideClockReset E.outputVerifierBitVector {-# INLINE outputVerifierBitVector #-} diff --git a/clash-prelude/src/Clash/Promoted/Nat.hs b/clash-prelude/src/Clash/Promoted/Nat.hs index eee0981ce2..962a5d31bc 100644 --- a/clash-prelude/src/Clash/Promoted/Nat.hs +++ b/clash-prelude/src/Clash/Promoted/Nat.hs @@ -129,7 +129,7 @@ snatToNum p@SNat = fromInteger (natVal p) -- | Unary representation of a type-level natural -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable data UNat :: Nat -> Type where UZero :: UNat 0 USucc :: UNat n -> UNat (n + 1) @@ -142,7 +142,7 @@ instance KnownNat n => ShowX (UNat n) where -- | Convert a singleton natural number to its unary representation -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable toUNat :: forall n . SNat n -> UNat n toUNat p@SNat = fromI @n (natVal p) where @@ -152,14 +152,14 @@ toUNat p@SNat = fromI @n (natVal p) -- | Convert a unary-encoded natural number to its singleton representation -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable fromUNat :: UNat n -> SNat n fromUNat UZero = SNat :: SNat 0 fromUNat (USucc x) = addSNat (fromUNat x) (SNat :: SNat 1) -- | Add two unary-encoded natural numbers -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable addUNat :: UNat n -> UNat m -> UNat (n + m) addUNat UZero y = y addUNat x UZero = x @@ -167,7 +167,7 @@ addUNat (USucc x) y = USucc (addUNat x y) -- | Multiply two unary-encoded natural numbers -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable mulUNat :: UNat n -> UNat m -> UNat (n * m) mulUNat UZero _ = UZero mulUNat _ UZero = UZero @@ -175,14 +175,14 @@ mulUNat (USucc x) y = addUNat y (mulUNat x y) -- | Power of two unary-encoded natural numbers -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable powUNat :: UNat n -> UNat m -> UNat (n ^ m) powUNat _ UZero = USucc UZero powUNat x (USucc y) = mulUNat x (powUNat x y) -- | Predecessor of a unary-encoded natural number -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable predUNat :: UNat (n+1) -> UNat n predUNat (USucc x) = x predUNat UZero = @@ -190,7 +190,7 @@ predUNat UZero = -- | Subtract two unary-encoded natural numbers -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable subUNat :: UNat (m+n) -> UNat n -> UNat m subUNat x UZero = x subUNat (USucc x) (USucc y) = subUNat x y @@ -278,7 +278,7 @@ compareSNat a b = -- | Base-2 encoded natural number -- -- * __NB__: The LSB is the left/outer-most constructor: --- * __NB__: Not synthesisable +-- * __NB__: Not synthesizable -- -- >>> B0 (B1 (B1 BT)) -- b6 @@ -335,7 +335,7 @@ showBNat = go [] -- | Convert a singleton natural number to its base-2 representation -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable toBNat :: SNat n -> BNat n toBNat s@SNat = toBNat' (natVal s) where @@ -347,7 +347,7 @@ toBNat s@SNat = toBNat' (natVal s) -- | Convert a base-2 encoded natural number to its singleton representation -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable fromBNat :: BNat n -> SNat n fromBNat BT = SNat :: SNat 0 fromBNat (B0 x) = mulSNat (SNat :: SNat 2) (fromBNat x) @@ -356,7 +356,7 @@ fromBNat (B1 x) = addSNat (mulSNat (SNat :: SNat 2) (fromBNat x)) -- | Add two base-2 encoded natural numbers -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable addBNat :: BNat n -> BNat m -> BNat (n+m) addBNat (B0 a) (B0 b) = B0 (addBNat a b) addBNat (B0 a) (B1 b) = B1 (addBNat a b) @@ -367,7 +367,7 @@ addBNat a BT = a -- | Multiply two base-2 encoded natural numbers -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable mulBNat :: BNat n -> BNat m -> BNat (n*m) mulBNat BT _ = BT mulBNat _ BT = BT @@ -376,7 +376,7 @@ mulBNat (B1 a) b = addBNat (B0 (mulBNat a b)) b -- | Power of two base-2 encoded natural numbers -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable powBNat :: BNat n -> BNat m -> BNat (n^m) powBNat _ BT = B1 BT powBNat a (B0 b) = let z = powBNat a b @@ -386,7 +386,7 @@ powBNat a (B1 b) = let z = powBNat a b -- | Successor of a base-2 encoded natural number -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable succBNat :: BNat n -> BNat (n+1) succBNat BT = B1 BT succBNat (B0 a) = B1 a @@ -394,7 +394,7 @@ succBNat (B1 a) = B0 (succBNat a) -- | Predecessor of a base-2 encoded natural number -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable predBNat :: (1 <= n) => BNat n -> BNat (n-1) predBNat (B1 a) = case stripZeros a of BT -> BT @@ -403,7 +403,7 @@ predBNat (B0 x) = B1 (predBNat x) -- | Divide a base-2 encoded natural number by 2 -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable div2BNat :: BNat (2*n) -> BNat n div2BNat BT = BT div2BNat (B0 x) = x @@ -411,14 +411,14 @@ div2BNat (B1 _) = error "div2BNat: impossible: 2*n ~ 2*n+1" -- | Subtract 1 and divide a base-2 encoded natural number by 2 -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable div2Sub1BNat :: BNat (2*n+1) -> BNat n div2Sub1BNat (B1 x) = x div2Sub1BNat _ = error "div2Sub1BNat: impossible: 2*n+1 ~ 2*n" -- | Get the log2 of a base-2 encoded natural number -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable log2BNat :: BNat (2^n) -> BNat n log2BNat BT = error "log2BNat: log2(0) not defined" log2BNat (B1 x) = case stripZeros x of @@ -437,7 +437,7 @@ log2BNat (B0 x) = succBNat (log2BNat x) -- >>> stripZeros (B1 (B0 (B0 (B0 BT)))) -- b1 -- --- __NB__: Not synthesisable +-- __NB__: Not synthesizable stripZeros :: BNat n -> BNat n stripZeros BT = BT stripZeros (B1 x) = B1 (stripZeros x) diff --git a/clash-prelude/src/Clash/Signal.hs b/clash-prelude/src/Clash/Signal.hs index 011e4f15f8..7e882fc152 100644 --- a/clash-prelude/src/Clash/Signal.hs +++ b/clash-prelude/src/Clash/Signal.hs @@ -1,21 +1,21 @@ {-| Copyright : (C) 2013-2016, University of Twente, - 2016 , Myrtle Software, + 2016-2019, Myrtle Software Ltd, 2017 , Google Inc. License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij -Clash has synchronous 'Signal's in the form of: +Clash has 'Signal's in the form of: @ -'Signal' (domain :: 'Domain') a +'Signal' (tag :: 'Domain') a @ Where /a/ is the type of the value of the 'Signal', for example /Int/ or /Bool/, -and /domain/ is the /clock-/ (and /reset-/) domain to which the memory elements +and /tag/ is the /clock-/ (and /reset-/) tag to which the memory elements manipulating these 'Signal's belong. -The type-parameter, /domain/, is of the kind 'Domain' which has types of the +The type-parameter, /tag/, is of the kind 'Domain' which has types of the following shape: @ @@ -23,9 +23,9 @@ data Domain = Dom { domainName :: 'GHC.TypeLits.Symbol', clkPeriod :: 'GHC.TypeL @ Where /domainName/ is a type-level string ('GHC.TypeLits.Symbol') representing -the name of the /clock-/ (and /reset-/) domain, and /clkPeriod/ is a type-level +the name of the /clock-/ (and /reset-/) tag, and /clkPeriod/ is a type-level natural number ('GHC.TypeLits.Nat') representing the clock period (in __ps__) -of the clock lines in the /clock-domain/. +of the clock lines in the /clock-tag/. * __NB__: \"Bad things\"™ happen when you actually use a clock period of @0@, so do __not__ do that! @@ -39,8 +39,6 @@ never create a clock that goes any faster! {-# LANGUAGE GADTs #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE RankNTypes #-} -{-# LANGUAGE RebindableSyntax #-} -{-# LANGUAGE OverloadedLabels #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} @@ -55,18 +53,30 @@ module Clash.Signal , BiSignalIn , BiSignalOut , BiSignalDefault(..) - , Domain (..) + -- * Domain + , KnownDomain(..) + , ActiveEdge(..) + , SActiveEdge(..) + , InitBehavior(..) + , SInitBehavior(..) + , ResetKind(..) + , SResetKind(..) + , Domain(..) + , SDomain(..) , System -- * Clock , Clock , ClockKind (..) -- * Reset , Reset - , ResetKind (..) - , unsafeFromAsyncReset - , unsafeToAsyncReset + , ResetPolarity(..) , fromSyncReset - , unsafeToSyncReset + , syncPolarity + , toHighPolarity + , toLowPolarity + , unsafeFromReset + , unsafeToActiveHighReset + , unsafeToActiveLowReset , resetSynchronizer -- * Hidden clocks and resets -- $hiddenclockandreset @@ -100,8 +110,7 @@ module Clash.Signal -- * Simulation and testbench functions , clockGen , tbClockGen - , asyncResetGen - , syncResetGen + , resetGen , systemClockGen , tbSystemClockGen , systemResetGen @@ -109,13 +118,13 @@ module Clash.Signal , (.&&.), (.||.) -- * Product/Signal isomorphism , Bundle(..) - -- * Simulation functions (not synthesisable) + -- * Simulation functions (not synthesizable) , simulate , simulateB -- ** lazy versions , simulate_lazy , simulateB_lazy - -- * List \<-\> Signal conversion (not synthesisable) + -- * List \<-\> Signal conversion (not synthesizable) , sample , sampleN , fromList @@ -138,7 +147,7 @@ module Clash.Signal ) where -import GHC.TypeLits (KnownNat, KnownSymbol) +import GHC.TypeLits (KnownNat, KnownSymbol, AppendSymbol) import Data.Bits (Bits) -- Haddock only import Data.Maybe (isJust, fromJust) import Prelude @@ -190,7 +199,7 @@ arguments: It has a hidden clock when it has a: @ -f :: 'HiddenClock' domain gated => ... +f :: 'HiddenClock' tag enabled => ... @ Constraint. @@ -198,7 +207,7 @@ Constraint. Or it has a hidden reset when it has a: @ -g :: 'HiddenReset' domain synchronous => ... +g :: 'HiddenReset' tag polarity => ... @ Constraint. @@ -207,7 +216,7 @@ Or it has both a hidden clock argument and a hidden reset argument when it has a: @ -h :: 'HiddenClockReset' domain gated synchronous => .. +h :: 'HiddenClockReset' tag enabled polarity => .. @ Constraint. @@ -216,20 +225,20 @@ Given a component with an explicit clock and reset arguments, you can turn them into hidden arguments using 'hideClock' and 'hideReset'. So given a: @ -f :: Clock domain gated -> Reset domain synchronous -> Signal domain a -> ... +f :: Clock tag enabled -> Reset tag polarity -> Signal tag a -> ... @ You hide the clock and reset arguments by: @ --- g :: 'HiddenClockReset' domain gated synchronous => Signal domain a -> ... +-- g :: 'HiddenClockReset' tag enabled polarity => Signal tag a -> ... g = 'hideClockReset' f @ Or, alternatively, by: @ --- h :: HiddenClockReset domain gated synchronous => Signal domain a -> ... +-- h :: HiddenClockReset tag enabled polarity dom => Signal tag a -> ... h = f 'hasClock' 'hasReset' @ @@ -238,23 +247,23 @@ h = f 'hasClock' 'hasReset' Given a component: @ -f :: HiddenClockReset domain gated synchronous - => Signal domain Int - -> Signal domain Int +f :: HiddenClockReset tag enabled polarity dom + => Signal tag Int + -> Signal tag Int @ which has hidden clock and routed reset arguments, we expose those hidden arguments so that we can explicitly apply them: @ --- g :: Clock domain gated -> Reset domain synchronous -> Signal domain Int -> Signal domain Int +-- g :: Clock tag enabled -> Reset tag polarity -> Signal tag Int -> Signal tag Int g = 'exposeClockReset' f @ or, alternatively, by: @ --- h :: Clock domain gated -> Reset domain synchronous -> Signal domain Int -> Signal domain Int +-- h :: Clock tag enabled -> Reset tag polarity -> Signal tag Int -> Signal tag Int h clk rst = withClock clk rst f @ @@ -292,49 +301,61 @@ topEntity2 clk rst = -} +type HiddenClockName tag = AppendSymbol tag "_clk" +type HiddenResetName tag = AppendSymbol tag "_rst" + -- | A /constraint/ that indicates the component has a hidden 'Clock' -- --