1+ {-|
2+ Copyright: (C) 2023 Google Inc.
3+ License: BSD2 (see the file LICENSE)
4+ Maintainer: QBayLogic B.V. <devops@qbaylogic.com>
5+
6+ Use generators to create signal data.
7+ -}
8+
19module Clash.Testbench.Generate where
210
311import Hedgehog
412import Hedgehog.Gen
5- import Control.Monad.State.Lazy (liftIO , get )
13+ import Control.Monad.State.Lazy (liftIO )
614import Data.IORef (newIORef , readIORef , writeIORef )
715
816import Clash.Prelude (KnownDomain (.. ), BitPack (.. ), NFDataX )
@@ -12,92 +20,21 @@ import Clash.Testbench.Internal.ID
1220import Clash.Testbench.Internal.Signal hiding (TBSignal , TBClock , TBReset , TBEnable )
1321import Clash.Testbench.Internal.Monad
1422
15- matchIOGen ::
16- (NFDataX i , BitPack i , KnownDomain dom , Eq o , Show o ) =>
17- TBSignal dom o -> Gen (i , o ) -> TB (TBSignal dom i )
18- matchIOGen expectedOutput gen = do
19- ST {.. } <- get
20-
21- vRef <- liftIO $ newIORef undefined
22- simStepCache <- liftIO (readIORef simStepRef >>= newIORef)
23-
24- mind SomeSignal $ IOInput
25- { signalId = NoID
26- , signalCurVal = do
27- v <- readIORef simStepRef
28- v' <- readIORef simStepCache
29-
30- if v == v'
31- then readIORef vRef
32- else do
33- (i, o) <- sample gen
34- signalExpect expectedOutput $ Expectation (v + 1 , verify o)
35-
36- writeIORef vRef i
37- writeIORef simStepCache v
38- return i
39- , signalPrint = Nothing
40- }
41- where
42- verify x y
43- | x == y = Nothing
44- | otherwise = Just $ " Expected " <> show x <> " but the output is " <> show y
45-
46-
47- matchIOGenN ::
48- (NFDataX i , BitPack i , KnownDomain dom , Eq o , Show o ) =>
49- TBSignal dom o -> Gen [(i , o )] -> TB (TBSignal dom i )
50- matchIOGenN expectedOutput gen = do
51- ST {.. } <- get
52-
53- vRef <- liftIO $ newIORef []
54- simStepCache <- liftIO (readIORef simStepRef >>= newIORef)
55-
56- mind SomeSignal $ IOInput
57- { signalId = NoID
58- , signalCurVal = do
59- v <- readIORef simStepRef
60- v' <- readIORef simStepCache
61-
62- if v == v'
63- then readIORef vRef >>= \ case
64- (i, _) : _ -> return i
65- [] -> do
66- (i, o) : xr <- sample gen
67- writeIORef vRef ((i, o) : xr)
68- return i
69- else do
70- writeIORef simStepCache v
71- readIORef vRef >>= \ case
72- _ : (i, o) : xr -> do
73- writeIORef vRef ((i, o) : xr)
74- signalExpect expectedOutput $ Expectation (v, verify o)
75- return i
76- _ -> do
77- (i, o) : xr <- sample gen
78- writeIORef vRef ((i, o) : xr)
79- signalExpect expectedOutput $ Expectation (v, verify o)
80- return i
81- , signalPrint = Nothing
82- }
83- where
84- verify x y
85- | x == y = Nothing
86- | otherwise = Just $ " Expected '" <> show x <> " ' but the output is '" <> show y <> " '"
87-
88-
23+ -- | Use a generator to create new signal data at every simulation
24+ -- step.
8925generate ::
26+ forall dom a .
9027 (NFDataX a , BitPack a , KnownDomain dom ) =>
9128 a -> Gen a -> TB (TBSignal dom a )
9229generate def gen = do
93- ST {.. } <- get
30+ TBDomain {.. } <- tbDomain @ dom
9431
9532 vRef <- liftIO $ newIORef def
9633 simStepCache <- liftIO (readIORef simStepRef >>= newIORef)
9734
9835 mind SomeSignal IOInput
9936 { signalId = NoID
100- , signalCurVal = do
37+ , signalCurVal = const $ do
10138 v <- readIORef simStepRef
10239 v' <- readIORef simStepCache
10340
@@ -111,18 +48,23 @@ generate def gen = do
11148 , signalPrint = Nothing
11249 }
11350
51+ -- | Extended version of 'generate', which allows to generate a finite
52+ -- sequence of data values, where one value is consumed per simulation
53+ -- step. The generator is repeatedly called after all steps of a
54+ -- generation has been consumed.
11455generateN ::
56+ forall dom a .
11557 (NFDataX a , BitPack a , KnownDomain dom ) =>
11658 a -> Gen [a ] -> TB (TBSignal dom a )
11759generateN def gen = do
118- ST {.. } <- get
60+ TBDomain {.. } <- tbDomain @ dom
11961
12062 vRef <- liftIO $ newIORef [def]
12163 simStepCache <- liftIO (readIORef simStepRef >>= newIORef)
12264
123- mindSignal IOInput
65+ mind SomeSignal IOInput
12466 { signalId = NoID
125- , signalCurVal = do
67+ , signalCurVal = const $ do
12668 v <- readIORef simStepRef
12769 v' <- readIORef simStepCache
12870
@@ -147,3 +89,86 @@ generateN def gen = do
14789 , signalPrint = Nothing
14890 , ..
14991 }
92+
93+ -- | Use an input/output generator to describe an IO relation that
94+ -- specifies valid behavior. The satisfaction of this relation is
95+ -- automatically checked during simulation.
96+ matchIOGen ::
97+ forall dom i o .
98+ (NFDataX i , BitPack i , KnownDomain dom , Eq o , Show o ) =>
99+ TBSignal dom o -> Gen (i , o ) -> TB (TBSignal dom i )
100+ matchIOGen expectedOutput gen = do
101+ TBDomain {.. } <- tbDomain @ dom
102+
103+ vRef <- liftIO $ newIORef undefined
104+ simStepCache <- liftIO (readIORef simStepRef >>= newIORef)
105+
106+ mind SomeSignal $ IOInput
107+ { signalId = NoID
108+ , signalCurVal = const $ do
109+ global <- readIORef simStepRef
110+ local <- readIORef simStepCache
111+
112+ if local == global
113+ then readIORef vRef
114+ else do
115+ (i, o) <- sample gen
116+ signalExpect expectedOutput $ Expectation (global + 1 , verify o)
117+
118+ writeIORef vRef i
119+ writeIORef simStepCache global
120+ return i
121+ , signalPrint = Nothing
122+ }
123+ where
124+ verify x y
125+ | x == y = Nothing
126+ | otherwise = Just $ " Expected " <> show x <> " but the output is " <> show y
127+
128+ -- | Extended version of 'matchIOGen', which allows to specify valid
129+ -- IO behavior over a finite amount of simulation steps. The generator
130+ -- is repeatedly called after all steps of a generation have been
131+ -- verified.
132+ matchIOGenN ::
133+ forall dom i o .
134+ (NFDataX i , BitPack i , KnownDomain dom , Eq o , Show o , Show i ) =>
135+ TBSignal dom o -> Gen [(i , o )] -> TB (TBSignal dom i )
136+ matchIOGenN expectedOutput gen = do
137+ TBDomain {.. } <- tbDomain @ dom
138+
139+ vRef <- liftIO $ newIORef []
140+ simStepCache <- liftIO (readIORef simStepRef >>= newIORef)
141+
142+ mind SomeSignal $ IOInput
143+ { signalId = NoID
144+ , signalCurVal = const $ do
145+ global <- readIORef simStepRef
146+ local <- readIORef simStepCache
147+
148+ if local == global
149+ then readIORef vRef >>= \ case
150+ (i, _) : _ -> return i
151+ [] -> do
152+ (i, o) : xr <- sample gen
153+ writeIORef vRef ((i, o) : xr)
154+ Prelude. print $ (i, o) : xr
155+ return i
156+ else do
157+ writeIORef simStepCache global
158+ readIORef vRef >>= \ case
159+ _ : (i, o) : xr -> do
160+ writeIORef vRef ((i, o) : xr)
161+ signalExpect expectedOutput $ Expectation (global + 1 , verify o)
162+ return i
163+ _ -> do
164+ (i, o) : xr <- sample gen
165+ Prelude. print $ (i, o) : xr
166+ writeIORef vRef ((i, o) : xr)
167+ signalExpect expectedOutput $ Expectation (global + 1 , verify o)
168+ return i
169+ , signalPrint = Nothing
170+ }
171+ where
172+ verify x y
173+ | x == y = Nothing
174+ | otherwise = Just $ " Expected '" <> show x <> " ' but the output is '" <> show y <> " '"
0 commit comments