From ff5065834a9dc8fe8a2c30feb3fd7a327f8536f6 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 26 Dec 2019 01:34:52 +0100 Subject: Add configuration for default Yosys location --- src/Verismith/Config.hs | 8 +++++++- src/Verismith/Fuzz.hs | 13 ++++++++----- src/Verismith/Result.hs | 14 +++++++++++++- 3 files changed, 28 insertions(+), 7 deletions(-) diff --git a/src/Verismith/Config.hs b/src/Verismith/Config.hs index cd7e501..2c239d7 100644 --- a/src/Verismith/Config.hs +++ b/src/Verismith/Config.hs @@ -72,6 +72,7 @@ module Verismith.Config , propCombine , propDeterminism , propNonDeterminism + , propDefaultYosys , parseConfigFile , parseConfig , encodeConfig @@ -239,6 +240,9 @@ data ConfProperty = ConfProperty { _propSize :: {-# UNPACK #-} !Int , _propDeterminism :: {-# UNPACK #-} !Int -- ^ @determinism@: the frequency at which determinism should -- be generated (currently modules are always deterministic). + , _propDefaultYosys :: !(Maybe Text) + -- ^ @default.yosys@: Default location for Yosys, which will be used for + -- equivalence checking. } deriving (Eq, Show) @@ -322,7 +326,7 @@ defaultConfig :: Config defaultConfig = Config (Info (pack $(gitHash)) (pack $ showVersion version)) (Probability defModItem defStmnt defExpr) - (ConfProperty 20 Nothing 3 2 5 "random" 10 False 0 1) + (ConfProperty 20 Nothing 3 2 5 "random" 10 False 0 1 Nothing) [] [fromYosys defaultYosys, fromVivado defaultVivado] where @@ -447,6 +451,8 @@ propCodec = .= _propNonDeterminism <*> defaultValue (defProp propDeterminism) (Toml.int "determinism") .= _propDeterminism + <*> Toml.dioptional (Toml.text (twoKey "default" "yosys")) + .= _propDefaultYosys where defProp i = defaultConfig ^. configProperty . i simulator :: TomlCodec SimDescription diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs index ff55011..50d6ae7 100644 --- a/src/Verismith/Fuzz.hs +++ b/src/Verismith/Fuzz.hs @@ -50,8 +50,8 @@ import Hedgehog.Internal.Seed (Seed) import qualified Hedgehog.Internal.Seed as Hog import qualified Hedgehog.Internal.Tree as Hog import Prelude hiding (FilePath) -import Shelly hiding (get) -import Shelly.Lifted (MonadSh, liftSh) +import Shelly hiding (get, sub) +import Shelly.Lifted (MonadSh, liftSh, sub) import System.FilePath.Posix (takeBaseName) import Verismith.Config import Verismith.CounterEg (CounterEg (..)) @@ -273,16 +273,17 @@ equivalence src = do datadir <- fmap _fuzzDataDir askOpts checker <- fmap _fuzzOptsChecker askOpts synth <- passedSynthesis + conf <- fmap _fuzzOptsConfig askOpts let synthComb = if doCrossCheck then nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth else nubBy tupEq . filter (uncurry (/=)) $ (,) defaultIdentitySynth <$> synth - resTimes <- liftSh $ mapM (uncurry (equiv checker datadir)) synthComb + resTimes <- liftSh $ mapM (uncurry (equiv (conf ^. configProperty . propDefaultYosys) checker datadir)) synthComb fuzzSynthResults .= toSynthResult synthComb resTimes liftSh $ inspect resTimes where tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') - equiv checker datadir a b = + equiv yosysloc checker datadir a b = toolRun ("equivalence check for " <> toText a <> " and " <> toText b) . runResultT $ do make dir @@ -297,7 +298,9 @@ equivalence src = do synthOutput b ) $ synthOutput b writefile "rtl.v" $ genSource src - runEquiv checker datadir a b src + sub $ do + maybe (return ()) (liftSh . prependToPath . fromText) yosysloc + runEquiv checker datadir a b src where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m () diff --git a/src/Verismith/Result.hs b/src/Verismith/Result.hs index 2ecb728..78c8dd6 100644 --- a/src/Verismith/Result.hs +++ b/src/Verismith/Result.hs @@ -29,13 +29,15 @@ module Verismith.Result ) where +import Control.Monad (liftM) import Control.Monad.Base import Control.Monad.IO.Class import Control.Monad.Trans.Class import Control.Monad.Trans.Control import Data.Bifunctor (Bifunctor (..)) import Shelly (RunFailed (..), Sh, catch_sh) -import Shelly.Lifted (MonadSh, liftSh) +import Shelly.Lifted (MonadSh, MonadShControl, ShM, + liftSh, liftShWith, restoreSh) -- | Result type which is equivalent to 'Either' or 'Error'. This is -- reimplemented so that there is full control over the 'Monad' definition and @@ -134,6 +136,16 @@ instance MonadBaseControl IO m => MonadBaseControl IO (ResultT a m) where {-# INLINABLE liftBaseWith #-} {-# INLINABLE restoreM #-} +instance (MonadShControl m) + => MonadShControl (ResultT a m) where + newtype ShM (ResultT a m) b = ResultTShM (ShM m (Result a b)) + liftShWith f = + ResultT $ liftM return $ liftShWith $ \runInSh -> f $ \k -> + liftM ResultTShM $ runInSh $ runResultT k + restoreSh (ResultTShM m) = ResultT . restoreSh $ m + {-# INLINE liftShWith #-} + {-# INLINE restoreSh #-} + infix 0 () :: (Monad m, Monoid a) => ResultT a m b -> a -> ResultT a m b -- cgit