aboutsummaryrefslogtreecommitdiffstats
path: root/src/VeriFuzz/Sim/Template.hs
diff options
context:
space:
mode:
authorYann Herklotz <git@ymhg.org>2019-05-07 15:01:23 +0100
committerYann Herklotz <git@ymhg.org>2019-05-07 15:01:23 +0100
commite811ba886d9adaed746abe1c9f37c1a87e58a964 (patch)
tree7397a9833508654e142b4cce1a62eb22baf5efe7 /src/VeriFuzz/Sim/Template.hs
parent70497d189ffb8ce8ad582e4eee941e3526eb9d72 (diff)
downloadverismith-e811ba886d9adaed746abe1c9f37c1a87e58a964.tar.gz
verismith-e811ba886d9adaed746abe1c9f37c1a87e58a964.zip
Add support for multiple modules
Had to manually change module names, as Yosys does not change the module name at instantiation. This is done using sed.
Diffstat (limited to 'src/VeriFuzz/Sim/Template.hs')
-rw-r--r--src/VeriFuzz/Sim/Template.hs9
1 files changed, 3 insertions, 6 deletions
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
index 771646d..f6e5a1e 100644
--- a/src/VeriFuzz/Sim/Template.hs
+++ b/src/VeriFuzz/Sim/Template.hs
@@ -88,8 +88,8 @@ write_verilog -force #{outf}
|]
-- brittany-disable-next-binding
-sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> Maybe b -> SourceInfo -> Text
-sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options]
+sbyConfig :: (Synthesiser a, Synthesiser b) => a -> Maybe b -> SourceInfo -> Text
+sbyConfig sim1 sim2 (SourceInfo top _) = [st|[options]
multiclock on
mode prove
@@ -99,9 +99,7 @@ smtbmc z3
[script]
#{readL}
read -formal #{outputText sim1}
-#{rename "_1" mis}
read -formal #{maybe "rtl.v" outputText sim2}
-#{rename "_2" mis}
read -formal top.v
prep -top #{top}
@@ -112,12 +110,11 @@ prep -top #{top}
top.v
|]
where
- mis = src ^.. getSourceId
deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v", "cells_yosys.v"]
depList =
T.intercalate "\n"
$ toTextIgnore
- . ((bd </> fromText "data") </>)
+ . (fromText "data" </>)
. fromText
<$> deps
readL = T.intercalate "\n" $ mappend "read -formal " <$> deps