diff options
Diffstat (limited to 'src/VeriFuzz/Fuzz.hs')
-rw-r--r-- | src/VeriFuzz/Fuzz.hs | 130 |
1 files changed, 93 insertions, 37 deletions
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') |