diff options
author | Yann Herklotz <git@yannherklotz.com> | 2019-10-29 12:06:05 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2019-10-29 12:06:05 +0000 |
commit | 4ee6646b8a78d4c20fe0b89d95f23d382e1c47fc (patch) | |
tree | 9b02e1b92f8abf0baf3dc108ab7f4fb8f33e753a /src/Verismith/Tool/Yosys.hs | |
parent | 1aaff80235237507572e0fb4be86f34cb1829b68 (diff) | |
parent | 01c2ab3f6a58d416528efce3057e2cf2f1604489 (diff) | |
download | verismith-4ee6646b8a78d4c20fe0b89d95f23d382e1c47fc.tar.gz verismith-4ee6646b8a78d4c20fe0b89d95f23d382e1c47fc.zip |
Merge branch 'master' into HEADfeature/nondeterminism
Diffstat (limited to 'src/Verismith/Tool/Yosys.hs')
-rw-r--r-- | src/Verismith/Tool/Yosys.hs | 127 |
1 files changed, 127 insertions, 0 deletions
diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs new file mode 100644 index 0000000..afbffe9 --- /dev/null +++ b/src/Verismith/Tool/Yosys.hs @@ -0,0 +1,127 @@ +{-| +Module : Verismith.Tool.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.Tool.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.Tool.Internal +import Verismith.Tool.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) => FilePath -> a -> b -> SourceInfo -> ResultSh () +runEquiv datadir 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 datadir 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 |