From e7f57642f068650ea362201b239efad1c9a841d9 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 18 Oct 2019 14:29:07 +0100 Subject: Rename Sim to Tool --- src/Verismith.hs | 6 +- src/Verismith/Config.hs | 8 +- src/Verismith/Fuzz.hs | 37 +++---- src/Verismith/Reduce.hs | 4 +- src/Verismith/Report.hs | 4 +- src/Verismith/Sim.hs | 51 ---------- src/Verismith/Sim/Icarus.hs | 188 ----------------------------------- src/Verismith/Sim/Identity.hs | 51 ---------- src/Verismith/Sim/Internal.hs | 215 ----------------------------------------- src/Verismith/Sim/Quartus.hs | 77 --------------- src/Verismith/Sim/Template.hs | 133 ------------------------- src/Verismith/Sim/Vivado.hs | 71 -------------- src/Verismith/Sim/XST.hs | 85 ---------------- src/Verismith/Sim/Yosys.hs | 127 ------------------------ src/Verismith/Tool.hs | 51 ++++++++++ src/Verismith/Tool/Icarus.hs | 188 +++++++++++++++++++++++++++++++++++ src/Verismith/Tool/Identity.hs | 51 ++++++++++ src/Verismith/Tool/Internal.hs | 215 +++++++++++++++++++++++++++++++++++++++++ src/Verismith/Tool/Quartus.hs | 77 +++++++++++++++ src/Verismith/Tool/Template.hs | 133 +++++++++++++++++++++++++ src/Verismith/Tool/Vivado.hs | 71 ++++++++++++++ src/Verismith/Tool/XST.hs | 85 ++++++++++++++++ src/Verismith/Tool/Yosys.hs | 127 ++++++++++++++++++++++++ verismith.cabal | 18 ++-- 24 files changed, 1034 insertions(+), 1039 deletions(-) delete mode 100644 src/Verismith/Sim.hs delete mode 100644 src/Verismith/Sim/Icarus.hs delete mode 100644 src/Verismith/Sim/Identity.hs delete mode 100644 src/Verismith/Sim/Internal.hs delete mode 100644 src/Verismith/Sim/Quartus.hs delete mode 100644 src/Verismith/Sim/Template.hs delete mode 100644 src/Verismith/Sim/Vivado.hs delete mode 100644 src/Verismith/Sim/XST.hs delete mode 100644 src/Verismith/Sim/Yosys.hs create mode 100644 src/Verismith/Tool.hs create mode 100644 src/Verismith/Tool/Icarus.hs create mode 100644 src/Verismith/Tool/Identity.hs create mode 100644 src/Verismith/Tool/Internal.hs create mode 100644 src/Verismith/Tool/Quartus.hs create mode 100644 src/Verismith/Tool/Template.hs create mode 100644 src/Verismith/Tool/Vivado.hs create mode 100644 src/Verismith/Tool/XST.hs create mode 100644 src/Verismith/Tool/Yosys.hs diff --git a/src/Verismith.hs b/src/Verismith.hs index e7d3ce6..85deca3 100644 --- a/src/Verismith.hs +++ b/src/Verismith.hs @@ -30,7 +30,7 @@ module Verismith , module Verismith.Verilog , module Verismith.Config , module Verismith.Circuit - , module Verismith.Sim + , module Verismith.Tool , module Verismith.Fuzz , module Verismith.Report ) @@ -65,8 +65,8 @@ import Verismith.Generate import Verismith.Reduce import Verismith.Report import Verismith.Result -import Verismith.Sim -import Verismith.Sim.Internal +import Verismith.Tool +import Verismith.Tool.Internal import Verismith.Verilog import Verismith.Verilog.Parser (parseSourceInfoFile) diff --git a/src/Verismith/Config.hs b/src/Verismith/Config.hs index 9d37fd2..decf1fb 100644 --- a/src/Verismith/Config.hs +++ b/src/Verismith/Config.hs @@ -92,10 +92,10 @@ import Paths_verismith (version) import Shelly (toTextIgnore) import Toml (TomlCodec, (.=)) import qualified Toml -import Verismith.Sim.Quartus -import Verismith.Sim.Vivado -import Verismith.Sim.XST -import Verismith.Sim.Yosys +import Verismith.Tool.Quartus +import Verismith.Tool.Vivado +import Verismith.Tool.XST +import Verismith.Tool.Yosys -- $conf -- diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs index 1f86739..81c00a0 100644 --- a/src/Verismith/Fuzz.hs +++ b/src/Verismith/Fuzz.hs @@ -59,9 +59,9 @@ import Verismith.Internal import Verismith.Reduce import Verismith.Report import Verismith.Result -import Verismith.Sim.Icarus -import Verismith.Sim.Internal -import Verismith.Sim.Yosys +import Verismith.Tool.Icarus +import Verismith.Tool.Internal +import Verismith.Tool.Yosys import Verismith.Verilog.AST import Verismith.Verilog.CodeGen @@ -194,24 +194,19 @@ equivalence src = do equiv a b = toolRun ("equivalence check for " <> toText a <> " and " <> toText b) . runResultT - $ do - make dir - pop dir $ do - liftSh $ do - cp - ( fromText ".." - fromText (toText a) - synthOutput a - ) - $ synthOutput a - cp - ( fromText ".." - fromText (toText b) - synthOutput b - ) - $ synthOutput b - writefile "rtl.v" $ genSource src - runEquiv a b src + $ do make dir + pop dir $ do + liftSh $ do + cp ( fromText ".." + fromText (toText a) + synthOutput a + ) $ synthOutput a + cp ( fromText ".." + fromText (toText b) + synthOutput b + ) $ synthOutput b + writefile "rtl.v" $ genSource src + runEquiv a b src where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m () diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs index 69674cc..88f0b42 100644 --- a/src/Verismith/Reduce.hs +++ b/src/Verismith/Reduce.hs @@ -49,8 +49,8 @@ import qualified Shelly import Shelly.Lifted (MonadSh, liftSh) import Verismith.Internal import Verismith.Result -import Verismith.Sim -import Verismith.Sim.Internal +import Verismith.Tool +import Verismith.Tool.Internal import Verismith.Verilog import Verismith.Verilog.AST import Verismith.Verilog.Mutate diff --git a/src/Verismith/Report.hs b/src/Verismith/Report.hs index b074be4..6c25f5c 100644 --- a/src/Verismith/Report.hs +++ b/src/Verismith/Report.hs @@ -63,8 +63,8 @@ import qualified Text.Blaze.Html5.Attributes as A import Verismith.Config import Verismith.Internal import Verismith.Result -import Verismith.Sim -import Verismith.Sim.Internal +import Verismith.Tool +import Verismith.Tool.Internal -- | Common type alias for synthesis results type UResult = Result Failed () diff --git a/src/Verismith/Sim.hs b/src/Verismith/Sim.hs deleted file mode 100644 index 5e31985..0000000 --- a/src/Verismith/Sim.hs +++ /dev/null @@ -1,51 +0,0 @@ -{-| -Module : Verismith.Sim -Description : Simulator implementations. -Copyright : (c) 2019, Yann Herklotz Grave -License : GPL-3 -Maintainer : yann [at] yannherklotz [dot] com -Stability : experimental -Portability : POSIX - -Simulator implementations. --} - -module Verismith.Sim - ( - -- * Simulators - -- ** Icarus - Icarus(..) - , defaultIcarus - -- * Synthesisers - -- ** Yosys - , Yosys(..) - , defaultYosys - -- ** Vivado - , Vivado(..) - , defaultVivado - -- ** XST - , XST(..) - , defaultXST - -- ** Quartus - , Quartus(..) - , defaultQuartus - -- ** Identity - , Identity(..) - , defaultIdentity - -- * Equivalence - , runEquiv - -- * Simulation - , runSim - -- * Synthesis - , runSynth - , logger - ) -where - -import Verismith.Sim.Icarus -import Verismith.Sim.Identity -import Verismith.Sim.Internal -import Verismith.Sim.Quartus -import Verismith.Sim.Vivado -import Verismith.Sim.XST -import Verismith.Sim.Yosys diff --git a/src/Verismith/Sim/Icarus.hs b/src/Verismith/Sim/Icarus.hs deleted file mode 100644 index 003f1de..0000000 --- a/src/Verismith/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/Verismith/Sim/Identity.hs b/src/Verismith/Sim/Identity.hs deleted file mode 100644 index 89c6b36..0000000 --- a/src/Verismith/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/Verismith/Sim/Internal.hs b/src/Verismith/Sim/Internal.hs deleted file mode 100644 index bcbc3af..0000000 --- a/src/Verismith/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/Verismith/Sim/Quartus.hs b/src/Verismith/Sim/Quartus.hs deleted file mode 100644 index 5fb1e49..0000000 --- a/src/Verismith/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/Verismith/Sim/Template.hs b/src/Verismith/Sim/Template.hs deleted file mode 100644 index 071e040..0000000 --- a/src/Verismith/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/Verismith/Sim/Vivado.hs b/src/Verismith/Sim/Vivado.hs deleted file mode 100644 index 2dad87d..0000000 --- a/src/Verismith/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/Verismith/Sim/XST.hs b/src/Verismith/Sim/XST.hs deleted file mode 100644 index 9144ba7..0000000 --- a/src/Verismith/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/Verismith/Sim/Yosys.hs b/src/Verismith/Sim/Yosys.hs deleted file mode 100644 index 9805140..0000000 --- a/src/Verismith/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 diff --git a/src/Verismith/Tool.hs b/src/Verismith/Tool.hs new file mode 100644 index 0000000..7e41180 --- /dev/null +++ b/src/Verismith/Tool.hs @@ -0,0 +1,51 @@ +{-| +Module : Verismith.Tool +Description : Simulator implementations. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Simulator implementations. +-} + +module Verismith.Tool + ( + -- * Simulators + -- ** Icarus + Icarus(..) + , defaultIcarus + -- * Synthesisers + -- ** Yosys + , Yosys(..) + , defaultYosys + -- ** Vivado + , Vivado(..) + , defaultVivado + -- ** XST + , XST(..) + , defaultXST + -- ** Quartus + , Quartus(..) + , defaultQuartus + -- ** Identity + , Identity(..) + , defaultIdentity + -- * Equivalence + , runEquiv + -- * Simulation + , runSim + -- * Synthesis + , runSynth + , logger + ) +where + +import Verismith.Tool.Icarus +import Verismith.Tool.Identity +import Verismith.Tool.Internal +import Verismith.Tool.Quartus +import Verismith.Tool.Vivado +import Verismith.Tool.XST +import Verismith.Tool.Yosys 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 diff --git a/verismith.cabal b/verismith.cabal index 36a7777..7afb640 100644 --- a/verismith.cabal +++ b/verismith.cabal @@ -53,15 +53,15 @@ library , Verismith.Reduce , Verismith.Report , Verismith.Result - , Verismith.Sim - , Verismith.Sim.Icarus - , Verismith.Sim.Identity - , Verismith.Sim.Internal - , Verismith.Sim.Quartus - , Verismith.Sim.Template - , Verismith.Sim.Vivado - , Verismith.Sim.XST - , Verismith.Sim.Yosys + , Verismith.Tool + , Verismith.Tool.Icarus + , Verismith.Tool.Identity + , Verismith.Tool.Internal + , Verismith.Tool.Quartus + , Verismith.Tool.Template + , Verismith.Tool.Vivado + , Verismith.Tool.XST + , Verismith.Tool.Yosys , Verismith.Verilog , Verismith.Verilog.AST , Verismith.Verilog.BitVec -- cgit