Add output information to Type

6 files changed, 36 insertions, 36 deletions

diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
index 2d06819..6e02482 100644
--- a/src/VeriFuzz/Sim/Internal.hs
+++ b/src/VeriFuzz/Sim/Internal.hs
@@ -80,7 +80,6 @@ instance Monoid Failed where
 class Tool a => Synthesiser a where
     runSynth :: a        -- ^ Synthesiser tool instance
              -> SourceInfo  -- ^ Run information
-             -> FilePath -- ^ Output verilog file for the module
              -> ResultSh ()    -- ^ does not return any values
     synthOutput :: a -> FilePath
     setSynthOutput :: a -> FilePath -> a
diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs
index beb7f10..5bda0be 100644
--- a/src/VeriFuzz/Sim/Quartus.hs
+++ b/src/VeriFuzz/Sim/Quartus.hs
@@ -37,13 +37,13 @@ instance Tool Quartus where
 instance Synthesiser Quartus where
     runSynth = runSynthQuartus
     synthOutput = quartusOutput
-    setSynthOutput (Quartus a _) f = Quartus a f
+    setSynthOutput (Quartus a _) = Quartus a
 
 defaultQuartus :: Quartus
-defaultQuartus = Quartus Nothing "quartus/syn_quartus.v"
+defaultQuartus = Quartus Nothing "syn_quartus.v"
 
-runSynthQuartus :: Quartus -> SourceInfo -> FilePath -> ResultSh ()
-runSynthQuartus sim (SourceInfo top src) outf = do
+runSynthQuartus :: Quartus -> SourceInfo -> ResultSh ()
+runSynthQuartus sim (SourceInfo top src) = do
     dir <- liftSh pwd
     let ex = execute_ SynthFail dir "quartus"
     liftSh $ do
@@ -54,7 +54,7 @@ runSynthQuartus sim (SourceInfo top src) outf = do
     ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"]
     ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"]
     liftSh $ do
-        cp (fromText "simulation/vcs" </> fromText top <.> "vo") outf
+        cp (fromText "simulation/vcs" </> fromText top <.> "vo") $ synthOutput sim
         echoP "Quartus synthesis done"
   where
     inpf = "rtl.v"
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
index f630ea6..93f24a3 100644
--- a/src/VeriFuzz/Sim/Template.hs
+++ b/src/VeriFuzz/Sim/Template.hs
@@ -43,16 +43,18 @@ doubleName :: Text -> Text
 doubleName n = n <> " " <> n
 {-# INLINE doubleName #-}
 
+outputText :: Synthesiser a => a -> Text
+outputText = toTextIgnore . synthOutput
+
 -- brittany-disable-next-binding
-yosysSatConfig :: (Tool a, Tool b) => a -> Maybe b -> SourceInfo -> Text
-yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog syn_#{toText sim1}.v
+yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> Maybe b -> SourceInfo -> Text
+yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog #{outputText sim1}
 #{rename "_1" mis}
 read_verilog syn_#{idSim2}.v
 #{rename "_2" mis}
 read_verilog #{top}.v
 proc; opt_clean
 flatten #{top}
-! touch test.#{toText sim1}.#{idSim2}.input_ok
 sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{top}
 |]
   where
@@ -86,7 +88,7 @@ write_verilog -force #{outf}
 |]
 
 -- brittany-disable-next-binding
-sbyConfig :: (Tool a, Tool b) => FilePath -> a -> Maybe b -> SourceInfo -> Text
+sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> Maybe b -> SourceInfo -> Text
 sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options]
 mode prove
 
@@ -95,17 +97,17 @@ smtbmc z3
 
 [script]
 #{readL}
-read -formal syn_#{toText sim1}.v
+read -formal #{outputText sim1}
 #{rename "_1" mis}
-read -formal syn_#{maybe "rtl" toText sim2}.v
+read -formal #{maybe "rtl.v" outputText sim2}
 #{rename "_2" mis}
 read -formal top.v
 prep -top #{top}
 
 [files]
 #{depList}
-syn_#{maybe "rtl" toText sim2}.v
-syn_#{toText sim1}.v
+#{maybe "rtl.v" outputText sim2}
+#{outputText sim1}
 top.v
 |]
   where
diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs
index 7cf6d4b..d213a12 100644
--- a/src/VeriFuzz/Sim/Vivado.hs
+++ b/src/VeriFuzz/Sim/Vivado.hs
@@ -38,16 +38,16 @@ instance Tool Vivado where
 instance Synthesiser Vivado where
     runSynth = runSynthVivado
     synthOutput = vivadoOutput
-    setSynthOutput (Vivado a _) f = Vivado a f
+    setSynthOutput (Vivado a _) = Vivado a
 
 defaultVivado :: Vivado
-defaultVivado = Vivado "vivado" "vivado/syn_vivado.v"
+defaultVivado = Vivado "vivado" "syn_vivado.v"
 
-runSynthVivado :: Vivado -> SourceInfo -> FilePath -> ResultSh ()
-runSynthVivado sim (SourceInfo top src) outf = do
+runSynthVivado :: Vivado -> SourceInfo -> ResultSh ()
+runSynthVivado sim (SourceInfo top src) = do
     dir <- liftSh pwd
     liftSh $ do
-        writefile vivadoTcl . vivadoSynthConfig top $ toTextIgnore outf
+        writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput sim
         writefile "rtl.v" $ genSource src
         run_ "sed" ["s/^module/(* use_dsp48=\"no\" *) module/;", "-i", "rtl.v"]
         echoP "Vivado: run"
diff --git a/src/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs
index b5b1b8b..e5e3e06 100644
--- a/src/VeriFuzz/Sim/XST.hs
+++ b/src/VeriFuzz/Sim/XST.hs
@@ -42,13 +42,13 @@ instance Tool XST where
 instance Synthesiser XST where
     runSynth = runSynthXST
     synthOutput = xstOutput
-    setSynthOutput (XST a b _) f = XST a b f
+    setSynthOutput (XST a b _) = XST a b
 
 defaultXST :: XST
-defaultXST = XST "xst" "netgen" "xst/syn_xst.v"
+defaultXST = XST "xst" "netgen" "syn_xst.v"
 
-runSynthXST :: XST -> SourceInfo -> FilePath -> ResultSh ()
-runSynthXST sim (SourceInfo top src) outf = do
+runSynthXST :: XST -> SourceInfo -> ResultSh ()
+runSynthXST sim (SourceInfo top src) = do
     dir <- liftSh pwd
     let exec = execute_ SynthFail dir "xst"
     liftSh $ do
@@ -64,7 +64,7 @@ runSynthXST sim (SourceInfo top src) outf = do
         , "-ofmt"
         , "verilog"
         , toTextIgnore $ modFile <.> "ngc"
-        , toTextIgnore outf
+        , toTextIgnore $ synthOutput sim
         ]
     liftSh $ do
         echoP "XST: clean"
@@ -72,7 +72,7 @@ runSynthXST sim (SourceInfo top src) outf = do
             "sed"
             [ "-i"
             , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;"
-            , toTextIgnore outf
+            , toTextIgnore $ synthOutput sim
             ]
         echoP "XST: done"
   where
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs
index 98244a6..f219e01 100644
--- a/src/VeriFuzz/Sim/Yosys.hs
+++ b/src/VeriFuzz/Sim/Yosys.hs
@@ -42,16 +42,16 @@ instance Tool Yosys where
 instance Synthesiser Yosys where
   runSynth = runSynthYosys
   synthOutput = yosysOutput
-  setSynthOutput (Yosys a _) f = Yosys a f
+  setSynthOutput (Yosys a _) = Yosys a
 
 instance Show Yosys where
     show _ = "yosys"
 
 defaultYosys :: Yosys
-defaultYosys = Yosys "yosys" "yosys/syn_yosys.v"
+defaultYosys = Yosys "yosys" "syn_yosys.v"
 
-runSynthYosys :: Yosys -> SourceInfo -> FilePath -> ResultSh ()
-runSynthYosys sim (SourceInfo _ src) outf = (<?> SynthFail) . liftSh $ do
+runSynthYosys :: Yosys -> SourceInfo -> ResultSh ()
+runSynthYosys sim (SourceInfo _ src) = (<?> SynthFail) . liftSh $ do
     dir <- pwd
     writefile inpf $ genSource src
     echoP "Yosys: synthesis"
@@ -63,13 +63,13 @@ runSynthYosys sim (SourceInfo _ src) outf = (<?> SynthFail) . liftSh $ do
   where
     inpf = "rtl.v"
     inp  = toTextIgnore inpf
-    out  = toTextIgnore outf
+    out  = toTextIgnore $ synthOutput sim
 
 runMaybeSynth :: (Synthesiser a) => Maybe a -> SourceInfo -> ResultSh ()
 runMaybeSynth (Just sim) srcInfo =
-    runSynth sim srcInfo $ fromText [st|syn_#{toText sim}.v|]
+    runSynth sim srcInfo
 runMaybeSynth Nothing (SourceInfo _ src) =
-    liftSh . writefile "syn_rtl.v" $ genSource src
+    liftSh . writefile "rtl.v" $ genSource src
 
 runEquivYosys
     :: (Synthesiser a, Synthesiser b)
@@ -87,7 +87,7 @@ runEquivYosys yosys sim1 sim2 srcInfo = do
             $  srcInfo
             ^. mainModule
         writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
-    runSynth sim1 srcInfo $ fromText [st|syn_#{toText sim1}.v|]
+    runSynth sim1 srcInfo
     runMaybeSynth sim2 srcInfo
     liftSh $ do
         echoP "Yosys: equivalence check"
@@ -108,7 +108,6 @@ runEquiv _ sim1 sim2 srcInfo = do
     root <- liftSh rootPath
     dir  <- liftSh pwd
     liftSh $ do
-        echoP "SymbiYosys: setup"
         writefile "top.v"
             .  genSource
             .  initMod
@@ -116,6 +115,6 @@ runEquiv _ sim1 sim2 srcInfo = do
             $  srcInfo
             ^. mainModule
         writefile "test.sby" $ sbyConfig root sim1 sim2 srcInfo
-    liftSh $ echoP "SymbiYosys: run"
+    liftSh $ echoP "Running SymbiYosys"
     execute_ EquivFail dir "symbiyosys" "sby" ["-f", "test.sby"]
-    liftSh $ echoP "SymbiYosys: done"
+    liftSh $ echoP "SymbiYosys equivalence check passed"