Hedgehog Integration (WIP)

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

@@ -12,6 +12,7 @@ module Clash.Testbench.Generate where
 
 import Hedgehog
 import Hedgehog.Gen
+import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.State.Lazy (liftIO, when, modify)
 import Data.IORef (newIORef, readIORef, writeIORef)
 
@@ -102,7 +103,7 @@ 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
+matchIOGen checkedOutput gen = do
   TBDomain{..} <- tbDomain @dom
 
   vRef <- liftIO $ newIORef undefined
@@ -116,24 +117,30 @@ matchIOGen expectedOutput gen = do
 
         if progress
         then do
-          (i, o) <- sample gen
+          (input, expectedOutput) <- sample gen
           curStep <- readIORef simStepRef
-          signalExpect expectedOutput $ Expectation (curStep, verify o)
-          writeIORef vRef i
-
-          return i
+          signalExpect checkedOutput $ Expectation (curStep, verifier expectedOutput)
+          writeIORef vRef input
+          return input
         else
           readIORef vRef
     , signalPrint  = Nothing
     , ..
     }
 
  where
-  verify x y = do
-    when (x /= y)
-      $ footnote
-      $ "Expected '" <> show x <> "' but the output is '" <> show y <> "'"
-    x === x
+  verifier :: o -> o -> Verifier
+  verifier expectedOutput observedOutput = Verifier $ \case
+    Simple   -> checkDifferenceWith error undefined
+    Hedgehog -> checkDifferenceWith footnote (expectedOutput === observedOutput)
+   where
+    checkDifferenceWith :: MonadIO m => (String -> m ()) -> m () -> m ()
+    checkDifferenceWith report abort =
+      when (expectedOutput /= observedOutput) $ do
+        report
+           $ "Expected to see the output '" <> show expectedOutput <> "',"
+          <> "but the observed output is '" <> show observedOutput <> "'."
+        abort
 
 -- | Extended version of 'matchIOGen', which allows to specify valid
 -- IO behavior over a finite amount of simulation steps. During native
@@ -168,15 +175,15 @@ matchIOGenN checkedOutput gen = mdo
               memorize signalHistory h
               writeIORef vRef ((i, o) : xr)
               curStep <- readIORef simStepRef
-              signalExpect checkedOutput $ Expectation (curStep, verify s i o)
+              signalExpect checkedOutput $ Expectation (curStep, verifier s i o)
               return i
             [(h, _)] -> do
               memorize signalHistory h
               (i, o) : xr <- sample gen
 
               writeIORef vRef ((i, o) : xr)
               curStep <- readIORef simStepRef
-              signalExpect checkedOutput $ Expectation (curStep, verify s i o)
+              signalExpect checkedOutput $ Expectation (curStep, verifier s i o)
               return i
             _ -> error "unreachable"
           else \case
@@ -193,8 +200,14 @@ matchIOGenN checkedOutput gen = mdo
   return s
 
  where
-  verify generatedInput currentInput expectedOutput observedOutput = do
-    when (expectedOutput /= observedOutput) $ do
+  verifier :: TBSignal dom i -> i -> o -> o -> Verifier
+  verifier generatedInput currentInput expectedOutput observedOutput =
+    Verifier $ \case
+      Simple   -> checkDifferenceWith error undefined
+      Hedgehog -> checkDifferenceWith footnote failure
+   where
+    checkDifferenceWith :: MonadIO m => (String -> m ()) -> m () -> m ()
+    checkDifferenceWith report abort = do
       xs <-
         (<> [(currentInput, observedOutput)])
           <$> (zip <$> history generatedInput <*> history checkedOutput)
@@ -207,21 +220,21 @@ matchIOGenN checkedOutput gen = mdo
         iLen = maximum $ (length iHeading :) $ fmap (length . show . fst) xs
         oLen = maximum $ (length oHeading :) $ fmap (length . show . snd) xs
 
-      footnote $ unlines $
-        [ "Expected to see the output '" <> show expectedOutput <> "',"
-        , "but the observed output is '" <> show observedOutput <> "'."
-        , ""
-        , "I/O History:"
-        , ""
-        , cHeading <>
-          replicate (iLen - length iHeading + 2) ' ' <> iHeading <>
-          replicate (oLen - length oHeading + 2) ' ' <> oHeading
-        , replicate (cLen + iLen + oLen + 4) '-'
-        ] <>
-        [ replicate (cLen - length (show c))     ' ' <> show c <>
-          replicate (iLen - length (show i) + 2) ' ' <> show i <>
-          replicate (oLen - length (show o) + 2) ' ' <> show o
-        | (c, (i, o)) <- zip [0 :: Int,1..] xs
-        ]
-
-      failure
+      when (expectedOutput /= observedOutput) $ do
+        report $ unlines $
+          [ "Expected to see the output '" <> show expectedOutput <> "',"
+          , "but the observed output is '" <> show observedOutput <> "'."
+          , ""
+          , "I/O History:"
+          , ""
+          , cHeading <>
+            replicate (iLen - length iHeading + 2) ' ' <> iHeading <>
+            replicate (oLen - length oHeading + 2) ' ' <> oHeading
+          , replicate (cLen + iLen + oLen + 4) '-'
+          ] <>
+          [ replicate (cLen - length (show c))     ' ' <> show c <>
+            replicate (iLen - length (show i) + 2) ' ' <> show i <>
+            replicate (oLen - length (show o) + 2) ' ' <> show o
+          | (c, (i, o)) <- zip [0 :: Int,1..] xs
+          ]
+        abort

clash-testbench/src/Clash/Testbench/Internal/Monad.hs

@@ -42,7 +42,7 @@ import Data.IORef (IORef, newIORef, readIORef, writeIORef, modifyIORef)
 import Data.List (partition, sort, sortBy, groupBy)
 import Data.Maybe (catMaybes)
 
-import qualified Data.Map as M
+import qualified Data.Map.Strict as M
 import qualified Data.Set as S
 import qualified Data.Array as A
 
@@ -243,18 +243,17 @@ instance
       , signalName = name
       , signalUpdate = Just (writeIORef extVal . Just)
       , signalExpect = modifyIORef expectations . (:)
-      , signalVerify = \mode -> do
+      , signalVerify = \sMode -> Verifier $ \vMode -> do
           curStep <- liftIO $ readIORef simStepRef
-          value <- liftIO $ signalCurVal mode
+          value <- liftIO $ signalCurVal sMode
           expct <- liftIO $ readIORef expectations
 
           let
             (current, later) =
               partition (`leq` Expectation (curStep + 1, undefined)) expct
 
           liftIO $ writeIORef expectations later
-          mapM_ ((value &) . snd . expectation) current
-
+          mapM_ ((`verifier` vMode) . (value &) . snd . expectation) current
       , signalPrint = Nothing
       , signalPlug = Nothing
       , ..
@@ -449,7 +448,6 @@ initializeLiftTB name x = liftTB accInit x
 progressCheck :: IORef Int -> Bool -> TB (IO Bool)
 progressCheck simStepRef initialProgress = do
   simStepCache <- liftIO ((offset <$> readIORef simStepRef) >>= newIORef)
-
   return $ do
     globalRef <- readIORef simStepRef
     localRef  <- readIORef simStepCache
@@ -458,13 +456,12 @@ progressCheck simStepRef initialProgress = do
       writeIORef simStepCache globalRef
 
     return $ globalRef > localRef
-
  where
   offset
     | initialProgress = (+ (-1))
     | otherwise       = id
 
-
+-- | Creates a new 'History' container.
 newHistory ::
   TB (History a)
 newHistory = do
@@ -474,6 +471,7 @@ newHistory = do
   historyBuffer <- liftIO $ newIORef Nothing
   return History{..}
 
+-- | Memorizes a value inside the given 'History' container.
 memorize :: MonadIO m => History a -> a -> m ()
 memorize History{..} value =
   liftIO $ readIORef historySize >>= \case
@@ -490,6 +488,8 @@ memorize History{..} value =
       writeArray buf pos $ Just value
       writeIORef historyBufferPos $ pos + 1
 
+-- | Reveals the history of a test bench signal. The returned list is
+-- given in temporal order.
 history ::
   (KnownDomain dom, MonadIO m) =>
   TBSignal dom a ->
@@ -499,11 +499,9 @@ history s = liftIO $ readIORef historyBuffer >>= \case
   Just buf -> do
     pos <- readIORef historyBufferPos
     catMaybes . uncurry (flip (<>)) . splitAt pos <$> getElems buf
-
  where
   History{..} = signalHistory s
 
-
 -- | Some generalized extender for the accumulated continuation.
 extendVia ::
   Monad m =>

clash-testbench/src/Clash/Testbench/Internal/Signal.hs

@@ -9,12 +9,12 @@ Lifted signal types and internal data structures for
 module Clash.Testbench.Internal.Signal where
 
 import Algebra.PartialOrd
+import Control.Monad.IO.Class (MonadIO)
+import Data.Array.IO (IOArray)
 import Data.Function (on)
-
+import Data.IORef (IORef)
 import Hedgehog (PropertyT)
 
-import Data.Array.IO (IOArray)
-import Data.IORef (IORef)
 import Clash.Prelude
   ( KnownDomain(..), BitPack(..), SDomainConfiguration(..), NFDataX, Type
   , Domain, Signal, Clock, Reset, Enable
@@ -23,6 +23,7 @@ import Clash.Prelude
 
 import Clash.FFI.VPI.Module (Module)
 import Clash.FFI.VPI.Port (Port, Direction)
+
 import Clash.Testbench.Internal.ID
 
 -- | Test bench design stages
@@ -38,12 +39,12 @@ data Stage :: Type where
   -- successfully. Post-processing also introduces the switch from
   -- 'USER' to 'FINAL' on the type level.
 
--- | The supported simulation modes sources.
-data SimMode where
-  Internal :: SimMode
-  -- ^ Internal pure Haskell based simulation
-  External :: SimMode
-  -- ^ Co-Simulation via Clash-FFI
+-- | Supported simulation modes sources
+data SimMode =
+    Internal
+    -- ^ Internal pure Haskell based simulation
+  | External
+    -- ^ Co-Simulation via Clash-FFI
 
 -- | Type family for handling simulation mode dependent types.
 -- 'SimMode' does not have to be fixed during test bench creation, but
@@ -53,7 +54,7 @@ type family SimModeDependent (s :: Stage) a where
   SimModeDependent 'USER  a = SimMode -> a
   SimModeDependent 'FINAL a = a
 
--- | Clash-FFI Port connector.
+-- | Clash-FFI port connector
 data PortInterface =
   PortInterface
     { port          :: Port
@@ -63,24 +64,25 @@ data PortInterface =
     , portDirection :: Direction
     }
 
--- | Clash-FFI Module connector.
+-- | Clash-FFI module connector
 data ModuleInterface =
   ModuleInterface
-    { module_       :: Module
+    { module_    :: Module
     , inputPort  :: ID () -> PortInterface
       -- TODO: multiple port support vie Bundle/Unbundle
     , outputPort :: PortInterface
     }
 
+-- | Size bounded signal history
 data History a =
   History
-    { historySize :: IORef Int
+    { historySize      :: IORef Int
     , historyBufferPos :: IORef Int
-    , historyBuffer :: IORef (Maybe (IOArray Int (Maybe a)))
+    , historyBuffer    :: IORef (Maybe (IOArray Int (Maybe a)))
     }
 
--- | Expectations on certain outputs at the given simulation step.
-newtype Expectation a = Expectation { expectation :: (Int, a -> PropertyT IO ()) }
+-- | Expectations on certain outputs at the given simulation step
+newtype Expectation a = Expectation { expectation :: (Int, a -> Verifier) }
 
 -- | Expectations cannot be compared: they are always unequal.
 instance Eq (Expectation a) where
@@ -92,6 +94,31 @@ instance PartialOrd (Expectation a) where
   leq        (Expectation (x, _)) (Expectation (y, _)) = x <= y
   comparable (Expectation (x, _)) (Expectation (y, _)) = x /= y
 
+-- | The verification mode determines the environment in which a
+-- verifier is executed.
+data VerificationMode m where
+  Simple   :: VerificationMode IO
+  Hedgehog :: VerificationMode (PropertyT IO)
+
+-- | Existential quantified container for passing different
+-- verification environments around.
+data Verifier =
+  Verifier
+    { verifier :: (forall m. MonadIO m => VerificationMode m -> m ())
+    }
+
+-- | Runs a verifier in a supported verification environment.
+class Verify m where
+  verify :: Verifier -> m ()
+
+instance Verify IO where
+  verify = \case
+    Verifier v -> v Simple
+
+instance Verify (PropertyT IO) where
+  verify = \case
+    Verifier v -> v Hedgehog
+
 -- | The lifted 'Clash.Signal.Signal' type to be used in
 -- 'Clash.Testbench.Internal.Monad.TB'.
 data TBSignal (s :: Stage) (dom :: Domain) a =
@@ -116,7 +143,7 @@ data TBSignal (s :: Stage) (dom :: Domain) a =
       , signalExpect :: Expectation a -> IO ()
       -- ^ Registers an expectation on the content of this signal to
       -- be verified during simulation
-      , signalVerify :: SimModeDependent s (PropertyT IO ())
+      , signalVerify :: SimModeDependent s Verifier
       -- ^ The expectation verifier
       , signalHistory :: History a
       -- ^ Bounded history of signal values