aboutsummaryrefslogtreecommitdiffstats
path: root/src/Verismith/Tool/Yosys.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Verismith/Tool/Yosys.hs')
-rw-r--r--src/Verismith/Tool/Yosys.hs206
1 files changed, 108 insertions, 98 deletions
diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs
index f68f39f..32c3fee 100644
--- a/src/Verismith/Tool/Yosys.hs
+++ b/src/Verismith/Tool/Yosys.hs
@@ -1,53 +1,53 @@
-{-|
-Module : Verismith.Tool.Yosys
-Description : Yosys simulator implementation.
-Copyright : (c) 2018-2019, Yann Herklotz
-License : GPL-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-Yosys simulator implementation.
--}
-
{-# LANGUAGE QuasiQuotes #-}
+-- |
+-- Module : Verismith.Tool.Yosys
+-- Description : Yosys simulator implementation.
+-- Copyright : (c) 2018-2019, Yann Herklotz
+-- License : GPL-3
+-- Maintainer : yann [at] yannherklotz [dot] com
+-- Stability : experimental
+-- Portability : POSIX
+--
+-- Yosys simulator implementation.
module Verismith.Tool.Yosys
- ( Yosys(..)
- , defaultYosys
- , runEquiv
- , runEquivYosys
- )
+ ( Yosys (..),
+ defaultYosys,
+ runEquiv,
+ runEquivYosys,
+ )
where
-import Control.DeepSeq (NFData, rnf, rwhnf)
-import Control.Lens
-import Control.Monad (void)
-import Data.Either (fromRight)
-import Data.Text (Text, unpack)
-import Prelude hiding (FilePath)
-import Shelly (FilePath, (</>))
-import qualified Shelly as S
-import Shelly.Lifted (liftSh, readfile)
-import Verismith.CounterEg (parseCounterEg)
-import Verismith.Result
-import Verismith.Tool.Internal
-import Verismith.Tool.Template
-import Verismith.Verilog.AST
-import Verismith.Verilog.CodeGen
-import Verismith.Verilog.Mutate
+import Control.DeepSeq (NFData, rnf, rwhnf)
+import Control.Lens
+import Control.Monad (void)
+import Data.Either (fromRight)
+import Data.Text (Text, unpack)
+import Shelly ((</>), FilePath)
+import qualified Shelly as S
+import Shelly.Lifted (liftSh, readfile)
+import Verismith.CounterEg (parseCounterEg)
+import Verismith.Result
+import Verismith.Tool.Internal
+import Verismith.Tool.Template
+import Verismith.Verilog.AST
+import Verismith.Verilog.CodeGen
+import Verismith.Verilog.Mutate
+import Prelude hiding (FilePath)
-data Yosys = Yosys { yosysBin :: !(Maybe FilePath)
- , yosysDesc :: !Text
- , yosysOutput :: !FilePath
- }
- deriving (Eq)
+data Yosys
+ = Yosys
+ { yosysBin :: !(Maybe FilePath),
+ yosysDesc :: !Text,
+ yosysOutput :: !FilePath
+ }
+ deriving (Eq)
instance Tool Yosys where
- toText (Yosys _ t _) = t
+ toText (Yosys _ t _) = t
instance Show Yosys where
- show t = unpack $ toText t
+ show t = unpack $ toText t
instance Synthesiser Yosys where
runSynth = runSynthYosys
@@ -55,7 +55,7 @@ instance Synthesiser Yosys where
setSynthOutput (Yosys a b _) = Yosys a b
instance NFData Yosys where
- rnf = rwhnf
+ rnf = rwhnf
defaultYosys :: Yosys
defaultYosys = Yosys Nothing "yosys" "syn_yosys.v"
@@ -65,68 +65,78 @@ yosysPath sim = maybe (S.fromText "yosys") (</> S.fromText "yosys") $ yosysBin s
runSynthYosys :: Show ann => Yosys -> (SourceInfo ann) -> ResultSh ()
runSynthYosys sim (SourceInfo _ src) = do
- dir <- liftSh $ do
- dir' <- S.pwd
- S.writefile inpf $ genSource src
- return dir'
- execute_
- SynthFail
- dir
- "yosys"
- (yosysPath sim)
- [ "-p"
- , "read_verilog " <> inp <> "; synth; write_verilog -noattr " <> out
- ]
+ dir <- liftSh $ do
+ dir' <- S.pwd
+ S.writefile inpf $ genSource src
+ return dir'
+ execute_
+ SynthFail
+ dir
+ "yosys"
+ (yosysPath sim)
+ [ "-p",
+ "read_verilog " <> inp <> "; synth; write_verilog -noattr " <> out
+ ]
where
inpf = "rtl.v"
- inp = S.toTextIgnore inpf
- out = S.toTextIgnore $ synthOutput sim
+ inp = S.toTextIgnore inpf
+ out = S.toTextIgnore $ synthOutput sim
-runEquivYosys
- :: (Synthesiser a, Synthesiser b, Show ann)
- => Yosys
- -> a
- -> b
- -> (SourceInfo ann)
- -> ResultSh ()
+runEquivYosys ::
+ (Synthesiser a, Synthesiser b, Show ann) =>
+ Yosys ->
+ a ->
+ b ->
+ (SourceInfo ann) ->
+ ResultSh ()
runEquivYosys yosys sim1 sim2 srcInfo = do
- liftSh $ do
- S.writefile "top.v"
- . genSource
- . initMod
- . makeTop 2
- $ srcInfo
- ^. mainModule
- S.writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
- runSynth sim1 srcInfo
- runSynth sim2 srcInfo
- liftSh $ S.run_ (yosysPath yosys) [S.toTextIgnore checkFile]
- where checkFile = S.fromText $ "test." <> toText sim1 <> "." <> toText sim2 <> ".ys"
+ liftSh $ do
+ S.writefile "top.v"
+ . genSource
+ . initMod
+ . makeTop 2
+ $ srcInfo
+ ^. mainModule
+ S.writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
+ runSynth sim1 srcInfo
+ runSynth sim2 srcInfo
+ liftSh $ S.run_ (yosysPath yosys) [S.toTextIgnore checkFile]
+ where
+ checkFile = S.fromText $ "test." <> toText sim1 <> "." <> toText sim2 <> ".ys"
-runEquiv :: (Synthesiser a, Synthesiser b, Show ann)
- => Maybe Text -> FilePath -> a -> b -> (SourceInfo ann) -> ResultSh ()
+runEquiv ::
+ (Synthesiser a, Synthesiser b, Show ann) =>
+ Maybe Text ->
+ FilePath ->
+ a ->
+ b ->
+ (SourceInfo ann) ->
+ ResultSh ()
runEquiv mt datadir sim1 sim2 srcInfo = do
- dir <- liftSh S.pwd
- liftSh $ do
- S.writefile "top.v"
- . genSource
- . initMod
- . makeTopAssert
- $ srcInfo
- ^. mainModule
- replaceMods (synthOutput sim1) "_1" srcInfo
- replaceMods (synthOutput sim2) "_2" 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 -> 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
+ dir <- liftSh S.pwd
+ liftSh $ do
+ S.writefile "top.v"
+ . genSource
+ . initMod
+ . makeTopAssert
+ $ srcInfo
+ ^. mainModule
+ replaceMods (synthOutput sim1) "_1" srcInfo
+ replaceMods (synthOutput sim2) "_2" 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 -> 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
exe dir name e = void . S.errExit False . logCommand dir name . timeout e
generated by cgit (git 2.34.1) at 2024-05-10 02:56:59 +0000