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/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 +++--- 5 files changed, 42 insertions(+), 33 deletions(-) (limited to 'src/Verismith') 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 -- cgit