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