diff options
author | Yann Herklotz <git@ymhg.org> | 2019-04-18 23:42:48 +0100 |
---|---|---|
committer | Yann Herklotz <git@ymhg.org> | 2019-04-18 23:42:48 +0100 |
commit | 72ca7b273a8adf421d481e0caa97caa8a565187a (patch) | |
tree | 7b243629884be5104a61f7378973d6b38e22a998 /src/VeriFuzz/Sim/Template.hs | |
parent | 97398438902d42b33aef475e3e357781582bec16 (diff) | |
download | verismith-72ca7b273a8adf421d481e0caa97caa8a565187a.tar.gz verismith-72ca7b273a8adf421d481e0caa97caa8a565187a.zip |
Add output information to Type
Diffstat (limited to 'src/VeriFuzz/Sim/Template.hs')
-rw-r--r-- | src/VeriFuzz/Sim/Template.hs | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs index f630ea6..93f24a3 100644 --- a/src/VeriFuzz/Sim/Template.hs +++ b/src/VeriFuzz/Sim/Template.hs @@ -43,16 +43,18 @@ doubleName :: Text -> Text doubleName n = n <> " " <> n {-# INLINE doubleName #-} +outputText :: Synthesiser a => a -> Text +outputText = toTextIgnore . synthOutput + -- brittany-disable-next-binding -yosysSatConfig :: (Tool a, Tool b) => a -> Maybe b -> SourceInfo -> Text -yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog syn_#{toText sim1}.v +yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> Maybe b -> SourceInfo -> Text +yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog #{outputText sim1} #{rename "_1" mis} read_verilog syn_#{idSim2}.v #{rename "_2" mis} read_verilog #{top}.v proc; opt_clean flatten #{top} -! touch test.#{toText sim1}.#{idSim2}.input_ok sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{top} |] where @@ -86,7 +88,7 @@ write_verilog -force #{outf} |] -- brittany-disable-next-binding -sbyConfig :: (Tool a, Tool b) => FilePath -> a -> Maybe b -> SourceInfo -> Text +sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> Maybe b -> SourceInfo -> Text sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options] mode prove @@ -95,17 +97,17 @@ smtbmc z3 [script] #{readL} -read -formal syn_#{toText sim1}.v +read -formal #{outputText sim1} #{rename "_1" mis} -read -formal syn_#{maybe "rtl" toText sim2}.v +read -formal #{maybe "rtl.v" outputText sim2} #{rename "_2" mis} read -formal top.v prep -top #{top} [files] #{depList} -syn_#{maybe "rtl" toText sim2}.v -syn_#{toText sim1}.v +#{maybe "rtl.v" outputText sim2} +#{outputText sim1} top.v |] where |