From d86cb8fd763e687cf2cd7ad40094d15ebba6bf87 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 7 Apr 2020 17:19:12 +0100 Subject: Remove shakespeare dependency --- src/Verismith/Tool/Template.hs | 199 +++++++++++++++++++++-------------------- src/Verismith/Tool/XST.hs | 3 +- src/Verismith/Tool/Yosys.hs | 3 +- verismith.cabal | 2 - 4 files changed, 103 insertions(+), 104 deletions(-) diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs index ad9860c..a2e0675 100644 --- a/src/Verismith/Tool/Template.hs +++ b/src/Verismith/Tool/Template.hs @@ -31,7 +31,6 @@ 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 @@ -53,112 +52,116 @@ outputText :: Synthesiser a => a -> Text outputText = toTextIgnore . synthOutput yosysSynthConfig :: Synthesiser a => Text -> a -> FilePath -> Text -yosysSynthConfig t a fp = [st|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) = [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} -|] +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 yosysSimConfig :: Text -yosysSimConfig = [st|read_verilog rtl.v; proc;; -rename mod mod_rtl -|] +yosysSimConfig = "read_verilog rtl.v; proc;;\nrename mod mod_rtl" quartusLightSynthConfig :: Synthesiser a => a -> FilePath -> Text -> FilePath -> Text -quartusLightSynthConfig q sdc top fp = [st|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 = [st|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 = [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" -|] +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 = [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} -|] +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 _) = [st|[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 = @@ -170,15 +173,15 @@ top.v readL = T.intercalate "\n" $ mappend "read -formal " <$> deps icarusTestbench :: (Synthesiser a) => FilePath -> (Verilog ann) -> a -> Text -icarusTestbench datadir t synth1 = [st| -`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 diff --git a/src/Verismith/Tool/XST.hs b/src/Verismith/Tool/XST.hs index 2bec7d9..1e37149 100644 --- a/src/Verismith/Tool/XST.hs +++ b/src/Verismith/Tool/XST.hs @@ -23,7 +23,6 @@ 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 @@ -62,7 +61,7 @@ runSynthXST sim (SourceInfo top src) = do (maybe (fromText n) ( fromText n) $ xstBin sim) liftSh $ do writefile xstFile $ xstSynthConfig top - writefile prjFile [st|verilog work "rtl.v"|] + writefile prjFile "verilog work \"rtl.v\"" writefile "rtl.v" $ genSource src exec "xst" ["-ifn", toTextIgnore xstFile] exec diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs index 9f536b7..24b83fd 100644 --- a/src/Verismith/Tool/Yosys.hs +++ b/src/Verismith/Tool/Yosys.hs @@ -29,7 +29,6 @@ import Prelude hiding (FilePath) import Shelly (FilePath, ()) import qualified Shelly as S import Shelly.Lifted (liftSh, readfile) -import Text.Shakespeare.Text (st) import Verismith.CounterEg (parseCounterEg) import Verismith.Result import Verismith.Tool.Internal @@ -102,7 +101,7 @@ runEquivYosys yosys sim1 sim2 srcInfo = do runSynth sim1 srcInfo runSynth sim2 srcInfo liftSh $ S.run_ (yosysPath yosys) [S.toTextIgnore checkFile] - where checkFile = S.fromText [st|test.#{toText sim1}.#{toText sim2}.ys|] + where checkFile = S.fromText $ "test." <> toText sim1 <> "." <> toText sim2 <> ".ys" runEquiv :: (Synthesiser a, Synthesiser b) => Maybe Text -> FilePath -> a -> b -> (SourceInfo ann) -> ResultSh () diff --git a/verismith.cabal b/verismith.cabal index 9754056..42a785b 100644 --- a/verismith.cabal +++ b/verismith.cabal @@ -95,7 +95,6 @@ library , prettyprinter >=1.2.0.1 && <1.7 , random >=1.1 && <1.2 , recursion-schemes >=5.0.2 && <5.2 - , shakespeare >=2 && <2.1 , shelly >=1.8.0 && <1.10 , template-haskell >=2.13.0 && <2.16 , text >=1.2 && <1.3 @@ -140,7 +139,6 @@ test-suite test , hedgehog >=1.0 && <1.2 , lens >=4.16.1 && <4.19 , parsec >= 3.1 && < 3.2 - , shakespeare >=2 && <2.1 , tasty >=1.0.1.1 && <1.3 , tasty-hedgehog >=1.0 && <1.1 , tasty-hunit >=0.10 && <0.11 -- cgit