Add output information to Type

8 files changed, 95 insertions, 82 deletions

diff --git a/.gitignore b/.gitignore
index 4608789..615416c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,6 +4,4 @@ TAGS
 # Folders
 .stack-work
 .shelly
-equiv*
-output*
 failed
\ No newline at end of file
diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs
index 084caee..5372d94 100644
--- a/src/VeriFuzz/Fuzz.hs
+++ b/src/VeriFuzz/Fuzz.hs
@@ -50,6 +50,7 @@ import           VeriFuzz.Sim.Vivado
 import           VeriFuzz.Sim.XST
 import           VeriFuzz.Sim.Yosys
 import           VeriFuzz.Verilog.AST
+import           VeriFuzz.Verilog.CodeGen
 
 -- | Common type alias for synthesis results
 type UResult = Result Failed ()
@@ -171,11 +172,16 @@ instance Monoid FuzzResult where
 -- read from and the current state of all the results.
 type Fuzz m = StateT FuzzResult (ReaderT FuzzEnv m)
 
-runFuzz :: (Monad m) => [SynthTool] -> [SimTool] -> Yosys -> Fuzz m b -> m b
-runFuzz synth sim yos m =
+runFuzz
+  :: MonadIO m =>
+     [SynthTool] -> [SimTool] -> Yosys -> Fuzz Sh a -> m a
+runFuzz synth sim yos m = shelly $ runFuzz' synth sim yos m
+
+runFuzz' :: Monad m => [SynthTool] -> [SimTool] -> Yosys -> Fuzz m b -> m b
+runFuzz' synth sim yos m =
     runReaderT (evalStateT m (FuzzResult [] [] [])) (FuzzEnv synth sim yos)
 
-synthesisers :: (Monad m) => Fuzz m [SynthTool]
+synthesisers :: Monad m => Fuzz m [SynthTool]
 synthesisers = lift $ asks getSynthesisers
 
 --simulators :: (Monad m) => Fuzz () m [SimTool]
@@ -184,71 +190,80 @@ synthesisers = lift $ asks getSynthesisers
 combinations :: [a] -> [b] -> [(a, b)]
 combinations l1 l2 = [ (x, y) | x <- l1, y <- l2 ]
 
-runInTmp :: (MonadSh m) => m a -> m a
-runInTmp a = liftSh (withTmpDir $ (\dir -> cd dir)) >> a
-
-mkAndRun :: (MonadSh m) => FilePath -> Sh a -> m a
-mkAndRun a = liftSh . chdir_p a
-
-liftWith'
-    :: (MonadIO m)
-    => (Sh (Result a b) -> Sh (Result a b))
-    -> ResultT a Sh b
-    -> m (Result a b)
-liftWith' a = liftIO . shellyFailDir . a . runResultT
-
---lift' :: (MonadIO m) => ResultT a Sh b -> m (Result a b)
---lift' = liftWith' id
-
-logT :: (MonadIO m) => Text -> m ()
-logT = liftIO . shelly . echoP
+logT :: MonadSh m => Text -> m ()
+logT = liftSh . echoP
 
-timeit :: (MonadIO m) => m a -> m (NominalDiffTime, a)
+timeit :: (MonadIO m, MonadSh m) => m a -> m (NominalDiffTime, a)
 timeit a = do
     start <- liftIO getCurrentTime
     result <- a
     end <- liftIO getCurrentTime
     return (diffUTCTime end start, result)
 
-synthesis :: (MonadIO m) => SourceInfo -> Fuzz m ()
+synthesis :: MonadSh m => SourceInfo -> Fuzz m ()
 synthesis src = do
     synth   <- synthesisers
-    results <- mapM
-        (\a -> liftWith' (mkAndRun . fromText $ showT a)
-            $ runSynth a src (fromText $ "syn_" <> showT a <> ".v")
-        )
-        synth
+    results <- liftSh $ mapM exec synth
     synthStatus .= zipWith SynthStatus synth results
-    liftIO $ print results
+    liftSh $ inspect results
+    where
+        exec a = runResultT $ do
+            liftSh . mkdir_p . fromText $ toText a
+            pop (fromText $ toText a) $ runSynth a src
 
-generateSample :: (MonadIO m) => Gen SourceInfo -> Fuzz m SourceInfo
+generateSample :: (MonadIO m, MonadSh m) => Gen SourceInfo -> Fuzz m SourceInfo
 generateSample gen = do
     logT "Sampling Verilog from generator"
     (t, src)   <- timeit $ Hog.sample gen
     logT $ "Generated Verilog (" <> showT t <> ")"
     return src
 
-passedSynthesis :: (MonadIO m) => Fuzz m [SynthTool]
+passedSynthesis :: MonadSh m => Fuzz m [SynthTool]
 passedSynthesis = fmap toSynth . filter passed . _synthStatus <$> get
     where
         passed (SynthStatus _ (Pass _)) = True
+        passed _                        = False
         toSynth (SynthStatus s _) = s
 
-fuzz :: (MonadIO m) => Gen SourceInfo -> Fuzz m FuzzResult
-fuzz gen = do
+make :: MonadSh m => FilePath -> m ()
+make f = liftSh $ do
+    mkdir_p f
+    cp_r "data" $ f </> fromText "data"
+
+pop :: MonadSh m => FilePath -> m a -> m a
+pop f a = do
+    dir <- liftSh pwd
+    liftSh $ cd f
+    ret <- a
+    liftSh $ cd dir
+    return ret
+
+equivalence :: MonadSh m => SourceInfo -> Fuzz m ()
+equivalence src = do
     yos   <- lift $ asks yosysInstance
-    src <- generateSample gen
-    synthesis src
     synth <- passedSynthesis
     let synthComb =
             nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth
-    results <- mapM (uncurry $ equivalence yos src) synthComb
-    liftIO $ print results
+    results <- liftSh $ mapM (uncurry $ equiv yos) synthComb
+    liftSh $ inspect results
+    where
+        tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a')
+        equiv yos a b = runResultT $ do
+            make dir
+            pop dir $ do
+                liftSh $ do
+                    cp (fromText ".." </> fromText (toText a) </> synthOutput a) $ synthOutput a
+                    cp (fromText ".." </> fromText (toText b) </> synthOutput b) $ synthOutput b
+                    writefile "rtl.v" $ genSource src
+                runEquiv yos a (Just b) src
+            where
+                dir = fromText $ "equiv_" <> toText a <> "_" <> toText b
+
+fuzz :: (MonadIO m, MonadSh m) => Gen SourceInfo -> Fuzz m FuzzResult
+fuzz gen = do
+    make "output"
+    pop "output" $ do
+        src <- generateSample gen
+        synthesis src
+        equivalence src
     return mempty
-  where
-    tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a')
-    equivalence yos src a b =
-        liftIO . shellyFailDir . runInTmp . runResultT $ runEquiv yos
-                                                                  a
-                                                                  (Just b)
-                                                                  src
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"