Add template file

4 files changed, 72 insertions, 47 deletions

diff --git a/src/VeriFuzz/Simulator/General.hs b/src/VeriFuzz/Simulator/General.hs
index 3615d3a..538ecaa 100644
--- a/src/VeriFuzz/Simulator/General.hs
+++ b/src/VeriFuzz/Simulator/General.hs
@@ -38,6 +38,11 @@ class (Simulator a) => Synthesize a where
            -> FilePath -- ^ Output verilog file for the module
            -> Sh ()    -- ^ does not return any values
 
+rootPath :: Sh FilePath
+rootPath = do
+  current <- pwd
+  maybe current fromText <$> get_env "VERIFUZZ_ROOT"
+
 timeout :: FilePath -> [Text] -> Sh Text
 timeout = command1 "timeout" ["180"] . toTextIgnore
 {-# INLINE timeout #-}
diff --git a/src/VeriFuzz/Simulator/Internal/Template.hs b/src/VeriFuzz/Simulator/Internal/Template.hs
new file mode 100644
index 0000000..d0542f1
--- /dev/null
+++ b/src/VeriFuzz/Simulator/Internal/Template.hs
@@ -0,0 +1,47 @@
+{-|
+Module      : VeriFuzz.Simulator.Internal.Template
+Description : Template file for different configuration files
+Copyright   : (c) 2019, Yann Herklotz Grave
+License     : GPL-3
+Maintainer  : ymherklotz [at] gmail [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Template file for different configuration files.
+-}
+
+{-# LANGUAGE QuasiQuotes #-}
+
+module VeriFuzz.Simulator.Internal.Template where
+
+import           Data.Text                  (Text)
+import           Text.Shakespeare.Text      (st)
+import           VeriFuzz.Simulator.General
+import           VeriFuzz.Verilog
+
+yosysSatConfig :: (Simulator a, Simulator b) => a -> Maybe b -> ModDecl -> Text
+yosysSatConfig sim1 sim2 m = [st|read_verilog syn_#{toText sim1}.v
+rename #{modName m} #{modName m}_1
+read_verilog syn_#{idSim2}.v
+rename #{modName m} #{modName m}_2
+read_verilog top.v
+proc; opt_clean
+flatten #{modName m}
+! touch test.#{toText sim1}.#{idSim2}.input_ok
+sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName m}
+|]
+  where
+    idSim2 = maybe "rtl" toText sim2
+
+yosysSimConfig :: Text
+yosysSimConfig = [st|read_verilog rtl.v; proc;;
+rename mod mod_rtl
+|]
+
+xstSynthConfig :: ModDecl -> Text
+xstSynthConfig m = [st|run
+-ifn #{modName m}.prj -ofn #{modName m} -p artix7 -top #{modName m}
+-iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO
+-fsm_extract YES -fsm_encoding Auto
+-change_error_to_warning "HDLCompiler:226 HDLCompiler:1832"
+|]
diff --git a/src/VeriFuzz/Simulator/Xst.hs b/src/VeriFuzz/Simulator/Xst.hs
index 7b6608b..2314dd1 100644
--- a/src/VeriFuzz/Simulator/Xst.hs
+++ b/src/VeriFuzz/Simulator/Xst.hs
@@ -14,13 +14,14 @@ Xst (ise) simulator implementation.
 
 module VeriFuzz.Simulator.Xst where
 
-import           Control.Lens               hiding ((<.>))
-import           Prelude                    hiding (FilePath)
+import           Control.Lens                         hiding ((<.>))
+import           Prelude                              hiding (FilePath)
 import           Shelly
-import           Text.Shakespeare.Text      (st)
+import           Text.Shakespeare.Text                (st)
 import           VeriFuzz.Simulator.General
-import           VeriFuzz.Verilog.AST
-import           VeriFuzz.Verilog.CodeGen
+import           VeriFuzz.Simulator.Internal.Template
+import           VeriFuzz.Verilog
+import           VeriFuzz.Verilog
 
 data Xst = Xst { xstPath    :: FilePath
                , netgenPath :: FilePath
@@ -39,19 +40,13 @@ defaultXst =
 -- brittany-disable-next-binding
 runSynthXst :: Xst -> ModDecl -> FilePath -> Sh ()
 runSynthXst sim m outf = do
-  writefile xstFile [st|run
--ifn #{modName}.prj -ofn #{modName} -p artix7 -top #{modName}
--iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO
--fsm_extract YES -fsm_encoding Auto
--change_error_to_warning "HDLCompiler:226 HDLCompiler:1832"
-|]
+  writefile xstFile $ xstSynthConfig m
   writefile prjFile [st|verilog work "rtl.v"|]
   writefile "rtl.v" $ genSource m
   timeout_ (xstPath sim) ["-ifn", toTextIgnore xstFile]
   run_ (netgenPath sim) ["-w", "-ofmt", "verilog", toTextIgnore $ modFile <.> "ngc", toTextIgnore outf]
   run_ "sed" ["-i", "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;", toTextIgnore outf]
   where
-    modName = m ^. modId . getIdentifier
-    modFile = fromText modName
+    modFile = fromText $ modName m
     xstFile = modFile <.> "xst"
     prjFile = modFile <.> "prj"
diff --git a/src/VeriFuzz/Simulator/Yosys.hs b/src/VeriFuzz/Simulator/Yosys.hs
index 90c40bf..4c2e0ad 100644
--- a/src/VeriFuzz/Simulator/Yosys.hs
+++ b/src/VeriFuzz/Simulator/Yosys.hs
@@ -14,13 +14,14 @@ Yosys simulator implementation.
 
 module VeriFuzz.Simulator.Yosys where
 
-import           Data.Maybe                 (fromMaybe)
-import           Data.Text                  (Text)
-import qualified Data.Text                  as T
-import           Prelude                    hiding (FilePath)
+import           Data.Maybe                           (fromMaybe)
+import           Data.Text                            (Text)
+import qualified Data.Text                            as T
+import           Prelude                              hiding (FilePath)
 import           Shelly
-import           Text.Shakespeare.Text      (st)
+import           Text.Shakespeare.Text                (st)
 import           VeriFuzz.Simulator.General
+import           VeriFuzz.Simulator.Internal.Template
 import           VeriFuzz.Verilog
 
 newtype Yosys = Yosys { yosysPath :: FilePath }
@@ -34,16 +35,13 @@ instance Synthesize Yosys where
 defaultYosys :: Yosys
 defaultYosys = Yosys "/usr/bin/yosys"
 
--- brittany-disable-next-binding
 writeSimFile :: Yosys    -- ^ Simulator instance
              -> ModDecl  -- ^ Current module
              -> FilePath -- ^ Output sim file
              -> Sh ()
 writeSimFile _ m file = do
   writefile "rtl.v" $ genSource m
-  writefile file [st|read_verilog rtl.v; proc;;
-rename mod mod_rtl
-|]
+  writefile file yosysSimConfig
 
 runSynthYosys :: Yosys -> ModDecl -> FilePath -> Sh ()
 runSynthYosys sim m outf = do
@@ -53,23 +51,7 @@ runSynthYosys sim m outf = do
   inpf = "rtl.v"
   inp  = toTextIgnore inpf
   out  = toTextIgnore outf
-
--- brittany-disable-next-binding
-writeSatFile :: (Synthesize a, Synthesize b) => FilePath -> a -> Maybe b -> ModDecl -> Sh ()
-writeSatFile checkFile sim1 sim2 m =
-  writefile checkFile [st|read_ilang syn_#{toText sim1}.il
-rename #{modName m} #{modName m}_1
-read_ilang syn_#{idSim2}.il
-rename #{modName m} #{modName m}_2
-read_verilog top.v
-proc; opt_clean
-flatten #{modName m}
-! touch test.#{toText sim1}.#{idSim2}.input_ok
-sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName m}
-|]
-  where
-    idSim2 = maybe "rtl" toText sim2
-    -- ids = T.intercalate "," $ allVars m ^.. traverse . getIdentifier
+  -- ids = T.intercalate "," $ allVars m ^.. traverse . getIdentifier
 
 runOtherSynth :: (Synthesize a) => Maybe a -> ModDecl -> Sh ()
 runOtherSynth (Just sim) m = runSynth sim m $ fromText [st|syn_#{toText sim}.v|]
@@ -78,13 +60,9 @@ runOtherSynth Nothing    m = writefile "syn_rtl.v" $ genSource m
 runEquiv :: (Synthesize a, Synthesize b) => Yosys -> a -> Maybe b -> ModDecl -> Sh ()
 runEquiv yosys sim1 sim2 m = do
   writefile "top.v" . genSource . initMod $ makeTop 2 m
-  writeSatFile checkFile sim1 sim2 m
+  writefile checkFile $ yosysSatConfig sim1 sim2 m
   runSynth sim1 m $ fromText [st|syn_#{toText sim1}.v|]
   runOtherSynth sim2 m
-  run_ (yosysPath yosys) [checkFile]
-  where checkFile = [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|]
-
--- | Generate @.il@ files for Yosys equivalence checking using the SAT solver.
-genIl :: (Synthesize a) => Yosys -> a -> ModDecl -> Sh ()
-genIl yosys sim m = do
-  return
+  run_ (yosysPath yosys) [toTextIgnore checkFile]
+  where
+    checkFile = fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|]