Hedgehog Integration (WIP)

kleinreact · kleinreact · commit ad42dc5f92f7 · 2023-06-29T14:44:20.000+02:00
diff --git a/clash-testbench/clash-testbench.cabal b/clash-testbench/clash-testbench.cabal
@@ -43,6 +43,7 @@ library
     Clash.Testbench.Internal.ID
     Clash.Testbench.Internal.Signal
     Clash.Testbench.Internal.Monad
+    Control.Monad.Extra
   build-depends:
     base,
     mtl,
diff --git a/clash-testbench/example/Main.hs b/clash-testbench/example/Main.hs
@@ -1,21 +1,28 @@
 {-# LANGUAGE RecursiveDo #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE OverloadedStrings #-}
 module Main where
 
 import Data.Bool (bool)
 
-import Clash.Prelude (Signed)
+import Clash.Prelude (Signal, Clock, Reset, Enable, Signed, System, exposeClockResetEnable, register, bundle, unsafeFromReset, hasReset, fromEnable, hasEnable)
 
 import Clash.Testbench
 
 import Calculator (OPC(..))
-import qualified Calculator (topEntity)
+--import qualified Calculator (topEntity)
+import qualified Register (topEntity)
+import qualified RegisterFail (topEntity)
 
+import Control.Monad (void)
+import Control.Monad.IO.Class
 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
@@ -43,17 +50,62 @@ genIO = do
 myTestbench
   :: TB ()
 myTestbench = mdo
---  input <- fromList Pop [Imm 1, Push, Imm 2, Push, Pop, Pop, Pop, ADD]
-  input <- matchIOGenN output genIO
+  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
+-}
+
+rstenb
+  :: Clock  System
+  -> Reset  System
+  -> Enable System
+  -> Signal System (Bool, Bool)
+rstenb = exposeClockResetEnable
+  $ bundle (unsafeFromReset hasReset, fromEnable hasEnable)
+
+myTestbench
+  :: TB ()
+myTestbench = mdo
+  input <- matchIOGenN output $ do
+    cs  <- Gen.list (Range.singleton 7) (genSigned Range.constantBounded)
+    return $ ((0,0) :) $ zip cs $ 0 : cs
+  output <- ("topEntity" @@ Register.topEntity) auto auto auto input
+--  x <- ("rstenb" @@ rstenb) auto auto auto
+--  watch x
+  watch input
+  watch output
+
+myTestbenchFail
+  :: TB ()
+myTestbenchFail = mdo
+  input <- matchIOGenN output $ do
+    cs  <- Gen.list (Range.singleton 7) (genSigned Range.constantBounded)
+    return $ ((0,0) :) $ zip cs $ 0 : cs
+  output <- ("topEntity" @@ RegisterFail.topEntity) auto auto auto input
+--  x <- ("rstenb" @@ rstenb) auto auto auto
+--  watch x
+  watch input
+  watch output
+
 
 main :: IO ()
-main = simulate 38 myTestbench
+main =
+--  simulate 10 myTestbench
+  void $ checkParallel $ Group "Default"
+    [ ("'successful test'", withTests 1 $ tbProperty myTestbench)
+    , ("'failing test'", withTests 1 $ tbProperty myTestbenchFail)
+    ]
 
 foreign export ccall "clash_ffi_main"
   ffiMain :: IO ()
 
 ffiMain :: IO ()
-ffiMain = simulateFFI 38 myTestbench
+ffiMain = do
+--  simulateFFI (SimSettings False False) myTestbench
+  sync <- ffiHedgehog
+  ffiCheckGroup sync $ Group "Default"
+    [ ("'successful test'", withTests 1 $ (tbPropertyFFI sync) myTestbench)
+--    [ ("'failing test'", withTests 1 $ (tbPropertyFFI sync) myTestbenchFail)
+    ]
diff --git a/clash-testbench/example/Register.hs b/clash-testbench/example/Register.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+module Register where
+
+import Clash.Prelude
+
+topEntity
+  :: Clock  System
+  -> Reset  System
+  -> Enable System
+  -> Signal System (Signed 4)
+  -> Signal System (Signed 4)
+  
+topEntity = exposeClockResetEnable reg
+  where
+    reg i = register 0 i
diff --git a/clash-testbench/example/RegisterFail.hs b/clash-testbench/example/RegisterFail.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE DataKinds #-}
+module RegisterFail where
+
+import Clash.Prelude
+
+topEntity
+  :: Clock  System
+  -> Reset  System
+  -> Enable System
+  -> Signal System (Signed 4)
+  -> Signal System (Signed 4)
+  
+topEntity = exposeClockResetEnable regFail
+  where    
+    reg i = register 0 i
+    
+    count ::
+      HiddenClockResetEnable dom =>
+      Signal dom (Signed 3)
+    count =
+      register 0 ((+1) <$> count)
+    
+    regFail ::
+      HiddenClockResetEnable dom =>
+      Signal dom (Signed 4) ->
+      Signal dom (Signed 4)
+      
+    regFail =
+      mux ((== 4) <$> count) 0 . reg    
+   
+    
diff --git a/clash-testbench/example/cabal.project b/clash-testbench/example/cabal.project
@@ -1,3 +1,6 @@
 packages: . .. ../../clash-ghc ../../clash-lib ../../clash-prelude ../../clash-ffi ../../clash-prelude-hedgehog
 
 write-ghc-environment-files: always
+
+--package *
+--  ghc-options: -fPIC -shared
diff --git a/clash-testbench/example/clash-testbench-example.cabal b/clash-testbench/example/clash-testbench-example.cabal
@@ -14,7 +14,7 @@ category:           Hardware
 common basic-config
   default-language: Haskell2010
   ghc-options:
-    -Wall -Wcompat
+    -Wall -Wcompat -threaded
     -fplugin GHC.TypeLits.Extra.Solver
     -fplugin GHC.TypeLits.Normalise
     -fplugin GHC.TypeLits.KnownNat.Solver
@@ -39,13 +39,19 @@ executable simulate
   import:           basic-config
   main-is:          Main.hs
   other-modules:    Calculator
+                    Register
+                    RegisterFail
   -- this option is required, since clash-ffi and clash-testbench come
   -- with unresovled symbols for the VPI interface
   ghc-options:      -optl -Wl,--unresolved-symbols=ignore-in-object-files
 
+
 foreign-library simulate-ffi
   import:           basic-config
   other-modules:    Main
                     Calculator
+                    Register
+                    RegisterFail
   type:             native-shared
+--  options:          standalone
   lib-version-info: 0:1:0
diff --git a/clash-testbench/example/run-iverilog.sh b/clash-testbench/example/run-iverilog.sh
@@ -26,9 +26,11 @@ VVP=vvp
 
 ${CABAL} build clash-testbench-example || exit $?
 ${CLASH} --verilog Calculator.hs || exit $?
-${IVERILOG} verilog/Calculator.topEntity/topEntity.v -o Calculator.vvp \
+${CLASH} --verilog Register.hs || exit $?
+${CLASH} --verilog RegisterFail.hs || exit $?
+${IVERILOG} verilog/Register.topEntity/topEntity.v -o Register.vvp \
   || exit $?
 echo ""
 echo "Running Icarus Verilog VVP runtime engine:"
 echo ""
-${VVP} -Mlib -mlibsimulate-ffi Calculator.vvp
+${VVP} -Mlib -mlibsimulate-ffi Register.vvp
diff --git a/clash-testbench/src/Clash/Testbench/Generate.hs b/clash-testbench/src/Clash/Testbench/Generate.hs
@@ -12,6 +12,7 @@ module Clash.Testbench.Generate where
 
 import Hedgehog
 import Hedgehog.Gen
+import Control.Monad.Extra ((<?>), (<:>))
 import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.State.Lazy (liftIO, when, modify)
 import Data.IORef (newIORef, readIORef, writeIORef)
@@ -33,24 +34,21 @@ generate gen = do
   TBDomain{..} <- tbDomain @dom
 
   vRef <- liftIO $ newIORef undefined
-  checkForProgress <- progressCheck simStepRef True
+  ifProgress <- progressCheck simStepRef True
   signalHistory <- newHistory
 
   mind SomeSignal IOInput
     { signalId     = NoID
-    , signalCurVal = const $ do
-        progress <- checkForProgress
-
-        if progress
-        then do
+    , signalCurVal = const $ ifProgress
+        <?> do
           x <- sample gen
           writeIORef vRef x
           memorize signalHistory x
           return x
-        else
+        <:>
           readIORef vRef
     , signalPrint  = Nothing
-    ,..
+    , ..
     }
 
 -- | Extended version of 'generate', which allows to generate a finite
@@ -65,28 +63,24 @@ generateN def gen = do
   TBDomain{..} <- tbDomain @dom
 
   vRef <- liftIO $ newIORef [def]
-  checkForProgress <- progressCheck simStepRef False
+  ifProgress <- progressCheck simStepRef False
   signalHistory <- newHistory
 
   mind SomeSignal IOInput
     { signalId     = NoID
-    , signalCurVal = const $ do
-        progress <- checkForProgress
-
-        if progress
-        then
-          readIORef vRef >>= \case
-            h : x : xr -> do
-              memorize signalHistory h
-              writeIORef vRef (x : xr)
-              return x
-            [h] -> do
-              memorize signalHistory h
-              x : xr <- sample gen
-              writeIORef vRef (x : xr)
-              return x
-            _ -> error "unreachable"
-        else readIORef vRef >>= \case
+    , signalCurVal = const $ ifProgress
+        <?> readIORef vRef >>= \case
+          h : x : xr -> do
+            memorize signalHistory h
+            writeIORef vRef (x : xr)
+            return x
+          [h] -> do
+            memorize signalHistory h
+            x : xr <- sample gen
+            writeIORef vRef (x : xr)
+            return x
+          _ -> error "unreachable"
+        <:> readIORef vRef >>= \case
           x : _ -> return x
           [] -> do
             x : xr <- sample gen
@@ -107,22 +101,19 @@ matchIOGen checkedOutput gen = do
   TBDomain{..} <- tbDomain @dom
 
   vRef <- liftIO $ newIORef undefined
-  checkForProgress <- progressCheck simStepRef False
+  ifProgress <- progressCheck simStepRef False
   signalHistory <- newHistory
 
   mind SomeSignal $ IOInput
     { signalId     = NoID
-    , signalCurVal = const $ do
-        progress <- checkForProgress
-
-        if progress
-        then do
+    , signalCurVal = const $ ifProgress
+        <?> do
           (input, expectedOutput) <- sample gen
           curStep <- readIORef simStepRef
           signalExpect checkedOutput $ Expectation (curStep, verifier expectedOutput)
           writeIORef vRef input
           return input
-        else
+        <:>
           readIORef vRef
     , signalPrint  = Nothing
     , ..
@@ -157,42 +148,37 @@ matchIOGenN checkedOutput gen = mdo
 
   xs <- liftIO $ sample gen
   modify $ \st@ST{..} -> st { simSteps = max simSteps $ length xs }
-  liftIO $ Prelude.print xs
 
   vRef <- liftIO $ newIORef xs
-  checkForProgress <- progressCheck simStepRef False
+  ifProgress <- progressCheck simStepRef False
   signalHistory <- newHistory
 
   s <- mind SomeSignal $ IOInput
     { signalId = NoID
-    , signalCurVal = const $ do
-        progress <- checkForProgress
-
-        readIORef vRef >>=
-          if progress
-          then \case
-            (h, _) : (i, o) : xr -> do
-              memorize signalHistory h
-              writeIORef vRef ((i, o) : xr)
-              curStep <- readIORef simStepRef
-              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, verifier s i o)
-              return i
-            _ -> error "unreachable"
-          else \case
-            (i, _) : _ -> return i
-            [] -> do
-              (i, o) : xr <- sample gen
-              writeIORef vRef ((i, o) : xr)
-              Prelude.print $ (i, o) : xr
-              return i
+    , signalCurVal = const $ ifProgress
+        <?> readIORef vRef >>= \case
+          (h, _) : (i, o) : xr -> do
+            memorize signalHistory h
+            writeIORef vRef ((i, o) : xr)
+            curStep <- readIORef simStepRef
+            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, verifier s i o)
+            return i
+          _ -> error "unreachable"
+        <:> readIORef vRef >>= \case
+          (i, _) : _ -> return i
+          [] -> do
+            (i, o) : xr <- sample gen
+            writeIORef vRef ((i, o) : xr)
+            Prelude.print $ (i, o) : xr
+            return i
     , signalPrint = Nothing
     , ..
     }
diff --git a/clash-testbench/src/Clash/Testbench/Internal/Monad.hs b/clash-testbench/src/Clash/Testbench/Internal/Monad.hs
diff --git a/clash-testbench/src/Clash/Testbench/Simulate.hs b/clash-testbench/src/Clash/Testbench/Simulate.hs
diff --git a/clash-testbench/src/Control/Monad/Extra.hs b/clash-testbench/src/Control/Monad/Extra.hs
