aboutsummaryrefslogtreecommitdiffstats
path: root/src/VeriSmith/Sim/Yosys.hs
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2019-09-18 19:06:32 +0200
committerYann Herklotz <git@yannherklotz.com>2019-09-18 19:06:32 +0200
commit8d96fd2a541a2602544ced741552ebd17714c67d (patch)
tree2f53addec05793cf5b3e0274a3e8e9e5f76a7abe /src/VeriSmith/Sim/Yosys.hs
parentd14196cce14d1b4a4a9fba768b9f5238c8626624 (diff)
downloadverismith-8d96fd2a541a2602544ced741552ebd17714c67d.tar.gz
verismith-8d96fd2a541a2602544ced741552ebd17714c67d.zip
Rename main modules
Diffstat (limited to 'src/VeriSmith/Sim/Yosys.hs')
-rw-r--r--src/VeriSmith/Sim/Yosys.hs127
1 files changed, 0 insertions, 127 deletions
diff --git a/src/VeriSmith/Sim/Yosys.hs b/src/VeriSmith/Sim/Yosys.hs
deleted file mode 100644
index 1f583a8..0000000
--- a/src/VeriSmith/Sim/Yosys.hs
+++ /dev/null
@@ -1,127 +0,0 @@
-{-|
-Module : VeriSmith.Sim.Yosys
-Description : Yosys simulator implementation.
-Copyright : (c) 2018-2019, Yann Herklotz
-License : BSD-3
-Maintainer : yann [at] yannherklotz [dot] com
-Stability : experimental
-Portability : POSIX
-
-Yosys simulator implementation.
--}
-
-{-# LANGUAGE QuasiQuotes #-}
-
-module VeriSmith.Sim.Yosys
- ( Yosys(..)
- , defaultYosys
- , runEquiv
- , runEquivYosys
- )
-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 VeriSmith.Result
-import VeriSmith.Sim.Internal
-import VeriSmith.Sim.Template
-import VeriSmith.Verilog.AST
-import VeriSmith.Verilog.CodeGen
-import VeriSmith.Verilog.Mutate
-
-data Yosys = Yosys { yosysBin :: !(Maybe FilePath)
- , yosysDesc :: {-# UNPACK #-} !Text
- , yosysOutput :: {-# UNPACK #-} !FilePath
- }
- deriving (Eq)
-
-instance Tool Yosys where
- toText (Yosys _ t _) = t
-
-instance Show Yosys where
- show t = unpack $ toText t
-
-instance Synthesiser Yosys where
- runSynth = runSynthYosys
- synthOutput = yosysOutput
- setSynthOutput (Yosys a b _) = Yosys a b
-
-instance NFData Yosys where
- rnf = rwhnf
-
-defaultYosys :: Yosys
-defaultYosys = Yosys Nothing "yosys" "syn_yosys.v"
-
-yosysPath :: Yosys -> FilePath
-yosysPath sim = maybe (fromText "yosys") (</> fromText "yosys") $ yosysBin sim
-
-runSynthYosys :: Yosys -> SourceInfo -> ResultSh ()
-runSynthYosys sim (SourceInfo _ src) = do
- dir <- liftSh $ do
- dir' <- pwd
- 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 = toTextIgnore inpf
- out = toTextIgnore $ synthOutput sim
-
-runEquivYosys
- :: (Synthesiser a, Synthesiser b)
- => Yosys
- -> a
- -> b
- -> SourceInfo
- -> ResultSh ()
-runEquivYosys yosys sim1 sim2 srcInfo = do
- liftSh $ do
- writefile "top.v"
- . genSource
- . initMod
- . makeTop 2
- $ srcInfo
- ^. mainModule
- writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
- runSynth sim1 srcInfo
- runSynth sim2 srcInfo
- liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile]
- where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]
-
-runEquiv
- :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> ResultSh ()
-runEquiv sim1 sim2 srcInfo = do
- dir <- liftSh pwd
- liftSh $ do
- writefile "top.v"
- . genSource
- . initMod
- . makeTopAssert
- $ srcInfo
- ^. mainModule
- replaceMods (synthOutput sim1) "_1" srcInfo
- replaceMods (synthOutput sim2) "_2" srcInfo
- writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo
- e <- liftSh $ do
- exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
- lastExitCode
- case e of
- 0 -> ResultT . return $ Pass ()
- 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