{-|
Copyright  :  (C) 2013-2016, University of Twente,
                  2017     , Google Inc.
                  2019     , Myrtle Software Ltd
License    :  BSD2 (see the file LICENSE)
Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
-}

{-# LANGUAGE TypeFamilies #-}

{-# LANGUAGE Unsafe #-}

{-# OPTIONS_HADDOCK show-extensions #-}

{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}

module Clash.Explicit.Testbench
  ( -- * Testbench functions for circuits
    assert
  , assertBitVector
  , ignoreFor
  , stimuliGenerator

  , tbClockGen
  , tbEnableGen
  , tbSystemClockGen

  , outputVerifier
  , outputVerifier'
  , outputVerifierBitVector
  , outputVerifierBitVector'
  , biTbClockGen
  )
where

import Control.Exception     (catch, evaluate)
import Debug.Trace           (trace)
import GHC.TypeLits          (KnownNat, type (+))
import Prelude               hiding ((!!), length)
import System.IO.Unsafe      (unsafeDupablePerformIO)

import Clash.Annotations.Primitive (hasBlackBox)
import Clash.Class.Num       (satSucc, SaturationMode(SatBound))
import Clash.Promoted.Nat    (SNat(..), snatToNum)
import Clash.Promoted.Symbol (SSymbol (..))
import Clash.Explicit.Signal
  (Clock, Reset, System, Signal, clockPeriod, toEnable, fromList, register,
  unbundle, unsafeSynchronizer, veryUnsafeSynchronizer)
import Clash.Signal.Internal (Clock (..), Reset (..))
import Clash.Signal
  (mux, DomainResetKind, ResetKind(Asynchronous), KnownDomain,
  Enable)
import Clash.Sized.Index     (Index)
import Clash.Sized.Internal.BitVector
  (BitVector, isLike)
import Clash.Sized.Vector    (Vec, (!!), length)
import Clash.XException      (ShowX (..), XException)

-- Note that outputVerifier' is used in $setup, while the examples mention
-- outputVerifier. This is fine, as the examples have explicit type
-- signatures, turning 'outputVerifier' into 'outputVerifier''.

{- $setup
>>> :set -XTemplateHaskell -XDataKinds -XTypeFamilies
>>> :m -Clash.Prelude
>>> :m -Clash.Prelude.Safe
>>> :m -Clash.Prelude.Testbench
>>> import Clash.Explicit.Prelude
>>> let testInput clk rst = stimuliGenerator clk rst $(listToVecTH [(1::Int),3..21])
>>> let expectedOutput clk rst = outputVerifier' clk rst $(listToVecTH ([70,99,2,3,4,5,7,8,9,10]::[Int]))
-}

-- | Compares the first two 'Signal's for equality and logs a warning when they
-- are not equal. The second 'Signal' is considered the expected value. This
-- function simply returns the third 'Signal' unaltered as its result. This
-- function is used by 'outputVerifier'.
--
--
-- __NB__: This function /can/ be used in synthesizable designs.
assert
  :: (KnownDomain dom, Eq a, ShowX a)
  => Clock dom
  -> Reset dom
  -> String
  -- ^ Additional message
  -> Signal dom a
  -- ^ Checked value
  -> Signal dom a
  -- ^ Expected value
  -> Signal dom b
  -- ^ Return value
  -> Signal dom b
assert :: Clock dom
-> Reset dom
-> String
-> Signal dom a
-> Signal dom a
-> Signal dom b
-> Signal dom b
assert Clock dom
clk (Reset Signal dom Bool
_) String
msg Signal dom a
checked Signal dom a
expected Signal dom b
returned =
  (\a
c a
e Integer
cnt b
r ->
      if a -> a -> Bool
forall a. Eq a => a -> a -> Bool
eqX a
c a
e
         then b
r
         else String -> b -> b
forall a. String -> a -> a
trace ([String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [ String
"\ncycle(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Clock dom -> String
forall a. Show a => a -> String
show Clock dom
clk String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"): "
                            , Integer -> String
forall a. Show a => a -> String
show Integer
cnt
                            , String
", "
                            , String
msg
                            , String
"\nexpected value: "
                            , a -> String
forall a. ShowX a => a -> String
showX a
e
                            , String
", not equal to actual value: "
                            , a -> String
forall a. ShowX a => a -> String
showX a
c
                            ]) b
r)
  (a -> a -> Integer -> b -> b)
-> Signal dom a -> Signal dom (a -> Integer -> b -> b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom a
checked Signal dom (a -> Integer -> b -> b)
-> Signal dom a -> Signal dom (Integer -> b -> b)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Signal dom a
expected Signal dom (Integer -> b -> b)
-> Signal dom Integer -> Signal dom (b -> b)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Integer] -> Signal dom Integer
forall a (dom :: Domain). NFDataX a => [a] -> Signal dom a
fromList [(Integer
0::Integer)..] Signal dom (b -> b) -> Signal dom b -> Signal dom b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Signal dom b
returned
  where
    eqX :: a -> a -> Bool
eqX a
a a
b = IO Bool -> Bool
forall a. IO a -> a
unsafeDupablePerformIO (IO Bool -> (XException -> IO Bool) -> IO Bool
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch (Bool -> IO Bool
forall a. a -> IO a
evaluate (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b))
                                            (\(XException
_ :: XException) -> Bool -> IO Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
False))
{-# NOINLINE assert #-}
{-# ANN assert hasBlackBox #-}

-- | The same as 'assert', but can handle don't care bits in it's expected value.
assertBitVector
  :: (KnownDomain dom, KnownNat n)
  => Clock dom
  -> Reset dom
  -> String
  -- ^ Additional message
  -> Signal dom (BitVector n)
  -- ^ Checked value
  -> Signal dom (BitVector n)
  -- ^ Expected value
  -> Signal dom b
  -- ^ Return value
  -> Signal dom b
assertBitVector :: Clock dom
-> Reset dom
-> String
-> Signal dom (BitVector n)
-> Signal dom (BitVector n)
-> Signal dom b
-> Signal dom b
assertBitVector Clock dom
clk (Reset Signal dom Bool
_) String
msg Signal dom (BitVector n)
checked Signal dom (BitVector n)
expected Signal dom b
returned =
  (\BitVector n
c BitVector n
e Integer
cnt b
r ->
      if BitVector n -> BitVector n -> Bool
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n -> Bool
eqX BitVector n
c BitVector n
e
         then b
r
         else String -> b -> b
forall a. String -> a -> a
trace ([String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [ String
"\ncycle(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Clock dom -> String
forall a. Show a => a -> String
show Clock dom
clk String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"): "
                            , Integer -> String
forall a. Show a => a -> String
show Integer
cnt
                            , String
", "
                            , String
msg
                            , String
"\nexpected value: "
                            , BitVector n -> String
forall a. ShowX a => a -> String
showX BitVector n
e
                            , String
", not equal to actual value: "
                            , BitVector n -> String
forall a. ShowX a => a -> String
showX BitVector n
c
                            ]) b
r)
  (BitVector n -> BitVector n -> Integer -> b -> b)
-> Signal dom (BitVector n)
-> Signal dom (BitVector n -> Integer -> b -> b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (BitVector n)
checked Signal dom (BitVector n -> Integer -> b -> b)
-> Signal dom (BitVector n) -> Signal dom (Integer -> b -> b)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Signal dom (BitVector n)
expected Signal dom (Integer -> b -> b)
-> Signal dom Integer -> Signal dom (b -> b)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Integer] -> Signal dom Integer
forall a (dom :: Domain). NFDataX a => [a] -> Signal dom a
fromList [(Integer
0::Integer)..] Signal dom (b -> b) -> Signal dom b -> Signal dom b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Signal dom b
returned
  where
    eqX :: BitVector n -> BitVector n -> Bool
eqX BitVector n
a BitVector n
b = IO Bool -> Bool
forall a. IO a -> a
unsafeDupablePerformIO (IO Bool -> (XException -> IO Bool) -> IO Bool
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch (Bool -> IO Bool
forall a. a -> IO a
evaluate (BitVector n
a BitVector n -> BitVector n -> Bool
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n -> Bool
`isLike` BitVector n
b))
                                            (\(XException
_ :: XException) -> Bool -> IO Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
False))
{-# NOINLINE assertBitVector #-}
{-# ANN assertBitVector hasBlackBox #-}



-- |
--
-- Example:
--
-- @
-- testInput
--   :: KnownDomain dom
--   => Clock dom
--   -> Reset dom
--   -> 'Signal' dom Int
-- testInput clk rst = 'stimuliGenerator' clk rst $('Clash.Sized.Vector.listToVecTH' [(1::Int),3..21])
-- @
--
-- >>> sampleN 14 (testInput systemClockGen resetGen)
-- [1,1,3,5,7,9,11,13,15,17,19,21,21,21]
stimuliGenerator
  :: forall l dom   a
   . ( KnownNat l
     , KnownDomain dom )
  => Clock dom
  -- ^ Clock to which to synchronize the output signal
  -> Reset dom
  -> Vec l a
  -- ^ Samples to generate
  -> Signal dom a
  -- ^ Signal of given samples
stimuliGenerator :: Clock dom -> Reset dom -> Vec l a -> Signal dom a
stimuliGenerator Clock dom
clk Reset dom
rst Vec l a
samples =
    let (Signal dom (Index l)
r,Signal dom a
o) = Signal dom (Index l, a) -> Unbundled dom (Index l, a)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
unbundle (Index l -> (Index l, a)
genT (Index l -> (Index l, a))
-> Signal dom (Index l) -> Signal dom (Index l, a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Clock dom
-> Reset dom
-> Enable dom
-> Index l
-> Signal dom (Index l)
-> Signal dom (Index l)
forall (dom :: Domain) a.
(KnownDomain dom, NFDataX a) =>
Clock dom
-> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
register Clock dom
clk Reset dom
rst (Signal dom Bool -> Enable dom
forall (dom :: Domain). Signal dom Bool -> Enable dom
toEnable (Bool -> Signal dom Bool
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True)) Index l
0 Signal dom (Index l)
r)
    in  Signal dom a
o
  where
    genT :: Index l -> (Index l,a)
    genT :: Index l -> (Index l, a)
genT Index l
s = (Index l
s',Vec l a
samples Vec l a -> Index l -> a
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
!! Index l
s)
      where
        maxI :: Index l
maxI = Int -> Index l
forall a. Enum a => Int -> a
toEnum (Vec l a -> Int
forall (n :: Nat) a. KnownNat n => Vec n a -> Int
length Vec l a
samples Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

        s' :: Index l
s' = if Index l
s Index l -> Index l -> Bool
forall a. Ord a => a -> a -> Bool
< Index l
maxI
                then Index l
s Index l -> Index l -> Index l
forall a. Num a => a -> a -> a
+ Index l
1
                else Index l
s
{-# INLINABLE stimuliGenerator #-}

-- | Same as 'outputVerifier' but used in cases where the testbench domain and
-- the domain of the circuit under test are the same.
outputVerifier'
  :: forall l a dom
   . ( KnownNat l
     , KnownDomain dom
     , DomainResetKind dom ~ 'Asynchronous
     , Eq a
     , ShowX a )
  => Clock dom
  -- ^ Clock to which the testbench is synchronized to
  -> Reset dom
  -- ^ Reset line of testbench
  -> Vec l a
  -- ^ Samples to compare with
  -> Signal dom a
  -- ^ Signal to verify
  -> Signal dom Bool
  -- ^ Indicator that all samples are verified
outputVerifier' :: Clock dom
-> Reset dom -> Vec l a -> Signal dom a -> Signal dom Bool
outputVerifier' =
  (KnownNat l, KnownDomain dom, KnownDomain dom,
 DomainResetKind dom ~ 'Asynchronous, Eq a, ShowX a) =>
Clock dom
-> Reset dom -> Vec l a -> Signal dom a -> Signal dom Bool
forall (l :: Nat) a (testDom :: Domain) (circuitDom :: Domain).
(KnownNat l, KnownDomain testDom, KnownDomain circuitDom,
 DomainResetKind testDom ~ 'Asynchronous, Eq a, ShowX a) =>
Clock testDom
-> Reset testDom
-> Vec l a
-> Signal circuitDom a
-> Signal testDom Bool
outputVerifier @l @a @dom @dom
{-# INLINABLE outputVerifier' #-}

-- | Compare a signal (coming from a circuit) to a vector of samples. If a
-- sample from the signal is not equal to the corresponding sample in the
-- vector, print to stderr and continue testing. This function is
-- synthesizable in the sense that HDL simulators will run it.
--
-- Example:
--
-- @
-- expectedOutput
--   :: Clock dom -> Reset dom
--   -> 'Signal' dom Int -> 'Signal' dom 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 resetGen (fromList (0:[0..10] List.++ [10,10,10])))
-- <BLANKLINE>
-- cycle(<Clock: System>): 0, outputVerifier
-- expected value: 70, not equal to actual value: 0
-- [False
-- cycle(<Clock: System>): 1, outputVerifier
-- expected value: 70, not equal to actual value: 0
-- ,False
-- cycle(<Clock: System>): 2, outputVerifier
-- expected value: 99, not equal to actual value: 1
-- ,False,False,False,False,False
-- cycle(<Clock: System>): 7, outputVerifier
-- expected value: 7, not equal to actual value: 6
-- ,False
-- cycle(<Clock: System>): 8, outputVerifier
-- expected value: 8, not equal to actual value: 7
-- ,False
-- cycle(<Clock: System>): 9, outputVerifier
-- expected value: 9, not equal to actual value: 8
-- ,False
-- cycle(<Clock: System>): 10, outputVerifier
-- expected value: 10, not equal to actual value: 9
-- ,False,True]
--
-- If your working with 'BitVector's containing don't care bits you should
-- use 'outputVerifierBitVector'.
outputVerifier
  :: forall l a testDom circuitDom
   . ( KnownNat l
     , KnownDomain testDom
     , KnownDomain circuitDom
     , DomainResetKind testDom ~ 'Asynchronous
     , Eq a
     , ShowX a )
  => Clock testDom
  -- ^ Clock to which the testbench is synchronized to (but not necessarily
  -- the circuit under test)
  -> Reset testDom
  -- ^ Reset line of testbench
  -> Vec l a
  -- ^ Samples to compare with
  -> Signal circuitDom a
  -- ^ Signal to verify
  -> Signal testDom Bool
  -- ^ True if all samples are verified
outputVerifier :: Clock testDom
-> Reset testDom
-> Vec l a
-> Signal circuitDom a
-> Signal testDom Bool
outputVerifier Clock testDom
clk Reset testDom
rst Vec l a
samples Signal circuitDom a
i0 =
    let t1 :: Int
t1    = SNat (DomainConfigurationPeriod (KnownConf circuitDom)) -> Int
forall a (n :: Nat). Num a => SNat n -> a
snatToNum (forall (period :: Nat).
(KnownDomain circuitDom,
 DomainConfigurationPeriod (KnownConf circuitDom) ~ period) =>
SNat period
forall (dom :: Domain) (period :: Nat).
(KnownDomain dom, DomainPeriod dom ~ period) =>
SNat period
clockPeriod @circuitDom)
        t2 :: Int
t2    = SNat (DomainConfigurationPeriod (KnownConf testDom)) -> Int
forall a (n :: Nat). Num a => SNat n -> a
snatToNum (forall (period :: Nat).
(KnownDomain testDom,
 DomainConfigurationPeriod (KnownConf testDom) ~ period) =>
SNat period
forall (dom :: Domain) (period :: Nat).
(KnownDomain dom, DomainPeriod dom ~ period) =>
SNat period
clockPeriod @testDom)
        i1 :: Signal testDom a
i1    = Int -> Int -> Signal circuitDom a -> Signal testDom a
forall (dom1 :: Domain) a (dom2 :: Domain).
Int -> Int -> Signal dom1 a -> Signal dom2 a
veryUnsafeSynchronizer Int
t1 Int
t2 Signal circuitDom a
i0
        en :: Enable dom
en    = Signal dom Bool -> Enable dom
forall (dom :: Domain). Signal dom Bool -> Enable dom
toEnable (Bool -> Signal dom Bool
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True)
        (Signal testDom (Index l)
s,Signal testDom (a, Bool)
o) = Signal testDom (Index l, (a, Bool))
-> Unbundled testDom (Index l, (a, Bool))
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
unbundle (Index l -> (Index l, (a, Bool))
genT (Index l -> (Index l, (a, Bool)))
-> Signal testDom (Index l) -> Signal testDom (Index l, (a, Bool))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Clock testDom
-> Reset testDom
-> Enable testDom
-> Index l
-> Signal testDom (Index l)
-> Signal testDom (Index l)
forall (dom :: Domain) a.
(KnownDomain dom, NFDataX a) =>
Clock dom
-> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
register Clock testDom
clk Reset testDom
rst Enable testDom
forall (dom :: Domain). Enable dom
en Index l
0 Signal testDom (Index l)
s)
        (Signal testDom a
e,Signal testDom Bool
f) = Signal testDom (a, Bool) -> Unbundled testDom (a, Bool)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
unbundle Signal testDom (a, Bool)
o
        f' :: Signal testDom Bool
f'    = Clock testDom
-> Reset testDom
-> Enable testDom
-> Bool
-> Signal testDom Bool
-> Signal testDom Bool
forall (dom :: Domain) a.
(KnownDomain dom, NFDataX a) =>
Clock dom
-> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
register Clock testDom
clk Reset testDom
rst Enable testDom
forall (dom :: Domain). Enable dom
en Bool
False Signal testDom Bool
f
        -- Only assert while not finished
    in  Signal testDom Bool
-> Signal testDom Bool
-> Signal testDom Bool
-> Signal testDom Bool
forall (f :: Type -> Type) a.
Applicative f =>
f Bool -> f a -> f a -> f a
mux Signal testDom Bool
f' Signal testDom Bool
f' (Signal testDom Bool -> Signal testDom Bool)
-> Signal testDom Bool -> Signal testDom Bool
forall a b. (a -> b) -> a -> b
$ Clock testDom
-> Reset testDom
-> String
-> Signal testDom a
-> Signal testDom a
-> Signal testDom Bool
-> Signal testDom Bool
forall (dom :: Domain) a b.
(KnownDomain dom, Eq a, ShowX a) =>
Clock dom
-> Reset dom
-> String
-> Signal dom a
-> Signal dom a
-> Signal dom b
-> Signal dom b
assert Clock testDom
clk Reset testDom
rst String
"outputVerifier" Signal testDom a
i1 Signal testDom a
e Signal testDom Bool
f'
  where
    genT :: Index l -> (Index l,(a,Bool))
    genT :: Index l -> (Index l, (a, Bool))
genT Index l
s = (Index l
s',(Vec l a
samples Vec l a -> Index l -> a
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
!! Index l
s,Bool
finished))
      where
        maxI :: Index l
maxI = Int -> Index l
forall a. Enum a => Int -> a
toEnum (Vec l a -> Int
forall (n :: Nat) a. KnownNat n => Vec n a -> Int
length Vec l a
samples Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

        s' :: Index l
s' = if Index l
s Index l -> Index l -> Bool
forall a. Ord a => a -> a -> Bool
< Index l
maxI
                then Index l
s Index l -> Index l -> Index l
forall a. Num a => a -> a -> a
+ Index l
1
                else Index l
s

        finished :: Bool
finished = Index l
s Index l -> Index l -> Bool
forall a. Eq a => a -> a -> Bool
== Index l
maxI
{-# INLINABLE outputVerifier #-}

-- | Same as 'outputVerifier'', but can handle don't care bits in it's expected
-- values.
outputVerifierBitVector'
  :: forall l n dom
   . ( KnownNat l
     , KnownNat n
     , KnownDomain dom
     , DomainResetKind dom ~ 'Asynchronous
     )
  => Clock dom
  -- ^ Clock to which the input signal is synchronized to
  -> Reset dom
  -> Vec l (BitVector n)
  -- ^ Samples to compare with
  -> Signal dom (BitVector n)
  -- ^ Signal to verify
  -> Signal dom Bool
  -- ^ Indicator that all samples are verified
outputVerifierBitVector' :: Clock dom
-> Reset dom
-> Vec l (BitVector n)
-> Signal dom (BitVector n)
-> Signal dom Bool
outputVerifierBitVector' =
  (KnownNat l, KnownNat n, KnownDomain dom, KnownDomain dom,
 DomainResetKind dom ~ 'Asynchronous) =>
Clock dom
-> Reset dom
-> Vec l (BitVector n)
-> Signal dom (BitVector n)
-> Signal dom Bool
forall (l :: Nat) (n :: Nat) (testDom :: Domain)
       (circuitDom :: Domain).
(KnownNat l, KnownNat n, KnownDomain testDom,
 KnownDomain circuitDom, DomainResetKind testDom ~ 'Asynchronous) =>
Clock testDom
-> Reset testDom
-> Vec l (BitVector n)
-> Signal circuitDom (BitVector n)
-> Signal testDom Bool
outputVerifierBitVector @l @n @dom @dom
{-# INLINABLE outputVerifierBitVector' #-}

-- | Same as 'outputVerifier', but can handle don't care bits in it's
-- expected values.
outputVerifierBitVector
  :: forall l n testDom circuitDom
   . ( KnownNat l
     , KnownNat n
     , KnownDomain testDom
     , KnownDomain circuitDom
     , DomainResetKind testDom ~ 'Asynchronous
     )
  => Clock testDom
  -- ^ Clock to which the input signal is synchronized to
  -> Reset testDom
  -> Vec l (BitVector n)
  -- ^ Samples to compare with
  -> Signal circuitDom (BitVector n)
  -- ^ Signal to verify
  -> Signal testDom Bool
  -- ^ Indicator that all samples are verified
outputVerifierBitVector :: Clock testDom
-> Reset testDom
-> Vec l (BitVector n)
-> Signal circuitDom (BitVector n)
-> Signal testDom Bool
outputVerifierBitVector Clock testDom
clk Reset testDom
rst Vec l (BitVector n)
samples Signal circuitDom (BitVector n)
i0 =
    let t1 :: Int
t1    = SNat (DomainConfigurationPeriod (KnownConf circuitDom)) -> Int
forall a (n :: Nat). Num a => SNat n -> a
snatToNum (forall (period :: Nat).
(KnownDomain circuitDom,
 DomainConfigurationPeriod (KnownConf circuitDom) ~ period) =>
SNat period
forall (dom :: Domain) (period :: Nat).
(KnownDomain dom, DomainPeriod dom ~ period) =>
SNat period
clockPeriod @circuitDom)
        t2 :: Int
t2    = SNat (DomainConfigurationPeriod (KnownConf testDom)) -> Int
forall a (n :: Nat). Num a => SNat n -> a
snatToNum (forall (period :: Nat).
(KnownDomain testDom,
 DomainConfigurationPeriod (KnownConf testDom) ~ period) =>
SNat period
forall (dom :: Domain) (period :: Nat).
(KnownDomain dom, DomainPeriod dom ~ period) =>
SNat period
clockPeriod @testDom)
        i1 :: Signal testDom (BitVector n)
i1    = Int
-> Int
-> Signal circuitDom (BitVector n)
-> Signal testDom (BitVector n)
forall (dom1 :: Domain) a (dom2 :: Domain).
Int -> Int -> Signal dom1 a -> Signal dom2 a
veryUnsafeSynchronizer Int
t1 Int
t2 Signal circuitDom (BitVector n)
i0
        en :: Enable dom
en    = Signal dom Bool -> Enable dom
forall (dom :: Domain). Signal dom Bool -> Enable dom
toEnable (Bool -> Signal dom Bool
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True)
        (Signal testDom (Index l)
s,Signal testDom (BitVector n, Bool)
o) = Signal testDom (Index l, (BitVector n, Bool))
-> Unbundled testDom (Index l, (BitVector n, Bool))
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
unbundle (Index l -> (Index l, (BitVector n, Bool))
genT (Index l -> (Index l, (BitVector n, Bool)))
-> Signal testDom (Index l)
-> Signal testDom (Index l, (BitVector n, Bool))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Clock testDom
-> Reset testDom
-> Enable testDom
-> Index l
-> Signal testDom (Index l)
-> Signal testDom (Index l)
forall (dom :: Domain) a.
(KnownDomain dom, NFDataX a) =>
Clock dom
-> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
register Clock testDom
clk Reset testDom
rst Enable testDom
forall (dom :: Domain). Enable dom
en Index l
0 Signal testDom (Index l)
s)
        (Signal testDom (BitVector n)
e,Signal testDom Bool
f) = Signal testDom (BitVector n, Bool)
-> Unbundled testDom (BitVector n, Bool)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
unbundle Signal testDom (BitVector n, Bool)
o
        f' :: Signal testDom Bool
f'    = Clock testDom
-> Reset testDom
-> Enable testDom
-> Bool
-> Signal testDom Bool
-> Signal testDom Bool
forall (dom :: Domain) a.
(KnownDomain dom, NFDataX a) =>
Clock dom
-> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
register Clock testDom
clk Reset testDom
rst Enable testDom
forall (dom :: Domain). Enable dom
en Bool
False Signal testDom Bool
f
        -- Only assert while not finished
    in  Signal testDom Bool
-> Signal testDom Bool
-> Signal testDom Bool
-> Signal testDom Bool
forall (f :: Type -> Type) a.
Applicative f =>
f Bool -> f a -> f a -> f a
mux Signal testDom Bool
f' Signal testDom Bool
f' (Signal testDom Bool -> Signal testDom Bool)
-> Signal testDom Bool -> Signal testDom Bool
forall a b. (a -> b) -> a -> b
$ Clock testDom
-> Reset testDom
-> String
-> Signal testDom (BitVector n)
-> Signal testDom (BitVector n)
-> Signal testDom Bool
-> Signal testDom Bool
forall (dom :: Domain) (n :: Nat) b.
(KnownDomain dom, KnownNat n) =>
Clock dom
-> Reset dom
-> String
-> Signal dom (BitVector n)
-> Signal dom (BitVector n)
-> Signal dom b
-> Signal dom b
assertBitVector Clock testDom
clk Reset testDom
rst String
"outputVerifierBitVector'" Signal testDom (BitVector n)
i1 Signal testDom (BitVector n)
e Signal testDom Bool
f'
  where
    genT :: Index l -> (Index l,(BitVector n,Bool))
    genT :: Index l -> (Index l, (BitVector n, Bool))
genT Index l
s = (Index l
s',(Vec l (BitVector n)
samples Vec l (BitVector n) -> Index l -> BitVector n
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
!! Index l
s,Bool
finished))
      where
        maxI :: Index l
maxI = Int -> Index l
forall a. Enum a => Int -> a
toEnum (Vec l (BitVector n) -> Int
forall (n :: Nat) a. KnownNat n => Vec n a -> Int
length Vec l (BitVector n)
samples Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

        s' :: Index l
s' = if Index l
s Index l -> Index l -> Bool
forall a. Ord a => a -> a -> Bool
< Index l
maxI
                then Index l
s Index l -> Index l -> Index l
forall a. Num a => a -> a -> a
+ Index l
1
                else Index l
s

        finished :: Bool
finished = Index l
s Index l -> Index l -> Bool
forall a. Eq a => a -> a -> Bool
== Index l
maxI
{-# INLINABLE outputVerifierBitVector #-}

-- | Ignore signal for a number of cycles, while outputting a static value.
ignoreFor
  :: forall dom  n a
   . KnownDomain dom
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> SNat n
  -- ^ Number of cycles to ignore incoming signal
  -> a
  -- ^ Value function produces when ignoring signal
  -> Signal dom a
  -- ^ Incoming signal
  -> Signal dom a
  -- ^ Either a passthrough of the incoming signal, or the static value
  -- provided as the second argument.
ignoreFor :: Clock dom
-> Reset dom
-> Enable dom
-> SNat n
-> a
-> Signal dom a
-> Signal dom a
ignoreFor Clock dom
clk Reset dom
rst Enable dom
en SNat n
SNat a
a Signal dom a
i =
  Signal dom Bool -> Signal dom a -> Signal dom a -> Signal dom a
forall (f :: Type -> Type) a.
Applicative f =>
f Bool -> f a -> f a -> f a
mux (Index (n + 1) -> Index (n + 1) -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Index (n + 1) -> Index (n + 1) -> Bool)
-> Signal dom (Index (n + 1)) -> Signal dom (Index (n + 1) -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Index (n + 1))
counter Signal dom (Index (n + 1) -> Bool)
-> Signal dom (Index (n + 1)) -> Signal dom Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (Index (n + 1) -> Signal dom (Index (n + 1))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Index (n + 1)
forall a. Bounded a => a
maxBound)) Signal dom a
i (a -> Signal dom a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
a)
 where
  counter :: Signal dom (Index (n+1))
  counter :: Signal dom (Index (n + 1))
counter = Clock dom
-> Reset dom
-> Enable dom
-> Index (n + 1)
-> Signal dom (Index (n + 1))
-> Signal dom (Index (n + 1))
forall (dom :: Domain) a.
(KnownDomain dom, NFDataX a) =>
Clock dom
-> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
register Clock dom
clk Reset dom
rst Enable dom
en Index (n + 1)
0 (SaturationMode -> Index (n + 1) -> Index (n + 1)
forall a. SaturatingNum a => SaturationMode -> a -> a
satSucc SaturationMode
SatBound (Index (n + 1) -> Index (n + 1))
-> Signal dom (Index (n + 1)) -> Signal dom (Index (n + 1))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Index (n + 1))
counter)

-- | Same as 'tbClockGen', but returns two clocks on potentially different
-- domains. To be used in situations where the circuit under test runs
-- in a different domain than the circuit testing it. Most commonly used
-- to test synchronous circuits (with an asynchronous test circuit).
biTbClockGen
  :: forall testDom circuitDom
   . ( KnownDomain testDom
     , KnownDomain circuitDom
     , DomainResetKind testDom ~ 'Asynchronous
     )
  => Signal testDom Bool
  -> (Clock testDom, Clock circuitDom)
biTbClockGen :: Signal testDom Bool -> (Clock testDom, Clock circuitDom)
biTbClockGen Signal testDom Bool
done = (Clock testDom
testClk, Clock circuitDom
circuitClk)
 where
  testClk :: Clock testDom
testClk = Signal testDom Bool -> Clock testDom
forall (testDom :: Domain).
KnownDomain testDom =>
Signal testDom Bool -> Clock testDom
tbClockGen Signal testDom Bool
done
  circuitClk :: Clock circuitDom
circuitClk = Signal circuitDom Bool -> Clock circuitDom
forall (testDom :: Domain).
KnownDomain testDom =>
Signal testDom Bool -> Clock testDom
tbClockGen (Clock testDom
-> Clock circuitDom
-> Signal testDom Bool
-> Signal circuitDom Bool
forall (dom1 :: Domain) (dom2 :: Domain) a.
(KnownDomain dom1, KnownDomain dom2) =>
Clock dom1 -> Clock dom2 -> Signal dom1 a -> Signal dom2 a
unsafeSynchronizer Clock testDom
testClk Clock circuitDom
circuitClk Signal testDom Bool
done)

-- | Clock generator to be used in the /testBench/ function.
--
-- To be used like:
--
-- @
-- clkSystem en = tbClockGen @System en
-- @
--
-- === __Example__
--
-- @
-- module Example where
--
-- import "Clash.Explicit.Prelude"
-- import "Clash.Explicit.Testbench"
--
-- -- Fast domain: twice as fast as \"Slow\"
-- 'createDomain' 'vSystem'{vName=\"Fast\", vPeriod=10}
--
-- -- Slow domain: twice as slow as "Fast"
-- 'createDomain' 'vSystem'{vName=\"Slow\", vPeriod=20}
--
-- topEntity
--   :: 'Clock' \"Fast\"
--   -> 'Reset' \"Fast\"
--   -> 'Enable' \"Fast\"
--   -> 'Clock' \"Slow\"
--   -> 'Signal' \"Fast\" (Unsigned 8)
--   -> 'Signal' \"Slow\" (Unsigned 8, Unsigned 8)
-- topEntity clk1 rst1 en1 clk2 i =
--   let h = register clk1 rst1 en1 0 (register clk1 rst1 en1 0 i)
--       l = register clk1 rst1 en1 0 i
--   in  unsafeSynchronizer clk1 clk2 (bundle (h, l))
--
-- testBench
--   :: 'Signal' \"Slow\" Bool
-- testBench = done
--   where
--     testInput      = 'Clash.Explicit.Testbench.stimuliGenerator' clkA1 rstA1 $('listToVecTH' [1::Unsigned 8,2,3,4,5,6,7,8])
--     expectedOutput = 'Clash.Explicit.Testbench.outputVerifier'   clkB2 rstB2 $('listToVecTH' [(0,0) :: (Unsigned 8, Unsigned 8),(1,2),(3,4),(5,6),(7,8)])
--     done           = expectedOutput (topEntity clkA1 rstA1 enableGen clkB2 testInput)
--     done'          = not \<$\> done
--     clkA1          = 'tbClockGen' \@\"Fast\" (unsafeSynchronizer clkB2 clkA1 done')
--     clkB2          = 'tbClockGen' \@\"Slow\" done'
--     rstA1          = 'resetGen' \@\"Fast\"
--     rstB2          = 'resetGen' \@\"Slow\"
-- @
tbClockGen
  :: KnownDomain testDom
  => Signal testDom Bool
  -> Clock testDom
tbClockGen :: Signal testDom Bool -> Clock testDom
tbClockGen Signal testDom Bool
done = SSymbol testDom -> Clock testDom
forall (dom :: Domain). SSymbol dom -> Clock dom
Clock (Signal testDom Bool
done Signal testDom Bool -> SSymbol testDom -> SSymbol testDom
`seq` SSymbol testDom
forall (s :: Domain). KnownSymbol s => SSymbol s
SSymbol)
{-# NOINLINE tbClockGen #-}
{-# ANN tbClockGen hasBlackBox #-}

-- | Enable signal that's always enabled. Because it has a blackbox definition
-- this enable signal is opaque to other blackboxes. It will therefore never
-- be optimized away.
tbEnableGen :: Enable tag
tbEnableGen :: Enable tag
tbEnableGen = Signal tag Bool -> Enable tag
forall (dom :: Domain). Signal dom Bool -> Enable dom
toEnable (Bool -> Signal tag Bool
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True)
{-# NOINLINE tbEnableGen #-}
{-# ANN tbEnableGen hasBlackBox #-}

-- | Clock generator for the 'System' clock domain.
--
-- __NB__: can be used in the /testBench/ function
--
-- === __Example__
--
-- @
-- topEntity :: Vec 2 (Vec 3 (Unsigned 8)) -> Vec 6 (Unsigned 8)
-- topEntity = concat
--
-- testBench :: Signal System Bool
-- testBench = done
--   where
--     testInput      = pure ((1 :> 2 :> 3 :> Nil) :> (4 :> 5 :> 6 :> Nil) :> Nil)
--     expectedOutput = outputVerifier ((1:>2:>3:>4:>5:>6:>Nil):>Nil)
--     done           = exposeClockResetEnable (expectedOutput (topEntity <$> testInput)) clk rst
--     clk            = 'tbSystemClockGen' (not <\$\> done)
--     rst            = systemResetGen
-- @
tbSystemClockGen
  :: Signal System Bool
  -> Clock System
tbSystemClockGen :: Signal System Bool -> Clock System
tbSystemClockGen = Signal System Bool -> Clock System
forall (testDom :: Domain).
KnownDomain testDom =>
Signal testDom Bool -> Clock testDom
tbClockGen