Add data-file installation path

This removes the need to recursively copy the data directory which will also
save on space.

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: