From 485ad904c33e767331dfb4794032f71f97432c07 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Grave Date: Fri, 1 Mar 2019 12:25:59 +0000 Subject: Moving general simulator options into Internal --- src/VeriFuzz/General.hs | 79 --------------------- src/VeriFuzz/Internal/Simulator.hs | 142 ++++++++++++++++++------------------- src/VeriFuzz/Internal/Template.hs | 102 ++++++++++++++++++++++++++ 3 files changed, 173 insertions(+), 150 deletions(-) delete mode 100644 src/VeriFuzz/General.hs create mode 100644 src/VeriFuzz/Internal/Template.hs (limited to 'src') diff --git a/src/VeriFuzz/General.hs b/src/VeriFuzz/General.hs deleted file mode 100644 index ecbb1da..0000000 --- a/src/VeriFuzz/General.hs +++ /dev/null @@ -1,79 +0,0 @@ -{-| -Module : VeriFuzz.General -Description : Class of the simulator. -Copyright : (c) 2018-2019, Yann Herklotz Grave -License : BSD-3 -Maintainer : ymherklotz [at] gmail [dot] com -Stability : experimental -Portability : POSIX - -Class of the simulator and the synthesize tool. --} - -module VeriFuzz.General where - -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.AST - --- | Simulator class. -class Simulator a where - toText :: a -> Text - --- | Simulation type class. -class (Simulator a) => Simulate a where - runSim :: a -- ^ Simulator instance - -> ModDecl -- ^ Module to simulate - -> [ByteString] -- ^ Inputs to simulate - -> Sh ByteString -- ^ Returns the value of the hash at the output of the testbench. - runSimWithFile :: a - -> FilePath - -> [ByteString] - -> Sh ByteString - --- | Synthesize type class. -class (Simulator a) => Synthesize a where - runSynth :: a -- ^ Synthesize tool instance - -> ModDecl -- ^ Module to synthesize - -> FilePath -- ^ Output verilog file for the module - -> Sh () -- ^ does not return any values - -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 - -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/Internal/Simulator.hs b/src/VeriFuzz/Internal/Simulator.hs index 0abdf8f..b9ffbab 100644 --- a/src/VeriFuzz/Internal/Simulator.hs +++ b/src/VeriFuzz/Internal/Simulator.hs @@ -1,91 +1,91 @@ {-| Module : VeriFuzz.Internal.Simulator -Description : Template file for different configuration files -Copyright : (c) 2019, Yann Herklotz Grave -License : GPL-3 +Description : Class of the simulator. +Copyright : (c) 2018-2019, Yann Herklotz Grave +License : BSD-3 Maintainer : ymherklotz [at] gmail [dot] com Stability : experimental Portability : POSIX -Template file for different configuration files. +Class of the simulator and the synthesize tool. -} -{-# LANGUAGE QuasiQuotes #-} - module VeriFuzz.Internal.Simulator where -import Data.Text (Text) -import qualified Data.Text as T -import Prelude hiding (FilePath) +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 Text.Shakespeare.Text (st) +import System.FilePath.Posix ( takeBaseName ) import VeriFuzz.AST -import VeriFuzz.General -import VeriFuzz.Internal.AST --- brittany-disable-next-binding -yosysSatConfig :: (Simulator a, Simulator b) => a -> Maybe b -> ModDecl -> Text -yosysSatConfig sim1 sim2 m = [st|read_verilog syn_#{toText sim1}.v -rename #{mi} #{mi}_1 -read_verilog syn_#{idSim2}.v -rename #{mi} #{mi}_2 -read_verilog top.v -proc; opt_clean -flatten #{mi} -! touch test.#{toText sim1}.#{idSim2}.input_ok -sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{mi} -|] - where - idSim2 = maybe "rtl" toText sim2 - mi = modName m +-- | Tool class. +class Tool a where + toText :: a -> Text --- brittany-disable-next-binding -yosysSimConfig :: Text -yosysSimConfig = [st|read_verilog rtl.v; proc;; -rename mod mod_rtl -|] +-- | 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 --- brittany-disable-next-binding -xstSynthConfig :: ModDecl -> Text -xstSynthConfig m = [st|run --ifn #{mi}.prj -ofn #{mi} -p artix7 -top #{mi} --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" -|] - where - mi = modName m +-- | 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 :: !VerilogSrc + } + +mainModule :: SourceInfo -> ModDecl +mainModule (SourceInfo main src) = head . filter ismain $ src ^.. getModule + where ismain v = v ^. modId . getIdentifier == main + +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_ #-} --- brittany-disable-next-binding -sbyConfig :: (Simulator a, Simulator b) => FilePath -> a -> Maybe b -> ModDecl -> Text -sbyConfig bd sim1 sim2 m = [st|[options] -mode prove +-- | Helper function to convert bytestrings to integers +bsToI :: ByteString -> Integer +bsToI = B.foldl' (\i b -> (i `shiftL` 8) + fromIntegral b) 0 +{-# INLINE bsToI #-} -[engines] -smtbmc +noPrint :: Sh a -> Sh a +noPrint = print_stdout False . print_stderr False +{-# INLINE noPrint #-} -[script] -#{readL} -read -formal syn_#{toText sim1}.v -rename #{mi} #{mi}_1 -read -formal syn_#{maybe "rtl" toText sim2}.v -rename #{mi} #{mi}_2 -read -formal top.v -prep -top #{mi} +echoP :: Text -> Sh () +echoP t = do + fn <- pwd + echo $ bname fn <> " - " <> t + where bname = T.pack . takeBaseName . T.unpack . toTextIgnore -[files] -#{depList} -syn_#{maybe "rtl" toText sim2}.v -syn_#{toText sim1}.v -top.v -|] +logger :: FilePath -> Text -> Sh a -> Sh a +logger fp name = log_stderr_with (l "_log.stderr.txt") + . log_stdout_with (l "_log.txt") where - mi = modName m - 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 + 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/Internal/Template.hs b/src/VeriFuzz/Internal/Template.hs new file mode 100644 index 0000000..b360bdd --- /dev/null +++ b/src/VeriFuzz/Internal/Template.hs @@ -0,0 +1,102 @@ +{-| +Module : VeriFuzz.Internal.Template +Description : Template file for different configuration files +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Template file for different configuration files. +-} + +{-# LANGUAGE QuasiQuotes #-} + +module VeriFuzz.Internal.Template 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.AST +import VeriFuzz.Internal.Simulator + +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 -- cgit