diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,25 @@ # Changelog for the Clash project +## 1.8.5 *Mar 24th, 2026* + +Added: +* `Clash.Annotation.SynthesisAtrributes.annotateReg`, a function to add synthesis attributes (e.g. `ASYNC_REG`) to register declarations in the HDL generated by the Clash compiler. + [#3093](https://github.com/clash-lang/clash-compiler/pull/3093) +* `registerSyncReset` [#3115](https://github.com/clash-lang/clash-compiler/issues/3115) + +Fixed: +* The `Clash.Explicit.Verification.check` blackbox now correctly uses the given clock line, not assuming any longer that it is already bound to an identifier in the first place. [#2907](https://github.com/clash-lang/clash-compiler/issues/2907) +* The type of string literals passed to the `Clash.Explicit.Verification.check` blackbox now matches with the input provided via `Clash.Explicit.Verification.name`. [#2908](https://github.com/clash-lang/clash-compiler/issues/2908) +* `toInteger`, `toEnum`, and `fromEnum` now correctly sign extend when using Verilog backend. [#2729](https://github.com/clash-lang/clash-compiler/issues/2729). +* `dumpVCD` now properly aligns the first clock edges in multi-domain designs. [#3075](https://github.com/clash-lang/clash-compiler/issues/3075) +* Removed the limit on the number of traces in `dumpVCD`. Also removed unnecessary double newlines after 1-bit signals. [#3082](https://github.com/clash-lang/clash-compiler/issues/3082) +* In Clash simulation, `pack` for `Vec` and `RTree` had all bits undefined when the spine of the value had an `XException`. Now, those elements with defined bits will output those defined bits. In HDL, this was already the case. Example: consider `xs = 1 :> undefined :> Nil :: Vec 2 (Unsigned 4)` and `ys = 1 :> undefined :: Vec 2 (Unsigned 4)`. `xs` merely has an undefined element, but `ys` has an undefined spine: it is a `:>` constructor that is undefined. `pack ys` used to be `0b...._....` but is now `0b0001_....`, just as `pack xs` already was. + [#3114](https://github.com/clash-lang/clash-compiler/pull/3114) +* Clash drops cached normalization result. [#3109](https://github.com/clash-lang/clash-compiler/issues/3109) +* Fix `holdReset` glitch behavior for asynchronous resets and wrong hold cycles for sync resets. [#3115](https://github.com/clash-lang/clash-compiler/issues/3115) +* Do not emit source locations if `-g` is not passed to clash [#3132](https://github.com/clash-lang/clash-compiler/issues/3132) +* `clash-ghc`: Remove `Opt_LlvmTBAA` from unwanted flags [#2508](https://github.com/clash-lang/clash-compiler/issues/2823) + ## 1.8.4 *Nov 6th 2025* Changed: @@ -314,7 +334,7 @@ Added: * `Clash.Class.Counter`: a class that defines a odometer-style supercounter. [#1763](https://github.com/clash-lang/clash-compiler/pull/1763) * `isLike` function for BitPack types. [#1774](https://github.com/clash-lang/clash-compiler/pull/1774) - * 'seqErrorX' for catching both `XException` and `ErrorCall`. [#1774](https://github.com/clash-lang/clash-compiler/pull/1774) + * 'seqErrorX' for catching both `XException` and `ErrorCall`. [#1839](https://github.com/clash-lang/clash-compiler/pull/1839) * `Clash.Explicit.BlockRam.File.memFile`, a function for creating the contents of the data files this blockRAM uses. Can also be imported from `Clash.Prelude.BlockRam.File`, `Clash.Prelude.ROM.File` and `Clash.Explicit.ROM.File`. [#1840](https://github.com/clash-lang/clash-compiler/pull/1840) * Support for Yosys compatible SVA to `Clash.Verification`. This enables formal verification using SymbiYosis for Verilog and SystemVerilog. [#1798](https://github.com/clash-lang/clash-compiler/pull/1798) * `Clash.Explicit.Signal.Delayed.forward`, a function that can be used to retime a `DSignal` into the future without applying any logic. [#1882](https://github.com/clash-lang/clash-compiler/pull/1882) diff --git a/clash-prelude.cabal b/clash-prelude.cabal --- a/clash-prelude.cabal +++ b/clash-prelude.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: clash-prelude -Version: 1.8.4 +Version: 1.8.5 Synopsis: Clash: a functional hardware description language - Prelude library Description: Clash is a functional hardware description language that borrows both its @@ -344,9 +344,9 @@ deepseq >= 1.4.1.0 && < 1.6, extra >= 1.6.17 && < 1.9, ghc-prim >= 0.5.1.0 && < 0.13, - ghc-typelits-extra >= 0.4 && < 0.5, - ghc-typelits-knownnat >= 0.7.2 && < 0.8, - ghc-typelits-natnormalise >= 0.7.2 && < 0.8, + ghc-typelits-extra >= 0.4 && < 0.6, + ghc-typelits-knownnat >= 0.7.2 && < 0.9, + ghc-typelits-natnormalise >= 0.7.2 && < 0.10, hashable >= 1.2.1.0 && < 1.6, half >= 0.2.2.3 && < 1.0, infinite-list ^>= 0.1, @@ -389,7 +389,7 @@ build-depends: base, clash-prelude, - doctest-parallel >= 0.2 && < 0.4, + doctest-parallel >= 0.2 && < 0.5, filepath if arch(x86_64) && flag(workaround-ghc-mmap-crash) @@ -420,17 +420,21 @@ ghc-typelits-extra, base, + binary, bytestring, + containers, deepseq, hedgehog >= 1.0.3 && < 1.6, hint >= 0.7 && < 0.10, + mmorph >= 1.1.5 && < 1.3, quickcheck-classes-base >= 0.6 && < 1.0, tasty >= 1.2 && < 1.6, tasty-hedgehog >= 1.2.0, tasty-hunit, tasty-th, tasty-quickcheck, - template-haskell + template-haskell, + text Other-Modules: Clash.Tests.AsyncFIFOSynchronizer @@ -441,6 +445,7 @@ Clash.Tests.BlockRam.Blob Clash.Tests.Clocks Clash.Tests.Counter + Clash.Tests.DumpVCD Clash.Tests.DerivingDataRepr Clash.Tests.DerivingDataReprTypes Clash.Tests.Fixed diff --git a/src/Clash/Annotations/Primitive.hs b/src/Clash/Annotations/Primitive.hs --- a/src/Clash/Annotations/Primitive.hs +++ b/src/Clash/Annotations/Primitive.hs @@ -265,11 +265,11 @@ -- @ data Primitive = Primitive [HDL] FilePath - -- ^ Description of a primitive for a given 'HDL's in a file at 'FilePath' + -- ^ Description of a primitive for given 'HDL's in a file at 'FilePath' | InlinePrimitive [HDL] String - -- ^ Description of a primitive for a given 'HDL's as an inline JSON 'String' + -- ^ Description of a primitive for given 'HDL's as an inline JSON 'String' | InlineYamlPrimitive [HDL] String - -- ^ Description of a primitive for a given 'HDL's as an inline YAML 'String' + -- ^ Description of a primitive for given 'HDL's as an inline YAML 'String' deriving (Show, Read, Data, Generic, NFData, Hashable, Eq) -- | Primitive guard to mark a value as either not translatable or as having a diff --git a/src/Clash/Annotations/SynthesisAttributes.hs b/src/Clash/Annotations/SynthesisAttributes.hs --- a/src/Clash/Annotations/SynthesisAttributes.hs +++ b/src/Clash/Annotations/SynthesisAttributes.hs @@ -21,6 +21,7 @@ ( Attr(..) , Annotate , annotate + , annotateReg , markDebug ) where @@ -155,3 +156,92 @@ :> Attr "noprune" :> Attr "preserve" :> Nil + +{- | Add synthesis attributes to register declarations in the HDL generated by the Clash +compiler. + +For example, given the following code: + +> import Clash.Explicit.Prelude +> import Clash.Annotations.SynthesisAttributes +> +> topEntity :: +> Clock System -> +> Reset System -> +> Signal System Bool -> +> Signal System Bool +> topEntity clk rst x = +> let r1 = setName @"r1" (annotateReg attrs (dflipflop clk x)) +> r2 = setName @"r2" (annotateReg attrs (register clk rst enableGen False r1)) +> in r2 +> where +> attrs = Attr "ASYNC_REG" :> Nil + +The clash compiler would generate the following Verilog: + +> `default_nettype none +> `timescale 100fs/100fs +> module topEntity +> ( // Inputs +> input wire clk // clock +> , input wire rst // reset +> , input wire x +> +> // Outputs +> , output wire result +> ); +> (* ASYNC_REG *) reg r1 = ({1 {1'bx}}); +> (* ASYNC_REG *) reg r2 = 1'b0; +> +> // delay begin +> always @(posedge clk) begin : r1_delay +> r1 <= x; +> end +> // delay end +> +> // register begin +> always @(posedge clk or posedge rst) begin : r2_register +> if ( rst) begin +> r2 <= 1'b0; +> end else begin +> r2 <= r1; +> end +> end +> // register end +> +> assign result = r2; +> +> +> endmodule +> `default_nettype wire + +Where we can see that the /r1/ and /r2/ registers are given the specified +/ASYNC_REG/ attribute. + +The above pattern can also be abstracted over, e.g. you could write: + +> topEntity :: +> Clock System -> +> Reset System -> +> Signal System Bool -> +> Signal System Bool +> topEntity clk rst = +> markAsync @"r1" (dflipflop clk) . +> markAsync @"r2" (register clk rst enableGen False) +> +> markAsync :: +> forall (name :: Symbol) dom a . +> (Signal dom a -> Signal dom a) -> +> Signal dom a -> +> Signal dom a +> markAsync f = \x -> setName @name (annotateReg attrs (f x)) +> where +> attrs = Attr "ASYNC_REG" :> Nil +> {-# INLINE markAsync #-} + +And it will generate exactly the same Verilog as above. +-} +annotateReg :: forall n dom a . Vec n (Attr String) -> Signal dom a -> Signal dom a +annotateReg !_ x = x +{-# CLASH_OPAQUE annotateReg #-} +{-# ANN annotateReg hasBlackBox #-} diff --git a/src/Clash/Class/BitPack/Internal.hs b/src/Clash/Class/BitPack/Internal.hs --- a/src/Clash/Class/BitPack/Internal.hs +++ b/src/Clash/Class/BitPack/Internal.hs @@ -109,6 +109,10 @@ type BitSize a = (CLog 2 (GConstructorCount (Rep a))) + (GFieldSize (Rep a)) -- | Convert element of type @a@ to a 'BitVector' -- + -- @pack@ will never raise @XException@; as @BitVector@ is three-valued, + -- @pack@ applied to an @XException@ will return a @BitVector@ filled with + -- undefined bits. + -- -- >>> pack (-5 :: Signed 6) -- 0b11_1011 pack :: a -> BitVector (BitSize a) @@ -164,7 +168,7 @@ -- | Pack both arguments to a 'BitVector' and use -- 'Clash.Sized.Internal.BitVector.isLike#' to compare them. This is a more --- lentiant comparison than '(==)', behaving more like (but not necessarily +-- lenient comparison than '(==)', behaving more like (but not necessarily -- exactly the same as) @std_match@ in VHDL or @casez@ in Verilog. -- -- Unlike '(==)', isLike is not symmetric. The reason for this is that a diff --git a/src/Clash/Explicit/Reset.hs b/src/Clash/Explicit/Reset.hs --- a/src/Clash/Explicit/Reset.hs +++ b/src/Clash/Explicit/Reset.hs @@ -1,5 +1,5 @@ {-| -Copyright : (C) 2020-2023, QBayLogic B.V., +Copyright : (C) 2020-2026, QBayLogic B.V., 2022-2023, Google LLC License : BSD2 (see the file LICENSE) Maintainer : QBayLogic B.V. @@ -23,6 +23,7 @@ , resetGlitchFilter , resetGlitchFilterWithReset , unsafeResetGlitchFilter + , registerSyncReset , holdReset , convertReset , noReset @@ -399,12 +400,54 @@ SActiveHigh -> True SActiveLow -> False --- | Hold reset for a number of cycles relative to an incoming reset signal. +-- | Register a synchronous reset signal. -- +-- `registerSyncReset` delays an incoming reset by one clock cycle using a +-- register. This can be useful to break combinational paths involving reset +-- logic. +-- +-- __NB__: This is not a synchronizer. Use `resetSynchronizer` to synchronize +-- a reset. +-- +-- Example: +-- +-- >>> let sampleReset = sampleN 7 . unsafeToActiveHigh +-- >>> let rst = unsafeFromActiveHigh (fromList [False, True, False, False, True, False]) +-- >>> sampleReset (registerSyncReset @XilinxSystem clockGen rst enableGen True) +-- [True,False,True,False,False,True,False] +-- +registerSyncReset + :: forall dom + . KnownDomain dom + => HasSynchronousReset dom + => Clock dom + -> Reset dom + -> Enable dom + -> Bool + -- ^ Initial assert value of the register if supported by the domain. + -- If True the initial reset value is asserted. + -- If False the initial reset value is de-asserted. + -> Reset dom +registerSyncReset clk (unsafeFromReset -> rst) en initialValue = unsafeToReset outRst + where + intialRst :: Bool + intialRst = + case resetPolarity @dom of + SActiveHigh -> initialValue + SActiveLow -> not initialValue + outRst = delay clk en intialRst rst + +-- | Hold reset for a number of cycles relative to an incoming reset +-- signal. +-- +-- __NB__: The output of this function is combinational for @n > 0@ on domains +-- with a synchronous reset. Use `registerSyncReset` to add an output register if +-- desired. +-- -- Example: -- --- >>> let sampleWithReset = sampleN 8 . unsafeToActiveHigh --- >>> sampleWithReset (holdReset @System clockGen enableGen (SNat @2) (resetGenN (SNat @3))) +-- >>> let sampleReset = sampleN 8 . unsafeToActiveHigh +-- >>> sampleReset (holdReset @System clockGen enableGen (SNat @2) (resetGenN (SNat @3))) -- [True,True,True,True,True,False,False,False] -- -- 'holdReset' holds the reset for an additional 2 clock cycles for a total @@ -412,7 +455,7 @@ -- intermediate assertions of the reset signal: -- -- >>> let rst = fromList [True, False, False, False, True, False, False, False] --- >>> sampleWithReset (holdReset @System clockGen enableGen (SNat @2) (unsafeFromActiveHigh rst)) +-- >>> sampleReset (holdReset @System clockGen enableGen (SNat @2) (unsafeFromActiveHigh rst)) -- [True,True,True,False,True,True,True,False] -- holdReset @@ -427,11 +470,66 @@ -> Reset dom -- ^ Reset to extend -> Reset dom -holdReset clk en SNat rst = - unsafeFromActiveHigh ((/=maxBound) <$> counter) +holdReset clk en n rst = case resetKind @dom of + SSynchronous -> holdResetSync clk en n rst + SAsynchronous -> holdResetAsync clk en n rst + +holdResetSync + :: forall dom n + . KnownDomain dom + => DomainResetKind dom ~ 'Synchronous + => Clock dom + -> Enable dom + -- ^ Global enable + -> SNat n + -- ^ Hold for /n/ cycles + -> Reset dom + -- ^ Reset to extend + -> Reset dom +holdResetSync clk en sn@SNat rst = rstOut where - counter :: Signal dom (Index (n+1)) - counter = register clk rst en 0 (satSucc SatBound <$> counter) + rstOut = case snatToInteger sn of + 0 -> rst + 1 -> orReset rst (unsafeToReset regReset) + where + isActiveHigh = case resetPolarity @dom of { SActiveHigh -> True; _ -> False } + regReset = register clk rst en isActiveHigh (pure (not isActiveHigh)) + _ -> orReset rst (unsafeToReset rawRst) + where + counter :: Signal dom (Index (n + 1)) + counter = register clk rst en 0 (satSucc SatBound <$> counter) + rawRst :: Signal dom Bool + rawRst = case resetPolarity @dom of + SActiveHigh -> (/=maxBound) <$> counter + SActiveLow -> (==maxBound) <$> counter + +holdResetAsync + :: forall dom n + . KnownDomain dom + => DomainResetKind dom ~ 'Asynchronous + => Clock dom + -> Enable dom + -- ^ Global enable + -> SNat n + -- ^ Hold for /n/ cycles + -> Reset dom + -- ^ Reset to extend + -> Reset dom +holdResetAsync clk en sn@SNat rst = rstOut + where + isActiveHigh = case resetPolarity @dom of { SActiveHigh -> True; _ -> False } + rstOut = case toUNat sn of + UZero -> rst + USucc UZero -> unsafeToReset (register clk rst en isActiveHigh (pure (not isActiveHigh))) + USucc (USucc _) -> unsafeToReset (register clk rst en isActiveHigh rawRst) + where + counter :: Signal dom (Index n) + counter = register clk rst en 0 (satSucc SatBound <$> counter) + rawRst :: Signal dom Bool + rawRst = case resetPolarity @dom of + SActiveHigh -> (/=maxBound) <$> counter + SActiveLow -> (==maxBound) <$> counter + -- | Convert between different types of reset, adding a synchronizer when -- the domains are not the same. See 'resetSynchronizer' for further details diff --git a/src/Clash/Explicit/Synchronizer.hs b/src/Clash/Explicit/Synchronizer.hs --- a/src/Clash/Explicit/Synchronizer.hs +++ b/src/Clash/Explicit/Synchronizer.hs @@ -30,7 +30,7 @@ where import Data.Bits (complement, shiftR, xor) -import Data.Constraint ((:-)(..), Dict (..)) +import Data.Constraint ((:-)(Sub), Dict (..)) import Data.Constraint.Nat (leTrans) import Data.Maybe (isJust) import GHC.TypeLits (type (+), type (-), type (<=), type (^), KnownNat) diff --git a/src/Clash/Explicit/Verification.hs b/src/Clash/Explicit/Verification.hs --- a/src/Clash/Explicit/Verification.hs +++ b/src/Clash/Explicit/Verification.hs @@ -167,7 +167,7 @@ {-# INLINE nextN #-} -- | Same as @a && next b@ but with a nice syntax. E.g., @a && next b@ could --- be written as @a `before` b@. Might be read as "a happens one cycle before b". +-- be written as @a \`before\` b@. Might be read as "a happens one cycle before b". before :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom before a0 b0 = Assertion IsTemporal (CvBefore a1 b1) where @@ -175,8 +175,8 @@ b1 = assertion (toAssertionValue b0) {-# INLINE before #-} --- | Same as @a `implies` next b@ but with a nice syntax. E.g., --- @a `implies` next b@ could be written as @a `timplies` b@. Might be read +-- | Same as @a \`implies\` next b@ but with a nice syntax. E.g., +-- @a \`implies\` next b@ could be written as @a \`timplies\` b@. Might be read -- as "a at cycle n implies b at cycle n+1". timplies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom timplies a0 b0 = Assertion IsTemporal (CvTemporalImplies 1 a1 b1) diff --git a/src/Clash/Signal.hs b/src/Clash/Signal.hs --- a/src/Clash/Signal.hs +++ b/src/Clash/Signal.hs @@ -2,7 +2,7 @@ Copyright : (C) 2013-2016, University of Twente, 2016-2019, Myrtle Software Ltd, 2017 , Google Inc., - 2021-2023, QBayLogic B.V. + 2021-2026, QBayLogic B.V. License : BSD2 (see the file LICENSE) Maintainer : QBayLogic B.V. @@ -152,6 +152,7 @@ #endif , resetSynchronizer , resetGlitchFilter + , registerSyncReset , holdReset -- * Enabling , Enable @@ -2272,22 +2273,60 @@ hideClock (hideClock E.unsafeSynchronizer) #endif --- | Hold reset for a number of cycles relative to an implicit reset signal. +-- | Register a synchronous reset signal. -- +-- `registerSyncReset` delays an incoming reset by one clock cycle using a +-- register. This can be useful to break combinational paths involving reset +-- logic. +-- +-- __NB__: This is not a synchronizer. Use `resetSynchronizer` to synchronize +-- a reset. +-- +-- Example: +-- +-- >>> registerSyncResetBool = unsafeToActiveHigh . (registerSyncReset @XilinxSystem) +-- >>> let rst = unsafeFromActiveHigh (fromList [False, True, False, False, True, False]) +-- >>> sampleN 7 (exposeReset (registerSyncResetBool True) rst) +-- [True,False,True,False,False,True,False] +-- +registerSyncReset + :: forall dom + . HiddenClockResetEnable dom + => KnownDomain dom + => DomainResetKind dom ~ 'Synchronous + => Bool + -- ^ Initial assert value of the register if supported by the domain. + -- If True the initial reset value is asserted. + -- If False the initial reset value is de-asserted. + -> Reset dom +registerSyncReset initialValue = hideClockResetEnable E.registerSyncReset initialValue + +-- | Hold reset for a number of cycles relative to an incoming reset +-- signal. +-- +-- __NB__: The output of this function is combinational for @n > 1@ on domains +-- with a synchronous reset. Use `registerSyncReset` to add an output register if +-- desired. +-- -- Example: -- --- >>> sampleN @System 8 (unsafeToActiveHigh (holdReset (SNat @2))) --- [True,True,True,False,False,False,False,False] +-- >>> holdResetBool = unsafeToActiveHigh . (holdReset @System) +-- >>> sampleN 8 (exposeReset (holdResetBool (SNat @2)) (resetGenN (SNat @3))) +-- [True,True,True,True,True,False,False,False] -- -- 'holdReset' holds the reset for an additional 2 clock cycles for a total --- of 3 clock cycles where the reset is asserted. +-- of 5 clock cycles where the reset is asserted. 'holdReset' also works on +-- intermediate assertions of the reset signal: -- +-- >>> let rst = fromList [True, False, False, False, True, False, False, False] +-- >>> sampleN 8 (exposeReset (holdResetBool (SNat @2)) (unsafeFromActiveHigh rst)) +-- [True,True,True,False,True,True,True,False] +-- holdReset :: forall dom m . HiddenClockResetEnable dom => SNat m - -- ^ Hold for /m/ cycles, counting from the moment the incoming reset - -- signal becomes deasserted. + -- ^ Hold for /m/ cycles -> Reset dom holdReset m = hideClockResetEnable (\clk rst en -> E.holdReset clk en m rst) diff --git a/src/Clash/Signal/Internal.hs b/src/Clash/Signal/Internal.hs --- a/src/Clash/Signal/Internal.hs +++ b/src/Clash/Signal/Internal.hs @@ -1367,7 +1367,7 @@ -- | The above type is a generalization for: -- -- @ --- __(.||.)__ :: 'Clash.Signal.Signal' 'Bool' -> 'Clash.Signal.Signal' 'Bool' -> 'Clash.Signal.Signal' 'Bool' +-- __(.||.)__ :: 'Clash.Signal.Signal' dom 'Bool' -> 'Clash.Signal.Signal' dom 'Bool' -> 'Clash.Signal.Signal' dom 'Bool' -- @ -- -- It is a version of ('||') that returns a 'Clash.Signal.Signal' of 'Bool' @@ -1378,7 +1378,7 @@ -- | The above type is a generalization for: -- -- @ --- __(.&&.)__ :: 'Clash.Signal.Signal' 'Bool' -> 'Clash.Signal.Signal' 'Bool' -> 'Clash.Signal.Signal' 'Bool' +-- __(.&&.)__ :: 'Clash.Signal.Signal' dom 'Bool' -> 'Clash.Signal.Signal' dom 'Bool' -> 'Clash.Signal.Signal' dom 'Bool' -- @ -- -- It is a version of ('&&') that returns a 'Clash.Signal.Signal' of 'Bool' @@ -1544,7 +1544,7 @@ -- | The above type is a generalization for: -- -- @ --- __mux__ :: 'Clash.Signal.Signal' 'Bool' -> 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' a +-- __mux__ :: 'Clash.Signal.Signal' dom 'Bool' -> 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom a -- @ -- -- A multiplexer. Given "@'mux' b t f@", output @t@ when @b@ is 'True', and @f@ @@ -1557,7 +1557,7 @@ -- | The above type is a generalization for: -- -- @ --- __(.==.)__ :: 'Eq' a => 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' 'Bool' +-- __(.==.)__ :: 'Eq' a => 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom 'Bool' -- @ -- -- It is a version of ('==') that returns a 'Clash.Signal.Signal' of 'Bool' @@ -1568,7 +1568,7 @@ -- | The above type is a generalization for: -- -- @ --- __(./=.)__ :: 'Eq' a => 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' 'Bool' +-- __(./=.)__ :: 'Eq' a => 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom 'Bool' -- @ -- -- It is a version of ('/=') that returns a 'Clash.Signal.Signal' of 'Bool' @@ -1579,7 +1579,7 @@ -- | The above type is a generalization for: -- -- @ --- __(.<.)__ :: 'Ord' a => 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' 'Bool' +-- __(.<.)__ :: 'Ord' a => 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom 'Bool' -- @ -- -- It is a version of ('<') that returns a 'Clash.Signal.Signal' of 'Bool' @@ -1590,7 +1590,7 @@ -- | The above type is a generalization for: -- -- @ --- __(.<=.)__ :: 'Ord' a => 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' 'Bool' +-- __(.<=.)__ :: 'Ord' a => 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom 'Bool' -- @ -- -- It is a version of ('GHC.TypeNats.<=') that returns a 'Clash.Signal.Signal' of 'Bool' @@ -1601,7 +1601,7 @@ -- | The above type is a generalization for: -- -- @ --- __(.>.)__ :: 'Ord' a => 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' 'Bool' +-- __(.>.)__ :: 'Ord' a => 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom 'Bool' -- @ -- -- It is a version of ('>') that returns a 'Clash.Signal.Signal' of 'Bool' @@ -1612,7 +1612,7 @@ -- | The above type is a generalization for: -- -- @ --- __(.>=.)__ :: 'Ord' a => 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' 'Bool' +-- __(.>=.)__ :: 'Ord' a => 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom a -> 'Clash.Signal.Signal' dom 'Bool' -- @ -- -- It is a version of ('>=') that returns a 'Clash.Signal.Signal' of 'Bool' @@ -1635,7 +1635,7 @@ -- | The above type is a generalization for: -- -- @ --- __testFor__ :: 'Int' -> 'Clash.Signal.Signal' Bool -> 'Property' +-- __testFor__ :: 'Int' -> 'Clash.Signal.Signal' dom Bool -> 'Property' -- @ -- -- @testFor n s@ tests the signal @s@ for @n@ cycles. @@ -1649,7 +1649,7 @@ -- | The above type is a generalization for: -- -- @ --- __sample__ :: 'Clash.Signal.Signal' a -> [a] +-- __sample__ :: 'Clash.Signal.Signal' dom a -> [a] -- @ -- -- Get an infinite list of samples from a 'Clash.Signal.Signal' @@ -1666,7 +1666,7 @@ -- | The above type is a generalization for: -- -- @ --- __sampleN__ :: Int -> 'Clash.Signal.Signal' a -> [a] +-- __sampleN__ :: Int -> 'Clash.Signal.Signal' dom a -> [a] -- @ -- -- Get a list of @n@ samples from a 'Clash.Signal.Signal' @@ -1694,7 +1694,7 @@ -- * Simulation functions (not synthesizable) --- | Simulate a (@'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' b@) function +-- | Simulate a (@'Clash.Signal.Signal' dom1 a -> 'Clash.Signal.Signal' dom2 b@) function -- given a list of samples of type @a@ -- -- >>> simulate (register systemClockGen resetGen enableGen 8) [1, 1, 2, 3] @@ -1708,7 +1708,7 @@ -- | The above type is a generalization for: -- -- @ --- __sample__ :: 'Clash.Signal.Signal' a -> [a] +-- __sample__ :: 'Clash.Signal.Signal' dom a -> [a] -- @ -- -- Get an infinite list of samples from a 'Clash.Signal.Signal' @@ -1725,7 +1725,7 @@ -- | The above type is a generalization for: -- -- @ --- __sampleN__ :: Int -> 'Clash.Signal.Signal' a -> [a] +-- __sampleN__ :: Int -> 'Clash.Signal.Signal' dom a -> [a] -- @ -- -- Get a list of @n@ samples from a 'Clash.Signal.Signal' @@ -1753,7 +1753,7 @@ -- * Simulation functions (not synthesizable) --- | Simulate a (@'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' b@) function +-- | Simulate a (@'Clash.Signal.Signal' dom1 a -> 'Clash.Signal.Signal' dom2 b@) function -- given a list of samples of type @a@ -- -- >>> simulate (register systemClockGen resetGen enableGen 8) [1, 1, 2, 3] diff --git a/src/Clash/Signal/Trace.hs b/src/Clash/Signal/Trace.hs --- a/src/Clash/Signal/Trace.hs +++ b/src/Clash/Signal/Trace.hs @@ -1,7 +1,7 @@ {-| Copyright : (C) 2018, Google Inc. 2019, Myrtle Software Ltd - 2022-2024, QBayLogic B.V. + 2022-2026, QBayLogic B.V. License : BSD2 (see the file LICENSE) Maintainer : QBayLogic B.V. @@ -49,6 +49,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} @@ -73,6 +74,14 @@ -- * Internal -- ** Types + , VCDFile(..) + , VCDTime + , IDCode + , TimeUnit(..) + , DeclarationCommand(..) + , Var(..) + , SimulationCommand(..) + , ValueChange(..) , Period , Changed , Value @@ -83,7 +92,8 @@ , traceSignal# , traceVecSignal# , dumpVCD# - , dumpVCD## + , dumpVCD0# + , dumpVCD1# , waitForTraces# , traceMap# ) where @@ -115,6 +125,7 @@ import Data.List (foldl') #endif import Data.List (foldl1', unzip4, transpose, uncons) +import Data.List.Extra (snoc) import qualified Data.Map.Strict as Map import Data.Maybe (fromMaybe, catMaybes) import qualified Data.Text as Text @@ -318,6 +329,50 @@ {-# CLASH_OPAQUE traceVecSignal1 #-} {-# ANN traceVecSignal1 hasBlackBox #-} +data VCDFile = VCDFile [DeclarationCommand] [SimulationCommand] + deriving (Show) + +type VCDTime = Int + +type IDCode = String + +data TimeUnit = S | MS | US | NS | PS | FS + +instance Show TimeUnit where + showsPrec _ S = ('s' :) + showsPrec _ MS = showString "ms" + showsPrec _ US = showString "us" + showsPrec _ NS = showString "ns" + showsPrec _ PS = showString "ps" + showsPrec _ FS = showString "fs" + +data DeclarationCommand + = TimeScale VCDTime TimeUnit + | Vars [Var] + deriving (Show) + +data Var + = Var + { varSize :: Width + , varIDCode :: IDCode + , varReference :: String + } + deriving (Show) + +data SimulationCommand + = DumpVars [ValueChange] + | SimulationTime VCDTime + | SimulationValueChange ValueChange + deriving (Show, Eq) + +data ValueChange + = ValueChange + { changeSize :: Width + , changeIDCode :: IDCode + , changeValue :: Value + } + deriving (Show, Eq) + iso8601Format :: UTCTime -> String iso8601Format = formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" @@ -335,45 +390,43 @@ printable :: Char -> Bool printable (ord -> c) = 33 <= c && c <= 126 --- | Same as @dumpVCD@, but supplied with a custom tracemap and a custom timestamp -dumpVCD## +-- | Worker for @dumpVCD0#@, containing all the actual work and producing a +-- 'VCDFile' representation of the VCD output +dumpVCD1# :: (Int, Int) -- ^ (offset, number of samples) -> TraceMap - -> UTCTime - -> Either String Text.Text -dumpVCD## (offset, cycles) traceMap now + -> Either String VCDFile +dumpVCD1# (offset, cycles) traceMap | offset < 0 = error $ "dumpVCD: offset was " ++ show offset ++ ", but cannot be negative." | cycles < 0 = error $ "dumpVCD: cycles was " ++ show cycles ++ ", but cannot be negative." | null traceMap = error $ "dumpVCD: no traces found. Extend the given trace names." - | Map.size traceMap > 126 - 33 = - Left $ "Tracemap contains more than 93 traces, which is not supported by VCD." | (nm:_) <- offensiveNames = Left $ unwords [ "Trace '" ++ nm ++ "' contains" , "non-printable ASCII characters, which is not" , "supported by VCD." ] | otherwise = - Right $ Text.unlines [ Text.unwords headerDate - , Text.unwords headerVersion - , Text.unwords headerComment - , Text.pack $ unwords headerTimescale - , "$scope module logic $end" - , Text.intercalate "\n" headerWires - , "$upscope $end" - , "$enddefinitions $end" - , "#0" - , "$dumpvars" - , Text.intercalate "\n" initValues - , "$end" - , Text.intercalate "\n" $ catMaybes bodyParts - ] + Right + ( VCDFile + [ TimeScale timescale PS + , Vars [Var w l n | (w, l, n) <- zip3 widths labels traceNames] + ] + ( [ SimulationTime 0 + , DumpVars initValues + ] + ++ concat (catMaybes bodyParts) + ) + ) where offensiveNames = filter (any (not . printable)) traceNames - labels = map chr [33..126] + -- Generate labels in the pattern a,b,c,aa,ab,ac,ba,bb,bc,ca,cb,cc,aaa,... + labels = concatMap (\s -> map (snoc s) alphabet) ([]: labels) + where + alphabet = map chr [33..126] timescale = foldl1' gcd (Map.keys periodMap) periodMap = toPeriodMap traceMap @@ -398,63 +451,126 @@ periods' = map (`quot` timescale) periods valuess' = map slice $ zipWith normalize periods' valuess - normalize period values = concatMap (replicate period) values + normalize period (initial:values) = initial : concatMap (replicate period) values + normalize _ [] = [] slice values = drop offset $ take cycles values - headerDate = ["$date", Text.pack $ iso8601Format now, "$end"] - -#ifdef CABAL - clashVer = Data.Version.showVersion Paths_clash_prelude.version -#else - clashVer = "development" -#endif - headerVersion = ["$version", "Generated by Clash", Text.pack clashVer , "$end"] - headerComment = ["$comment", "No comment", "$end"] - headerTimescale = ["$timescale", (show timescale) ++ "ps", "$end"] - headerWires = [ Text.unwords $ headerWire w l n - | (w, l, n) <- (zip3 widths labels traceNames)] - headerWire w l n = map Text.pack ["$var wire", show w, [l], n, "$end"] - initValues = map Text.pack $ zipWith ($) formatters inits + initValues = zipWith ($) formatters inits - formatters = zipWith format widths labels + formatters = zipWith ValueChange widths labels inits = map (maybe (error "dumpVCD##: empty value") fst . uncons) valuess' tails = map changed valuess' - -- | Format single value according to VCD spec - format :: Width -> Char -> Value -> String - format 1 label (0,0) = ['0', label, '\n'] - format 1 label (0,1) = ['1', label, '\n'] - format 1 label (1,_) = ['x', label, '\n'] - format 1 label (mask,val) = - error $ "Can't format 1 bit wide value for " ++ show label ++ ": value " ++ show val ++ " and mask " ++ show mask - format n label (mask,val) = - "b" ++ map digit (reverse [0..n-1]) ++ " " ++ [label] - where - digit d = case (testBit mask d, testBit val d) of - (False,False) -> '0' - (False,True) -> '1' - (True,_) -> 'x' - - -- | Given a list of values, return a list of list of bools indicating + -- Given a list of values, return a list of list of bools indicating -- if a value changed. The first value is *not* included in the result. changed :: [Value] -> [(Changed, Value)] changed (s:ss) = zip (zipWith (/=) (s:ss) ss) ss changed [] = [] - bodyParts :: [Maybe Text.Text] - bodyParts = zipWith go [0..] (map bodyPart (Data.List.transpose tails)) - where - go :: Int -> Maybe Text.Text -> Maybe Text.Text - go (Text.pack . show -> n) t = - let pre = Text.concat ["#", n, "\n"] in - fmap (Text.append pre) t + bodyParts :: [Maybe [SimulationCommand]] + bodyParts = zipWith go [0 ..] (map bodyPart (Data.List.transpose tails)) + where + go :: VCDTime -> Maybe [SimulationCommand] -> Maybe [SimulationCommand] + go t vc = fmap (SimulationTime t :) vc - bodyPart :: [(Changed, Value)] -> Maybe Text.Text + bodyPart :: [(Changed, Value)] -> Maybe [SimulationCommand] bodyPart values = - let formatted = [(c, f v) | (f, (c,v)) <- zip formatters values] - formatted' = map (Text.pack . snd) $ filter fst $ formatted in - if null formatted' then Nothing else Just $ Text.intercalate "\n" formatted' + let + formatted = [(c, SimulationValueChange (f v)) | (f, (c, v)) <- zip formatters values] + formatted' = map snd $ filter fst $ formatted + in + if null formatted' then Nothing else Just formatted' +-- | Same as @dumpVCD@, but supplied with a custom tracemap and a custom timestamp +dumpVCD0# + :: (Int, Int) + -- ^ (offset, number of samples) + -> TraceMap + -> UTCTime + -> Either String Text.Text +dumpVCD0# slice traceMap now = + fmap renderVCD (dumpVCD1# slice traceMap) + where + renderVCD (VCDFile decCmds simCmds) = + Text.unlines $ + [ Text.unwords headerDate + , Text.unwords headerVersion + , Text.unwords headerComment + ] + ++ renderDecCmds decCmds + ++ "$enddefinitions $end" + : renderSimCmds simCmds + + renderDecCmds [] = [] + renderDecCmds ((TimeScale s u) : cmds) = + [ Text.unwords + [ "$timescale" + , Text.pack $ shows s $ show u + , "$end" + ] + ] + ++ renderDecCmds cmds + renderDecCmds ((Vars vs) : cmds) = + [ "$scope module logic $end" + , Text.intercalate "\n" (map renderVar vs) + , "$upscope $end" + ] + ++ renderDecCmds cmds + + renderVar Var{..} = + (Text.unwords . map Text.pack) + [ "$var wire" + , show varSize + , varIDCode + , varReference + , "$end" + ] + + renderSimCmds [] = [] + renderSimCmds ((DumpVars vars) : cmds) = + "$dumpvars" + : map renderValueChange vars + ++ "$end" + : renderSimCmds cmds + renderSimCmds ((SimulationTime t) : cmds) = + Text.pack ('#' : show t) : renderSimCmds cmds + renderSimCmds ((SimulationValueChange vc) : cmds) = + renderValueChange vc : renderSimCmds cmds + + renderValueChange (ValueChange 1 idCode (0, 0)) = + Text.pack $ '0' : idCode + renderValueChange (ValueChange 1 idCode (0, 1)) = + Text.pack $ '1' : idCode + renderValueChange (ValueChange 1 idCode (1, _)) = + Text.pack $ 'x' : idCode + renderValueChange (ValueChange 1 idCode (mask, val)) = + error $ + "Can't format 1 bit wide value for " + ++ show idCode + ++ ": value " + ++ show val + ++ " and mask " + ++ show mask + renderValueChange ValueChange{..} = + Text.pack $ 'b' : map digit (reverse [0 .. changeSize - 1]) ++ [' '] ++ changeIDCode + where + (mask, val) = changeValue + digit d = case (testBit mask d, testBit val d) of + (False,False) -> '0' + (False,True) -> '1' + (True,_) -> 'x' + + headerDate = ["$date", Text.pack $ iso8601Format now, "$end"] + +#ifdef CABAL + clashVer = Data.Version.showVersion Paths_clash_prelude.version +#else + clashVer = "development" +#endif + + headerVersion = ["$version", "Generated by Clash", Text.pack clashVer , "$end"] + headerComment = ["$comment", "No comment", "$end"] + -- | Same as @dumpVCD@, but supplied with a custom tracemap dumpVCD# :: NFDataX a @@ -470,7 +586,7 @@ dumpVCD# traceMap slice signal traceNames = do waitForTraces# traceMap signal traceNames m <- readIORef traceMap - fmap (dumpVCD## slice m) getCurrentTime + fmap (dumpVCD0# slice m) getCurrentTime -- | Produce a four-state VCD (Value Change Dump) according to IEEE -- 1364-{1995,2001}. This function fails if a trace name contains either @@ -519,7 +635,7 @@ -- | Take a serialized signal (dumped with @dumpReplayable@) and convert it -- back into a signal. Will error if dumped type does not match requested -- type. The first value in the signal that fails to decode will stop the --- decoding process and yield an error. Not that this always happens if you +-- decoding process and yield an error. Note that this always happens if you -- evaluate more values than were originally dumped. replay :: forall a dom n diff --git a/src/Clash/Sized/RTree.hs b/src/Clash/Sized/RTree.hs --- a/src/Clash/Sized/RTree.hs +++ b/src/Clash/Sized/RTree.hs @@ -81,7 +81,7 @@ import Test.QuickCheck (Arbitrary (..), CoArbitrary (..)) import Clash.Annotations.Primitive (hasBlackBox) -import Clash.Class.BitPack (BitPack (..), packXWith) +import Clash.Class.BitPack (BitPack (..)) import Clash.Promoted.Nat (SNat (..), UNat (..), pow2SNat, snatToNum, subSNat, toUNat) import Clash.Promoted.Nat.Literals (d1) @@ -223,7 +223,7 @@ instance (KnownNat d, BitPack a) => BitPack (RTree d a) where type BitSize (RTree d a) = (2^d) * (BitSize a) - pack = packXWith (pack . t2v) + pack = pack . t2v . lazyT unpack = v2t . unpack type instance Lens.Index (RTree d a) = Int @@ -310,13 +310,13 @@ populationCount' = tfold (resize . bv2i . pack) add . v2t . bv2v :} :... - • Couldn't match type: (((2 ^ d) + 1) + ((2 ^ d) + 1)) - 1 - with: (2 ^ d) + 1 +... Expected: Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) Actual: Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) -> AResult (Index ((2 ^ d) + 1)) (Index ((2 ^ d) + 1)) +... • In the second argument of ‘tfold’, namely ‘add’ In the first argument of ‘(.)’, namely ‘tfold (resize . bv2i . pack) add’ @@ -334,13 +334,13 @@ :} :... - • Couldn't match type: (((2 ^ d) + 1) + ((2 ^ d) + 1)) - 1 - with: (2 ^ d) + 1 +... Expected: Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) Actual: Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) -> AResult (Index ((2 ^ d) + 1)) (Index ((2 ^ d) + 1)) +... • In the second argument of ‘tfold’, namely ‘add’ In the first argument of ‘(.)’, namely ‘tfold (resize . bv2i . pack) add’ @@ -357,8 +357,7 @@ :} :... - • Couldn't match type ‘(((2 ^ d) + 1) + ((2 ^ d) + 1)) - 1’ - with ‘(2 ^ d) + 1’ +... Expected type: Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) Actual type: Index ((2 ^ d) + 1) diff --git a/src/Clash/Sized/Vector.hs b/src/Clash/Sized/Vector.hs --- a/src/Clash/Sized/Vector.hs +++ b/src/Clash/Sized/Vector.hs @@ -103,7 +103,7 @@ import Control.DeepSeq (NFData (..)) import qualified Control.Lens as Lens hiding (pattern (:>), pattern (:<)) import Data.Bits ((.|.), shiftL) -import Data.Constraint ((:-)(..), Dict (..)) +import Data.Constraint ((:-)(Sub), Dict (..)) import Data.Constraint.Nat (leZero) import Data.Data (Data (..), Constr, DataType, Fixity (..), Typeable, mkConstr, mkDataType) @@ -153,7 +153,7 @@ import Clash.Sized.Internal.BitVector (Bit, BitVector (..), split#) import Clash.Sized.Index (Index) -import Clash.Class.BitPack (packXWith, BitPack (..)) +import Clash.Class.BitPack (BitPack (..)) import Clash.XException (ShowX (..), NFDataX (..), seqX, isX) {- $setup @@ -2680,7 +2680,7 @@ instance (KnownNat n, BitPack a) => BitPack (Vec n a) where type BitSize (Vec n a) = n * (BitSize a) - pack = packXWith (concatBitVector# . map pack) + pack = concatBitVector# . map pack . lazyV unpack = map unpack . unconcatBitVector# concatBitVector# diff --git a/src/Clash/Verification.hs b/src/Clash/Verification.hs --- a/src/Clash/Verification.hs +++ b/src/Clash/Verification.hs @@ -52,6 +52,8 @@ import Clash.Verification.Internal import Data.Text (Text) +-- | Print property as PSL/SVA in HDL. Clash simulation support not yet +-- implemented. check :: ( KnownDomain dom , HiddenClock dom @@ -65,6 +67,8 @@ -> Signal dom AssertionResult check = EV.check hasClock hasReset +-- | Same as 'check', but doesn't require a design to explicitly carried to +-- top-level. checkI :: ( KnownDomain dom , HiddenClock dom diff --git a/src/Clash/XException.hs b/src/Clash/XException.hs --- a/src/Clash/XException.hs +++ b/src/Clash/XException.hs @@ -558,7 +558,7 @@ instance NFDataX b => NFDataX (a -> b) where deepErrorX = pure . deepErrorX rnfX = rwhnfX - hasUndefined = error "hasUndefined on Undefined (a -> b): Not Yet Implemented" + hasUndefined = error "hasUndefined on NFDataX (a -> b): Not Yet Implemented" ensureSpine = id instance NFDataX a => NFDataX (Down a) where diff --git a/tests/Clash/Tests/BitPack.hs b/tests/Clash/Tests/BitPack.hs --- a/tests/Clash/Tests/BitPack.hs +++ b/tests/Clash/Tests/BitPack.hs @@ -9,8 +9,11 @@ import Test.Tasty.HUnit import Clash.Class.BitPack -import Clash.Sized.Vector +import Clash.Sized.RTree import Clash.Sized.Signed +import Clash.Sized.Unsigned +import Clash.Sized.Vector +import Clash.XException import GHC.Generics (Generic) @@ -26,6 +29,24 @@ rtt :: (Eq a, Show a, BitPack a) => a -> Assertion rtt u = unpack (pack u) @?= u +{- +@pack@ will still output defined elements even if the spine is not fully defined. +-} +undefSpineVec :: Assertion +undefSpineVec = showX (pack v) @?= "0b0001_...._...." + where + v :: Vec 3 (Unsigned 4) + v = 1 :> Clash.XException.undefined + +{- +@pack@ will still output defined elements even if the spine is not fully defined. +-} +undefSpineRTree :: Assertion +undefSpineRTree = showX (pack t) @?= "0b...._...._0101_...." + where + t :: RTree 2 (Unsigned 4) + t = BR Clash.XException.undefined (BR (LR 5) Clash.XException.undefined) + tests :: TestTree tests = testGroup @@ -46,7 +67,8 @@ , testCase "SP2" (rtt (P 10)) , testCase "Rec1" (rtt (Rec1 10)) , testCase "Rec2" (rtt (Rec2 10 30)) - , testCase "Vec" (rtt ((1 :: Signed 6) :> 2 :> (-5) :> 4 :> Nil)) ] + , testCase "Vec" (rtt ((1 :: Signed 6) :> 2 :> (-5) :> 4 :> Nil)) + , testCase "undefSpineVec" undefSpineVec + , testCase "undefSpineRTree" undefSpineRTree ] - diff --git a/tests/Clash/Tests/DumpVCD.hs b/tests/Clash/Tests/DumpVCD.hs new file mode 100644 --- /dev/null +++ b/tests/Clash/Tests/DumpVCD.hs @@ -0,0 +1,260 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} + +module Clash.Tests.DumpVCD where + +import Control.Monad (foldM) +import Control.Monad.Morph (generalize, hoist) +import Data.Binary (encode) +import Data.Map.Strict (Map) +import Data.Maybe (isJust) +import GHC.Stack (HasCallStack, withFrozenCallStack) +import Test.Tasty +import Test.Tasty.Hedgehog (testPropertyNamed) +import Type.Reflection (typeRep) + +import Clash.Signal.Trace +import Clash.Sized.BitVector (BitVector, size#) +import Hedgehog.Extra (LockstepWalk (..), combinations, lockstepWalk) + +import qualified Data.List as L +import qualified Data.Map.Strict as Map +import qualified Hedgehog as H +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +type SignalData = BitVector 32 + +failWithMsg :: (H.MonadTest m, HasCallStack) => String -> m a +failWithMsg msg = withFrozenCallStack $ H.annotate msg >> H.failure + +data Metadata + = Metadata + { timeScale :: VCDTime + , nameMap :: Map String IDCode + } + deriving (Show) + +parseMetadata :: + [DeclarationCommand] -> + Either String Metadata +parseMetadata dcs = go Nothing Nothing dcs + where + go Nothing m (TimeScale t u : dcs0) = do + let + scale u0 = + case u0 of + S -> (* 1000) <$> scale MS + MS -> (* 1000) <$> scale US + US -> (* 1000) <$> scale NS + NS -> (* 1000) <$> scale PS + PS -> Right t + FS -> Left "$timescale fs unsupported; raw time in ps" + t0 <- scale u + go (Just t0) m dcs0 + go ts Nothing (Vars vs : dcs0) = do + map0 <- goVars Map.empty vs + go ts (Just map0) dcs0 + go (Just ts) (Just m) [] = Right $ Metadata ts m + go Nothing _ [] = Left "No $timescale in declarations" + go _ Nothing [] = Left "No $scope section in declarations" + go _ _ (TimeScale _ _ : _) = Left "Multiple $timescale sections in declarations" + go _ _ (Vars _ : _) = + -- This is not an error in VCD files, but we don't emit it so we don't handle it. + Left "Don't know what to do with multiple $scope sections in declarations" + + goVars map0 [] = Right map0 + goVars map0 (Var{..} : vs) + | Map.member varReference map0 = + Left $ "Duplicate $var section for variable named " <> show varReference + | otherwise = goVars (Map.insert varReference varIDCode map0) vs + +-- Are time stamps in order? Do they start at 0? Is every time stamp followed by actual +-- data? +-- +-- We exploit knowledge about how @dumpVCD@ formats the resulting file. The @fixedStart@ +-- is not mandated by VCD, it's just what @dumpVCD@ currently outputs. +saneTimestamps :: + (H.MonadTest m) => + LockstepWalk m SimulationCommand +saneTimestamps = LockstepWalk $ fixedStart (0 :: Int) [] + where + fixedStart 3 [SimulationTime t0, DumpVars _, SimulationTime t1] end sc = do + H.diff t1 (>=) 0 + H.diff t0 (<) t1 + go True t1 end sc + fixedStart 3 starts _ _ = + failWithMsg $ + "Simulation doesn't start with proper $dumpvars\n\n" + <> "The simulation starts with:\n" + <> show starts + fixedStart n starts False sc = pure $ LockstepWalk $ fixedStart (n + 1) (starts ++ [sc]) + fixedStart _ _ True _ = failWithMsg "Simulation ends prematurely" + + go _ t0 _ (SimulationValueChange _) = pure $ LockstepWalk $ go False t0 + go False t0 False (SimulationTime t1) = H.diff t0 (<) t1 >> pure (LockstepWalk $ go True t1) + go True t0 _ (SimulationTime _) = + failWithMsg $ "At time " <> show t0 <> ": Timestamp without change data" + go _ _ True sc@(SimulationTime _) = + -- A simulation can't end with a timestamp, a timestamp is always followed by values. + failWithMsg $ "The final simulation command is " <> show sc + go _ _ _ (DumpVars _) = + -- This is not an error in VCD files, but we don't emit it so we don't handle it. + failWithMsg $ "Don't know what to do with multiple $dumpvars sections" + +-- The signal changes every period. Are all the samples there, and are there no extra +-- samples? +signalCorrect :: + forall m. + (H.MonadTest m, HasCallStack) => + String -> + IDCode -> + VCDTime -> + VCDTime -> + [Value] -> + LockstepWalk m SimulationCommand +signalCorrect name idCode period end es = LockstepWalk initF + where + initF _ (SimulationTime t) = + pure $ LockstepWalk $ go t (zip (-1 : [0, period .. end]) es) + initF _ sc = + failWithMsg $ "First simulation command is not SimulationTime but " <> show sc + + go t es0 lastC (SimulationValueChange (ValueChange _ idCode0 v)) + | idCode /= idCode0 = checkFinal lastC es0 >> pure (LockstepWalk $ go t es0) + | otherwise = do + es1 <- parseChange t es0 idCode0 v + checkFinal lastC es1 + pure $ LockstepWalk $ go t es1 + go _ es0 _ (SimulationTime t) = pure $ LockstepWalk $ go t es0 + go t es0 _ (DumpVars vars) = do + es2 <- + foldM + (\es1 (ValueChange _ idCode0 val) -> parseChange t es1 idCode0 val) + es0 + vars + pure $ LockstepWalk $ go t es2 + + checkFinal False _ = pure () + checkFinal True ((t, _) : _) = do + annotateSignal + failWithMsg $ "Sample at time " <> show t <> " never came" + checkFinal True _ = pure () + + parseChange _ es0 idCode0 _ + | idCode /= idCode0 = pure es0 + parseChange t (e : es1) _ v + | (t, v) == e = pure es1 + | otherwise = do + annotateSignal + (t, v) H.=== e + H.failure + parseChange _ [] _ _ = do + annotateSignal + failWithMsg $ "Too many samples in VCD file" + + annotateSignal :: (HasCallStack) => m () + annotateSignal = + withFrozenCallStack $ + H.annotate $ + "Signal name: " + <> show name + <> "\n" + <> "Signal identifier code: " + <> show idCode + +{- | Check timing of individual signals when tracing multiple domains + +If we have multiple signals, each with their own period, that change every sample, does +the resulting VCD contain all the samples at the right times, and do timestamps and value +changes strictly alternate? + +This test would have caught the issue that PR #3076 fixed, and serves as a good +basic sanity check of VCD generation. +-} +multiDomainTrace :: H.Property +multiDomainTrace = + H.property $ + -- By default, property tests run in @PropertyT IO@. But we do a /lot/ of binds, and + -- I'm unsure whether binds have an inherent cost in 'IO'. It doesn't seem like it, + -- but running in 'IO' also doesn't give us anything. + -- So we run in @PropertyT Identity@ instead. + hoist generalize $ do + -- It seems silly to test a single signal, but we do want it as a shrink option just + -- in case the error occurs even for a single signal. + k <- + H.forAll $ + Gen.shrink (\x -> if x > 1 then [1] else []) $ + Gen.int $ + Range.linear 2 4 + -- @common@ scales all periods by a common power of ten factor + common <- H.forAll $ fmap (10 ^) $ Gen.integral_ $ Range.constant (0 :: Int) 4 + -- Interesting behavior of multiple signals is captured by the relation between them. + -- The relation is defined by the ratios between the periods, which depends only on + -- the prime factors they do not share. Hence, primes are excellent candidates. It + -- feels prudent to also include 1 as the other extreme, where for /every/ sample of + -- a slower signal, there is also a new sample of the fastest signal. + periodFactors <- H.forAll $ combinations [1, 2, 3, 5, 7, 11, 13, 17, 19, 23] k + -- Maybe add one more signal in one of the domains + duplSignal <- H.forAll $ Gen.maybe $ Gen.integral_ $ Range.constant 0 (k - 1) + let + -- After @product periods@ time, the timing starts to repeat, so this seems a good + -- time to stop. + -- + -- Maximum duration is about 10,000 samples with the list of primes above. That + -- does make the test run pretty long, though. It seems unlikely that an anomaly + -- would show up only after 1,000 samples. + -- + -- The end of sampling is defined pretty weirdly in 'dumpVCD' currently, but with + -- this definition of @sampleDuration@, we should have enough samples and not + -- oversample too much. + sampleDuration = min 1000 $ product periodFactors + 10 + signalNames = + take k ["a", "b", "c", "d"] ++ if isJust duplSignal then ["e"] else [] + periods = map (* common) periodFactors + periods0 + | Just i <- duplSignal = periods ++ [periods !! i] + | otherwise = periods + traceMap = Map.fromAscList $ zipWith (\n p -> (n, oneTrace p)) signalNames periods0 + VCDFile vcdDecs vcdSims <- H.evalEither $ dumpVCD1# (0, sampleDuration) traceMap + Metadata{..} <- H.evalEither $ parseMetadata vcdDecs + Map.keysSet nameMap H.=== Map.keysSet traceMap + -- 'dumpVCD' currently outputs timestamp 0 twice: once for $dumpvars and again for + -- the first real value changes. But this is probably a bug; the standard doesn't + -- say, and GTKWave and Surfer accept it, but it sounds like it's not well-formed. + -- For now, we alter the timestamp for $dumpvars. The timestamp -1 is not valid in a + -- VCD file, but we can match on it in our tests. + vcdSims0 <- + case L.uncons vcdSims of + Just (sc, vcdSims1) -> + sc H.=== SimulationTime 0 >> pure (SimulationTime (-1) : vcdSims1) + Nothing -> + failWithMsg "VCDFile has no SimulationCommands" + let + -- The end of sampling is defined pretty weirdly in 'dumpVCD' currently + end = sampleDuration - 2 + signalCorrects = + map + ( \(name, (idCode, period, vs)) -> + signalCorrect name idCode (period `div` timeScale) end vs + ) + $ Map.assocs + $ Map.intersectionWith + (\idCode (_, period, _, vs) -> (idCode, period, vs)) + nameMap + traceMap + lockstepWalk (saneTimestamps : signalCorrects) vcdSims0 + where + oneTrace period = + ( encode (typeRep @SignalData) + , period + , size# (0 :: SignalData) + , map (0,) [0 ..] + ) + +tests :: TestTree +tests = + testGroup + "DumpVCD" + [ testPropertyNamed "multiDomainTrace" "multiDomainTrace" $ multiDomainTrace + ] diff --git a/tests/Hedgehog/Extra.hs b/tests/Hedgehog/Extra.hs --- a/tests/Hedgehog/Extra.hs +++ b/tests/Hedgehog/Extra.hs @@ -3,14 +3,19 @@ module Hedgehog.Extra ( throwsException , throwsDeepException + , LockstepWalk(..) + , lockstepWalk + , combinations ) where import Control.DeepSeq (NFData, force) -import Hedgehog (failure, MonadTest, success) +import Hedgehog (failure, MonadGen, MonadTest, success) import Hedgehog.Internal.Exception (tryEvaluate) import Hedgehog.Internal.Source (HasCallStack, withFrozenCallStack) +import qualified Hedgehog.Gen as Gen + throwsException :: ( MonadTest m , HasCallStack @@ -31,3 +36,70 @@ -> m () throwsDeepException = throwsException . force + +{- | Test individual samples of a list through 'lockstepWalk' + +@m@ is expected to be a 'MonadTest' monad. + +The function gets a boolean indicating if this is the last sample in the list, plus the +current sample. It should return the function to test the next sample with. +-} +newtype LockstepWalk m a + = LockstepWalk {unLockstepWalk :: Bool -> a -> m (LockstepWalk m a)} + +{- | Walk a lazy list testing multiple properties + +For each sample, multiple properties are tested. This way multiple tests can share a +walk of the list instead of the usual order where the first test would evaluate the +list fully even before the second test runs. +-} +lockstepWalk :: + forall m a. + (MonadTest m) => + [LockstepWalk m a] -> + [a] -> + m () +lockstepWalk _ [] = pure () +lockstepWalk ts (a : as) = do + ts0 <- sequence $ map (\t -> unLockstepWalk t (null as) a) ts + lockstepWalk ts0 as + +{- | Generate combinations of k elements from a list + +The generator shrinks towards the start of the list. +-} + +{- +To generate combinations, if we consider the first element, we note that we can either +pick it or skip it. From the n choose k combinations, there are (n-1) choose (k-1) +combinations where we picked the element, and (n-1) choose k combinations where we skipped +the element. So let's define + +pick = (n-1) choose (k-1) +skip = (n-1) choose k + +We only need to know the ratio pick:skip. Working out the binomial coefficients, we come +to the following equivalent ratio: + +pick' = k +skip' = n-k +-} +combinations :: + (MonadGen m) => + [a] -> + Int -> + m [a] +combinations es k + | k < 0 = error $ "combinations: impossible, k < 0. k = " <> show k + | otherwise = combinations0 n k es + where + n = length es + combinations0 _ 0 _ = pure [] + combinations0 n0 k0 es0 | n0 == k0 = pure es0 + combinations0 n0 k0 (e : es0) = + Gen.frequency + [ (k0, (e :) <$> combinations0 (n0 - 1) (k0 - 1) es0) + , (n0 - k0, combinations0 (n0 - 1) k0 es0) + ] + combinations0 _ _ [] = + error $ "combinations: impossible, k > n. k = " <> show k <> ", n = " <> show n diff --git a/tests/unittests.hs b/tests/unittests.hs --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -11,6 +11,7 @@ import qualified Clash.Tests.Clocks import qualified Clash.Tests.Counter import qualified Clash.Tests.DerivingDataRepr +import qualified Clash.Tests.DumpVCD import qualified Clash.Tests.Fixed import qualified Clash.Tests.FixedExhaustive import qualified Clash.Tests.MaybeX @@ -40,6 +41,7 @@ , Clash.Tests.Clocks.tests , Clash.Tests.Counter.tests , Clash.Tests.DerivingDataRepr.tests + , Clash.Tests.DumpVCD.tests , Clash.Tests.Fixed.tests , Clash.Tests.FixedExhaustive.tests , Clash.Tests.MaybeX.tests