diff options
Diffstat (limited to 'src/Verismith/Tool')
| -rw-r--r-- | src/Verismith/Tool/Internal.hs | 2 | ||||
| -rw-r--r-- | src/Verismith/Tool/Template.hs | 7 | ||||
| -rw-r--r-- | src/Verismith/Tool/Yosys.hs | 12 |
3 files changed, 12 insertions, 9 deletions
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 |