8 files changed, 947 insertions, 0 deletions

diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs
new file mode 100644
index 0000000..b783033
--- /dev/null
+++ b/src/Verismith/Tool/Icarus.hs
@@ -0,0 +1,188 @@
+{-|
+Module      : Verismith.Tool.Icarus
+Description : Icarus verilog module.
+Copyright   : (c) 2018-2019, Yann Herklotz
+License     : BSD-3
+Maintainer  : yann [at] yannherklotz [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Icarus verilog module.
+-}
+
+module Verismith.Tool.Icarus
+    ( Icarus(..)
+    , defaultIcarus
+    , runSimIc
+    )
+where
+
+import           Control.DeepSeq            (NFData, rnf, rwhnf)
+import           Control.Lens
+import           Control.Monad              (void)
+import           Crypto.Hash                (Digest, hash)
+import           Crypto.Hash.Algorithms     (SHA256)
+import           Data.Binary                (encode)
+import           Data.Bits
+import qualified Data.ByteArray             as BA (convert)
+import           Data.ByteString            (ByteString)
+import qualified Data.ByteString            as B
+import           Data.ByteString.Lazy       (toStrict)
+import qualified Data.ByteString.Lazy       as L (ByteString)
+import           Data.Char                  (digitToInt)
+import           Data.Foldable              (fold)
+import           Data.List                  (transpose)
+import           Data.Maybe                 (listToMaybe)
+import           Data.Text                  (Text)
+import qualified Data.Text                  as T
+import           Numeric                    (readInt)
+import           Prelude                    hiding (FilePath)
+import           Shelly
+import           Shelly.Lifted              (liftSh)
+import           Verismith.Tool.Internal
+import           Verismith.Tool.Template
+import           Verismith.Verilog.AST
+import           Verismith.Verilog.BitVec
+import           Verismith.Verilog.CodeGen
+import           Verismith.Verilog.Internal
+import           Verismith.Verilog.Mutate
+
+data Icarus = Icarus { icarusPath :: FilePath
+                     , vvpPath    :: FilePath
+                     }
+              deriving (Eq)
+
+instance Show Icarus where
+    show _ = "iverilog"
+
+instance Tool Icarus where
+  toText _ = "iverilog"
+
+instance Simulator Icarus where
+  runSim = runSimIcarus
+  runSimWithFile = runSimIcarusWithFile
+
+instance NFData Icarus where
+    rnf = rwhnf
+
+defaultIcarus :: Icarus
+defaultIcarus = Icarus "iverilog" "vvp"
+
+addDisplay :: [Statement] -> [Statement]
+addDisplay s = concat $ transpose
+    [ s
+    , replicate l $ TimeCtrl 1 Nothing
+    , replicate l . SysTaskEnable $ Task "display" ["%b", Id "y"]
+    ]
+    where l = length s
+
+assignFunc :: [Port] -> ByteString -> Statement
+assignFunc inp bs =
+    NonBlockAssign
+        . Assign conc Nothing
+        . Number
+        . BitVec (B.length bs * 8)
+        $ bsToI bs
+    where conc = RegConcat (portToExpr <$> inp)
+
+convert :: Text -> ByteString
+convert =
+    toStrict
+        . (encode :: Integer -> L.ByteString)
+        . maybe 0 fst
+        . listToMaybe
+        . readInt 2 (`elem` ("01" :: String)) digitToInt
+        . T.unpack
+
+mask :: Text -> Text
+mask = T.replace "x" "0"
+
+callback :: ByteString -> Text -> ByteString
+callback b t = b <> convert (mask t)
+
+runSimIcarus :: Icarus -> SourceInfo -> [ByteString] -> ResultSh ByteString
+runSimIcarus sim rinfo bss = do
+    let tb = ModDecl
+            "main"
+            []
+            []
+            [ Initial
+              $  fold (addDisplay $ assignFunc (_modInPorts m) <$> bss)
+              <> (SysTaskEnable $ Task "finish" [])
+            ]
+            []
+    let newtb     = instantiateMod m tb
+    let modWithTb = Verilog [newtb, m]
+    liftSh . writefile "main.v" $ genSource modWithTb
+    annotate SimFail $ runSimWithFile sim "main.v" bss
+    where m = rinfo ^. mainModule
+
+runSimIcarusWithFile
+    :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString
+runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do
+    dir <- pwd
+    logCommand_ dir "icarus"
+        $ run (icarusPath sim) ["-o", "main", toTextIgnore f]
+    B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logCommand
+        dir
+        "vvp"
+        (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"])
+
+fromBytes :: ByteString -> Integer
+fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b
+
+runSimIc
+    :: (Synthesiser b)
+    => Icarus
+    -> b
+    -> SourceInfo
+    -> [ByteString]
+    -> ResultSh ByteString
+runSimIc sim1 synth1 srcInfo bss = do
+    dir <- liftSh pwd
+    let top      = srcInfo ^. mainModule
+    let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts)))
+    let
+        tb = instantiateMod top $ ModDecl
+            "testbench"
+            []
+            []
+            [ Initial
+            $  fold
+                   [ BlockAssign (Assign "clk" Nothing 0)
+                   , BlockAssign (Assign inConcat Nothing 0)
+                   ]
+            <> fold
+                   (   (\r -> TimeCtrl
+                           10
+                           (Just $ BlockAssign (Assign inConcat Nothing r))
+                       )
+                   .   fromInteger
+                   .   fromBytes
+                   <$> bss
+                   )
+            <> (SysTaskEnable $ Task "finish" [])
+            , Always . TimeCtrl 5 . Just $ BlockAssign
+                (Assign "clk" Nothing (UnOp UnNot (Id "clk")))
+            , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task
+                "strobe"
+                ["%b", Id "y"]
+            ]
+            []
+
+    liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1
+    liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"]
+    liftSh
+        $   B.take 8
+        .   BA.convert
+        .   (hash :: ByteString -> Digest SHA256)
+        <$> logCommand
+                dir
+                "vvp"
+                (runFoldLines (mempty :: ByteString)
+                              callback
+                              (vvpPath sim1)
+                              ["main"]
+                )
+  where
+    exe dir name e = void . errExit False . logCommand dir name . timeout e
diff --git a/src/Verismith/Tool/Identity.hs b/src/Verismith/Tool/Identity.hs
new file mode 100644
index 0000000..93b05d5
--- /dev/null
+++ b/src/Verismith/Tool/Identity.hs
@@ -0,0 +1,51 @@
+{-|
+Module      : Verismith.Tool.Identity
+Description : The identity simulator and synthesiser.
+Copyright   : (c) 2019, Yann Herklotz Grave
+License     : GPL-3
+Maintainer  : yann [at] yannherklotz [dot] com
+Stability   : experimental
+Portability : POSIX
+
+The identity simulator and synthesiser.
+-}
+
+module Verismith.Tool.Identity
+    ( Identity(..)
+    , defaultIdentity
+    )
+where
+
+import           Control.DeepSeq           (NFData, rnf, rwhnf)
+import           Data.Text                 (Text, unpack)
+import           Prelude                   hiding (FilePath)
+import           Shelly                    (FilePath)
+import           Shelly.Lifted             (writefile)
+import           Verismith.Tool.Internal
+import           Verismith.Verilog.AST
+import           Verismith.Verilog.CodeGen
+
+data Identity = Identity { identityDesc   :: {-# UNPACK #-} !Text
+                         , identityOutput :: {-# UNPACK #-} !FilePath
+                         }
+              deriving (Eq)
+
+instance Tool Identity where
+    toText (Identity d _) = d
+
+instance Show Identity where
+    show t = unpack $ toText t
+
+instance Synthesiser Identity where
+    runSynth = runSynthIdentity
+    synthOutput = identityOutput
+    setSynthOutput (Identity a _) = Identity a
+
+instance NFData Identity where
+    rnf = rwhnf
+
+runSynthIdentity :: Identity -> SourceInfo -> ResultSh ()
+runSynthIdentity (Identity _ out) = writefile out . genSource
+
+defaultIdentity :: Identity
+defaultIdentity = Identity "identity" "syn_identity.v"
diff --git a/src/Verismith/Tool/Internal.hs b/src/Verismith/Tool/Internal.hs
new file mode 100644
index 0000000..c2e3a0c
--- /dev/null
+++ b/src/Verismith/Tool/Internal.hs
@@ -0,0 +1,215 @@
+{-|
+Module      : Verismith.Tool.Internal
+Description : Class of the simulator.
+Copyright   : (c) 2018-2019, Yann Herklotz
+License     : BSD-3
+Maintainer  : yann [at] yannherklotz [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Class of the simulator and the synthesize tool.
+-}
+
+{-# LANGUAGE DeriveFunctor #-}
+
+module Verismith.Tool.Internal
+    ( ResultSh
+    , resultSh
+    , Tool(..)
+    , Simulator(..)
+    , Synthesiser(..)
+    , Failed(..)
+    , renameSource
+    , checkPresent
+    , checkPresentModules
+    , replace
+    , replaceMods
+    , rootPath
+    , timeout
+    , timeout_
+    , bsToI
+    , noPrint
+    , logger
+    , logCommand
+    , logCommand_
+    , execute
+    , execute_
+    , (<?>)
+    , annotate
+    )
+where
+
+import           Control.Lens
+import           Control.Monad         (forM, void)
+import           Control.Monad.Catch   (throwM)
+import           Data.Bits             (shiftL)
+import           Data.ByteString       (ByteString)
+import qualified Data.ByteString       as B
+import           Data.Maybe            (catMaybes)
+import           Data.Text             (Text)
+import qualified Data.Text             as T
+import           Data.Time.Format      (defaultTimeLocale, formatTime)
+import           Data.Time.LocalTime   (getZonedTime)
+import           Prelude               hiding (FilePath)
+import           Shelly
+import           Shelly.Lifted         (MonadSh, liftSh)
+import           System.FilePath.Posix (takeBaseName)
+import           Verismith.Internal
+import           Verismith.Result
+import           Verismith.Verilog.AST
+
+-- | Tool class.
+class Tool a where
+  toText :: a -> Text
+
+-- | Simulation type class.
+class Tool a => Simulator a where
+  runSim :: a             -- ^ Simulator instance
+         -> SourceInfo       -- ^ Run information
+         -> [ByteString]  -- ^ Inputs to simulate
+         -> ResultSh ByteString -- ^ Returns the value of the hash at the output of the testbench.
+  runSimWithFile :: a
+                 -> FilePath
+                 -> [ByteString]
+                 -> ResultSh ByteString
+
+data Failed = EmptyFail
+            | EquivFail
+            | EquivError
+            | SimFail
+            | SynthFail
+            | TimeoutError
+            deriving (Eq, Show)
+
+instance Semigroup Failed where
+    EmptyFail <> a = a
+    b <> _ = b
+
+instance Monoid Failed where
+    mempty = EmptyFail
+
+-- | Synthesiser type class.
+class Tool a => Synthesiser a where
+    runSynth :: a        -- ^ Synthesiser tool instance
+             -> SourceInfo  -- ^ Run information
+             -> ResultSh ()    -- ^ does not return any values
+    synthOutput :: a -> FilePath
+    setSynthOutput :: a -> FilePath -> a
+
+renameSource :: (Synthesiser a) => a -> SourceInfo -> SourceInfo
+renameSource a src =
+    src & infoSrc . _Wrapped . traverse . modId . _Wrapped %~ (<> toText a)
+
+-- | Type synonym for a 'ResultT' that will be used throughout 'Verismith'. This
+-- has instances for 'MonadSh' and 'MonadIO' if the 'Monad' it is parametrised
+-- with also has those instances.
+type ResultSh = ResultT Failed Sh
+
+resultSh :: ResultSh a -> Sh a
+resultSh s = do
+    result <- runResultT s
+    case result of
+        Fail e  -> throwM . RunFailed "" [] 1 $ showT e
+        Pass s' -> return s'
+
+checkPresent :: FilePath -> Text -> Sh (Maybe Text)
+checkPresent fp t = do
+    errExit False $ run_ "grep" [t, toTextIgnore fp]
+    i <- lastExitCode
+    if i == 0 then return $ Just t else return Nothing
+
+-- | Checks what modules are present in the synthesised output, as some modules
+-- may have been inlined. This could be improved if the parser worked properly.
+checkPresentModules :: FilePath -> SourceInfo -> Sh [Text]
+checkPresentModules fp (SourceInfo _ src) = do
+    vals <- forM (src ^.. _Wrapped . traverse . modId . _Wrapped)
+        $ checkPresent fp
+    return $ catMaybes vals
+
+-- | Uses sed to replace a string in a text file.
+replace :: FilePath -> Text -> Text -> Sh ()
+replace fp t1 t2 = do
+    errExit False . noPrint $ run_
+        "sed"
+        ["-i", "s/" <> t1 <> "/" <> t2 <> "/g", toTextIgnore fp]
+
+-- | This is used because rename only renames the definitions of modules of
+-- course, so instead this just searches and replaces all the module names. This
+-- should find all the instantiations and definitions. This could again be made
+-- much simpler if the parser works.
+replaceMods :: FilePath -> Text -> SourceInfo -> Sh ()
+replaceMods fp t (SourceInfo _ src) =
+    void
+        . forM (src ^.. _Wrapped . traverse . modId . _Wrapped)
+        $ (\a -> replace fp a (a <> t))
+
+rootPath :: Sh FilePath
+rootPath = do
+    current <- pwd
+    maybe current fromText <$> get_env "VERISMITH_ROOT"
+
+timeout :: FilePath -> [Text] -> Sh Text
+timeout = command1 "timeout" ["300"] . toTextIgnore
+{-# INLINE timeout #-}
+
+timeout_ :: FilePath -> [Text] -> Sh ()
+timeout_ = command1_ "timeout" ["300"] . toTextIgnore
+{-# INLINE timeout_ #-}
+
+-- | Helper function to convert bytestrings to integers
+bsToI :: ByteString -> Integer
+bsToI = B.foldl' (\i b -> (i `shiftL` 8) + fromIntegral b) 0
+{-# INLINE bsToI #-}
+
+noPrint :: Sh a -> Sh a
+noPrint = print_stdout False . print_stderr False
+{-# INLINE noPrint #-}
+
+logger :: Text -> Sh ()
+logger t = do
+    fn          <- pwd
+    currentTime <- liftIO getZonedTime
+    echo
+        $  "Verismith "
+        <> T.pack (formatTime defaultTimeLocale "%H:%M:%S " currentTime)
+        <> bname fn
+        <> " - "
+        <> t
+    where bname = T.pack . takeBaseName . T.unpack . toTextIgnore
+
+logCommand :: FilePath -> Text -> Sh a -> Sh a
+logCommand fp name = log_stderr_with (l "_stderr.log")
+    . log_stdout_with (l ".log")
+  where
+    l s t = appendFile (file s) (T.unpack t) >> appendFile (file s) "\n"
+    file s = T.unpack (toTextIgnore $ fp </> fromText name) <> s
+
+logCommand_ :: FilePath -> Text -> Sh a -> Sh ()
+logCommand_ fp name = void . logCommand fp name
+
+execute
+    :: (MonadSh m, Monad m)
+    => Failed
+    -> FilePath
+    -> Text
+    -> FilePath
+    -> [Text]
+    -> ResultT Failed m Text
+execute f dir name e cs = do
+    (res, exitCode) <- liftSh $ do
+        res <- errExit False . logCommand dir name $ timeout e cs
+        (,) res <$> lastExitCode
+    case exitCode of
+        0   -> ResultT . return $ Pass res
+        124 -> ResultT . return $ Fail TimeoutError
+        _   -> ResultT . return $ Fail f
+
+execute_
+    :: (MonadSh m, Monad m)
+    => Failed
+    -> FilePath
+    -> Text
+    -> FilePath
+    -> [Text]
+    -> ResultT Failed m ()
+execute_ a b c d = void . execute a b c d
diff --git a/src/Verismith/Tool/Quartus.hs b/src/Verismith/Tool/Quartus.hs
new file mode 100644
index 0000000..109d46c
--- /dev/null
+++ b/src/Verismith/Tool/Quartus.hs
@@ -0,0 +1,77 @@
+{-|
+Module      : Verismith.Tool.Quartus
+Description : Quartus synthesiser implementation.
+Copyright   : (c) 2019, Yann Herklotz Grave
+License     : GPL-3
+Maintainer  : yann [at] yannherklotz [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Quartus synthesiser implementation.
+-}
+
+module Verismith.Tool.Quartus
+    ( Quartus(..)
+    , defaultQuartus
+    )
+where
+
+import           Control.DeepSeq           (NFData, rnf, rwhnf)
+import           Data.Text                 (Text, unpack)
+import           Prelude                   hiding (FilePath)
+import           Shelly
+import           Shelly.Lifted             (liftSh)
+import           Verismith.Tool.Internal
+import           Verismith.Verilog.AST
+import           Verismith.Verilog.CodeGen
+
+data Quartus = Quartus { quartusBin    :: !(Maybe FilePath)
+                       , quartusDesc   :: {-# UNPACK #-} !Text
+                       , quartusOutput :: {-# UNPACK #-} !FilePath
+                       }
+                deriving (Eq)
+
+instance Tool Quartus where
+    toText (Quartus _ t _) = t
+
+instance Show Quartus where
+    show t = unpack $ toText t
+
+instance Synthesiser Quartus where
+    runSynth = runSynthQuartus
+    synthOutput = quartusOutput
+    setSynthOutput (Quartus a b _) = Quartus a b
+
+instance NFData Quartus where
+    rnf = rwhnf
+
+defaultQuartus :: Quartus
+defaultQuartus = Quartus Nothing "quartus" "syn_quartus.v"
+
+runSynthQuartus :: Quartus -> SourceInfo -> ResultSh ()
+runSynthQuartus sim (SourceInfo top src) = do
+    dir <- liftSh pwd
+    let ex = execute_ SynthFail dir "quartus"
+    liftSh . writefile inpf $ genSource src
+    liftSh . noPrint $ run_
+        "sed"
+        [ "-i"
+        , "s/^module/(* multstyle = \"logic\" *) module/;"
+        , toTextIgnore inpf
+        ]
+    ex (exec "quartus_map")
+       [top, "--source=" <> toTextIgnore inpf, "--family=Cyclone V"]
+    ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"]
+    ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"]
+    liftSh $ do
+        cp (fromText "simulation/vcs" </> fromText top <.> "vo")
+            $ synthOutput sim
+        run_
+            "sed"
+            [ "-ri"
+            , "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;"
+            , toTextIgnore $ synthOutput sim
+            ]
+  where
+    inpf = "rtl.v"
+    exec s = maybe (fromText s) (</> fromText s) $ quartusBin sim
diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs
new file mode 100644
index 0000000..c0cbfe1
--- /dev/null
+++ b/src/Verismith/Tool/Template.hs
@@ -0,0 +1,133 @@
+{-|
+Module      : Verismith.Tool.Template
+Description : Template file for different configuration files
+Copyright   : (c) 2019, Yann Herklotz
+License     : GPL-3
+Maintainer  : yann [at] yannherklotz [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Template file for different configuration files.
+-}
+
+{-# LANGUAGE QuasiQuotes #-}
+
+module Verismith.Tool.Template
+    ( yosysSatConfig
+    , yosysSimConfig
+    , xstSynthConfig
+    , vivadoSynthConfig
+    , sbyConfig
+    , icarusTestbench
+    )
+where
+
+import           Control.Lens              ((^..))
+import           Data.Text                 (Text)
+import qualified Data.Text                 as T
+import           Prelude                   hiding (FilePath)
+import           Shelly
+import           Text.Shakespeare.Text     (st)
+import           Verismith.Tool.Internal
+import           Verismith.Verilog.AST
+import           Verismith.Verilog.CodeGen
+
+rename :: Text -> [Text] -> Text
+rename end entries =
+    T.intercalate "\n"
+        $   flip mappend end
+        .   mappend "rename "
+        .   doubleName
+        <$> entries
+{-# INLINE rename #-}
+
+doubleName :: Text -> Text
+doubleName n = n <> " " <> n
+{-# INLINE doubleName #-}
+
+outputText :: Synthesiser a => a -> Text
+outputText = toTextIgnore . synthOutput
+
+-- brittany-disable-next-binding
+yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text
+yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog #{outputText sim1}
+#{rename "_1" mis}
+read_verilog syn_#{outputText sim2}.v
+#{rename "_2" mis}
+read_verilog #{top}.v
+proc; opt_clean
+flatten #{top}
+sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{top}
+|]
+  where
+    mis = src ^.. getSourceId
+
+-- brittany-disable-next-binding
+yosysSimConfig :: Text
+yosysSimConfig = [st|read_verilog rtl.v; proc;;
+rename mod mod_rtl
+|]
+
+-- brittany-disable-next-binding
+xstSynthConfig :: Text -> Text
+xstSynthConfig top = [st|run
+-ifn #{top}.prj -ofn #{top} -p artix7 -top #{top}
+-iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO
+-fsm_extract YES -fsm_encoding Auto
+-change_error_to_warning "HDLCompiler:226 HDLCompiler:1832"
+|]
+
+-- brittany-disable-next-binding
+vivadoSynthConfig :: Text -> Text -> Text
+vivadoSynthConfig top outf = [st|
+# CRITICAL WARNING: [Synth 8-5821] Potential divide by zero
+set_msg_config -id {Synth 8-5821} -new_severity {WARNING}
+
+read_verilog rtl.v
+synth_design -part xc7k70t -top #{top}
+write_verilog -force #{outf}
+|]
+
+-- brittany-disable-next-binding
+sbyConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text
+sbyConfig sim1 sim2 (SourceInfo top _) = [st|[options]
+multiclock on
+mode prove
+
+[engines]
+abc pdr
+
+[script]
+#{readL}
+read -formal #{outputText sim1}
+read -formal #{outputText sim2}
+read -formal top.v
+prep -top #{top}
+
+[files]
+#{depList}
+#{outputText sim2}
+#{outputText sim1}
+top.v
+|]
+  where
+    deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v", "cells_yosys.v"]
+    depList =
+      T.intercalate "\n"
+        $   toTextIgnore
+        .   (fromText "data" </>)
+        .   fromText
+        <$> deps
+    readL = T.intercalate "\n" $ mappend "read -formal " <$> deps
+
+icarusTestbench :: (Synthesiser a) => Verilog -> a -> Text
+icarusTestbench t synth1 = [st|
+`include "data/cells_cmos.v"
+`include "data/cells_cyclone_v.v"
+`include "data/cells_verific.v"
+`include "data/cells_xilinx_7.v"
+`include "data/cells_yosys.v"
+`include "#{toTextIgnore $ synthOutput synth1}"
+
+#{genSource t}
+|]
diff --git a/src/Verismith/Tool/Vivado.hs b/src/Verismith/Tool/Vivado.hs
new file mode 100644
index 0000000..272311e
--- /dev/null
+++ b/src/Verismith/Tool/Vivado.hs
@@ -0,0 +1,71 @@
+{-|
+Module      : Verismith.Tool.Vivado
+Description : Vivado Synthesiser implementation.
+Copyright   : (c) 2019, Yann Herklotz Grave
+License     : GPL-3
+Maintainer  : yann [at] yannherklotz [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Vivado Synthesiser implementation.
+-}
+
+module Verismith.Tool.Vivado
+    ( Vivado(..)
+    , defaultVivado
+    )
+where
+
+import           Control.DeepSeq           (NFData, rnf, rwhnf)
+import           Data.Text                 (Text, unpack)
+import           Prelude                   hiding (FilePath)
+import           Shelly
+import           Shelly.Lifted             (liftSh)
+import           Verismith.Tool.Internal
+import           Verismith.Tool.Template
+import           Verismith.Verilog.AST
+import           Verismith.Verilog.CodeGen
+
+data Vivado = Vivado { vivadoBin    :: !(Maybe FilePath)
+                     , vivadoDesc   :: {-# UNPACK #-} !Text
+                     , vivadoOutput :: {-# UNPACK #-} !FilePath
+                     }
+               deriving (Eq)
+
+instance Tool Vivado where
+    toText (Vivado _ t _) = t
+
+instance Show Vivado where
+    show t = unpack $ toText t
+
+instance Synthesiser Vivado where
+    runSynth = runSynthVivado
+    synthOutput = vivadoOutput
+    setSynthOutput (Vivado a b _) = Vivado a b
+
+instance NFData Vivado where
+    rnf = rwhnf
+
+defaultVivado :: Vivado
+defaultVivado = Vivado Nothing "vivado" "syn_vivado.v"
+
+runSynthVivado :: Vivado -> SourceInfo -> ResultSh ()
+runSynthVivado sim (SourceInfo top src) = do
+    dir <- liftSh pwd
+    liftSh $ do
+        writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput
+            sim
+        writefile "rtl.v" $ genSource src
+        run_
+            "sed"
+            [ "s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;"
+            , "-i"
+            , "rtl.v"
+            ]
+    let exec_ n = execute_
+            SynthFail
+            dir
+            "vivado"
+            (maybe (fromText n) (</> fromText n) $ vivadoBin sim)
+    exec_ "vivado" ["-mode", "batch", "-source", toTextIgnore vivadoTcl]
+    where vivadoTcl = fromText ("vivado_" <> top) <.> "tcl"
diff --git a/src/Verismith/Tool/XST.hs b/src/Verismith/Tool/XST.hs
new file mode 100644
index 0000000..c713e0b
--- /dev/null
+++ b/src/Verismith/Tool/XST.hs
@@ -0,0 +1,85 @@
+{-|
+Module      : Verismith.Tool.XST
+Description : XST (ise) simulator implementation.
+Copyright   : (c) 2018-2019, Yann Herklotz
+License     : BSD-3
+Maintainer  : yann [at] yannherklotz [dot] com
+Stability   : experimental
+Portability : POSIX
+
+XST (ise) simulator implementation.
+-}
+
+{-# LANGUAGE QuasiQuotes #-}
+
+module Verismith.Tool.XST
+    ( XST(..)
+    , defaultXST
+    )
+where
+
+import           Control.DeepSeq           (NFData, rnf, rwhnf)
+import           Data.Text                 (Text, unpack)
+import           Prelude                   hiding (FilePath)
+import           Shelly
+import           Shelly.Lifted             (liftSh)
+import           Text.Shakespeare.Text     (st)
+import           Verismith.Tool.Internal
+import           Verismith.Tool.Template
+import           Verismith.Verilog.AST
+import           Verismith.Verilog.CodeGen
+
+data XST = XST { xstBin    :: !(Maybe FilePath)
+               , xstDesc   :: {-# UNPACK #-} !Text
+               , xstOutput :: {-# UNPACK #-} !FilePath
+               }
+         deriving (Eq)
+
+instance Tool XST where
+    toText (XST _ t _) = t
+
+instance Show XST where
+    show t = unpack $ toText t
+
+instance Synthesiser XST where
+    runSynth = runSynthXST
+    synthOutput = xstOutput
+    setSynthOutput (XST a b _) = XST a b
+
+instance NFData XST where
+    rnf = rwhnf
+
+defaultXST :: XST
+defaultXST = XST Nothing "xst" "syn_xst.v"
+
+runSynthXST :: XST -> SourceInfo -> ResultSh ()
+runSynthXST sim (SourceInfo top src) = do
+    dir <- liftSh pwd
+    let exec n = execute_
+            SynthFail
+            dir
+            "xst"
+            (maybe (fromText n) (</> fromText n) $ xstBin sim)
+    liftSh $ do
+        writefile xstFile $ xstSynthConfig top
+        writefile prjFile [st|verilog work "rtl.v"|]
+        writefile "rtl.v" $ genSource src
+    exec "xst" ["-ifn", toTextIgnore xstFile]
+    exec
+        "netgen"
+        [ "-w"
+        , "-ofmt"
+        , "verilog"
+        , toTextIgnore $ modFile <.> "ngc"
+        , toTextIgnore $ synthOutput sim
+        ]
+    liftSh . noPrint $ run_
+        "sed"
+        [ "-i"
+        , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;"
+        , toTextIgnore $ synthOutput sim
+        ]
+  where
+    modFile = fromText top
+    xstFile = modFile <.> "xst"
+    prjFile = modFile <.> "prj"
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