Add support for multiple modules

Had to manually change module names, as Yosys does not change the
module name at instantiation.

This is done using sed.

4 files changed, 41 insertions, 11 deletions

diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
index 6e02482..6d36348 100644
--- a/src/VeriFuzz/Sim/Internal.hs
+++ b/src/VeriFuzz/Sim/Internal.hs
@@ -18,6 +18,10 @@ module VeriFuzz.Sim.Internal
     , Simulator(..)
     , Synthesiser(..)
     , Failed(..)
+    , checkPresent
+    , checkPresentModules
+    , replace
+    , replaceMods
     , rootPath
     , timeout
     , timeout_
@@ -33,10 +37,12 @@ module VeriFuzz.Sim.Internal
     )
 where
 
-import           Control.Monad         (void)
+import           Control.Lens
+import           Control.Monad         (forM, void)
 import           Data.Bits             (shiftL)
 import           Data.ByteString       (ByteString)
 import qualified Data.ByteString       as B
+import           Data.Maybe            (catMaybes)
 import           Data.Text             (Text)
 import qualified Data.Text             as T
 import           Data.Time.LocalTime   (getZonedTime)
@@ -89,6 +95,32 @@ class Tool a => Synthesiser a where
 -- with also has those instances.
 type ResultSh = ResultT Failed Sh
 
+checkPresent :: FilePath -> Text -> Sh (Maybe Text)
+checkPresent fp t = do
+    errExit False $ run_ "grep" [t, toTextIgnore fp]
+    i <- lastExitCode
+    if i == 0 then return $ Just t else return Nothing
+
+-- | Checks what modules are present in the synthesised output, as some modules
+-- may have been inlined. This could be improved if the parser worked properly.
+checkPresentModules :: FilePath -> SourceInfo -> Sh [Text]
+checkPresentModules fp (SourceInfo _ src) = do
+    vals <- forM (src ^.. _Wrapped . traverse . modId . _Wrapped) $ checkPresent fp
+    return $ catMaybes vals
+
+-- | Uses sed to replace a string in a text file.
+replace :: FilePath -> Text -> Text -> Sh ()
+replace fp t1 t2 = do
+    errExit False . noPrint $ run_ "sed" ["-i", "s/" <> t1 <> "/" <> t2 <> "/g", toTextIgnore fp]
+
+-- | This is used because rename only renames the definitions of modules of
+-- course, so instead this just searches and replaces all the module names. This
+-- should find all the instantiations and definitions. This could again be made
+-- much simpler if the parser works.
+replaceMods :: FilePath -> Text -> SourceInfo -> Sh ()
+replaceMods fp t (SourceInfo _ src) =
+    void . forM (src ^.. _Wrapped . traverse . modId . _Wrapped) $ (\a -> replace fp a (a <> t))
+
 rootPath :: Sh FilePath
 rootPath = do
     current <- pwd
@@ -108,7 +140,7 @@ bsToI = B.foldl' (\i b -> (i `shiftL` 8) + fromIntegral b) 0
 {-# INLINE bsToI #-}
 
 noPrint :: Sh a -> Sh a
-noPrint = liftSh . print_stdout False . print_stderr False
+noPrint = print_stdout False . print_stderr False
 {-# INLINE noPrint #-}
 
 echoP :: Text -> Sh ()
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
index 771646d..f6e5a1e 100644
--- a/src/VeriFuzz/Sim/Template.hs
+++ b/src/VeriFuzz/Sim/Template.hs
@@ -88,8 +88,8 @@ write_verilog -force #{outf}
 |]
 
 -- brittany-disable-next-binding
-sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> Maybe b -> SourceInfo -> Text
-sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options]
+sbyConfig :: (Synthesiser a, Synthesiser b) => a -> Maybe b -> SourceInfo -> Text
+sbyConfig sim1 sim2 (SourceInfo top _) = [st|[options]
 multiclock on
 mode prove
 
@@ -99,9 +99,7 @@ smtbmc z3
 [script]
 #{readL}
 read -formal #{outputText sim1}
-#{rename "_1" mis}
 read -formal #{maybe "rtl.v" outputText sim2}
-#{rename "_2" mis}
 read -formal top.v
 prep -top #{top}
 
@@ -112,12 +110,11 @@ prep -top #{top}
 top.v
 |]
   where
-    mis = src ^.. getSourceId
     deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v", "cells_yosys.v"]
     depList =
       T.intercalate "\n"
         $   toTextIgnore
-        .   ((bd </> fromText "data") </>)
+        .   (fromText "data" </>)
         .   fromText
         <$> deps
     readL = T.intercalate "\n" $ mappend "read -formal " <$> deps
diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs
index 6ede8b5..1994a57 100644
--- a/src/VeriFuzz/Sim/Vivado.hs
+++ b/src/VeriFuzz/Sim/Vivado.hs
@@ -50,7 +50,7 @@ runSynthVivado sim (SourceInfo top src) = do
         writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput
             sim
         writefile "rtl.v" $ genSource src
-        run_ "sed" ["s/^module/(* use_dsp48=\"no\" *) module/;", "-i", "rtl.v"]
+        run_ "sed" ["s/^module/(* use_dsp=\"no\" *) module/;", "-i", "rtl.v"]
         echoP "Vivado: run"
     execute_ SynthFail
              dir
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs
index f72fb1a..1bff975 100644
--- a/src/VeriFuzz/Sim/Yosys.hs
+++ b/src/VeriFuzz/Sim/Yosys.hs
@@ -104,7 +104,6 @@ runEquiv
     -> SourceInfo
     -> ResultSh ()
 runEquiv _ sim1 sim2 srcInfo = do
-    root <- liftSh rootPath
     dir  <- liftSh pwd
     liftSh $ do
         writefile "top.v"
@@ -113,7 +112,9 @@ runEquiv _ sim1 sim2 srcInfo = do
             .  makeTopAssert
             $  srcInfo
             ^. mainModule
-        writefile "test.sby" $ sbyConfig root sim1 sim2 srcInfo
+        replaceMods (synthOutput sim1) "_1" srcInfo
+        replaceMods (maybe "rtl.v" synthOutput sim2) "_2" srcInfo
+        writefile "test.sby" $ sbyConfig sim1 sim2 srcInfo
     liftSh $ echoP "Running SymbiYosys"
     execute_ EquivFail dir "symbiyosys" "sby" ["-f", "test.sby"]
     liftSh $ echoP "SymbiYosys equivalence check passed"