Skip to content

Commit 0008eab

Browse files
committed
Hedgehog Integration (WIP)
1 parent a7a8671 commit 0008eab

File tree

5 files changed

+234
-143
lines changed

5 files changed

+234
-143
lines changed

clash-testbench/src/Clash/Testbench/Generate.hs

Lines changed: 50 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module Clash.Testbench.Generate where
1010

1111
import Hedgehog
1212
import Hedgehog.Gen
13-
import Control.Monad.State.Lazy (liftIO)
13+
import Control.Monad.State.Lazy (liftIO, when, modify)
1414
import Data.IORef (newIORef, readIORef, writeIORef)
1515

1616
import Clash.Prelude (KnownDomain(..), BitPack(..), NFDataX)
@@ -101,74 +101,85 @@ matchIOGen expectedOutput gen = do
101101
TBDomain{..} <- tbDomain @dom
102102

103103
vRef <- liftIO $ newIORef undefined
104-
simStepCache <- liftIO (readIORef simStepRef >>= newIORef)
104+
checkForProgress <- progressCheck simStepRef False
105105

106106
mind SomeSignal $ IOInput
107107
{ signalId = NoID
108108
, signalCurVal = const $ do
109-
global <- readIORef simStepRef
110-
local <- readIORef simStepCache
109+
progress <- checkForProgress
111110

112-
if local == global
113-
then readIORef vRef
114-
else do
111+
if progress
112+
then do
115113
(i, o) <- sample gen
116-
signalExpect expectedOutput $ Expectation (global + 1, verify o)
117-
114+
curStep <- readIORef simStepRef
115+
signalExpect expectedOutput $ Expectation (curStep, verify o)
118116
writeIORef vRef i
119-
writeIORef simStepCache global
117+
120118
return i
119+
else
120+
readIORef vRef
121121
, signalPrint = Nothing
122122
}
123+
123124
where
124-
verify x y
125-
| x == y = Nothing
126-
| otherwise = Just $ "Expected " <> show x <> " but the output is " <> show y
125+
verify x y = do
126+
when (x /= y)
127+
$ footnote
128+
$ "Expected '" <> show x <> "' but the output is '" <> show y <> "'"
129+
x === x
127130

128131
-- | 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+
-- IO behavior over a finite amount of simulation steps. During native
133+
-- simulation (no property check), the generator is repeatedly called
134+
-- after all the generated simulation steps have been consumed. The
135+
-- generator is only called once if the test bench is converted to a
136+
-- property instead.
132137
matchIOGenN ::
133138
forall dom i o.
134139
(NFDataX i, BitPack i, KnownDomain dom, Eq o, Show o, Show i) =>
135140
TBSignal dom o -> Gen [(i, o)] -> TB (TBSignal dom i)
136141
matchIOGenN expectedOutput gen = do
137142
TBDomain{..} <- tbDomain @dom
138143

139-
vRef <- liftIO $ newIORef []
140-
simStepCache <- liftIO (readIORef simStepRef >>= newIORef)
144+
xs <- liftIO $ sample gen
145+
modify $ \st@ST{..} -> st { simSteps = max simSteps $ length xs }
146+
147+
vRef <- liftIO $ newIORef xs
148+
checkForProgress <- progressCheck simStepRef False
141149

142150
mind SomeSignal $ IOInput
143-
{ signalId = NoID
151+
{ signalId = NoID
144152
, signalCurVal = const $ do
145-
global <- readIORef simStepRef
146-
local <- readIORef simStepCache
153+
progress <- checkForProgress
147154

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
155+
readIORef vRef >>=
156+
if progress
157+
then \case
159158
_ : (i, o) : xr -> do
160159
writeIORef vRef ((i, o) : xr)
161-
signalExpect expectedOutput $ Expectation (global + 1, verify o)
160+
curStep <- readIORef simStepRef
161+
signalExpect expectedOutput $ Expectation (curStep, verify o)
162162
return i
163163
_ -> do
164164
(i, o) : xr <- sample gen
165-
Prelude.print $ (i, o) : xr
165+
166166
writeIORef vRef ((i, o) : xr)
167-
signalExpect expectedOutput $ Expectation (global + 1, verify o)
167+
curStep <- readIORef simStepRef
168+
signalExpect expectedOutput $ Expectation (curStep, verify o)
168169
return i
169-
, signalPrint = Nothing
170+
else \case
171+
(i, _) : _ -> return i
172+
[] -> do
173+
(i, o) : xr <- sample gen
174+
writeIORef vRef ((i, o) : xr)
175+
Prelude.print $ (i, o) : xr
176+
return i
177+
, signalPrint = Nothing
170178
}
179+
171180
where
172-
verify x y
173-
| x == y = Nothing
174-
| otherwise = Just $ "Expected '" <> show x <> "' but the output is '" <> show y <> "'"
181+
verify x y = do
182+
when (x /= y)
183+
$ footnote
184+
$ "Expected '" <> show x <> "' but the output is '" <> show y <> "'"
185+
x === x

clash-testbench/src/Clash/Testbench/Input.hs

Lines changed: 42 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,6 @@ module Clash.Testbench.Input
1212

1313
import Control.Monad.State.Lazy
1414
import Data.IORef
15-
import Data.Maybe (fromMaybe)
16-
import Data.List (uncons)
1715

1816
import Clash.Prelude (KnownDomain(..), BitPack(..), NFDataX)
1917

@@ -22,33 +20,58 @@ import Clash.Testbench.Internal.Signal hiding (TBSignal)
2220
import Clash.Testbench.Internal.Monad
2321
import Clash.Testbench.Internal.ID
2422

23+
-- | The mode defines how to expand finite lists towards infinite
24+
-- ones. If a list is already infinite, then it does not matter which
25+
-- mode is chosen at this point.
26+
data ExpansionMode a =
27+
Repeat
28+
-- ^ Repeat a finite list indefinitely. This mode causes an error
29+
-- if the list to be repeated is the empty list.
30+
| Default a
31+
-- ^ Repeat a given default value after the end of a finite list
32+
-- has been reached.
33+
| IsInfinite
34+
-- ^ The list has to be infinite. This mode causes an error if the
35+
-- end of a finite list is reached.
36+
2537
-- | Creates an input signal whose values are taken from a finite or
2638
-- infinite list. If the list is finite and the number of simulation
2739
-- steps exceeds the length of the list, then the value of the first
2840
-- argument is used repeatedly.
2941
fromList :: forall dom a.
30-
(KnownDomain dom, BitPack a, NFDataX a, Show a) =>
31-
a -> [a] -> TB (TBSignal dom a)
32-
fromList x xs = do
42+
(KnownDomain dom, BitPack a, NFDataX a) =>
43+
ExpansionMode a -> [a] -> TB (TBSignal dom a)
44+
45+
fromList Repeat [] =
46+
error $ "Clash.Testbench.Input.fromList: "
47+
<> "The empty list cannot be repeated indefinitely."
48+
49+
fromList mode xs = do
3350
TBDomain{..} <- tbDomain @dom
3451

35-
listRef <- liftIO $ newIORef $ x : xs
36-
simStepCache <- liftIO (readIORef simStepRef >>= newIORef)
52+
vRef <- liftIO $ newIORef xs
53+
checkForProgress <- progressCheck simStepRef False
3754

3855
mind SomeSignal $ IOInput
3956
{ signalId = NoID
4057
, signalPrint = Nothing
4158
, signalCurVal = const $ do
42-
(r, rs) <- fromMaybe (x, []) . uncons <$> readIORef listRef
43-
global <- readIORef simStepRef
44-
local <- readIORef simStepCache
45-
46-
if local == global
47-
then return r
48-
else do
49-
writeIORef listRef rs
50-
writeIORef simStepCache global
51-
return $ case rs of
52-
[] -> x
53-
y:_ -> y
59+
readIORef vRef >>= \case
60+
[] -> case mode of
61+
Repeat -> do
62+
let (x : xr) = xs
63+
writeIORef vRef xr
64+
return x
65+
Default v ->
66+
return v
67+
IsInfinite ->
68+
error $ "Clash.Testbench.Input.fromList: "
69+
<> "End of list reached."
70+
x : xr -> do
71+
progress <- checkForProgress
72+
73+
when progress $
74+
writeIORef vRef xr
75+
76+
return x
5477
}

0 commit comments

Comments
 (0)