Add more reporting to equivalence check

3 files changed, 22 insertions, 8 deletions

diff --git a/src/VeriFuzz/Report.hs b/src/VeriFuzz/Report.hs
index c288652..f2d5ce4 100644
--- a/src/VeriFuzz/Report.hs
+++ b/src/VeriFuzz/Report.hs
@@ -209,11 +209,13 @@ descriptionToSynth s =
     error $ "Could not find implementation for synthesiser '" <> show s <> "'"
 
 status :: Result Failed () -> Html
-status (Pass _)         = "Passed"
-status (Fail EmptyFail) = "Failed"
-status (Fail EquivFail) = "Equivalence failed"
-status (Fail SimFail)   = "Simulation failed"
-status (Fail SynthFail) = "Synthesis failed"
+status (Pass _)            = "Passed"
+status (Fail EmptyFail)    = "Failed"
+status (Fail EquivFail)    = "Equivalence failed"
+status (Fail SimFail)      = "Simulation failed"
+status (Fail SynthFail)    = "Synthesis failed"
+status (Fail EquivError)   = "Equivalence error"
+status (Fail TimeoutError) = "Time out"
 
 synthStatusHtml :: SynthStatus -> Html
 synthStatusHtml (SynthStatus synth res) = H.tr $ do
@@ -230,7 +232,7 @@ resultReport :: Text -> FuzzReport -> Html
 resultReport name (FuzzReport synth _ stat) = H.docTypeHtml $ do
     H.head . H.title $ "Fuzz Report - " <> H.toHtml name
     H.body $ do
-        H.h1 "Fuzz Report"
+        H.h1 $ "Fuzz Report - " <> H.toHtml name
         H.h2 "Synthesis Failure"
         H.table . H.toHtml $
             (H.tr . H.toHtml $
diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
index 091520c..ea90122 100644
--- a/src/VeriFuzz/Sim/Internal.hs
+++ b/src/VeriFuzz/Sim/Internal.hs
@@ -74,8 +74,10 @@ class Tool a => Simulator a where
 
 data Failed = EmptyFail
             | EquivFail
+            | EquivError
             | SimFail
             | SynthFail
+            | TimeoutError
             deriving (Eq, Show)
 
 instance Semigroup Failed where
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs
index 07125df..8552d89 100644
--- a/src/VeriFuzz/Sim/Yosys.hs
+++ b/src/VeriFuzz/Sim/Yosys.hs
@@ -22,11 +22,13 @@ where
 
 import           Control.DeepSeq          (NFData, rnf, rwhnf)
 import           Control.Lens
+import           Control.Monad            (void)
 import           Data.Text                (Text, unpack)
 import           Prelude                  hiding (FilePath)
 import           Shelly
 import           Shelly.Lifted            (liftSh)
 import           Text.Shakespeare.Text    (st)
+import           VeriFuzz.Result
 import           VeriFuzz.Sim.Internal
 import           VeriFuzz.Sim.Template
 import           VeriFuzz.Verilog.AST
@@ -119,5 +121,13 @@ runEquiv sim1 sim2 srcInfo = do
         replaceMods (synthOutput sim2) "_2" srcInfo
         writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo
     liftSh $ logger "Running SymbiYosys"
-    execute_ EquivFail dir "symbiyosys" "sby" ["proof.sby"]
-    liftSh $ logger "SymbiYosys equivalence check passed"
+    e <- liftSh $ do
+        exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
+        lastExitCode
+    case e of
+        0   -> liftSh $ logger "SymbiYosys equivalence check passed"
+        2   -> ResultT . return $ Fail EquivFail
+        124 -> ResultT . return $ Fail TimeoutError
+        _   -> ResultT . return $ Fail EquivError
+    where
+        exe dir name e = void . errExit False . logCommand dir name . timeout e