Skip to content

Commit

Permalink
backend cleanup & more documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
kleinreact committed May 16, 2023
1 parent 14f75bb commit a7a8671
Show file tree
Hide file tree
Showing 10 changed files with 1,189 additions and 777 deletions.
2 changes: 0 additions & 2 deletions clash-testbench/clash-testbench.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -40,11 +40,9 @@ library
Clash.Testbench.Output
Clash.Testbench.Simulate
Clash.Testbench.Generate
other-modules:
Clash.Testbench.Internal.ID
Clash.Testbench.Internal.Signal
Clash.Testbench.Internal.Monad
Clash.Testbench.Internal.Auto
build-depends:
base,
mtl,
Expand Down
185 changes: 105 additions & 80 deletions clash-testbench/src/Clash/Testbench/Generate.hs
Original file line number Diff line number Diff line change
@@ -1,8 +1,16 @@
{-|
Copyright: (C) 2023 Google Inc.
License: BSD2 (see the file LICENSE)
Maintainer: QBayLogic B.V. <[email protected]>
Use generators to create signal data.
-}

module Clash.Testbench.Generate where

import Hedgehog
import Hedgehog.Gen
import Control.Monad.State.Lazy (liftIO, get)
import Control.Monad.State.Lazy (liftIO)
import Data.IORef (newIORef, readIORef, writeIORef)

import Clash.Prelude (KnownDomain(..), BitPack(..), NFDataX)
Expand All @@ -12,92 +20,21 @@ import Clash.Testbench.Internal.ID
import Clash.Testbench.Internal.Signal hiding (TBSignal, TBClock, TBReset, TBEnable)
import Clash.Testbench.Internal.Monad

matchIOGen ::
(NFDataX i, BitPack i, KnownDomain dom, Eq o, Show o) =>
TBSignal dom o -> Gen (i, o) -> TB (TBSignal dom i)
matchIOGen expectedOutput gen = do
ST{..} <- get

vRef <- liftIO $ newIORef undefined
simStepCache <- liftIO (readIORef simStepRef >>= newIORef)

mind SomeSignal $ IOInput
{ signalId = NoID
, signalCurVal = do
v <- readIORef simStepRef
v' <- readIORef simStepCache

if v == v'
then readIORef vRef
else do
(i, o) <- sample gen
signalExpect expectedOutput $ Expectation (v + 1, verify o)

writeIORef vRef i
writeIORef simStepCache v
return i
, signalPrint = Nothing
}
where
verify x y
| x == y = Nothing
| otherwise = Just $ "Expected " <> show x <> " but the output is " <> show y


matchIOGenN ::
(NFDataX i, BitPack i, KnownDomain dom, Eq o, Show o) =>
TBSignal dom o -> Gen [(i, o)] -> TB (TBSignal dom i)
matchIOGenN expectedOutput gen = do
ST{..} <- get

vRef <- liftIO $ newIORef []
simStepCache <- liftIO (readIORef simStepRef >>= newIORef)

mind SomeSignal $ IOInput
{ signalId = NoID
, signalCurVal = do
v <- readIORef simStepRef
v' <- readIORef simStepCache

if v == v'
then readIORef vRef >>= \case
(i, _) : _ -> return i
[] -> do
(i, o) : xr <- sample gen
writeIORef vRef ((i, o) : xr)
return i
else do
writeIORef simStepCache v
readIORef vRef >>= \case
_ : (i, o) : xr -> do
writeIORef vRef ((i, o) : xr)
signalExpect expectedOutput $ Expectation (v, verify o)
return i
_ -> do
(i, o) : xr <- sample gen
writeIORef vRef ((i, o) : xr)
signalExpect expectedOutput $ Expectation (v, verify o)
return i
, signalPrint = Nothing
}
where
verify x y
| x == y = Nothing
| otherwise = Just $ "Expected '" <> show x <> "' but the output is '" <> show y <> "'"


-- | Use a generator to create new signal data at every simulation
-- step.
generate ::
forall dom a.
(NFDataX a, BitPack a, KnownDomain dom) =>
a -> Gen a -> TB (TBSignal dom a)
generate def gen = do
ST{..} <- get
TBDomain{..} <- tbDomain @dom

vRef <- liftIO $ newIORef def
simStepCache <- liftIO (readIORef simStepRef >>= newIORef)

mind SomeSignal IOInput
{ signalId = NoID
, signalCurVal = do
, signalCurVal = const $ do
v <- readIORef simStepRef
v' <- readIORef simStepCache

Expand All @@ -111,18 +48,23 @@ generate def gen = do
, signalPrint = Nothing
}

-- | Extended version of 'generate', which allows to generate a finite
-- sequence of data values, where one value is consumed per simulation
-- step. The generator is repeatedly called after all steps of a
-- generation has been consumed.
generateN ::
forall dom a.
(NFDataX a, BitPack a, KnownDomain dom) =>
a -> Gen [a] -> TB (TBSignal dom a)
generateN def gen = do
ST{..} <- get
TBDomain{..} <- tbDomain @dom

vRef <- liftIO $ newIORef [def]
simStepCache <- liftIO (readIORef simStepRef >>= newIORef)

mindSignal IOInput
mind SomeSignal IOInput
{ signalId = NoID
, signalCurVal = do
, signalCurVal = const $ do
v <- readIORef simStepRef
v' <- readIORef simStepCache

Expand All @@ -147,3 +89,86 @@ generateN def gen = do
, signalPrint = Nothing
, ..
}

-- | Use an input/output generator to describe an IO relation that
-- specifies valid behavior. The satisfaction of this relation is
-- automatically checked during simulation.
matchIOGen ::
forall dom i o.
(NFDataX i, BitPack i, KnownDomain dom, Eq o, Show o) =>
TBSignal dom o -> Gen (i, o) -> TB (TBSignal dom i)
matchIOGen expectedOutput gen = do
TBDomain{..} <- tbDomain @dom

vRef <- liftIO $ newIORef undefined
simStepCache <- liftIO (readIORef simStepRef >>= newIORef)

mind SomeSignal $ IOInput
{ signalId = NoID
, signalCurVal = const $ do
global <- readIORef simStepRef
local <- readIORef simStepCache

if local == global
then readIORef vRef
else do
(i, o) <- sample gen
signalExpect expectedOutput $ Expectation (global + 1, verify o)

writeIORef vRef i
writeIORef simStepCache global
return i
, signalPrint = Nothing
}
where
verify x y
| x == y = Nothing
| otherwise = Just $ "Expected " <> show x <> " but the output is " <> show y

-- | Extended version of 'matchIOGen', which allows to specify valid
-- IO behavior over a finite amount of simulation steps. The generator
-- is repeatedly called after all steps of a generation have been
-- verified.
matchIOGenN ::
forall dom i o.
(NFDataX i, BitPack i, KnownDomain dom, Eq o, Show o, Show i) =>
TBSignal dom o -> Gen [(i, o)] -> TB (TBSignal dom i)
matchIOGenN expectedOutput gen = do
TBDomain{..} <- tbDomain @dom

vRef <- liftIO $ newIORef []
simStepCache <- liftIO (readIORef simStepRef >>= newIORef)

mind SomeSignal $ IOInput
{ signalId = NoID
, signalCurVal = const $ do
global <- readIORef simStepRef
local <- readIORef simStepCache

if local == global
then readIORef vRef >>= \case
(i, _) : _ -> return i
[] -> do
(i, o) : xr <- sample gen
writeIORef vRef ((i, o) : xr)
Prelude.print $ (i, o) : xr
return i
else do
writeIORef simStepCache global
readIORef vRef >>= \case
_ : (i, o) : xr -> do
writeIORef vRef ((i, o) : xr)
signalExpect expectedOutput $ Expectation (global + 1, verify o)
return i
_ -> do
(i, o) : xr <- sample gen
Prelude.print $ (i, o) : xr
writeIORef vRef ((i, o) : xr)
signalExpect expectedOutput $ Expectation (global + 1, verify o)
return i
, signalPrint = Nothing
}
where
verify x y
| x == y = Nothing
| otherwise = Just $ "Expected '" <> show x <> "' but the output is '" <> show y <> "'"
30 changes: 16 additions & 14 deletions clash-testbench/src/Clash/Testbench/Input.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@ Copyright: (C) 2023 Google Inc.
License: BSD2 (see the file LICENSE)
Maintainer: QBayLogic B.V. <[email protected]>
Input sources for simulating 'TB' defined testbenches.
Input sources for simulating 'Clash.Testbench.Simulate.TB' defined
test benches.
-}
module Clash.Testbench.Input
( fromList
Expand All @@ -21,31 +22,32 @@ import Clash.Testbench.Internal.Signal hiding (TBSignal)
import Clash.Testbench.Internal.Monad
import Clash.Testbench.Internal.ID

-- | Generates input that is taken from a finite or infinite list. If
-- the list is finite and the number of simulation steps exceeds the
-- length of the list, then the value of the first argument is
-- used instead.
fromList
:: (KnownDomain dom, BitPack a, NFDataX a) => a -> [a] -> TB (TBSignal dom a)
-- | Creates an input signal whose values are taken from a finite or
-- infinite list. If the list is finite and the number of simulation
-- steps exceeds the length of the list, then the value of the first
-- argument is used repeatedly.
fromList :: forall dom a.
(KnownDomain dom, BitPack a, NFDataX a, Show a) =>
a -> [a] -> TB (TBSignal dom a)
fromList x xs = do
ST{..} <- get
TBDomain{..} <- tbDomain @dom

listRef <- liftIO $ newIORef $ x : xs
simStepCache <- liftIO (readIORef simStepRef >>= newIORef)

mindSignal $ IOInput
mind SomeSignal $ IOInput
{ signalId = NoID
, signalPrint = Nothing
, signalCurVal = do
, signalCurVal = const $ do
(r, rs) <- fromMaybe (x, []) . uncons <$> readIORef listRef
v <- readIORef simStepRef
v' <- readIORef simStepCache
global <- readIORef simStepRef
local <- readIORef simStepCache

if v == v'
if local == global
then return r
else do
writeIORef listRef rs
writeIORef simStepCache v
writeIORef simStepCache global
return $ case rs of
[] -> x
y:_ -> y
Expand Down
43 changes: 0 additions & 43 deletions clash-testbench/src/Clash/Testbench/Internal/Auto.hs

This file was deleted.

Loading

0 comments on commit a7a8671

Please sign in to comment.