From fd4b0b5152f94cd406f2e5de86ce7ed0a4d2cbd0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Apr 2019 19:47:32 +0100 Subject: Large refactor with passing tests --- src/VeriFuzz/Sim/Env.hs | 58 +++++++++++++++ src/VeriFuzz/Sim/Icarus.hs | 112 +++++++++++++++++++++++++++++ src/VeriFuzz/Sim/Internal.hs | 112 +++++++++++++++++++++++++++++ src/VeriFuzz/Sim/Reduce.hs | 165 +++++++++++++++++++++++++++++++++++++++++++ src/VeriFuzz/Sim/Template.hs | 108 ++++++++++++++++++++++++++++ src/VeriFuzz/Sim/XST.hs | 70 ++++++++++++++++++ src/VeriFuzz/Sim/Yosys.hs | 106 +++++++++++++++++++++++++++ 7 files changed, 731 insertions(+) create mode 100644 src/VeriFuzz/Sim/Env.hs create mode 100644 src/VeriFuzz/Sim/Icarus.hs create mode 100644 src/VeriFuzz/Sim/Internal.hs create mode 100644 src/VeriFuzz/Sim/Reduce.hs create mode 100644 src/VeriFuzz/Sim/Template.hs create mode 100644 src/VeriFuzz/Sim/XST.hs create mode 100644 src/VeriFuzz/Sim/Yosys.hs (limited to 'src/VeriFuzz/Sim') 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" -- cgit