diff options
Diffstat (limited to 'src/VeriFuzz/Sim')
-rw-r--r-- | src/VeriFuzz/Sim/Internal.hs | 2 | ||||
-rw-r--r-- | src/VeriFuzz/Sim/Yosys.hs | 14 |
2 files changed, 14 insertions, 2 deletions
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 |