From 01c2ab3f6a58d416528efce3057e2cf2f1604489 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 29 Oct 2019 11:53:43 +0000 Subject: Add data-file installation path This removes the need to recursively copy the data directory which will also save on space. --- src/Verismith.hs | 19 ++++++++++++++----- src/Verismith/Fuzz.hs | 29 ++++++++++++++++------------- src/Verismith/Reduce.hs | 7 ++++--- src/Verismith/Tool/Icarus.hs | 11 +++++++---- src/Verismith/Tool/Template.hs | 22 ++++++++++++---------- src/Verismith/Tool/Yosys.hs | 6 +++--- verismith.cabal | 4 ++-- 7 files changed, 58 insertions(+), 40 deletions(-) diff --git a/src/Verismith.hs b/src/Verismith.hs index 6a2bc72..41d845d 100644 --- a/src/Verismith.hs +++ b/src/Verismith.hs @@ -54,6 +54,7 @@ import Hedgehog (Gen) import qualified Hedgehog.Gen as Hog import Hedgehog.Internal.Seed (Seed) import Options.Applicative +import Paths_verismith (getDataDir) import Prelude hiding (FilePath) import Shelly hiding (command) import Shelly.Lifted (liftSh) @@ -71,6 +72,9 @@ import Verismith.Tool.Internal import Verismith.Verilog import Verismith.Verilog.Parser (parseSourceInfoFile) +toFP :: String -> FilePath +toFP = fromText . T.pack + myForkIO :: IO () -> IO (MVar ()) myForkIO io = do mvar <- newEmptyMVar @@ -124,9 +128,10 @@ randomise config@(Config a _ c d e) = do handleOpts :: Opts -> IO () handleOpts (Fuzz o configF f k n nosim noequiv noreduction) = do config <- getConfig configF + datadir <- getDataDir _ <- runFuzz (FuzzOpts (Just $ fromText o) - f k n nosim noequiv noreduction config) + f k n nosim noequiv noreduction config (toFP datadir)) defaultYosys (fuzzMultiple (proceduralSrc "top" config)) return () @@ -145,13 +150,14 @@ handleOpts (Parse f) = do where file = T.unpack . toTextIgnore $ f handleOpts (Reduce f t _ ls' False) = do src <- parseSourceInfoFile t (toTextIgnore f) + datadir <- getDataDir case descriptionToSynth <$> ls' of a : b : _ -> do putStrLn "Reduce with equivalence check" shelly $ do make dir pop dir $ do - src' <- reduceSynth a b src + src' <- reduceSynth (toFP datadir) a b src writefile (fromText ".." dir <.> "v") $ genSource src' a : _ -> do putStrLn "Reduce with synthesis failure" @@ -166,6 +172,7 @@ handleOpts (Reduce f t _ ls' False) = do where dir = fromText "reduce" handleOpts (Reduce f t _ ls' True) = do src <- parseSourceInfoFile t (toTextIgnore f) + datadir <- getDataDir case descriptionToSynth <$> ls' of a : b : _ -> do putStrLn "Starting equivalence check" @@ -174,7 +181,7 @@ handleOpts (Reduce f t _ ls' True) = do pop dir $ do runSynth a src runSynth b src - runEquiv a b src + runEquiv (toFP datadir) a b src case res of Pass _ -> putStrLn "Equivalence check passed" Fail EquivFail -> putStrLn "Equivalence check failed" @@ -264,10 +271,11 @@ checkEquivalence :: SourceInfo -> Text -> IO Bool checkEquivalence src dir = shellyFailDir $ do mkdir_p (fromText dir) curr <- toTextIgnore <$> pwd + datadir <- liftIO getDataDir setenv "VERISMITH_ROOT" curr cd (fromText dir) catch_sh - ((runResultT $ runEquiv defaultYosys defaultVivado src) >> return True) + ((runResultT $ runEquiv (toFP datadir) defaultYosys defaultVivado src) >> return True) ((\_ -> return False) :: RunFailed -> Sh Bool) -- | Run a fuzz run and check if all of the simulators passed by checking if the @@ -284,6 +292,7 @@ runEquivalence seed gm t d k i = do (_, m) <- shelly $ sampleSeed seed gm let srcInfo = SourceInfo "top" m rand <- generateByteString 20 + datadir <- getDataDir shellyFailDir $ do mkdir_p (fromText d fromText n) curr <- toTextIgnore <$> pwd @@ -292,7 +301,7 @@ runEquivalence seed gm t d k i = do _ <- catch_sh ( runResultT - $ runEquiv defaultYosys defaultVivado srcInfo + $ runEquiv (toFP datadir) defaultYosys defaultVivado srcInfo >> liftSh (logger "Test OK") ) $ onFailure n diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs index eeafaa6..d14e74b 100644 --- a/src/Verismith/Fuzz.hs +++ b/src/Verismith/Fuzz.hs @@ -72,6 +72,7 @@ data FuzzOpts = FuzzOpts { _fuzzOptsOutput :: !(Maybe FilePath) , _fuzzOptsNoEquiv :: !Bool , _fuzzOptsNoReduction :: !Bool , _fuzzOptsConfig :: {-# UNPACK #-} !Config + , _fuzzDataDir :: {-# UNPACK #-} !FilePath } deriving (Show, Eq) @@ -86,6 +87,7 @@ defaultFuzzOpts = FuzzOpts { _fuzzOptsOutput = Nothing , _fuzzOptsNoEquiv = False , _fuzzOptsNoReduction = False , _fuzzOptsConfig = defaultConfig + , _fuzzDataDir = fromText "." } data FuzzEnv = FuzzEnv { _getSynthesisers :: ![SynthTool] @@ -225,9 +227,7 @@ failedSynthesis = fmap toSynth . filter failed . _fuzzSynthStatus <$> get toSynth (SynthStatus s _ _) = s make :: MonadSh m => FilePath -> m () -make f = liftSh $ do - mkdir_p f - cp_r "data" $ f fromText "data" +make f = liftSh $ mkdir_p f pop :: (MonadBaseControl IO m, MonadSh m) => FilePath -> m a -> m a pop f a = do @@ -255,6 +255,7 @@ toolRun t m = do equivalence :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () equivalence src = do + datadir <- fmap _fuzzDataDir askOpts synth <- passedSynthesis -- let synthComb = -- nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth @@ -263,12 +264,12 @@ equivalence src = do . filter (uncurry (/=)) $ (,) defaultIdentitySynth <$> synth - resTimes <- liftSh $ mapM (uncurry equiv) synthComb + resTimes <- liftSh $ mapM (uncurry (equiv datadir)) synthComb fuzzSynthResults .= toSynthResult synthComb resTimes liftSh $ inspect resTimes where tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') - equiv a b = + equiv datadir a b = toolRun ("equivalence check for " <> toText a <> " and " <> toText b) . runResultT $ do make dir @@ -283,28 +284,29 @@ equivalence src = do synthOutput b ) $ synthOutput b writefile "rtl.v" $ genSource src - runEquiv a b src + runEquiv datadir a b src where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m () simulation src = do + datadir <- fmap _fuzzDataDir askOpts synth <- passedSynthesis vals <- liftIO $ generateByteString 20 - ident <- liftSh $ equiv vals defaultIdentitySynth - resTimes <- liftSh $ mapM (equiv vals) synth + ident <- liftSh $ equiv datadir vals defaultIdentitySynth + resTimes <- liftSh $ mapM (equiv datadir vals) synth liftSh . inspect $ (\(_, r) -> bimap show (T.unpack . T.take 10 . showBS) r) <$> (ident : resTimes) where - equiv b a = toolRun ("simulation for " <> toText a) . runResultT $ do + equiv datadir b 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 defaultIcarus a src b + runSimIc datadir defaultIcarus a src b where dir = fromText $ "simulation_" <> toText a -- | Generate a specific number of random bytestrings of size 256. @@ -336,16 +338,17 @@ passEquiv = filter withIdentity . _fuzzSynthResults <$> get -- | Always reduces with respect to 'Identity'. reduction :: (MonadSh m) => SourceInfo -> Fuzz m () reduction src = do + datadir <- fmap _fuzzDataDir askOpts fails <- failEquivWithIdentity synthFails <- failedSynthesis - _ <- liftSh $ mapM red fails + _ <- liftSh $ mapM (red datadir) fails _ <- liftSh $ mapM redSynth synthFails return () where - red (SynthResult a b _ _) = do + red datadir (SynthResult a b _ _) = do make dir pop dir $ do - s <- reduceSynth a b src + s <- reduceSynth datadir a b src writefile (fromText ".." dir <.> "v") $ genSource s return s where dir = fromText $ "reduce_" <> toText a <> "_" <> toText b diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs index 88f0b42..a7ec3f8 100644 --- a/src/Verismith/Reduce.hs +++ b/src/Verismith/Reduce.hs @@ -582,17 +582,18 @@ reduceWithScript top script file = do -- | Reduce a 'SourceInfo' using two 'Synthesiser' that are passed to it. reduceSynth :: (Synthesiser a, Synthesiser b, MonadSh m) - => a + => Shelly.FilePath + -> a -> b -> SourceInfo -> m SourceInfo -reduceSynth a b = reduce synth +reduceSynth datadir a b = reduce synth where synth src' = liftSh $ do r <- runResultT $ do runSynth a src' runSynth b src' - runEquiv a b src' + runEquiv datadir a b src' return $ case r of Fail EquivFail -> True Fail _ -> False diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs index b783033..9d4281f 100644 --- a/src/Verismith/Tool/Icarus.hs +++ b/src/Verismith/Tool/Icarus.hs @@ -133,15 +133,16 @@ fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b runSimIc :: (Synthesiser b) - => Icarus + => FilePath + -> Icarus -> b -> SourceInfo -> [ByteString] -> ResultSh ByteString -runSimIc sim1 synth1 srcInfo bss = do +runSimIc datadir sim1 synth1 srcInfo bss = do dir <- liftSh pwd let top = srcInfo ^. mainModule - let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts))) + let inConcat = (RegConcat . filter filterClk $ (Id . fromPort <$> (top ^. modInPorts))) let tb = instantiateMod top $ ModDecl "testbench" @@ -170,7 +171,7 @@ runSimIc sim1 synth1 srcInfo bss = do ] [] - liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1 + liftSh . writefile "testbench.v" $ icarusTestbench datadir (Verilog [tb]) synth1 liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"] liftSh $ B.take 8 @@ -186,3 +187,5 @@ runSimIc sim1 synth1 srcInfo bss = do ) where exe dir name e = void . errExit False . logCommand dir name . timeout e + filterClk (Id "clk") = False + filterClk (Id _) = True diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs index c0cbfe1..d02daf8 100644 --- a/src/Verismith/Tool/Template.hs +++ b/src/Verismith/Tool/Template.hs @@ -89,8 +89,8 @@ write_verilog -force #{outf} |] -- brittany-disable-next-binding -sbyConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text -sbyConfig sim1 sim2 (SourceInfo top _) = [st|[options] +sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> Text +sbyConfig datadir sim1 sim2 (SourceInfo top _) = [st|[options] multiclock on mode prove @@ -115,19 +115,21 @@ top.v depList = T.intercalate "\n" $ toTextIgnore - . (fromText "data" ) + . (datadir fromText "data" ) . fromText <$> deps readL = T.intercalate "\n" $ mappend "read -formal " <$> deps -icarusTestbench :: (Synthesiser a) => Verilog -> a -> Text -icarusTestbench t synth1 = [st| -`include "data/cells_cmos.v" -`include "data/cells_cyclone_v.v" -`include "data/cells_verific.v" -`include "data/cells_xilinx_7.v" -`include "data/cells_yosys.v" +icarusTestbench :: (Synthesiser a) => FilePath -> Verilog -> a -> Text +icarusTestbench datadir t synth1 = [st| +`include "#{ddir}/data/cells_cmos.v" +`include "#{ddir}/data/cells_cyclone_v.v" +`include "#{ddir}/data/cells_verific.v" +`include "#{ddir}/data/cells_xilinx_7.v" +`include "#{ddir}/data/cells_yosys.v" `include "#{toTextIgnore $ synthOutput synth1}" #{genSource t} |] + where + ddir = toTextIgnore datadir diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs index 9c0a864..afbffe9 100644 --- a/src/Verismith/Tool/Yosys.hs +++ b/src/Verismith/Tool/Yosys.hs @@ -102,8 +102,8 @@ runEquivYosys yosys sim1 sim2 srcInfo = do where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|] runEquiv - :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> ResultSh () -runEquiv sim1 sim2 srcInfo = do + :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> ResultSh () +runEquiv datadir sim1 sim2 srcInfo = do dir <- liftSh pwd liftSh $ do writefile "top.v" @@ -114,7 +114,7 @@ runEquiv sim1 sim2 srcInfo = do ^. mainModule replaceMods (synthOutput sim1) "_1" srcInfo replaceMods (synthOutput sim2) "_2" srcInfo - writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo + writefile "proof.sby" $ sbyConfig datadir sim1 sim2 srcInfo e <- liftSh $ do exe dir "symbiyosys" "sby" ["-f", "proof.sby"] lastExitCode diff --git a/verismith.cabal b/verismith.cabal index 389ca16..61fd087 100644 --- a/verismith.cabal +++ b/verismith.cabal @@ -14,11 +14,11 @@ category: Hardware build-type: Custom cabal-version: >=1.10 extra-source-files: README.md - , data/*.v , examples/*.v , examples/config.toml , scripts/*.py , scripts/*.sh +data-files: data/*.v source-repository head type: git @@ -27,7 +27,7 @@ source-repository head source-repository this type: git location: https://github.com/ymherklotz/verismith - tag: v0.4.0.0 + tag: v0.4.0.1 custom-setup setup-depends: -- cgit