From c22396d8d80dc090897631ab89a35ab91d0e0c07 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 20 Jan 2019 15:53:58 +0000 Subject: Add template file --- src/VeriFuzz/Simulator/General.hs | 5 +++ src/VeriFuzz/Simulator/Internal/Template.hs | 47 +++++++++++++++++++++++++++++ src/VeriFuzz/Simulator/Xst.hs | 21 +++++-------- src/VeriFuzz/Simulator/Yosys.hs | 46 ++++++++-------------------- 4 files changed, 72 insertions(+), 47 deletions(-) create mode 100644 src/VeriFuzz/Simulator/Internal/Template.hs diff --git a/src/VeriFuzz/Simulator/General.hs b/src/VeriFuzz/Simulator/General.hs index 3615d3a..538ecaa 100644 --- a/src/VeriFuzz/Simulator/General.hs +++ b/src/VeriFuzz/Simulator/General.hs @@ -38,6 +38,11 @@ class (Simulator a) => Synthesize a where -> 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" ["180"] . toTextIgnore {-# INLINE timeout #-} diff --git a/src/VeriFuzz/Simulator/Internal/Template.hs b/src/VeriFuzz/Simulator/Internal/Template.hs new file mode 100644 index 0000000..d0542f1 --- /dev/null +++ b/src/VeriFuzz/Simulator/Internal/Template.hs @@ -0,0 +1,47 @@ +{-| +Module : VeriFuzz.Simulator.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.Simulator.Internal.Template where + +import Data.Text (Text) +import Text.Shakespeare.Text (st) +import VeriFuzz.Simulator.General +import VeriFuzz.Verilog + +yosysSatConfig :: (Simulator a, Simulator b) => a -> Maybe b -> ModDecl -> Text +yosysSatConfig sim1 sim2 m = [st|read_verilog syn_#{toText sim1}.v +rename #{modName m} #{modName m}_1 +read_verilog syn_#{idSim2}.v +rename #{modName m} #{modName m}_2 +read_verilog top.v +proc; opt_clean +flatten #{modName m} +! touch test.#{toText sim1}.#{idSim2}.input_ok +sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName m} +|] + where + idSim2 = maybe "rtl" toText sim2 + +yosysSimConfig :: Text +yosysSimConfig = [st|read_verilog rtl.v; proc;; +rename mod mod_rtl +|] + +xstSynthConfig :: ModDecl -> Text +xstSynthConfig m = [st|run +-ifn #{modName m}.prj -ofn #{modName m} -p artix7 -top #{modName m} +-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" +|] diff --git a/src/VeriFuzz/Simulator/Xst.hs b/src/VeriFuzz/Simulator/Xst.hs index 7b6608b..2314dd1 100644 --- a/src/VeriFuzz/Simulator/Xst.hs +++ b/src/VeriFuzz/Simulator/Xst.hs @@ -14,13 +14,14 @@ Xst (ise) simulator implementation. module VeriFuzz.Simulator.Xst where -import Control.Lens hiding ((<.>)) -import Prelude hiding (FilePath) +import Control.Lens hiding ((<.>)) +import Prelude hiding (FilePath) import Shelly -import Text.Shakespeare.Text (st) +import Text.Shakespeare.Text (st) import VeriFuzz.Simulator.General -import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.CodeGen +import VeriFuzz.Simulator.Internal.Template +import VeriFuzz.Verilog +import VeriFuzz.Verilog data Xst = Xst { xstPath :: FilePath , netgenPath :: FilePath @@ -39,19 +40,13 @@ defaultXst = -- brittany-disable-next-binding runSynthXst :: Xst -> ModDecl -> FilePath -> Sh () runSynthXst sim m outf = do - writefile xstFile [st|run --ifn #{modName}.prj -ofn #{modName} -p artix7 -top #{modName} --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" -|] + writefile xstFile $ xstSynthConfig m writefile prjFile [st|verilog work "rtl.v"|] writefile "rtl.v" $ genSource m timeout_ (xstPath sim) ["-ifn", toTextIgnore xstFile] run_ (netgenPath sim) ["-w", "-ofmt", "verilog", toTextIgnore $ modFile <.> "ngc", toTextIgnore outf] run_ "sed" ["-i", "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;", toTextIgnore outf] where - modName = m ^. modId . getIdentifier - modFile = fromText modName + modFile = fromText $ modName m xstFile = modFile <.> "xst" prjFile = modFile <.> "prj" diff --git a/src/VeriFuzz/Simulator/Yosys.hs b/src/VeriFuzz/Simulator/Yosys.hs index 90c40bf..4c2e0ad 100644 --- a/src/VeriFuzz/Simulator/Yosys.hs +++ b/src/VeriFuzz/Simulator/Yosys.hs @@ -14,13 +14,14 @@ Yosys simulator implementation. module VeriFuzz.Simulator.Yosys where -import Data.Maybe (fromMaybe) -import Data.Text (Text) -import qualified Data.Text as T -import Prelude hiding (FilePath) +import Data.Maybe (fromMaybe) +import Data.Text (Text) +import qualified Data.Text as T +import Prelude hiding (FilePath) import Shelly -import Text.Shakespeare.Text (st) +import Text.Shakespeare.Text (st) import VeriFuzz.Simulator.General +import VeriFuzz.Simulator.Internal.Template import VeriFuzz.Verilog newtype Yosys = Yosys { yosysPath :: FilePath } @@ -34,16 +35,13 @@ instance Synthesize Yosys where defaultYosys :: Yosys defaultYosys = Yosys "/usr/bin/yosys" --- brittany-disable-next-binding writeSimFile :: Yosys -- ^ Simulator instance -> ModDecl -- ^ Current module -> FilePath -- ^ Output sim file -> Sh () writeSimFile _ m file = do writefile "rtl.v" $ genSource m - writefile file [st|read_verilog rtl.v; proc;; -rename mod mod_rtl -|] + writefile file yosysSimConfig runSynthYosys :: Yosys -> ModDecl -> FilePath -> Sh () runSynthYosys sim m outf = do @@ -53,23 +51,7 @@ runSynthYosys sim m outf = do inpf = "rtl.v" inp = toTextIgnore inpf out = toTextIgnore outf - --- brittany-disable-next-binding -writeSatFile :: (Synthesize a, Synthesize b) => FilePath -> a -> Maybe b -> ModDecl -> Sh () -writeSatFile checkFile sim1 sim2 m = - writefile checkFile [st|read_ilang syn_#{toText sim1}.il -rename #{modName m} #{modName m}_1 -read_ilang syn_#{idSim2}.il -rename #{modName m} #{modName m}_2 -read_verilog top.v -proc; opt_clean -flatten #{modName m} -! touch test.#{toText sim1}.#{idSim2}.input_ok -sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName m} -|] - where - idSim2 = maybe "rtl" toText sim2 - -- ids = T.intercalate "," $ allVars m ^.. traverse . getIdentifier + -- ids = T.intercalate "," $ allVars m ^.. traverse . getIdentifier runOtherSynth :: (Synthesize a) => Maybe a -> ModDecl -> Sh () runOtherSynth (Just sim) m = runSynth sim m $ fromText [st|syn_#{toText sim}.v|] @@ -78,13 +60,9 @@ runOtherSynth Nothing m = writefile "syn_rtl.v" $ genSource m runEquiv :: (Synthesize a, Synthesize b) => Yosys -> a -> Maybe b -> ModDecl -> Sh () runEquiv yosys sim1 sim2 m = do writefile "top.v" . genSource . initMod $ makeTop 2 m - writeSatFile checkFile sim1 sim2 m + writefile checkFile $ yosysSatConfig sim1 sim2 m runSynth sim1 m $ fromText [st|syn_#{toText sim1}.v|] runOtherSynth sim2 m - run_ (yosysPath yosys) [checkFile] - where checkFile = [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] - --- | Generate @.il@ files for Yosys equivalence checking using the SAT solver. -genIl :: (Synthesize a) => Yosys -> a -> ModDecl -> Sh () -genIl yosys sim m = do - return + run_ (yosysPath yosys) [toTextIgnore checkFile] + where + checkFile = fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] -- cgit