Do not run counter example if no rerunner is specified

7 files changed, 40 insertions, 26 deletions

diff --git a/src/Verismith.hs b/src/Verismith.hs
index c4616aa..ac1f1c9 100644
--- a/src/Verismith.hs
+++ b/src/Verismith.hs
@@ -144,13 +144,13 @@ randomise config@(Config a _ c d e) = do
     ce = config ^. configProbability . probExpr
 
 handleOpts :: Opts -> IO ()
-handleOpts (Fuzz o configF f k n nosim noequiv noreduction file top cc) = do
+handleOpts (Fuzz o configF f k n nosim noequiv noreduction file top cc checker) = do
     config <- getConfig configF
     gen <- getGenerator config top file
     datadir <- getDataDir
     _      <- runFuzz
         (FuzzOpts (Just $ fromText o)
-         f k n nosim noequiv noreduction config (toFP datadir) cc)
+         f k n nosim noequiv noreduction config (toFP datadir) cc checker)
         defaultYosys
         (fuzzMultiple gen)
     return ()
@@ -183,7 +183,7 @@ handleOpts (Reduce f t _ ls' False) = do
             shelly $ do
                 make dir
                 pop dir $ do
-                    src' <- reduceSynth (toFP datadir) a b src
+                    src' <- reduceSynth Nothing (toFP datadir) a b src
                     writefile (fromText ".." </> dir <.> "v") $ genSource src'
         a : _ -> do
             putStrLn "Reduce with synthesis failure"
@@ -207,7 +207,7 @@ handleOpts (Reduce f t _ ls' True) = do
                 pop dir $ do
                     runSynth a src
                     runSynth b src
-                    runEquiv (toFP datadir) a b src
+                    runEquiv Nothing (toFP datadir) a b src
             case res of
                 Pass _             -> putStrLn "Equivalence check passed"
                 Fail (EquivFail _) -> putStrLn "Equivalence check failed"
@@ -288,7 +288,7 @@ checkEquivalence src dir = shellyFailDir $ do
     setenv "VERISMITH_ROOT" curr
     cd (fromText dir)
     catch_sh
-        ((runResultT $ runEquiv (toFP datadir) defaultYosys defaultVivado src) >> return True)
+        ((runResultT $ runEquiv Nothing (toFP datadir) defaultYosys defaultVivado src) >> return True)
         ((\_ -> return False) :: RunFailed -> Sh Bool)
 
 -- | Run a fuzz run and check if all of the simulators passed by checking if the
@@ -314,7 +314,7 @@ runEquivalence seed gm t d k i = do
         _ <-
             catch_sh
                     (  runResultT
-                    $  runEquiv (toFP datadir) defaultYosys defaultVivado srcInfo
+                    $  runEquiv Nothing (toFP datadir) defaultYosys defaultVivado srcInfo
                     >> liftSh (logger "Test OK")
                     )
                 $ onFailure n
diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs
index f111118..ff55011 100644
--- a/src/Verismith/Fuzz.hs
+++ b/src/Verismith/Fuzz.hs
@@ -75,6 +75,7 @@ data FuzzOpts = FuzzOpts { _fuzzOptsOutput      :: !(Maybe FilePath)
                          , _fuzzOptsConfig      :: {-# UNPACK #-} !Config
                          , _fuzzDataDir         :: {-# UNPACK #-} !FilePath
                          , _fuzzOptsCrossCheck  :: !Bool
+                         , _fuzzOptsChecker     :: !(Maybe Text)
                          }
               deriving (Show, Eq)
 
@@ -91,6 +92,7 @@ defaultFuzzOpts = FuzzOpts { _fuzzOptsOutput      = Nothing
                            , _fuzzOptsConfig      = defaultConfig
                            , _fuzzDataDir = fromText "."
                            , _fuzzOptsCrossCheck = False
+                           , _fuzzOptsChecker = Nothing
                            }
 
 data FuzzEnv = FuzzEnv { _getSynthesisers :: ![SynthTool]
@@ -269,17 +271,18 @@ equivalence :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m ()
 equivalence src = do
     doCrossCheck <- fmap _fuzzOptsCrossCheck askOpts
     datadir <- fmap _fuzzDataDir askOpts
+    checker <- fmap _fuzzOptsChecker askOpts
     synth <- passedSynthesis
     let synthComb =
             if doCrossCheck
             then nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth
             else nubBy tupEq . filter (uncurry (/=)) $ (,) defaultIdentitySynth <$> synth
-    resTimes <- liftSh $ mapM (uncurry (equiv datadir)) synthComb
+    resTimes <- liftSh $ mapM (uncurry (equiv checker datadir)) synthComb
     fuzzSynthResults .= toSynthResult synthComb resTimes
     liftSh $ inspect resTimes
   where
     tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a')
-    equiv datadir a b =
+    equiv checker datadir a b =
         toolRun ("equivalence check for " <> toText a <> " and " <> toText b)
             . runResultT
             $ do make dir
@@ -294,7 +297,7 @@ equivalence src = do
                               </> synthOutput b
                             ) $ synthOutput b
                          writefile "rtl.v" $ genSource src
-                     runEquiv datadir a b src
+                     runEquiv checker datadir a b src
         where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b
 
 simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m ()
@@ -321,7 +324,8 @@ simulation src = do
                 writefile "rtl.v" $ genSource src
             runSimIc datadir defaultIcarus a src b i
         where dir = fromText $ "simulation_" <> toText a
-    simCounterEg datadir (a, b) = toolRun ("counter-example simulation for " <> toText a) . runResultT $ do
+    simCounterEg datadir (a, Nothing) = toolRun ("counter-example simulation for " <> toText a) . return $ Fail EmptyFail
+    simCounterEg datadir (a, Just b) = toolRun ("counter-example simulation for " <> toText a) . runResultT $ do
         make dir
         pop dir $ do
             liftSh $ do
@@ -351,7 +355,7 @@ failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get
     withIdentity (SynthResult _ (IdentitySynth _) (Fail (EquivFail _)) _) = True
     withIdentity _                                                    = False
 
-failEquivWithIdentityCE :: (MonadSh m) => Fuzz m [(SynthTool, CounterEg)]
+failEquivWithIdentityCE :: (MonadSh m) => Fuzz m [(SynthTool, Maybe CounterEg)]
 failEquivWithIdentityCE = catMaybes . fmap withIdentity . _fuzzSynthResults <$> get
   where
     withIdentity (SynthResult (IdentitySynth _) s (Fail (EquivFail c)) _) = Just (s, c)
@@ -374,16 +378,17 @@ passEquiv = filter withIdentity . _fuzzSynthResults <$> get
 reduction :: (MonadSh m) => SourceInfo -> Fuzz m ()
 reduction src = do
     datadir <- fmap _fuzzDataDir askOpts
+    checker <- fmap _fuzzOptsChecker askOpts
     fails      <- failEquivWithIdentity
     synthFails <- failedSynthesis
     simFails <- failedSimulations
-    _          <- liftSh $ mapM (red datadir) fails
+    _          <- liftSh $ mapM (red checker datadir) fails
     _          <- liftSh $ mapM redSynth synthFails
     _ <- liftSh $ mapM (redSim datadir) simFails
     return ()
   where
-    red datadir (SynthResult a b _ _) = do
-        r <- reduceSynth datadir a b src
+    red checker datadir (SynthResult a b _ _) = do
+        r <- reduceSynth checker datadir a b src
         writefile (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") $ genSource r
     redSynth a = do
         r <- reduceSynthesis a src
diff --git a/src/Verismith/OptParser.hs b/src/Verismith/OptParser.hs
index 37d00fd..27ff4b4 100644
--- a/src/Verismith/OptParser.hs
+++ b/src/Verismith/OptParser.hs
@@ -35,6 +35,7 @@ data Opts = Fuzz { fuzzOutput          :: {-# UNPACK #-} !Text
                  , fuzzExistingFile    :: !(Maybe FilePath)
                  , fuzzExistingFileTop :: !Text
                  , fuzzCrossCheck      :: !Bool
+                 , fuzzChecker         :: !(Maybe Text)
                  }
           | Generate { generateFilename   :: !(Maybe FilePath)
                      , generateConfigFile :: !(Maybe FilePath)
@@ -131,6 +132,10 @@ fuzzOpts =
                 <> Opt.value "top")
         <*> (Opt.switch $ Opt.long "crosscheck" <> Opt.help
                 "Do not only compare against the original design, but also against other netlists.")
+        <*> (Opt.optional . textOption $
+                Opt.long "checker"
+                <> Opt.metavar "CHECKER"
+                <> Opt.help "Define the checker to use.")
 
 genOpts :: Parser Opts
 genOpts =
diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs
index 022dd1d..8f7bd7b 100644
--- a/src/Verismith/Reduce.hs
+++ b/src/Verismith/Reduce.hs
@@ -607,18 +607,19 @@ reduceWithScript top script file = do
 -- | Reduce a 'SourceInfo' using two 'Synthesiser' that are passed to it.
 reduceSynth
     :: (Synthesiser a, Synthesiser b, MonadSh m)
-    => Shelly.FilePath
+    => Maybe Text
+    -> Shelly.FilePath
     -> a
     -> b
     -> SourceInfo
     -> m SourceInfo
-reduceSynth datadir a b = reduce (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") synth
+reduceSynth mt datadir a b = reduce (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") synth
   where
     synth src' = liftSh $ do
         r <- runResultT $ do
             runSynth a src'
             runSynth b src'
-            runEquiv datadir a b src'
+            runEquiv mt datadir a b src'
         return $ case r of
             Fail (EquivFail _) -> True
             _                  -> False
diff --git a/src/Verismith/Tool/Internal.hs b/src/Verismith/Tool/Internal.hs
index b97c2f1..dfa3f46 100644
--- a/src/Verismith/Tool/Internal.hs
+++ b/src/Verismith/Tool/Internal.hs
@@ -75,7 +75,7 @@ class Tool a => Simulator a where
                  -> ResultSh ByteString
 
 data Failed = EmptyFail
-            | EquivFail CounterEg
+            | EquivFail (Maybe CounterEg)
             | EquivError
             | SimFail ByteString
             | SynthFail
diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs
index 0b63e91..ffa7240 100644
--- a/src/Verismith/Tool/Template.hs
+++ b/src/Verismith/Tool/Template.hs
@@ -26,6 +26,7 @@ module Verismith.Tool.Template
 where
 
 import           Control.Lens              ((^..))
+import           Data.Maybe                (fromMaybe)
 import           Data.Text                 (Text)
 import qualified Data.Text                 as T
 import           Prelude                   hiding (FilePath)
@@ -136,11 +137,11 @@ synth_design -part xc7k70t -top #{top}
 write_verilog -force #{outf}
 |]
 
-sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> Text
-sbyConfig datadir sim1 sim2 (SourceInfo top _) = [st|[options]
+sbyConfig :: (Synthesiser a, Synthesiser b) => Maybe Text -> FilePath -> a -> b -> SourceInfo -> Text
+sbyConfig mt datadir sim1 sim2 (SourceInfo top _) = [st|[options]
 multiclock on
 mode prove
-aigsmt none
+aigsmt #{fromMaybe "none" mt}
 
 [engines]
 abc pdr
diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs
index 67f8536..3507ac2 100644
--- a/src/Verismith/Tool/Yosys.hs
+++ b/src/Verismith/Tool/Yosys.hs
@@ -105,8 +105,8 @@ runEquivYosys yosys sim1 sim2 srcInfo = do
     where checkFile = S.fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]
 
 runEquiv
-    :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> ResultSh ()
-runEquiv datadir sim1 sim2 srcInfo = do
+    :: (Synthesiser a, Synthesiser b) => Maybe Text -> FilePath -> a -> b -> SourceInfo -> ResultSh ()
+runEquiv mt datadir sim1 sim2 srcInfo = do
     dir <- liftSh S.pwd
     liftSh $ do
         S.writefile "top.v"
@@ -117,14 +117,16 @@ runEquiv datadir sim1 sim2 srcInfo = do
             ^. mainModule
         replaceMods (synthOutput sim1) "_1" srcInfo
         replaceMods (synthOutput sim2) "_2" srcInfo
-        S.writefile "proof.sby" $ sbyConfig datadir sim1 sim2 srcInfo
+        S.writefile "proof.sby" $ sbyConfig mt datadir sim1 sim2 srcInfo
     e <- liftSh $ do
         exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
         S.lastExitCode
     case e of
         0   -> ResultT . return $ Pass ()
-        2   -> ResultT $ Fail . EquivFail . fromRight mempty
-                       . parseCounterEg <$> readfile "proof/engine_0/trace.smtc"
+        2   -> case mt of
+                   Nothing -> ResultT . return . Fail $ EquivFail Nothing
+                   Just _ -> ResultT $ Fail . EquivFail . Just . fromRight mempty
+                             . parseCounterEg <$> readfile "proof/engine_0/trace.smtc"
         124 -> ResultT . return $ Fail TimeoutError
         _   -> ResultT . return $ Fail EquivError
   where