From 02849780204c36fd9c130a398c0a6901b461f8f5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 12 Nov 2019 16:51:32 +0000 Subject: Add reduction for simulation failures --- src/Verismith/Fuzz.hs | 67 +++++++++++++++++++----- src/Verismith/Reduce.hs | 33 ++++++++++-- src/Verismith/Report.hs | 10 ++-- src/Verismith/Result.hs | 10 ++++ src/Verismith/Tool/Icarus.hs | 112 ++++++++++++++++++++++++----------------- src/Verismith/Tool/Internal.hs | 12 ++++- verismith.cabal | 4 +- 7 files changed, 176 insertions(+), 72 deletions(-) diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs index b600d68..c38601a 100644 --- a/src/Verismith/Fuzz.hs +++ b/src/Verismith/Fuzz.hs @@ -39,7 +39,7 @@ import Control.Monad.Trans.Control (MonadBaseControl) import qualified Crypto.Random.DRBG as C import Data.ByteString (ByteString) import Data.List (nubBy, sort) -import Data.Maybe (fromMaybe, isNothing) +import Data.Maybe (catMaybes, fromMaybe, isNothing) import Data.Text (Text) import qualified Data.Text as T import Data.Time @@ -54,6 +54,7 @@ import Shelly hiding (get) import Shelly.Lifted (MonadSh, liftSh) import System.FilePath.Posix (takeBaseName) import Verismith.Config +import Verismith.CounterEg (CounterEg (..)) import Verismith.Internal import Verismith.Reduce import Verismith.Report @@ -166,8 +167,8 @@ filterSynth (SynthResult _ _ (Pass _) _) = True filterSynth _ = False filterSim :: SimResult -> Bool -filterSim (SimResult _ _ (Pass _) _) = True -filterSim _ = False +filterSim (SimResult _ _ _ (Pass _) _) = True +filterSim _ = False filterSynthStat :: SynthStatus -> Bool filterSynthStat (SynthStatus _ (Pass _) _) = True @@ -240,12 +241,19 @@ applyList a b = apply' <$> zip a b where apply' (a', b') = a' b' applyLots :: (a -> b -> c -> d -> e) -> [(a, b)] -> [(c, d)] -> [e] applyLots func a b = applyList (uncurry . uncurry func <$> a) b -toSynthResult - :: [(SynthTool, SynthTool)] - -> [(NominalDiffTime, Result Failed ())] - -> [SynthResult] +toSynthResult :: [(SynthTool, SynthTool)] + -> [(NominalDiffTime, Result Failed ())] + -> [SynthResult] toSynthResult a b = applyLots SynthResult a $ fmap swap b +toSimResult :: SimTool + -> [ByteString] + -> [SynthTool] + -> [(NominalDiffTime, Result Failed ByteString)] + -> [SimResult] +toSimResult sima bs as b = + applyList (applyList (repeat uncurry) (applyList (applyList (SimResult <$> as) (repeat sima)) (repeat bs))) $ fmap swap b + toolRun :: (MonadIO m, MonadSh m) => Text -> m a -> m (NominalDiffTime, a) toolRun t m = do logT $ "Running " <> t @@ -291,23 +299,35 @@ simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m () simulation src = do datadir <- fmap _fuzzDataDir askOpts synth <- passedSynthesis + counterEgs <- failEquivWithIdentityCE vals <- liftIO $ generateByteString 20 - ident <- liftSh $ equiv datadir vals defaultIdentitySynth - resTimes <- liftSh $ mapM (equiv datadir vals) synth + ident <- liftSh $ sim datadir vals Nothing defaultIdentitySynth + resTimes <- liftSh $ mapM (sim datadir vals (justPass $ snd ident)) synth + resTimes2 <- liftSh $ mapM (simCounterEg datadir) counterEgs + fuzzSimResults .= toSimResult defaultIcarusSim vals synth resTimes liftSh . inspect $ (\(_, r) -> bimap show (T.unpack . T.take 10 . showBS) r) <$> (ident : resTimes) where - equiv datadir b a = toolRun ("simulation for " <> toText a) . runResultT $ do + sim datadir b i a = toolRun ("simulation for " <> toText a) . runResultT $ do make dir pop dir $ do liftSh $ do cp (fromText ".." fromText (toText a) synthOutput a) $ synthOutput a writefile "rtl.v" $ genSource src - runSimIc datadir defaultIcarus a src b + runSimIc datadir defaultIcarus a src b i where dir = fromText $ "simulation_" <> toText a + simCounterEg datadir (a, b) = toolRun ("counter-example simulation for " <> toText a) . runResultT $ do + make dir + pop dir $ do + liftSh $ do + cp (fromText ".." fromText (toText a) synthOutput a) $ synthOutput a + writefile "rtl.v" $ genSource src + ident <- runSimIcEC datadir defaultIcarus defaultIdentitySynth src b Nothing + runSimIcEC datadir defaultIcarus a src b (Just ident) + where dir = fromText $ "countereg_sim_" <> toText a -- | Generate a specific number of random bytestrings of size 256. randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString] @@ -329,6 +349,19 @@ failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get withIdentity (SynthResult _ (IdentitySynth _) (Fail (EquivFail _)) _) = True withIdentity _ = False +failEquivWithIdentityCE :: (MonadSh m) => Fuzz m [(SynthTool, CounterEg)] +failEquivWithIdentityCE = catMaybes . fmap withIdentity . _fuzzSynthResults <$> get + where + withIdentity (SynthResult (IdentitySynth _) s (Fail (EquivFail c)) _) = Just (s, c) + withIdentity (SynthResult s (IdentitySynth _) (Fail (EquivFail c)) _) = Just (s, c) + withIdentity _ = Nothing + +failedSimulations :: (MonadSh m) => Fuzz m [SimResult] +failedSimulations = filter failedSim . _fuzzSimResults <$> get + where + failedSim (SimResult _ _ _ (Fail (SimFail _)) _) = True + failedSim _ = False + passEquiv :: (MonadSh m) => Fuzz m [SynthResult] passEquiv = filter withIdentity . _fuzzSynthResults <$> get where @@ -341,8 +374,10 @@ reduction src = do datadir <- fmap _fuzzDataDir askOpts fails <- failEquivWithIdentity synthFails <- failedSynthesis + simFails <- failedSimulations _ <- liftSh $ mapM (red datadir) fails _ <- liftSh $ mapM redSynth synthFails + _ <- liftSh $ mapM (redSim datadir) simFails return () where red datadir (SynthResult a b _ _) = do @@ -359,6 +394,13 @@ reduction src = do writefile (fromText ".." dir <.> "v") $ genSource s return s where dir = fromText $ "reduce_" <> toText a + redSim datadir (SimResult t _ bs _ _) = do + make dir + pop dir $ do + s <- reduceSimIc datadir bs t src + writefile (fromText ".." dir <.> "v") $ genSource s + return s + where dir = fromText $ "reduce_sim_" <> toText t titleRun :: (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a) @@ -447,9 +489,10 @@ fuzz gen = do then return (0, mempty) else titleRun "Simulation" $ simulation src fails <- failEquivWithIdentity + failedSim <- failedSimulations synthFails <- failedSynthesis redResult <- - whenMaybe (not (null fails && null synthFails) + whenMaybe (not (null failedSim && null fails && null synthFails) && not (_fuzzOptsNoReduction opts)) . titleRun "Reduction" $ reduction src diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs index 69b5e17..e7614e6 100644 --- a/src/Verismith/Reduce.hs +++ b/src/Verismith/Reduce.hs @@ -18,6 +18,7 @@ module Verismith.Reduce reduceWithScript , reduceSynth , reduceSynthesis + , reduceSimIc , reduce , reduce_ , Replacement(..) @@ -40,6 +41,7 @@ where import Control.Lens hiding ((<.>)) import Control.Monad (void) import Control.Monad.IO.Class (MonadIO, liftIO) +import Data.ByteString (ByteString) import Data.Foldable (foldrM) import Data.List (nub) import Data.List.NonEmpty (NonEmpty (..)) @@ -48,10 +50,12 @@ import Data.Maybe (mapMaybe) import Data.Text (Text) import Shelly ((<.>)) import qualified Shelly -import Shelly.Lifted (MonadSh, liftSh) +import Shelly.Lifted (MonadSh, liftSh, rm_rf) import Verismith.Internal import Verismith.Result import Verismith.Tool +import Verismith.Tool.Icarus +import Verismith.Tool.Identity import Verismith.Tool.Internal import Verismith.Verilog import Verismith.Verilog.AST @@ -614,8 +618,7 @@ reduceSynth datadir a b = reduce synth runEquiv datadir a b src' return $ case r of Fail (EquivFail _) -> True - Fail _ -> False - Pass _ -> False + _ -> False reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo reduceSynthesis a = reduce synth @@ -624,5 +627,25 @@ reduceSynthesis a = reduce synth r <- runResultT $ runSynth a src return $ case r of Fail SynthFail -> True - Fail _ -> False - Pass _ -> False + _ -> False + +runInTmp :: Shelly.Sh a -> Shelly.Sh a +runInTmp a = Shelly.withTmpDir $ (\f -> do + dir <- Shelly.pwd + Shelly.cd f + r <- a + Shelly.cd dir + return r) + +reduceSimIc :: (Synthesiser a, MonadSh m) => Shelly.FilePath -> [ByteString] -> a -> SourceInfo -> m SourceInfo +reduceSimIc fp bs a = reduce synth + where + synth src = liftSh . runInTmp $ do + r <- runResultT $ do + runSynth a src + runSynth defaultIdentity src + i <- runSimIc fp defaultIcarus defaultIdentity src bs Nothing + runSimIc fp defaultIcarus a src bs $ Just i + return $ case r of + Fail (SimFail _) -> True + _ -> False diff --git a/src/Verismith/Report.hs b/src/Verismith/Report.hs index 743240d..dbaf613 100644 --- a/src/Verismith/Report.hs +++ b/src/Verismith/Report.hs @@ -155,15 +155,15 @@ defaultIcarusSim = IcarusSim defaultIcarus -- | 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 !NominalDiffTime +data SimResult = SimResult !SynthTool !SimTool ![ByteString] !BResult !NominalDiffTime deriving (Eq) instance Show SimResult where - show (SimResult synth sim r d) = show synth <> ", " <> show sim <> ": " <> show (bimap show (T.unpack . showBS) r) <> " (" <> show d <> ")" + show (SimResult synth sim _ r d) = show synth <> ", " <> show sim <> ": " <> show (bimap show (T.unpack . showBS) r) <> " (" <> show d <> ")" getSimResult :: SimResult -> UResult -getSimResult (SimResult _ _ (Pass _) _) = Pass () -getSimResult (SimResult _ _ (Fail b) _) = Fail b +getSimResult (SimResult _ _ _ (Pass _) _) = Pass () +getSimResult (SimResult _ _ _ (Fail b) _) = Fail b -- | The results of comparing the synthesised outputs of two files using a -- formal equivalence checker. This will either return a failure or an output @@ -239,7 +239,7 @@ status :: Result Failed () -> Html status (Pass _ ) = H.td ! A.class_ "is-success" $ "Passed" status (Fail EmptyFail ) = H.td ! A.class_ "is-danger" $ "Failed" status (Fail (EquivFail _)) = H.td ! A.class_ "is-danger" $ "Equivalence failed" -status (Fail SimFail ) = H.td ! A.class_ "is-danger" $ "Simulation failed" +status (Fail (SimFail _)) = H.td ! A.class_ "is-danger" $ "Simulation failed" status (Fail SynthFail ) = H.td ! A.class_ "is-danger" $ "Synthesis failed" status (Fail EquivError ) = H.td ! A.class_ "is-danger" $ "Equivalence error" status (Fail TimeoutError) = H.td ! A.class_ "is-warning" $ "Time out" diff --git a/src/Verismith/Result.hs b/src/Verismith/Result.hs index d8efd2f..2ecb728 100644 --- a/src/Verismith/Result.hs +++ b/src/Verismith/Result.hs @@ -22,6 +22,8 @@ needed in "Verismith". module Verismith.Result ( Result(..) , ResultT(..) + , justPass + , justFail , () , annotate ) @@ -42,6 +44,14 @@ data Result a b = Fail a | Pass b deriving (Eq, Show) +justPass :: Result a b -> Maybe b +justPass (Fail _) = Nothing +justPass (Pass a) = Just a + +justFail :: Result a b -> Maybe a +justFail (Pass _) = Nothing +justFail (Fail a) = Just a + instance Semigroup (Result a b) where Pass _ <> a = a a <> _ = a diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs index 9d4281f..68273a2 100644 --- a/src/Verismith/Tool/Icarus.hs +++ b/src/Verismith/Tool/Icarus.hs @@ -14,6 +14,7 @@ module Verismith.Tool.Icarus ( Icarus(..) , defaultIcarus , runSimIc + , runSimIcEC ) where @@ -39,6 +40,8 @@ import Numeric (readInt) import Prelude hiding (FilePath) import Shelly import Shelly.Lifted (liftSh) +import Verismith.CounterEg (CounterEg (..)) +import Verismith.Result import Verismith.Tool.Internal import Verismith.Tool.Template import Verismith.Verilog.AST @@ -114,12 +117,12 @@ runSimIcarus sim rinfo bss = do let newtb = instantiateMod m tb let modWithTb = Verilog [newtb, m] liftSh . writefile "main.v" $ genSource modWithTb - annotate SimFail $ runSimWithFile sim "main.v" bss + annotate (SimFail mempty) $ runSimWithFile sim "main.v" bss where m = rinfo ^. mainModule runSimIcarusWithFile :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString -runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do +runSimIcarusWithFile sim f _ = annotate (SimFail mempty) . liftSh $ do dir <- pwd logCommand_ dir "icarus" $ run (icarusPath sim) ["-o", "main", toTextIgnore f] @@ -131,49 +134,46 @@ runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do fromBytes :: ByteString -> Integer fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b -runSimIc - :: (Synthesiser b) - => FilePath - -> Icarus - -> b - -> SourceInfo - -> [ByteString] - -> ResultSh ByteString -runSimIc datadir sim1 synth1 srcInfo bss = do - dir <- liftSh pwd - let top = srcInfo ^. mainModule - let inConcat = (RegConcat . filter filterClk $ (Id . fromPort <$> (top ^. modInPorts))) - let - tb = instantiateMod top $ ModDecl - "testbench" - [] - [] - [ Initial - $ fold - [ BlockAssign (Assign "clk" Nothing 0) - , BlockAssign (Assign inConcat Nothing 0) - ] - <> fold - ( (\r -> TimeCtrl - 10 - (Just $ BlockAssign (Assign inConcat Nothing r)) - ) - . fromInteger - . fromBytes - <$> bss - ) - <> (SysTaskEnable $ Task "finish" []) - , Always . TimeCtrl 5 . Just $ BlockAssign +tbModule :: [ByteString] -> ModDecl -> Verilog +tbModule bss top = + Verilog [ instantiateMod top $ ModDecl "testbench" [] [] + [ Initial + $ fold [ BlockAssign (Assign "clk" Nothing 0) + , BlockAssign (Assign inConcat Nothing 0) + ] + <> fold ((\r -> TimeCtrl 10 + (Just $ BlockAssign (Assign inConcat Nothing r))) + . fromInteger . fromBytes <$> bss) + <> (SysTaskEnable $ Task "finish" []) + , Always . TimeCtrl 5 . Just $ BlockAssign (Assign "clk" Nothing (UnOp UnNot (Id "clk"))) - , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task - "strobe" - ["%b", Id "y"] + , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable + $ Task "strobe" ["%b", Id "y"] + ] [] ] - [] + where + inConcat = (RegConcat . filter (/= (Id "clk")) $ (Id . fromPort <$> (top ^. modInPorts))) - liftSh . writefile "testbench.v" $ icarusTestbench datadir (Verilog [tb]) synth1 - liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"] - liftSh +counterTestBench :: CounterEg -> ModDecl -> Verilog +counterTestBench (CounterEg _ states) m = tbModule filtered m + where + filtered = convert . fold . fmap snd . filter ((/= "clk") . fst) <$> states + +runSimIc' :: (Synthesiser b) => ([ByteString] -> ModDecl -> Verilog) + -> FilePath + -> Icarus + -> b + -> SourceInfo + -> [ByteString] + -> Maybe ByteString + -> ResultSh ByteString +runSimIc' fun datadir sim1 synth1 srcInfo bss bs = do + dir <- liftSh pwd + let top = srcInfo ^. mainModule + let tb = fun bss top + liftSh . writefile tbname $ icarusTestbench datadir tb synth1 + liftSh $ exe dir "icarus" "iverilog" ["-o", exename, toTextIgnore tbname] + s <- liftSh $ B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) @@ -183,9 +183,29 @@ runSimIc datadir sim1 synth1 srcInfo bss = do (runFoldLines (mempty :: ByteString) callback (vvpPath sim1) - ["main"] - ) + [exename]) + case (bs, s) of + (Nothing, s') -> ResultT . return $ Pass s' + (Just bs', s') -> if bs' == s' + then ResultT . return $ Pass s' + else ResultT . return $ Fail (SimFail s') where exe dir name e = void . errExit False . logCommand dir name . timeout e - filterClk (Id "clk") = False - filterClk (Id _) = True + tbname = fromText $ toText synth1 <> "_testbench.v" + exename = toText synth1 <> "_main" + +runSimIc :: (Synthesiser b) + => FilePath -- ^ Data directory. + -> Icarus -- ^ Icarus simulator. + -> b -- ^ Synthesis tool to be tested. + -> SourceInfo -- ^ Original generated program to test. + -> [ByteString] -- ^ Test vectors to be passed as inputs to the generated Verilog. + -> Maybe ByteString -- ^ What the correct output should be. If + -- 'Nothing' is passed, then just return 'Pass + -- ByteString' with the answer. + -> ResultSh ByteString +runSimIc = runSimIc' tbModule + +runSimIcEC :: (Synthesiser b) => FilePath -> Icarus -> b + -> SourceInfo -> CounterEg -> Maybe ByteString -> ResultSh ByteString +runSimIcEC a b c d e = runSimIc' (const $ counterTestBench e) a b c d [] diff --git a/src/Verismith/Tool/Internal.hs b/src/Verismith/Tool/Internal.hs index ee31c4e..b97c2f1 100644 --- a/src/Verismith/Tool/Internal.hs +++ b/src/Verismith/Tool/Internal.hs @@ -77,10 +77,18 @@ class Tool a => Simulator a where data Failed = EmptyFail | EquivFail CounterEg | EquivError - | SimFail + | SimFail ByteString | SynthFail | TimeoutError - deriving (Eq, Show) + deriving (Eq) + +instance Show Failed where + show EmptyFail = "EmptyFail" + show (EquivFail _) = "EquivFail" + show EquivError = "EquivError" + show (SimFail bs) = "SimFail " <> T.unpack (T.take 10 $ showBS bs) + show SynthFail = "SynthFail" + show TimeoutError = "TimeoutError" instance Semigroup Failed where EmptyFail <> a = a diff --git a/verismith.cabal b/verismith.cabal index b54e522..76fc97b 100644 --- a/verismith.cabal +++ b/verismith.cabal @@ -1,5 +1,5 @@ name: verismith -version: 0.4.0.1 +version: 0.4.1.0 synopsis: Random verilog generation and simulator testing. description: Verismith provides random verilog generation modules @@ -27,7 +27,7 @@ source-repository head source-repository this type: git location: https://github.com/ymherklotz/verismith - tag: v0.4.0.1 + tag: v0.4.1.0 custom-setup setup-depends: -- cgit