aboutsummaryrefslogtreecommitdiffstats
path: root/src/Verismith/Tool/Template.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Verismith/Tool/Template.hs')
-rw-r--r--src/Verismith/Tool/Template.hs288
1 files changed, 147 insertions, 141 deletions
diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs
index 5a20ff5..d141d46 100644
--- a/src/Verismith/Tool/Template.hs
+++ b/src/Verismith/Tool/Template.hs
@@ -1,47 +1,45 @@
-{-|
-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
+-- 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.
module Verismith.Tool.Template
- ( yosysSynthConfigStd
- , yosysSatConfig
- , yosysSimConfig
- , quartusLightSynthConfig
- , quartusSynthConfig
- , xstSynthConfig
- , vivadoSynthConfig
- , sbyConfig
- , icarusTestbench
- )
+ ( yosysSynthConfigStd,
+ yosysSatConfig,
+ yosysSimConfig,
+ quartusLightSynthConfig,
+ quartusSynthConfig,
+ xstSynthConfig,
+ vivadoSynthConfig,
+ sbyConfig,
+ icarusTestbench,
+ )
where
-import Control.Lens ((^..))
-import Data.Maybe (fromMaybe)
-import Data.Text (Text)
-import qualified Data.Text as T
-import Prelude hiding (FilePath)
-import Shelly
-import Verismith.Tool.Internal
-import Verismith.Verilog.AST
-import Verismith.Verilog.CodeGen
+import Control.Lens ((^..))
+import Data.Maybe (fromMaybe)
+import Data.Text (Text)
+import qualified Data.Text as T
+import Shelly
+import Verismith.Tool.Internal
+import Verismith.Verilog.AST
+import Verismith.Verilog.CodeGen
+import Prelude hiding (FilePath)
rename :: Text -> [Text] -> Text
rename end entries =
- T.intercalate "\n"
- $ flip mappend end
- . mappend "rename "
- . doubleName
- <$> entries
+ T.intercalate "\n" $
+ flip mappend end
+ . mappend "rename "
+ . doubleName
+ <$> entries
{-# INLINE rename #-}
doubleName :: Text -> Text
@@ -52,26 +50,28 @@ outputText :: Synthesiser a => a -> Text
outputText = toTextIgnore . synthOutput
yosysSynthConfig :: Synthesiser a => Text -> a -> FilePath -> Text
-yosysSynthConfig t a fp = T.unlines
- [ "read_verilog " <> toTextIgnore fp
- , t
- , "write_verilog " <> outputText a
- ]
+yosysSynthConfig t a fp =
+ T.unlines
+ [ "read_verilog " <> toTextIgnore fp,
+ t,
+ "write_verilog " <> outputText a
+ ]
yosysSynthConfigStd :: Synthesiser a => a -> FilePath -> Text
yosysSynthConfigStd = yosysSynthConfig "synth"
yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> (SourceInfo ann) -> Text
-yosysSatConfig sim1 sim2 (SourceInfo top src) = T.unlines
- [ "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
- ]
+yosysSatConfig sim1 sim2 (SourceInfo top src) =
+ T.unlines
+ [ "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
@@ -79,109 +79,115 @@ yosysSimConfig :: Text
yosysSimConfig = "read_verilog rtl.v; proc;;\nrename mod mod_rtl"
quartusLightSynthConfig :: Synthesiser a => a -> FilePath -> Text -> FilePath -> Text
-quartusLightSynthConfig q sdc top fp = T.unlines
- [ "load_package flow"
- , ""
- , "project_new -overwrite " <> top
- , ""
- , "set_global_assignment -name FAMILY \"Cyclone V\""
- , "set_global_assignment -name SYSTEMVERILOG_FILE " <> toTextIgnore fp
- , "set_global_assignment -name TOP_LEVEL_ENTITY " <> top
- , "set_global_assignment -name SDC_FILE " <> toTextIgnore sdc
- , "set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\""
- , "set_global_assignment -name NUM_PARALLEL_PROCESSORS 2"
- , "set_instance_assignment -name VIRTUAL_PIN ON -to *"
- , ""
- , "execute_module -tool map"
- , "execute_module -tool fit"
- , "execute_module -tool sta -args \"--mode=implement\""
- , "execute_module -tool eda -args \"--simulation --tool=vcs\""
- , ""
- , "project_close"
- ]
+quartusLightSynthConfig q sdc top fp =
+ T.unlines
+ [ "load_package flow",
+ "",
+ "project_new -overwrite " <> top,
+ "",
+ "set_global_assignment -name FAMILY \"Cyclone V\"",
+ "set_global_assignment -name SYSTEMVERILOG_FILE " <> toTextIgnore fp,
+ "set_global_assignment -name TOP_LEVEL_ENTITY " <> top,
+ "set_global_assignment -name SDC_FILE " <> toTextIgnore sdc,
+ "set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\"",
+ "set_global_assignment -name NUM_PARALLEL_PROCESSORS 2",
+ "set_instance_assignment -name VIRTUAL_PIN ON -to *",
+ "",
+ "execute_module -tool map",
+ "execute_module -tool fit",
+ "execute_module -tool sta -args \"--mode=implement\"",
+ "execute_module -tool eda -args \"--simulation --tool=vcs\"",
+ "",
+ "project_close"
+ ]
quartusSynthConfig :: Synthesiser a => a -> FilePath -> Text -> FilePath -> Text
-quartusSynthConfig q sdc top fp = T.unlines
- [ "load_package flow"
- , ""
- , "project_new -overwrite " <> top
- , ""
- , "set_global_assignment -name FAMILY \"Cyclone 10 GX\""
- , "set_global_assignment -name SYSTEMVERILOG_FILE " <> toTextIgnore fp
- , "set_global_assignment -name TOP_LEVEL_ENTITY " <> top
- , "set_global_assignment -name SDC_FILE " <> toTextIgnore sdc
- , "set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\""
- , "set_global_assignment -name NUM_PARALLEL_PROCESSORS 2"
- , "set_instance_assignment -name VIRTUAL_PIN ON -to *"
- , ""
- , "execute_module -tool syn"
- , "execute_module -tool eda -args \"--simulation --tool=vcs\""
- , ""
- , "project_close"
- ]
+quartusSynthConfig q sdc top fp =
+ T.unlines
+ [ "load_package flow",
+ "",
+ "project_new -overwrite " <> top,
+ "",
+ "set_global_assignment -name FAMILY \"Cyclone 10 GX\"",
+ "set_global_assignment -name SYSTEMVERILOG_FILE " <> toTextIgnore fp,
+ "set_global_assignment -name TOP_LEVEL_ENTITY " <> top,
+ "set_global_assignment -name SDC_FILE " <> toTextIgnore sdc,
+ "set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\"",
+ "set_global_assignment -name NUM_PARALLEL_PROCESSORS 2",
+ "set_instance_assignment -name VIRTUAL_PIN ON -to *",
+ "",
+ "execute_module -tool syn",
+ "execute_module -tool eda -args \"--simulation --tool=vcs\"",
+ "",
+ "project_close"
+ ]
xstSynthConfig :: Text -> Text
-xstSynthConfig top = T.unlines
- [ "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\""
- ]
+xstSynthConfig top =
+ T.unlines
+ [ "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\""
+ ]
vivadoSynthConfig :: Text -> Text -> Text
-vivadoSynthConfig top outf = T.unlines
- [ "# 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
- ]
+vivadoSynthConfig top outf =
+ T.unlines
+ [ "# 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
+ ]
sbyConfig :: (Synthesiser a, Synthesiser b) => Maybe Text -> FilePath -> a -> b -> (SourceInfo ann) -> Text
-sbyConfig mt datadir sim1 sim2 (SourceInfo top _) = T.unlines
- [ "[options]"
- , "multiclock on"
- , "mode prove"
- , "aigsmt " <> fromMaybe "none" mt
- , ""
- , "[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"
- ]
+sbyConfig mt datadir sim1 sim2 (SourceInfo top _) =
+ T.unlines
+ [ "[options]",
+ "multiclock on",
+ "mode prove",
+ "aigsmt " <> fromMaybe "none" mt,
+ "",
+ "[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
- . (datadir </> fromText "data" </>)
- . fromText
- <$> deps
+ T.intercalate "\n" $
+ toTextIgnore
+ . (datadir </> fromText "data" </>)
+ . fromText
+ <$> deps
readL = T.intercalate "\n" $ mappend "read -formal " <$> deps
icarusTestbench :: (Synthesiser a, Show ann) => FilePath -> (Verilog ann) -> a -> Text
-icarusTestbench datadir t synth1 = T.unlines
- [ "`include \"" <> ddir <> "/data/cells_cmos.v\""
- , "`include \"" <> ddir <> "/data/cells_cyclone_v.v\""
- , "`include \"" <> ddir <> "/data/cells_verific.v\""
- , "`include \"" <> ddir <> "/data/cells_xilinx_7.v\""
- , "`include \"" <> ddir <> "/data/cells_yosys.v\""
- , "`include \"" <> toTextIgnore (synthOutput synth1) <> "\""
- , ""
- , genSource t
- ]
+icarusTestbench datadir t synth1 =
+ T.unlines
+ [ "`include \"" <> ddir <> "/data/cells_cmos.v\"",
+ "`include \"" <> ddir <> "/data/cells_cyclone_v.v\"",
+ "`include \"" <> ddir <> "/data/cells_verific.v\"",
+ "`include \"" <> ddir <> "/data/cells_xilinx_7.v\"",
+ "`include \"" <> ddir <> "/data/cells_yosys.v\"",
+ "`include \"" <> toTextIgnore (synthOutput synth1) <> "\"",
+ "",
+ genSource t
+ ]
where
ddir = toTextIgnore datadir
generated by cgit (git 2.34.1) at 2024-05-10 17:15:46 +0000