From e7f57642f068650ea362201b239efad1c9a841d9 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 18 Oct 2019 14:29:07 +0100
Subject: Rename Sim to Tool

---
 src/Verismith/Tool/Yosys.hs | 127 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 127 insertions(+)
 create mode 100644 src/Verismith/Tool/Yosys.hs

(limited to 'src/Verismith/Tool/Yosys.hs')

diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs
new file mode 100644
index 0000000..9c0a864
--- /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) => 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
-- 
cgit 


From 01c2ab3f6a58d416528efce3057e2cf2f1604489 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 29 Oct 2019 11:53:43 +0000
Subject: Add data-file installation path

This removes the need to recursively copy the data directory which will also
save on space.
---
 src/Verismith/Tool/Yosys.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src/Verismith/Tool/Yosys.hs')

diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs
index 9c0a864..afbffe9 100644
--- a/src/Verismith/Tool/Yosys.hs
+++ b/src/Verismith/Tool/Yosys.hs
@@ -102,8 +102,8 @@ runEquivYosys yosys sim1 sim2 srcInfo = do
     where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]
 
 runEquiv
-    :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> ResultSh ()
-runEquiv sim1 sim2 srcInfo = do
+    :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> ResultSh ()
+runEquiv datadir sim1 sim2 srcInfo = do
     dir <- liftSh pwd
     liftSh $ do
         writefile "top.v"
@@ -114,7 +114,7 @@ runEquiv sim1 sim2 srcInfo = do
             ^. mainModule
         replaceMods (synthOutput sim1) "_1" srcInfo
         replaceMods (synthOutput sim2) "_2" srcInfo
-        writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo
+        writefile "proof.sby" $ sbyConfig datadir sim1 sim2 srcInfo
     e <- liftSh $ do
         exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
         lastExitCode
-- 
cgit