From 404a828cd1bb7d69d1e879882a6b79f3378cd98d Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 25 May 2019 22:37:01 +0100
Subject: Add more command line options for replay

---
 src/VeriFuzz.hs | 76 +++++++++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 69 insertions(+), 7 deletions(-)

diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs
index 66c795f..6d4f839 100644
--- a/src/VeriFuzz.hs
+++ b/src/VeriFuzz.hs
@@ -28,7 +28,7 @@ module VeriFuzz
 where
 
 import           Control.Concurrent
-import           Control.Lens
+import           Control.Lens             hiding ((<.>))
 import           Control.Monad.IO.Class   (liftIO)
 import qualified Crypto.Random.DRBG       as C
 import           Data.ByteString          (ByteString)
@@ -58,6 +58,7 @@ import           VeriFuzz.Result
 import           VeriFuzz.Sim
 import           VeriFuzz.Sim.Internal
 import           VeriFuzz.Verilog
+import           VeriFuzz.Verilog.Parser  (parseSourceInfoFile)
 
 data OptTool = TYosys
           | TXST
@@ -79,9 +80,11 @@ data Opts = Fuzz { fuzzOutput :: {-# UNPACK #-} !Text
                      }
           | Parse { fileName :: {-# UNPACK #-} !FilePath
                   }
-          | Reduce { fileName     :: {-# UNPACK #-} !FilePath
-                   , top          :: {-# UNPACK #-} !Text
-                   , reduceScript :: {-# UNPACK #-} !FilePath
+          | Reduce { fileName        :: {-# UNPACK #-} !FilePath
+                   , top             :: {-# UNPACK #-} !Text
+                   , reduceScript    :: {-# UNPACK #-} !(Maybe FilePath)
+                   , synthesiserDesc :: ![SynthDescription]
+                   , rerun           :: Bool
                    }
           | ConfigOpt { writeConfig :: !(Maybe FilePath)
                       , configFile  :: !(Maybe FilePath)
@@ -107,6 +110,14 @@ parseSynth val | val == "yosys" = Just TYosys
                | val == "xst"   = Just TXST
                | otherwise      = Nothing
 
+parseSynthDesc :: String -> Maybe SynthDescription
+parseSynthDesc val | val == "yosys" = Just $ SynthDescription "yosys" Nothing Nothing Nothing
+                   | val == "vivado" = Just $ SynthDescription "vivado" Nothing Nothing Nothing
+                   | val == "xst"   = Just $ SynthDescription "xst" Nothing Nothing Nothing
+                   | val == "quartus"   = Just $ SynthDescription "quartus" Nothing Nothing Nothing
+                   | val == "identity"   = Just $ SynthDescription "identity" Nothing Nothing Nothing
+                   | otherwise      = Nothing
+
 parseSim :: String -> Maybe OptTool
 parseSim val | val == "icarus" = Just TIcarus
              | otherwise       = Nothing
@@ -180,13 +191,22 @@ reduceOpts =
                 <> showDefault
                 <> value "top"
                 )
-        <*> (  strOption
+        <*> (  optional . strOption
             $  long "script"
-            <> short 's'
             <> metavar "SCRIPT"
             <> help
                    "Script that determines if the current file is interesting, which is determined by the script returning 0."
             )
+        <*> (many . option (optReader parseSynthDesc) $
+                 short 's'
+                 <> long "synth"
+                 <> metavar "SYNTH"
+                 <> help "Specify synthesiser to use."
+                 )
+    <*> (switch $
+        short 'r'
+        <> long "rerun"
+        <> help "Only rerun the current synthesis file with all the synthesisers.")
 
 configOpts :: Parser Opts
 configOpts =
@@ -346,7 +366,49 @@ handleOpts (Parse f) = do
         Left  l -> print l
         Right v -> print $ GenVerilog v
     where file = T.unpack . toTextIgnore $ f
-handleOpts (Reduce    f t    s) = shelly $ reduceWithScript t s f
+handleOpts (Reduce f t _ ls' False) = do
+    src <- parseSourceInfoFile t (toTextIgnore f)
+    case descriptionToSynth <$> ls' of
+        a : b : _ -> do
+            putStrLn "Reduce with equivalence check"
+            shelly $ do
+                make dir
+                pop dir $ do
+                    src' <- reduceSynth a b src
+                    writefile (fromText ".." </> dir <.> "v") $ genSource src'
+        a : _ -> do
+            putStrLn "Reduce with synthesis failure"
+            shelly $ do
+                make dir
+                pop dir $ do
+                    src' <- reduceSynthesis a src
+                    writefile (fromText ".." </> dir <.> "v") $ genSource src'
+        _ -> do
+            putStrLn "Not reducing because no synthesiser was specified"
+            return ()
+    where
+        dir = fromText "reduce"
+handleOpts (Reduce f t _ ls' True) = do
+    src <- parseSourceInfoFile t (toTextIgnore f)
+    case descriptionToSynth <$> ls' of
+        a : b : _ -> do
+            putStrLn "Starting equivalence check"
+            res <- shelly . runResultT $ do
+                make dir
+                pop dir $ do
+                    runSynth a src
+                    runSynth b src
+                    runEquiv a b src
+            case res of
+                Pass _         -> putStrLn "Equivalence check passed"
+                Fail EquivFail -> error "Equivalence check failed"
+                Fail _         -> error "Equivalence check errored out"
+            return ()
+        as -> do
+            putStrLn "Synthesis check"
+            _ <- shelly . runResultT $ mapM (flip runSynth src) as
+            return ()
+        where dir = fromText "equiv"
 handleOpts (ConfigOpt c conf r) = do
     config <- if r then getConfig conf >>= randomise else getConfig conf
     maybe (T.putStrLn . encodeConfig $ config) (`encodeConfigFile` config)
-- 
cgit