From f33355b68fa500a8ee9af8ea44923ec43ec5a3cd Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@ymhg.org>
Date: Wed, 17 Apr 2019 19:19:25 +0100
Subject: Add new Fuzzing technique, that checks simulators against each other

---
 src/VeriFuzz/Fuzz.hs | 108 +++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 97 insertions(+), 11 deletions(-)

(limited to 'src/VeriFuzz')

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
-- 
cgit