diff options
| -rw-r--r-- | src/VeriFuzz/Simulator/Internal/Template.hs | 50 |
1 files changed, 45 insertions, 5 deletions
diff --git a/src/VeriFuzz/Simulator/Internal/Template.hs b/src/VeriFuzz/Simulator/Internal/Template.hs index d0542f1..6813e72 100644 --- a/src/VeriFuzz/Simulator/Internal/Template.hs +++ b/src/VeriFuzz/Simulator/Internal/Template.hs @@ -15,23 +15,27 @@ Template file for different configuration files. module VeriFuzz.Simulator.Internal.Template where import Data.Text (Text) +import qualified Data.Text as T +import Prelude hiding (FilePath) +import Shelly 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 +rename #{mi} #{mi}_1 read_verilog syn_#{idSim2}.v -rename #{modName m} #{modName m}_2 +rename #{mi} #{mi}_2 read_verilog top.v proc; opt_clean -flatten #{modName m} +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 #{modName m} +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 yosysSimConfig :: Text yosysSimConfig = [st|read_verilog rtl.v; proc;; @@ -40,8 +44,44 @@ rename mod mod_rtl xstSynthConfig :: ModDecl -> Text xstSynthConfig m = [st|run --ifn #{modName m}.prj -ofn #{modName m} -p artix7 -top #{modName m} +-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 + +sbyConfig :: (Simulator a, Simulator b) => FilePath -> a -> Maybe b -> ModDecl -> Text +sbyConfig bd sim1 sim2 m = [st|[options] +mode prove + +[engines] +smtbmc + +[script] +#{readL} +read syn_#{toText sim1}.v +rename #{mi} #{mi}_1 +read syn_#{maybe "rtl" toText sim2}.v +rename #{mi} #{mi}_2 +read -formal top.v +prep -top #{mi} + +[files] +#{depList} +syn_#{maybe "rtl" toText sim2}.v +syn_#{toText sim1}.v +top.v +|] + where + mi = modName m + deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v"] + depList = + T.intercalate "\n" + . zipWith mappend ((<>" ") <$> deps) + $ toTextIgnore + . ((bd </> fromText "data") </>) + . fromText + <$> deps + readL = T.intercalate "\n" $ mappend "read " <$> deps |