aboutsummaryrefslogtreecommitdiffstats
path: root/src/VeriFuzz/Fuzz.hs
diff options
context:
space:
mode:
authorYann Herklotz <git@ymhg.org>2019-04-17 19:19:25 +0100
committerYann Herklotz <git@ymhg.org>2019-04-17 19:19:25 +0100
commitf33355b68fa500a8ee9af8ea44923ec43ec5a3cd (patch)
tree5980931c6caef140ea237acf5e709a4595b603f5 /src/VeriFuzz/Fuzz.hs
parent56583318135a6a281d0f880637d5e0408ef690ee (diff)
downloadverismith-f33355b68fa500a8ee9af8ea44923ec43ec5a3cd.tar.gz
verismith-f33355b68fa500a8ee9af8ea44923ec43ec5a3cd.zip
Add new Fuzzing technique, that checks simulators against each other
Diffstat (limited to 'src/VeriFuzz/Fuzz.hs')
-rw-r--r--src/VeriFuzz/Fuzz.hs108
1 files changed, 97 insertions, 11 deletions
diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs
index 7a754cc..5ccc8a9 100644
--- a/src/VeriFuzz/Fuzz.hs
+++ b/src/VeriFuzz/Fuzz.hs
@@ -17,6 +17,11 @@ module VeriFuzz.Fuzz
, Fuzz
, fuzz
, runFuzz
+ , defaultIcarusSim
+ , defaultVivadoSynth
+ , defaultYosysSynth
+ , defaultXSTSynth
+ , defaultQuartusSynth
)
where
@@ -25,8 +30,15 @@ import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Reader hiding (local)
import Control.Monad.Trans.State.Strict
import Data.List (nubBy)
+import Data.Text (Text)
+import qualified Data.Text as T
+import Data.Time
import Hedgehog (Gen)
+import qualified Hedgehog.Gen as Hog
import Prelude hiding (FilePath)
+import Shelly
+import Shelly.Lifted (MonadSh, liftSh)
+import VeriFuzz.Internal
import VeriFuzz.Result
import VeriFuzz.Sim.Icarus
import VeriFuzz.Sim.Internal
@@ -40,7 +52,13 @@ data SynthTool = XSTSynth {-# UNPACK #-} !XST
| VivadoSynth {-# UNPACK #-} !Vivado
| YosysSynth {-# UNPACK #-} !Yosys
| QuartusSynth !Quartus
- deriving (Eq, Show)
+ deriving (Eq)
+
+instance Show SynthTool where
+ show (XSTSynth xst) = show xst
+ show (VivadoSynth vivado) = show vivado
+ show (YosysSynth yosys) = show yosys
+ show (QuartusSynth quartus) = show quartus
instance Tool SynthTool where
toText (XSTSynth xst) = toText xst
@@ -54,8 +72,20 @@ instance Synthesiser SynthTool where
runSynth (YosysSynth yosys) = runSynth yosys
runSynth (QuartusSynth quartus) = runSynth quartus
+defaultYosysSynth :: SynthTool
+defaultYosysSynth = YosysSynth defaultYosys
+
+defaultQuartusSynth :: SynthTool
+defaultQuartusSynth = QuartusSynth defaultQuartus
+
+defaultVivadoSynth :: SynthTool
+defaultVivadoSynth = VivadoSynth defaultVivado
+
+defaultXSTSynth :: SynthTool
+defaultXSTSynth = XSTSynth defaultXST
+
newtype SimTool = IcarusSim Icarus
- deriving (Eq, Show)
+ deriving (Eq)
instance Tool SimTool where
toText (IcarusSim icarus) = toText icarus
@@ -64,8 +94,15 @@ instance Simulator SimTool where
runSim (IcarusSim icarus) = runSim icarus
runSimWithFile (IcarusSim icarus) = runSimWithFile icarus
+instance Show SimTool where
+ show (IcarusSim icarus) = show icarus
+
+defaultIcarusSim :: SimTool
+defaultIcarusSim = IcarusSim defaultIcarus
+
data FuzzEnv = FuzzEnv { getSynthesisers :: ![SynthTool]
, getSimulators :: ![SimTool]
+ , yosysInstance :: {-# UNPACK #-} !Yosys
}
deriving (Eq, Show)
@@ -88,25 +125,74 @@ instance Monoid (FuzzResult a) where
type Fuzz a m = StateT (FuzzResult a) (ReaderT FuzzEnv m)
-runFuzz :: (Monad m) => [SynthTool] -> [SimTool] -> Fuzz a m b -> m b
-runFuzz synth sim m =
- runReaderT (evalStateT m (FuzzResult [] [])) (FuzzEnv synth sim)
+runFuzz :: (Monad m) => [SynthTool] -> [SimTool] -> Yosys -> Fuzz a m b -> m b
+runFuzz synth sim yos m =
+ runReaderT (evalStateT m (FuzzResult [] [])) (FuzzEnv synth sim yos)
synthesisers :: (Monad m) => Fuzz () m [SynthTool]
synthesisers = lift $ asks getSynthesisers
-simulators :: (Monad m) => Fuzz () m [SimTool]
-simulators = lift $ asks getSimulators
+--simulators :: (Monad m) => Fuzz () m [SimTool]
+--simulators = lift $ asks getSimulators
combinations :: [a] -> [b] -> [(a, b)]
combinations l1 l2 = [ (x, y) | x <- l1, y <- l2 ]
+runInTmp :: (MonadSh m) => m a -> m a
+runInTmp a = liftSh (withTmpDir $ (\dir -> cd dir)) >> a
+
+mkAndRun :: (MonadSh m) => FilePath -> Sh a -> m a
+mkAndRun a = liftSh . chdir_p a
+
+liftWith'
+ :: (MonadIO m)
+ => (Sh (Result a b) -> Sh (Result a b))
+ -> ResultT a Sh b
+ -> m (Result a b)
+liftWith' a = liftIO . shellyFailDir . a . runResultT
+
+lift' :: (MonadIO m) => ResultT a Sh b -> m (Result a b)
+lift' = liftWith' id
+
+logT :: (MonadIO m) => Text -> m ()
+logT = liftIO . shelly . echoP
+
+synthesis :: (MonadIO m) => SourceInfo -> Fuzz () m (FuzzResult ())
+synthesis src = do
+ synth <- synthesisers
+ results <- mapM
+ (\a -> liftWith' (mkAndRun . fromText $ showT a)
+ $ runSynth a src (fromText $ "syn_" <> showT a <> ".v")
+ )
+ synth
+ liftIO $ print results
+ return mempty
+
+timeit :: (MonadIO m) => m a -> m (NominalDiffTime, a)
+timeit a = do
+ start <- liftIO getCurrentTime
+ result <- a
+ end <- liftIO getCurrentTime
+ return (diffUTCTime end start, result)
+
fuzz :: (MonadIO m) => Gen SourceInfo -> Fuzz () m (FuzzResult ())
-fuzz _ = do
+fuzz gen = do
synth <- synthesisers
- sim <- simulators
+ logT "Sampling Verilog from generator"
+ (t, src) <- timeit $ Hog.sample gen
+ logT $ "Generated Verilog (" <> showT t <> ")"
+ yos <- lift $ asks yosysInstance
+ _ <- synthesis src
let synthComb =
nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth
- let simComb = combinations synth sim
+ --let simComb = combinations synth sim
+ --results <- mapM (uncurry $ equivalence yos src) synthComb
+ --liftIO $ print results
return mempty
- where tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a')
+ where
+ tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a')
+ equivalence yos src a b =
+ liftIO . shellyFailDir . runInTmp . runResultT $ runEquiv yos
+ a
+ (Just b)
+ src