From 97398438902d42b33aef475e3e357781582bec16 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 18 Apr 2019 18:16:35 +0100 Subject: Add output path to each simulator --- src/VeriFuzz/Fuzz.hs | 130 +++++++++++++++++++++++++++++++------------ src/VeriFuzz/Sim/Internal.hs | 10 ++-- src/VeriFuzz/Sim/Quartus.hs | 8 ++- src/VeriFuzz/Sim/Vivado.hs | 8 ++- src/VeriFuzz/Sim/XST.hs | 5 +- src/VeriFuzz/Sim/Yosys.hs | 10 ++-- 6 files changed, 121 insertions(+), 50 deletions(-) (limited to 'src/VeriFuzz') diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs index 5ccc8a9..084caee 100644 --- a/src/VeriFuzz/Fuzz.hs +++ b/src/VeriFuzz/Fuzz.hs @@ -10,6 +10,8 @@ Portability : POSIX Environment to run the simulator and synthesisers in a matrix. -} +{-# LANGUAGE TemplateHaskell #-} + module VeriFuzz.Fuzz ( SynthTool(..) , SimTool(..) @@ -25,18 +27,19 @@ module VeriFuzz.Fuzz ) where +import Control.Lens import Control.Monad.IO.Class import Control.Monad.Trans.Class (lift) import Control.Monad.Trans.Reader hiding (local) import Control.Monad.Trans.State.Strict +import Data.ByteString (ByteString) 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 hiding (get) import Shelly.Lifted (MonadSh, liftSh) import VeriFuzz.Internal import VeriFuzz.Result @@ -48,6 +51,12 @@ import VeriFuzz.Sim.XST import VeriFuzz.Sim.Yosys import VeriFuzz.Verilog.AST +-- | Common type alias for synthesis results +type UResult = Result Failed () + +-- | Commont type alias for simulation results +type BResult = Result Failed ByteString + data SynthTool = XSTSynth {-# UNPACK #-} !XST | VivadoSynth {-# UNPACK #-} !Vivado | YosysSynth {-# UNPACK #-} !Yosys @@ -72,6 +81,16 @@ instance Synthesiser SynthTool where runSynth (YosysSynth yosys) = runSynth yosys runSynth (QuartusSynth quartus) = runSynth quartus + synthOutput (XSTSynth xst) = synthOutput xst + synthOutput (VivadoSynth vivado) = synthOutput vivado + synthOutput (YosysSynth yosys) = synthOutput yosys + synthOutput (QuartusSynth quartus) = synthOutput quartus + + setSynthOutput (YosysSynth yosys) = YosysSynth . setSynthOutput yosys + setSynthOutput (XSTSynth xst) = XSTSynth . setSynthOutput xst + setSynthOutput (VivadoSynth vivado) = VivadoSynth . setSynthOutput vivado + setSynthOutput (QuartusSynth quartus) = QuartusSynth . setSynthOutput quartus + defaultYosysSynth :: SynthTool defaultYosysSynth = YosysSynth defaultYosys @@ -106,30 +125,57 @@ data FuzzEnv = FuzzEnv { getSynthesisers :: ![SynthTool] } deriving (Eq, Show) -data SimResult a = SimResult !SynthTool !SimTool !(Result Failed a) - deriving (Eq, Show) - -data SynthResult a = SynthResult !SynthTool !SynthTool !(Result Failed a) - deriving (Eq, Show) - -data FuzzResult a = FuzzResult { getSynthResults :: ![SynthResult a] - , getSimResults :: ![SimResult a] - } +-- | The results from running a tool through a simulator. It can either fail or +-- return a result, which is most likely a 'ByteString'. +data SimResult = SimResult !SynthTool !SimTool !(BResult) + deriving (Eq) + +instance Show SimResult where + show (SimResult synth sim r) = show synth <> ", " <> show sim <> ": " <> show r + +-- | The results of comparing the synthesised outputs of two files using a +-- formal equivalence checker. This will either return a failure or an output +-- which is most likely '()'. +data SynthResult = SynthResult !SynthTool !SynthTool !(UResult) + deriving (Eq) + +instance Show SynthResult where + show (SynthResult synth synth2 r) = show synth <> ", " <> show synth2 <> ": " <> show r + +-- | The status of the synthesis using a simulator. This will be checked before +-- attempting to run the equivalence checks on the simulator, as that would be +-- unnecessary otherwise. +data SynthStatus = SynthStatus !SynthTool !(UResult) + deriving (Eq) + +instance Show SynthStatus where + show (SynthStatus synth r) = "synthesis " <> show synth <> ": " <> show r + +-- | The complete state that will be used during fuzzing, which contains the +-- results from all the operations. +data FuzzResult = FuzzResult { _synthResults :: ![SynthResult] + , _simResults :: ![SimResult] + , _synthStatus :: ![SynthStatus] + } deriving (Eq, Show) -instance Semigroup (FuzzResult a) where - FuzzResult a1 b1 <> FuzzResult a2 b2 = FuzzResult (a1 <> a2) (b1 <> b2) +$(makeLenses ''FuzzResult) -instance Monoid (FuzzResult a) where - mempty = FuzzResult [] [] +instance Semigroup FuzzResult where + FuzzResult a1 b1 c1 <> FuzzResult a2 b2 c2 = FuzzResult (a1 <> a2) (b1 <> b2) (c1 <> c2) -type Fuzz a m = StateT (FuzzResult a) (ReaderT FuzzEnv m) +instance Monoid FuzzResult where + mempty = FuzzResult [] [] [] -runFuzz :: (Monad m) => [SynthTool] -> [SimTool] -> Yosys -> Fuzz a m b -> m b +-- | The main type for the fuzzing, which contains an environment that can be +-- read from and the current state of all the results. +type Fuzz m = StateT FuzzResult (ReaderT FuzzEnv m) + +runFuzz :: (Monad m) => [SynthTool] -> [SimTool] -> Yosys -> Fuzz m b -> m b runFuzz synth sim yos m = - runReaderT (evalStateT m (FuzzResult [] [])) (FuzzEnv synth sim yos) + runReaderT (evalStateT m (FuzzResult [] [] [])) (FuzzEnv synth sim yos) -synthesisers :: (Monad m) => Fuzz () m [SynthTool] +synthesisers :: (Monad m) => Fuzz m [SynthTool] synthesisers = lift $ asks getSynthesisers --simulators :: (Monad m) => Fuzz () m [SimTool] @@ -151,13 +197,20 @@ liftWith' -> m (Result a b) liftWith' a = liftIO . shellyFailDir . a . runResultT -lift' :: (MonadIO m) => ResultT a Sh b -> m (Result a b) -lift' = liftWith' id +--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 ()) +timeit :: (MonadIO m) => m a -> m (NominalDiffTime, a) +timeit a = do + start <- liftIO getCurrentTime + result <- a + end <- liftIO getCurrentTime + return (diffUTCTime end start, result) + +synthesis :: (MonadIO m) => SourceInfo -> Fuzz m () synthesis src = do synth <- synthesisers results <- mapM @@ -165,29 +218,32 @@ synthesis src = do $ runSynth a src (fromText $ "syn_" <> showT a <> ".v") ) synth + synthStatus .= zipWith SynthStatus synth results 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 gen = do - synth <- synthesisers +generateSample :: (MonadIO m) => Gen SourceInfo -> Fuzz m SourceInfo +generateSample gen = do logT "Sampling Verilog from generator" (t, src) <- timeit $ Hog.sample gen logT $ "Generated Verilog (" <> showT t <> ")" + return src + +passedSynthesis :: (MonadIO m) => Fuzz m [SynthTool] +passedSynthesis = fmap toSynth . filter passed . _synthStatus <$> get + where + passed (SynthStatus _ (Pass _)) = True + toSynth (SynthStatus s _) = s + +fuzz :: (MonadIO m) => Gen SourceInfo -> Fuzz m FuzzResult +fuzz gen = do yos <- lift $ asks yosysInstance - _ <- synthesis src + src <- generateSample gen + synthesis src + synth <- passedSynthesis let synthComb = nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth - --let simComb = combinations synth sim - --results <- mapM (uncurry $ equivalence yos src) synthComb - --liftIO $ print results + 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') diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs index 8327ad8..2d06819 100644 --- a/src/VeriFuzz/Sim/Internal.hs +++ b/src/VeriFuzz/Sim/Internal.hs @@ -78,10 +78,12 @@ instance Monoid Failed where -- | Synthesiser type class. class Tool a => Synthesiser a where - runSynth :: a -- ^ Synthesiser tool instance - -> SourceInfo -- ^ Run information - -> FilePath -- ^ Output verilog file for the module - -> ResultSh () -- ^ does not return any values + runSynth :: a -- ^ Synthesiser tool instance + -> SourceInfo -- ^ Run information + -> FilePath -- ^ Output verilog file for the module + -> ResultSh () -- ^ does not return any values + synthOutput :: a -> FilePath + setSynthOutput :: a -> FilePath -> a -- | Type synonym for a 'ResultT' that will be used throughout 'VeriFuzz'. This -- has instances for 'MonadSh' and 'MonadIO' if the 'Monad' it is parametrised diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs index 0463009..beb7f10 100644 --- a/src/VeriFuzz/Sim/Quartus.hs +++ b/src/VeriFuzz/Sim/Quartus.hs @@ -23,7 +23,9 @@ import VeriFuzz.Sim.Internal import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.CodeGen -newtype Quartus = Quartus { quartusBin :: Maybe FilePath } +data Quartus = Quartus { quartusBin :: !(Maybe FilePath) + , quartusOutput :: {-# UNPACK #-} !FilePath + } deriving (Eq) instance Show Quartus where @@ -34,9 +36,11 @@ instance Tool Quartus where instance Synthesiser Quartus where runSynth = runSynthQuartus + synthOutput = quartusOutput + setSynthOutput (Quartus a _) f = Quartus a f defaultQuartus :: Quartus -defaultQuartus = Quartus Nothing +defaultQuartus = Quartus Nothing "quartus/syn_quartus.v" runSynthQuartus :: Quartus -> SourceInfo -> FilePath -> ResultSh () runSynthQuartus sim (SourceInfo top src) outf = do diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs index fb43ceb..7cf6d4b 100644 --- a/src/VeriFuzz/Sim/Vivado.hs +++ b/src/VeriFuzz/Sim/Vivado.hs @@ -24,7 +24,9 @@ import VeriFuzz.Sim.Template import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.CodeGen -newtype Vivado = Vivado { vivadoPath :: FilePath } +data Vivado = Vivado { vivadoPath :: {-# UNPACK #-} !FilePath + , vivadoOutput :: {-# UNPACK #-} !FilePath + } deriving (Eq) instance Show Vivado where @@ -35,9 +37,11 @@ instance Tool Vivado where instance Synthesiser Vivado where runSynth = runSynthVivado + synthOutput = vivadoOutput + setSynthOutput (Vivado a _) f = Vivado a f defaultVivado :: Vivado -defaultVivado = Vivado "vivado" +defaultVivado = Vivado "vivado" "vivado/syn_vivado.v" runSynthVivado :: Vivado -> SourceInfo -> FilePath -> ResultSh () runSynthVivado sim (SourceInfo top src) outf = do diff --git a/src/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs index 488c404..b5b1b8b 100644 --- a/src/VeriFuzz/Sim/XST.hs +++ b/src/VeriFuzz/Sim/XST.hs @@ -29,6 +29,7 @@ import VeriFuzz.Verilog.CodeGen data XST = XST { xstPath :: {-# UNPACK #-} !FilePath , netgenPath :: {-# UNPACK #-} !FilePath + , xstOutput :: {-# UNPACK #-} !FilePath } deriving (Eq) @@ -40,9 +41,11 @@ instance Tool XST where instance Synthesiser XST where runSynth = runSynthXST + synthOutput = xstOutput + setSynthOutput (XST a b _) f = XST a b f defaultXST :: XST -defaultXST = XST "xst" "netgen" +defaultXST = XST "xst" "netgen" "xst/syn_xst.v" runSynthXST :: XST -> SourceInfo -> FilePath -> ResultSh () runSynthXST sim (SourceInfo top src) outf = do diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs index 17f52df..98244a6 100644 --- a/src/VeriFuzz/Sim/Yosys.hs +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -31,7 +31,9 @@ import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.CodeGen import VeriFuzz.Verilog.Mutate -newtype Yosys = Yosys { yosysPath :: FilePath } +data Yosys = Yosys { yosysPath :: {-# UNPACK #-} !FilePath + , yosysOutput :: {-# UNPACK #-} !FilePath + } deriving (Eq) instance Tool Yosys where @@ -39,12 +41,14 @@ instance Tool Yosys where instance Synthesiser Yosys where runSynth = runSynthYosys + synthOutput = yosysOutput + setSynthOutput (Yosys a _) f = Yosys a f instance Show Yosys where show _ = "yosys" defaultYosys :: Yosys -defaultYosys = Yosys "yosys" +defaultYosys = Yosys "yosys" "yosys/syn_yosys.v" runSynthYosys :: Yosys -> SourceInfo -> FilePath -> ResultSh () runSynthYosys sim (SourceInfo _ src) outf = ( SynthFail) . liftSh $ do @@ -112,8 +116,6 @@ runEquiv _ sim1 sim2 srcInfo = do $ srcInfo ^. mainModule writefile "test.sby" $ sbyConfig root sim1 sim2 srcInfo - runSynth sim1 srcInfo $ fromText [st|syn_#{toText sim1}.v|] - runMaybeSynth sim2 srcInfo liftSh $ echoP "SymbiYosys: run" execute_ EquivFail dir "symbiyosys" "sby" ["-f", "test.sby"] liftSh $ echoP "SymbiYosys: done" -- cgit