Renaming to VeriSmith

8 files changed, 0 insertions, 947 deletions

diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs
deleted file mode 100644
index f104630..0000000
--- a/src/VeriFuzz/Sim/Icarus.hs
+++ /dev/null
@@ -1,188 +0,0 @@
-{-|
-Module      : VeriSmith.Sim.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.Sim.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.Sim.Internal
-import           VeriSmith.Sim.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/VeriFuzz/Sim/Identity.hs b/src/VeriFuzz/Sim/Identity.hs
deleted file mode 100644
index cac230f..0000000
--- a/src/VeriFuzz/Sim/Identity.hs
+++ /dev/null
@@ -1,51 +0,0 @@
-{-|
-Module      : VeriSmith.Sim.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.Sim.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.Sim.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/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
deleted file mode 100644
index 017faad..0000000
--- a/src/VeriFuzz/Sim/Internal.hs
+++ /dev/null
@@ -1,215 +0,0 @@
-{-|
-Module      : VeriSmith.Sim.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.Sim.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/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs
deleted file mode 100644
index 6837133..0000000
--- a/src/VeriFuzz/Sim/Quartus.hs
+++ /dev/null
@@ -1,77 +0,0 @@
-{-|
-Module      : VeriSmith.Sim.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.Sim.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.Sim.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/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
deleted file mode 100644
index d232420..0000000
--- a/src/VeriFuzz/Sim/Template.hs
+++ /dev/null
@@ -1,133 +0,0 @@
-{-|
-Module      : VeriSmith.Sim.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.Sim.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.Sim.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/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs
deleted file mode 100644
index e8d8f0d..0000000
--- a/src/VeriFuzz/Sim/Vivado.hs
+++ /dev/null
@@ -1,71 +0,0 @@
-{-|
-Module      : VeriSmith.Sim.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.Sim.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.Sim.Internal
-import           VeriSmith.Sim.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/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs
deleted file mode 100644
index 30a4b0b..0000000
--- a/src/VeriFuzz/Sim/XST.hs
+++ /dev/null
@@ -1,85 +0,0 @@
-{-|
-Module      : VeriSmith.Sim.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.Sim.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.Sim.Internal
-import           VeriSmith.Sim.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/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs
deleted file mode 100644
index 1f583a8..0000000
--- a/src/VeriFuzz/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