Skip to content

Commit

Permalink
Hedgehog Integration (WIP)
Browse files Browse the repository at this point in the history
  • Loading branch information
kleinreact committed May 16, 2023
1 parent fdf0667 commit 14f75bb
Show file tree
Hide file tree
Showing 8 changed files with 337 additions and 130 deletions.
1 change: 1 addition & 0 deletions clash-testbench/clash-testbench.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ library
base,
mtl,
array,
lattices,
hedgehog,
containers,
bytestring,
Expand Down
41 changes: 38 additions & 3 deletions clash-testbench/example/Main.hs
Original file line number Diff line number Diff line change
@@ -1,24 +1,59 @@
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE DataKinds #-}
module Main where

import Data.Bool (bool)

import Clash.Prelude (Signed)

import Clash.Testbench

import Calculator (OPC(..))
import qualified Calculator (topEntity)

import Clash.Hedgehog.Sized.Signed
import Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range

genIO :: Gen [(OPC (Signed 4), Maybe (Signed 4))]
genIO = do
-- generate 7 constants
cs <- Gen.list (Range.singleton 7) (genSigned Range.constantBounded)
-- generate 6 operations
ops <- map (bool (ADD, (+)) (MUL, (*))) <$> Gen.list (Range.singleton 6) Gen.bool

let
-- push the constants to the stack
in1 = concatMap ((: [Push]) . Imm) cs -- inputs
eo1 = concatMap ((: [Nothing]) . Just) cs -- expected outputs

-- calculate the results of the applied operations
x : xr = reverse cs
rs = [ foldl (\a (op, b) -> op a b) x $ zip (map snd ops) $ take n xr
| n <- [1,2..length xr]
]

-- apply the operations
in2 = concatMap ((replicate 3 Pop <>) . pure . fst) ops -- inputs
eo2 = concatMap ((replicate 3 Nothing <>) . pure . Just) rs -- expected outputs

return $ zip (in1 <> in2) (eo1 <> eo2)

myTestbench
:: TB ()
myTestbench = mdo
input <- fromList Pop [Imm 1, Push, Imm 2, Push, Pop, Pop, Pop, ADD]
-- input <- fromList Pop [Imm 1, Push, Imm 2, Push, Pop, Pop, Pop, ADD]
input <- matchIOGenN output genIO
output <- ("topEntity" @@ Calculator.topEntity) auto auto auto input
watch input
watch output

main :: IO ()
main = simulate 10 myTestbench
main = simulate 38 myTestbench

foreign export ccall "clash_ffi_main"
ffiMain :: IO ()

ffiMain :: IO ()
ffiMain = simulateFFI 10 myTestbench
ffiMain = simulateFFI 38 myTestbench
2 changes: 1 addition & 1 deletion clash-testbench/example/cabal.project
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
packages: . .. ../../clash-ghc ../../clash-lib ../../clash-prelude ../../clash-ffi
packages: . .. ../../clash-ghc ../../clash-lib ../../clash-prelude ../../clash-ffi ../../clash-prelude-hedgehog

write-ghc-environment-files: always
2 changes: 2 additions & 0 deletions clash-testbench/example/clash-testbench-example.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,9 @@ common basic-config
-fplugin GHC.TypeLits.KnownNat.Solver
build-depends:
base,
hedgehog,
clash-prelude,
clash-prelude-hedgehog,
clash-testbench,
ghc-typelits-extra,
ghc-typelits-knownnat,
Expand Down
137 changes: 131 additions & 6 deletions clash-testbench/src/Clash/Testbench/Generate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ module Clash.Testbench.Generate where

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

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

Expand All @@ -10,15 +12,138 @@ 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 <> "'"


generate ::
(NFDataX a, BitPack a, KnownDomain dom) =>
Gen a -> TB (TBSignal dom a)
generate generator =
mindSignal Generator
a -> Gen a -> TB (TBSignal dom a)
generate def gen = do
ST{..} <- get

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

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

if v == v'
then readIORef vRef
else do
x <- sample gen
writeIORef vRef x
writeIORef simStepCache v
return x
, signalPrint = Nothing
, ..
}


generateN ::
(NFDataX a, BitPack a, KnownDomain dom) =>
a -> Gen [a] -> TB (TBSignal dom a)
generateN def gen = do
ST{..} <- get

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

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

if v == v'
then readIORef vRef >>= \case
x : _ -> return x
[] -> do
x : xr <- sample gen
writeIORef vRef (x : xr)
return x

else do
writeIORef simStepCache v
readIORef vRef >>= \case
_ : x : xr -> do
writeIORef vRef (x : xr)
return x
_ -> do
x : xr <- sample gen
writeIORef vRef (x : xr)
return x
, signalPrint = Nothing
, ..
}
Loading

0 comments on commit 14f75bb

Please sign in to comment.