From 1940ee0912a95382c0045e150b01617b61238871 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 23 Apr 2019 13:34:03 +0100 Subject: Add simulator support to the config file --- src/VeriFuzz/Config.hs | 72 +++++++++++++---- src/VeriFuzz/Fuzz.hs | 208 +++++++++++-------------------------------------- 2 files changed, 101 insertions(+), 179 deletions(-) diff --git a/src/VeriFuzz/Config.hs b/src/VeriFuzz/Config.hs index 28a0ad8..a863d53 100644 --- a/src/VeriFuzz/Config.hs +++ b/src/VeriFuzz/Config.hs @@ -17,6 +17,8 @@ module VeriFuzz.Config , defaultConfig , configProbability , configProperty + , configSimulators + , configSynthesisers , Probability(..) , probModItem , probStmnt @@ -50,6 +52,8 @@ module VeriFuzz.Config , propStmntDepth , propModDepth , propMaxModules + , SimDescription(..) + , SynthDescription(..) , parseConfigFile , parseConfig , configEncode @@ -57,7 +61,7 @@ module VeriFuzz.Config ) where -import Control.Applicative (Alternative) +import Control.Applicative (Alternative, (<|>)) import Control.Lens hiding ((.=)) import Data.List.NonEmpty (NonEmpty (..)) import Data.Maybe (fromMaybe) @@ -112,8 +116,16 @@ data Property = Property { _propSize :: {-# UNPACK #-} !Int } deriving (Eq, Show) -data Config = Config { _configProbability :: {-# UNPACK #-} !Probability - , _configProperty :: {-# UNPACK #-} !Property +data SimDescription = SimDescription { _simName :: {-# UNPACK #-} !Text } + deriving (Eq, Show) + +data SynthDescription = SynthDescription { _synthName :: {-# UNPACK #-} !Text } + deriving (Eq, Show) + +data Config = Config { _configProbability :: {-# UNPACK #-} !Probability + , _configProperty :: {-# UNPACK #-} !Property + , _configSimulators :: ![SimDescription] + , _configSynthesisers :: ![SynthDescription] } deriving (Eq, Show) @@ -133,13 +145,16 @@ defaultValue defaultValue x = Toml.dimap Just (fromMaybe x) . Toml.dioptional defaultConfig :: Config -defaultConfig = Config (Probability defModItem defStmnt defExpr defEvent) - (Property 20 Nothing 3 2 5) +defaultConfig = Config + (Probability defModItem defStmnt defExpr defEvent) + (Property 20 Nothing 3 2 5) + [] + [SynthDescription "yosys", SynthDescription "vivado"] where defModItem = ProbModItem 5 1 1 defStmnt = ProbStatement 0 15 1 1 defExpr = ProbExpr 1 1 1 1 1 1 0 1 1 - defEvent = ProbEventList 1 1 1 + defEvent = ProbEventList 1 1 1 twoKey :: Toml.Piece -> Toml.Piece -> Toml.Key twoKey a b = Toml.Key (a :| [b]) @@ -203,15 +218,15 @@ modItemCodec = eventListCodec :: TomlCodec ProbEventList eventListCodec = ProbEventList - <$> defaultValue (defProb probEventListClk) (intE "clk") - .= _probEventListClk - <*> defaultValue (defProb probEventListClk) (intE "all") - .= _probEventListAll - <*> defaultValue (defProb probEventListClk) (intE "var") - .= _probEventListClk - where - defProb i = defaultConfig ^. configProbability . probEventList . i - intE = int "eventlist" + <$> defaultValue (defProb probEventListClk) (intE "clk") + .= _probEventListClk + <*> defaultValue (defProb probEventListClk) (intE "all") + .= _probEventListAll + <*> defaultValue (defProb probEventListClk) (intE "var") + .= _probEventListClk + where + defProb i = defaultConfig ^. configProbability . probEventList . i + intE = int "eventlist" probCodec :: TomlCodec Probability probCodec = @@ -223,7 +238,7 @@ probCodec = <*> defaultValue (defProb probExpr) exprCodec .= _probExpr <*> defaultValue (defProb probEventList) eventListCodec - .= _probEventList + .= _probEventList where defProb i = defaultConfig ^. configProbability . i propCodec :: TomlCodec Property @@ -241,6 +256,23 @@ propCodec = .= _propMaxModules where defProp i = defaultConfig ^. configProperty . i +simulator :: TomlCodec SimDescription +simulator = Toml.textBy pprint parseIcarus "name" + where + parseIcarus i@"icarus" = Right $ SimDescription i + parseIcarus s = Left $ "Could not match '" <> s <> "' with a simulator." + pprint (SimDescription a) = a + +synthesiser :: TomlCodec SynthDescription +synthesiser = Toml.textBy pprint parseIcarus "name" + where + parseIcarus s@"yosys" = Right $ SynthDescription s + parseIcarus s@"vivado" = Right $ SynthDescription s + parseIcarus s@"quartus" = Right $ SynthDescription s + parseIcarus s@"xst" = Right $ SynthDescription s + parseIcarus s = Left $ "Could not match '" <> s <> "' with a synthesiser." + pprint (SynthDescription a) = a + configCodec :: TomlCodec Config configCodec = Config @@ -250,6 +282,12 @@ configCodec = <*> defaultValue (defaultConfig ^. configProperty) (Toml.table propCodec "property") .= _configProperty + <*> defaultValue (defaultConfig ^. configSimulators) + (Toml.list simulator "simulator") + .= _configSimulators + <*> defaultValue (defaultConfig ^. configSynthesisers) + (Toml.list synthesiser "synthesiser") + .= _configSynthesisers parseConfigFile :: FilePath -> IO Config parseConfigFile = Toml.decodeFile configCodec @@ -262,7 +300,7 @@ parseConfig t = case Toml.decode configCodec t of Left (Toml.TableNotFound k) -> error $ "Table " ++ show k ++ " not found" Left (Toml.TypeMismatch k _ _) -> error $ "Type mismatch with key " ++ show k - Left (Toml.ParseError _) -> error "Config file parse error" + Left _ -> error "Config file parse error" configEncode :: Config -> Text configEncode = Toml.encode configCodec diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs index e61d0b6..dd3bfd4 100644 --- a/src/VeriFuzz/Fuzz.hs +++ b/src/VeriFuzz/Fuzz.hs @@ -15,22 +15,11 @@ Environment to run the simulator and synthesisers in a matrix. {-# LANGUAGE TemplateHaskell #-} module VeriFuzz.Fuzz - ( SynthTool(..) - , SimTool(..) - , FuzzResult(..) - , synthResults - , simResults - , synthStatus - , Fuzz + ( Fuzz , fuzz , fuzzInDir , fuzzMultiple , runFuzz - , defaultIcarusSim - , defaultVivadoSynth - , defaultYosysSynth - , defaultXSTSynth - , defaultQuartusSynth ) where @@ -51,7 +40,9 @@ import qualified Hedgehog.Gen as Hog import Prelude hiding (FilePath) import Shelly hiding (get) import Shelly.Lifted (MonadSh, liftSh) +import VeriFuzz.Config import VeriFuzz.Internal +import VeriFuzz.Report import VeriFuzz.Result import VeriFuzz.Sim.Icarus import VeriFuzz.Sim.Internal @@ -62,136 +53,28 @@ import VeriFuzz.Sim.Yosys import VeriFuzz.Verilog.AST import VeriFuzz.Verilog.CodeGen -type MonadFuzz m = (MonadBaseControl IO m, MonadIO m, MonadSh m) - --- | 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 - | QuartusSynth !Quartus - 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 - toText (VivadoSynth vivado) = toText vivado - toText (YosysSynth yosys) = toText yosys - toText (QuartusSynth quartus) = toText quartus - -instance Synthesiser SynthTool where - runSynth (XSTSynth xst) = runSynth xst - runSynth (VivadoSynth vivado) = runSynth vivado - 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 - -defaultQuartusSynth :: SynthTool -defaultQuartusSynth = QuartusSynth defaultQuartus - -defaultVivadoSynth :: SynthTool -defaultVivadoSynth = VivadoSynth defaultVivado - -defaultXSTSynth :: SynthTool -defaultXSTSynth = XSTSynth defaultXST - -newtype SimTool = IcarusSim Icarus - deriving (Eq) - -instance Tool SimTool where - toText (IcarusSim icarus) = toText icarus - -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) --- | 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) - -$(makeLenses ''FuzzResult) - -instance Semigroup FuzzResult where - FuzzResult a1 b1 c1 <> FuzzResult a2 b2 c2 = FuzzResult (a1 <> a2) (b1 <> b2) (c1 <> c2) - -instance Monoid FuzzResult where - mempty = FuzzResult [] [] [] - -- | 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) +type Fuzz m = StateT FuzzReport (ReaderT FuzzEnv m) -runFuzz - :: MonadIO m => - [SynthTool] -> [SimTool] -> Yosys -> Fuzz Sh a -> m a -runFuzz synth sim yos m = shelly $ runFuzz' synth sim yos m +type MonadFuzz m = (MonadBaseControl IO m, MonadIO m, MonadSh m) + +runFuzz :: MonadIO m => Config -> Yosys -> Fuzz Sh a -> m a +runFuzz conf yos m = shelly $ runFuzz' conf yos 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) +runFuzz' :: Monad m => Config -> Yosys -> Fuzz m b -> m b +runFuzz' conf yos m = runReaderT + (evalStateT m (FuzzReport [] [] [])) + (FuzzEnv (descriptionToSynth <$> conf ^. configSynthesisers) + (descriptionToSim <$> conf ^. configSimulators) + yos + ) synthesisers :: Monad m => Fuzz m [SynthTool] synthesisers = lift $ asks getSynthesisers @@ -207,9 +90,9 @@ logT = liftSh . echoP timeit :: (MonadIO m, MonadSh m) => m a -> m (NominalDiffTime, a) timeit a = do - start <- liftIO getCurrentTime + start <- liftIO getCurrentTime result <- a - end <- liftIO getCurrentTime + end <- liftIO getCurrentTime return (diffUTCTime end start, result) synthesis :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () @@ -218,24 +101,24 @@ synthesis src = do results <- liftSh $ mapM exec synth synthStatus .= zipWith SynthStatus synth results liftSh $ inspect results - where - exec a = runResultT $ do - liftSh . mkdir_p . fromText $ toText a - pop (fromText $ toText a) $ runSynth a src + where + exec a = runResultT $ do + liftSh . mkdir_p . fromText $ toText a + pop (fromText $ toText a) $ runSynth a src generateSample :: (MonadIO m, MonadSh m) => Gen SourceInfo -> Fuzz m SourceInfo generateSample gen = do logT "Sampling Verilog from generator" - (t, src) <- timeit $ Hog.sample gen + (t, src) <- timeit $ Hog.sample gen logT $ "Generated Verilog (" <> showT t <> ")" return src passedSynthesis :: MonadSh m => Fuzz m [SynthTool] passedSynthesis = fmap toSynth . filter passed . _synthStatus <$> get - where - passed (SynthStatus _ (Pass _)) = True - passed _ = False - toSynth (SynthStatus s _) = s + where + passed (SynthStatus _ (Pass _)) = True + passed _ = False + toSynth (SynthStatus s _) = s make :: MonadSh m => FilePath -> m () make f = liftSh $ do @@ -255,35 +138,36 @@ equivalence src = do nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth results <- liftSh $ mapM (uncurry $ equiv yos) synthComb liftSh $ inspect results - where - tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') - equiv yos a b = runResultT $ do - make dir - pop dir $ do - liftSh $ do - cp (fromText ".." fromText (toText a) synthOutput a) $ synthOutput a - cp (fromText ".." fromText (toText b) synthOutput b) $ synthOutput b - writefile "rtl.v" $ genSource src - runEquiv yos a (Just b) src - where - dir = fromText $ "equiv_" <> toText a <> "_" <> toText b - -fuzz :: MonadFuzz m => Gen SourceInfo -> Fuzz m FuzzResult + where + tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') + equiv yos a b = runResultT $ do + make dir + pop dir $ do + liftSh $ do + cp (fromText ".." fromText (toText a) synthOutput a) + $ synthOutput a + cp (fromText ".." fromText (toText b) synthOutput b) + $ synthOutput b + writefile "rtl.v" $ genSource src + runEquiv yos a (Just b) src + where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b + +fuzz :: MonadFuzz m => Gen SourceInfo -> Fuzz m FuzzReport fuzz gen = do src <- generateSample gen synthesis src equivalence src return mempty -fuzzInDir :: MonadFuzz m => FilePath -> Gen SourceInfo -> Fuzz m FuzzResult +fuzzInDir :: MonadFuzz m => FilePath -> Gen SourceInfo -> Fuzz m FuzzReport fuzzInDir fp src = do make fp pop fp $ fuzz src -fuzzMultiple :: MonadFuzz m => Int -> FilePath -> Gen SourceInfo -> Fuzz m FuzzResult +fuzzMultiple + :: MonadFuzz m => Int -> FilePath -> Gen SourceInfo -> Fuzz m FuzzReport fuzzMultiple n fp src = do make fp - void . pop fp $ forM [1..n] fuzzDir + void . pop fp $ forM [1 .. n] fuzzDir return mempty - where - fuzzDir n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src + where fuzzDir n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src -- cgit