Large refactor with passing tests

7 files changed, 731 insertions, 0 deletions

diff --git a/src/VeriFuzz/Sim/Env.hs b/src/VeriFuzz/Sim/Env.hs
new file mode 100644
index 0000000..187afb3
--- /dev/null
+++ b/src/VeriFuzz/Sim/Env.hs
@@ -0,0 +1,58 @@
+{-|
+Module      : VeriFuzz.Sim.Env
+Description : Environment to run the simulator and synthesisers in a matrix.
+Copyright   : (c) 2019, Yann Herklotz
+License     : GPL-3
+Maintainer  : ymherklotz [at] gmail [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Environment to run the simulator and synthesisers in a matrix.
+-}
+
+module VeriFuzz.Sim.Env
+    ( SynthTool(..)
+    , SimTool(..)
+    , SimEnv(..)
+    , SynthEnv(..)
+    )
+where
+
+import           Prelude               hiding (FilePath)
+import           Shelly
+import           VeriFuzz.Sim.Icarus
+import           VeriFuzz.Sim.Internal
+import           VeriFuzz.Sim.XST
+import           VeriFuzz.Sim.Yosys
+
+data SynthTool = XSTSynth {-# UNPACK #-} !XST
+               | YosysSynth {-# UNPACK #-} !Yosys
+               deriving (Eq, Show)
+
+instance Tool SynthTool where
+    toText (XSTSynth xst)     = toText xst
+    toText (YosysSynth yosys) = toText yosys
+
+instance Synthesisor SynthTool where
+    runSynth (XSTSynth xst)     = runSynth xst
+    runSynth (YosysSynth yosys) = runSynth yosys
+
+newtype SimTool = IcarusSim Icarus
+                deriving (Eq, Show)
+
+instance Tool SimTool where
+    toText (IcarusSim icarus) = toText icarus
+
+instance Simulator SimTool where
+    runSim (IcarusSim icarus) = runSim icarus
+    runSimWithFile (IcarusSim icarus) = runSimWithFile icarus
+
+data SimEnv = SimEnv { simTools :: [SimTool]
+                     , simDir   :: FilePath
+                     }
+
+data SynthEnv = SynthEnv { synthTools :: [SynthTool]
+                         , synthDir   :: FilePath
+                         }
+
+
diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs
new file mode 100644
index 0000000..6bf21f4
--- /dev/null
+++ b/src/VeriFuzz/Sim/Icarus.hs
@@ -0,0 +1,112 @@
+{-|
+Module      : VeriFuzz.Sim.Icarus
+Description : Icarus verilog module.
+Copyright   : (c) 2018-2019, Yann Herklotz
+License     : BSD-3
+Maintainer  : ymherklotz [at] gmail [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Icarus verilog module.
+-}
+
+module VeriFuzz.Sim.Icarus
+    ( Icarus(..)
+    , defaultIcarus
+    )
+where
+
+import           Control.Lens
+import           Crypto.Hash               (Digest, hash)
+import           Crypto.Hash.Algorithms    (SHA256)
+import           Data.Binary               (encode)
+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           VeriFuzz.Sim.Internal
+import           VeriFuzz.Verilog.AST
+import           VeriFuzz.Verilog.CodeGen
+import           VeriFuzz.Verilog.Internal
+import           VeriFuzz.Verilog.Mutate
+
+data Icarus = Icarus { icarusPath :: FilePath
+                     , vvpPath    :: FilePath
+                     }
+              deriving (Eq, Show)
+
+instance Tool Icarus where
+  toText _ = "iverilog"
+
+instance Simulator Icarus where
+  runSim = runSimIcarus
+  runSimWithFile = runSimIcarusWithFile
+
+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 (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] -> Sh 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 $ Description <$> [newtb, m]
+    writefile "main.v" $ genSource modWithTb
+    runSimWithFile sim "main.v" bss
+    where m = rinfo ^. mainModule
+
+runSimIcarusWithFile :: Icarus -> FilePath -> [ByteString] -> Sh ByteString
+runSimIcarusWithFile sim f _ = do
+    dir <- pwd
+    echoP "Icarus: Compile"
+    _ <- logger dir "icarus"
+        $ run (icarusPath sim) ["-o", "main", toTextIgnore f]
+    echoP "Icarus: Run"
+    B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logger
+        dir
+        "vvp"
+        (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"])
diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
new file mode 100644
index 0000000..e3082b7
--- /dev/null
+++ b/src/VeriFuzz/Sim/Internal.hs
@@ -0,0 +1,112 @@
+{-|
+Module      : VeriFuzz.Sim.Internal
+Description : Class of the simulator.
+Copyright   : (c) 2018-2019, Yann Herklotz
+License     : BSD-3
+Maintainer  : ymherklotz [at] gmail [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Class of the simulator and the synthesize tool.
+-}
+
+module VeriFuzz.Sim.Internal
+    ( Tool(..)
+    , Simulator(..)
+    , Synthesisor(..)
+    , SourceInfo(..)
+    , mainModule
+    , rootPath
+    , timeout
+    , timeout_
+    , bsToI
+    , noPrint
+    , echoP
+    , logger
+    )
+where
+
+import           Control.Lens
+import           Data.Bits             (shiftL)
+import           Data.ByteString       (ByteString)
+import qualified Data.ByteString       as B
+import           Data.Text             (Text)
+import qualified Data.Text             as T
+import           Prelude               hiding (FilePath)
+import           Shelly
+import           System.FilePath.Posix (takeBaseName)
+import           VeriFuzz.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
+         -> Sh ByteString -- ^ Returns the value of the hash at the output of the testbench.
+  runSimWithFile :: a
+                 -> FilePath
+                 -> [ByteString]
+                 -> Sh ByteString
+
+-- | Synthesisor type class.
+class (Tool a) => Synthesisor a where
+  runSynth :: a        -- ^ Synthesisor tool instance
+           -> SourceInfo  -- ^ Run information
+           -> FilePath -- ^ Output verilog file for the module
+           -> Sh ()    -- ^ does not return any values
+
+data SourceInfo = SourceInfo { runMainModule :: {-# UNPACK #-} !Text
+                             , runSource     :: !Verilog
+                             }
+                  deriving (Eq, Show)
+
+-- | May need to change this to Traversal to be safe. For now it will fail when
+-- the main has not been properly set with.
+mainModule :: Lens' SourceInfo ModDecl
+mainModule = lens get_ set_
+  where
+    set_ (SourceInfo top main) v =
+        SourceInfo top (main & getModule %~ update top v)
+    update top v m@(ModDecl (Identifier i) _ _ _) | i == top  = v
+                                                  | otherwise = m
+    get_ (SourceInfo top main) = head . filter (f top) $ main ^.. getModule
+    f top (ModDecl (Identifier i) _ _ _) = i == top
+
+rootPath :: Sh FilePath
+rootPath = do
+    current <- pwd
+    maybe current fromText <$> get_env "VERIFUZZ_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 #-}
+
+echoP :: Text -> Sh ()
+echoP t = do
+    fn <- pwd
+    echo $ bname fn <> " - " <> t
+    where bname = T.pack . takeBaseName . T.unpack . toTextIgnore
+
+logger :: FilePath -> Text -> Sh a -> Sh a
+logger fp name = log_stderr_with (l "_log.stderr.txt")
+    . log_stdout_with (l "_log.txt")
+  where
+    l s t = appendFile (file s) (T.unpack t) >> appendFile (file s) "\n"
+    file s = T.unpack (toTextIgnore $ fp </> fromText name) <> s
diff --git a/src/VeriFuzz/Sim/Reduce.hs b/src/VeriFuzz/Sim/Reduce.hs
new file mode 100644
index 0000000..bed1169
--- /dev/null
+++ b/src/VeriFuzz/Sim/Reduce.hs
@@ -0,0 +1,165 @@
+{-|
+Module      : VeriFuzz.Sim.Reduce
+Description : Test case reducer implementation.
+Copyright   : (c) 2019, Yann Herklotz
+License     : GPL-3
+Maintainer  : ymherklotz [at] gmail [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Test case reducer implementation.
+-}
+
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module VeriFuzz.Sim.Reduce
+    ( reduce
+    )
+where
+
+import           Control.Lens
+import           VeriFuzz.Sim.Internal
+import           VeriFuzz.Verilog.AST
+import           VeriFuzz.Verilog.CodeGen
+import           VeriFuzz.Verilog.Mutate
+
+data Replacement a = Dual a a
+                   | Single a
+                   | None
+                   deriving (Eq, Show)
+
+instance Functor Replacement where
+    fmap f (Dual a b) = Dual (f a) $ f b
+    fmap f (Single a) = Single $ f a
+    fmap _ None       = None
+
+instance Applicative Replacement where
+    pure = Single
+    (Dual a b) <*> (Dual c d) = Dual (a c) $ b d
+    (Dual a b) <*> (Single c) = Dual (a c) $ b c
+    (Single a) <*> (Dual b c) = Dual (a b) $ a c
+    (Single a) <*> (Single b) = Single $ a b
+    None <*> _ = None
+    _ <*> None = None
+
+instance Foldable Replacement where
+    foldMap _ None       = mempty
+    foldMap f (Single a) = f a
+    foldMap f (Dual a b) = f a <> f b
+
+instance Traversable Replacement where
+    traverse _ None       = pure None
+    traverse f (Single a) = Single <$> f a
+    traverse f (Dual a b) = Dual <$> f a <*> f b
+
+-- | Split a list in two halves.
+halve :: [a] -> Replacement [a]
+halve []  = None
+halve [a] = Single [a]
+halve l   = Dual a b where (a, b) = splitAt (length l `div` 2) l
+
+combine :: Lens' a b -> (b -> Replacement b) -> a -> Replacement a
+combine l f i = modify <$> f (i ^. l) where modify res = i & l .~ res
+
+filterExpr :: [Identifier] -> Expr -> Expr
+filterExpr ids (Id i) = if i `notElem` ids then Number 1 0 else Id i
+filterExpr _   e      = e
+
+filterDecl :: [Identifier] -> ModItem -> Bool
+filterDecl ids (Decl Nothing (Port _ _ _ i)) = i `elem` ids
+filterDecl _   _                             = True
+
+filterAssigns :: [Port] -> ModItem -> Bool
+filterAssigns out (ModCA (ContAssign i _)) =
+    notElem i $ out ^.. traverse . portName
+filterAssigns _ _ = False
+
+cleanUndefined :: [Identifier] -> [ModItem] -> [ModItem]
+cleanUndefined ids mis =
+    filter (filterDecl usedWires) mis
+        &  traverse
+        .  modContAssign
+        .  contAssignExpr
+        %~ transform (filterExpr usedWires)
+  where
+    usedWires = mis ^.. traverse . modContAssign . contAssignNetLVal <> ids
+
+halveModAssign :: ModDecl -> Replacement ModDecl
+halveModAssign m = cleanMod m $ modify <$> assigns (m ^. modItems)
+  where
+    assigns = halve . filter (filterAssigns $ m ^. modOutPorts)
+    modify l = m & modItems .~ l
+
+cleanMod :: ModDecl -> Replacement ModDecl -> Replacement ModDecl
+cleanMod m newm = modify . change <$> newm
+  where
+    mis = m ^. modItems
+    modify l = m & modItems .~ l
+    change l =
+        cleanUndefined (m ^.. modInPorts . traverse . portName)
+            .  combineAssigns (head $ m ^. modOutPorts)
+            .  (filter (not . filterAssigns []) mis <>)
+            $  l
+            ^. modItems
+
+-- | Split a module declaration in half by trying to remove assign statements.
+halveAssigns :: SourceInfo -> Replacement SourceInfo
+halveAssigns = combine mainModule halveModAssign
+
+halveIndExpr :: Expr -> Replacement Expr
+halveIndExpr (Concat l      ) = Concat <$> halve l
+halveIndExpr (BinOp e1 _  e2) = Dual e1 e2
+halveIndExpr (Cond  _  e1 e2) = Dual e1 e2
+halveIndExpr (UnOp _ e      ) = Single e
+halveIndExpr (Func _ e      ) = Single e
+halveIndExpr e                = Single e
+
+halveModExpr :: ModItem -> Replacement ModItem
+halveModExpr (ModCA ca) = ModCA <$> combine contAssignExpr halveIndExpr ca
+halveModExpr a          = Single a
+
+halveExpr :: SourceInfo -> Replacement SourceInfo
+halveExpr = combine contexpr $ traverse halveModExpr
+  where
+    contexpr :: Lens' SourceInfo [ModItem]
+    contexpr = mainModule . modItems
+
+reduce_
+    :: (SourceInfo -> Replacement SourceInfo)
+    -> (SourceInfo -> IO Bool)
+    -> SourceInfo
+    -> IO SourceInfo
+reduce_ repl eval src = do
+    replAnswer <- sequenceA $ evalIfNotEmpty <$> replacement
+    case (replacement, replAnswer) of
+        (Single s, Single False) -> runIf s
+        (Dual _ l, Dual True False) -> runIf l
+        (Dual r _, Dual False True) -> runIf r
+        (Dual r l, Dual False False) -> do
+            lreduced <- runIf l
+            rreduced <- runIf r
+            if runSource lreduced < runSource rreduced
+                then return lreduced
+                else return rreduced
+        (None, None) -> return src
+        _ -> return src
+  where
+    replacement = repl src
+    runIf s = if s /= src then reduce eval s else return s
+    evalIfNotEmpty m = do
+        print
+            $   GenVerilog
+            <$> m
+            ^.. mainModule
+            .   modItems
+            .   traverse
+            .   modContAssign
+        eval m
+
+-- | Reduce an input to a minimal representation.
+reduce
+    :: (SourceInfo -> IO Bool) -- ^ Failed or not.
+    -> SourceInfo              -- ^ Input verilog source to be reduced.
+    -> IO SourceInfo           -- ^ Reduced output.
+reduce eval src = reduce_ halveAssigns eval src >>= reduce_ halveExpr eval
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
new file mode 100644
index 0000000..5226106
--- /dev/null
+++ b/src/VeriFuzz/Sim/Template.hs
@@ -0,0 +1,108 @@
+{-|
+Module      : VeriFuzz.Sim.Template
+Description : Template file for different configuration files
+Copyright   : (c) 2019, Yann Herklotz
+License     : GPL-3
+Maintainer  : ymherklotz [at] gmail [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Template file for different configuration files.
+-}
+
+{-# LANGUAGE QuasiQuotes #-}
+
+module VeriFuzz.Sim.Template
+    ( yosysSatConfig
+    , yosysSimConfig
+    , xstSynthConfig
+    , sbyConfig
+    )
+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           VeriFuzz.Sim.Internal
+import           VeriFuzz.Verilog.AST
+
+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 #-}
+
+-- brittany-disable-next-binding
+yosysSatConfig :: (Tool a, Tool b) => a -> Maybe b -> SourceInfo -> Text
+yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog syn_#{toText sim1}.v
+#{rename "_1" mis}
+read_verilog syn_#{idSim2}.v
+#{rename "_2" mis}
+read_verilog #{top}.v
+proc; opt_clean
+flatten #{top}
+! touch test.#{toText sim1}.#{idSim2}.input_ok
+sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{top}
+|]
+  where
+    idSim2 = maybe "rtl" toText sim2
+    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
+sbyConfig :: (Tool a, Tool b) => FilePath -> a -> Maybe b -> SourceInfo -> Text
+sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options]
+mode prove
+
+[engines]
+smtbmc
+
+[script]
+#{readL}
+read -formal syn_#{toText sim1}.v
+#{rename "_1" mis}
+read -formal syn_#{maybe "rtl" toText sim2}.v
+#{rename "_2" mis}
+read -formal top.v
+prep -top #{top}
+
+[files]
+#{depList}
+syn_#{maybe "rtl" toText sim2}.v
+syn_#{toText sim1}.v
+top.v
+|]
+  where
+    mis = src ^.. getSourceId
+    deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v"]
+    depList =
+      T.intercalate "\n"
+        $   toTextIgnore
+        .   ((bd </> fromText "data") </>)
+        .   fromText
+        <$> deps
+    readL = T.intercalate "\n" $ mappend "read -formal " <$> deps
diff --git a/src/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs
new file mode 100644
index 0000000..359b587
--- /dev/null
+++ b/src/VeriFuzz/Sim/XST.hs
@@ -0,0 +1,70 @@
+{-|
+Module      : VeriFuzz.Sim.XST
+Description : XST (ise) simulator implementation.
+Copyright   : (c) 2018-2019, Yann Herklotz
+License     : BSD-3
+Maintainer  : ymherklotz [at] gmail [dot] com
+Stability   : experimental
+Portability : POSIX
+
+XST (ise) simulator implementation.
+-}
+
+{-# LANGUAGE QuasiQuotes #-}
+
+module VeriFuzz.Sim.XST
+    ( XST(..)
+    , defaultXST
+    )
+where
+
+import           Prelude                  hiding (FilePath)
+import           Shelly
+import           Text.Shakespeare.Text    (st)
+import           VeriFuzz.Sim.Internal
+import           VeriFuzz.Sim.Template
+import           VeriFuzz.Verilog.CodeGen
+
+data XST = XST { xstPath    :: {-# UNPACK #-} !FilePath
+               , netgenPath :: {-# UNPACK #-} !FilePath
+               }
+           deriving (Eq, Show)
+
+instance Tool XST where
+  toText _ = "xst"
+
+instance Synthesisor XST where
+  runSynth = runSynthXST
+
+defaultXST :: XST
+defaultXST = XST "xst" "netgen"
+
+runSynthXST :: XST -> SourceInfo -> FilePath -> Sh ()
+runSynthXST sim (SourceInfo top src) outf = do
+    dir <- pwd
+    writefile xstFile $ xstSynthConfig top
+    writefile prjFile [st|verilog work "rtl.v"|]
+    writefile "rtl.v" $ genSource src
+    echoP "XST: run"
+    _ <- logger dir "xst" $ timeout (xstPath sim) ["-ifn", toTextIgnore xstFile]
+    echoP "XST: netgen"
+    _ <- logger dir "netgen" $ run
+        (netgenPath sim)
+        [ "-w"
+        , "-ofmt"
+        , "verilog"
+        , toTextIgnore $ modFile <.> "ngc"
+        , toTextIgnore outf
+        ]
+    echoP "XST: clean"
+    noPrint $ run_
+        "sed"
+        [ "-i"
+        , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;"
+        , toTextIgnore outf
+        ]
+    echoP "XST: done"
+  where
+    modFile = fromText top
+    xstFile = modFile <.> "xst"
+    prjFile = modFile <.> "prj"
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs
new file mode 100644
index 0000000..0d0c98b
--- /dev/null
+++ b/src/VeriFuzz/Sim/Yosys.hs
@@ -0,0 +1,106 @@
+{-|
+Module      : VeriFuzz.Sim.Yosys
+Description : Yosys simulator implementation.
+Copyright   : (c) 2018-2019, Yann Herklotz
+License     : BSD-3
+Maintainer  : ymherklotz [at] gmail [dot] com
+Stability   : experimental
+Portability : POSIX
+
+Yosys simulator implementation.
+-}
+
+{-# LANGUAGE QuasiQuotes #-}
+
+module VeriFuzz.Sim.Yosys
+    ( Yosys(..)
+    , defaultYosys
+    , runEquiv
+    , runEquivYosys
+    )
+where
+
+import           Control.Lens
+import           Prelude                  hiding (FilePath)
+import           Shelly
+import           Text.Shakespeare.Text    (st)
+import           VeriFuzz.Sim.Internal
+import           VeriFuzz.Sim.Template
+import           VeriFuzz.Verilog.CodeGen
+import           VeriFuzz.Verilog.Mutate
+
+newtype Yosys = Yosys { yosysPath :: FilePath }
+              deriving (Eq, Show)
+
+instance Tool Yosys where
+  toText _ = "yosys"
+
+instance Synthesisor Yosys where
+  runSynth = runSynthYosys
+
+defaultYosys :: Yosys
+defaultYosys = Yosys "yosys"
+
+runSynthYosys :: Yosys -> SourceInfo -> FilePath -> Sh ()
+runSynthYosys sim (SourceInfo _ src) outf = do
+    dir <- pwd
+    writefile inpf $ genSource src
+    echoP "Yosys: synthesis"
+    _ <- logger dir "yosys"
+        $ timeout
+              (yosysPath sim)
+              ["-b", "verilog -noattr", "-o", out, "-S", inp]
+    echoP "Yosys: synthesis done"
+  where
+    inpf = "rtl.v"
+    inp  = toTextIgnore inpf
+    out  = toTextIgnore outf
+
+runMaybeSynth :: (Synthesisor a) => Maybe a -> SourceInfo -> Sh ()
+runMaybeSynth (Just sim) srcInfo =
+    runSynth sim srcInfo $ fromText [st|syn_#{toText sim}.v|]
+runMaybeSynth Nothing (SourceInfo _ src) =
+    writefile "syn_rtl.v" $ genSource src
+
+runEquivYosys
+    :: (Synthesisor a, Synthesisor b)
+    => Yosys
+    -> a
+    -> Maybe b
+    -> SourceInfo
+    -> Sh ()
+runEquivYosys yosys sim1 sim2 srcInfo = do
+    writefile "top.v" . genSource . initMod . makeTop 2 $ srcInfo ^. mainModule
+    writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
+    runSynth sim1 srcInfo $ fromText [st|syn_#{toText sim1}.v|]
+    runMaybeSynth sim2 srcInfo
+    echoP "Yosys: equivalence check"
+    run_ (yosysPath yosys) [toTextIgnore checkFile]
+    echoP "Yosys: equivalence done"
+  where
+    checkFile =
+        fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|]
+
+runEquiv
+    :: (Synthesisor a, Synthesisor b)
+    => Yosys
+    -> a
+    -> Maybe b
+    -> SourceInfo
+    -> Sh ()
+runEquiv _ sim1 sim2 srcInfo = do
+    root <- rootPath
+    dir  <- pwd
+    echoP "SymbiYosys: setup"
+    writefile "top.v"
+        .  genSource
+        .  initMod
+        .  makeTopAssert
+        $  srcInfo
+        ^. mainModule
+    writefile "test.sby" $ sbyConfig root sim1 sim2 srcInfo
+    runSynth sim1 srcInfo $ fromText [st|syn_#{toText sim1}.v|]
+    runMaybeSynth sim2 srcInfo
+    echoP "SymbiYosys: run"
+    _ <- logger dir "symbiyosys" $ run "sby" ["-f", "test.sby"]
+    echoP "SymbiYosys: done"