diff options
| author | Yann Herklotz <git@ymhg.org> | 2019-05-13 16:31:46 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@ymhg.org> | 2019-05-13 16:31:46 +0100 |
| commit | 5fe3cbc3ba41cb7bfd9f4be737b0c5bc94d7e24a (patch) | |
| tree | 90ee539e72196a2f870bada3ff3454ca0ddafe95 /src/VeriFuzz/Sim/Template.hs | |
| parent | 0e0dd6ee036c333cd3026917e696cf37996af341 (diff) | |
| download | verismith-5fe3cbc3ba41cb7bfd9f4be737b0c5bc94d7e24a.tar.gz verismith-5fe3cbc3ba41cb7bfd9f4be737b0c5bc94d7e24a.zip | |
Remove Maybe from equivalence check
Diffstat (limited to 'src/VeriFuzz/Sim/Template.hs')
| -rw-r--r-- | src/VeriFuzz/Sim/Template.hs | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs index 1085eba..4aa07f6 100644 --- a/src/VeriFuzz/Sim/Template.hs +++ b/src/VeriFuzz/Sim/Template.hs @@ -47,10 +47,10 @@ outputText :: Synthesiser a => a -> Text outputText = toTextIgnore . synthOutput -- brittany-disable-next-binding -yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> Maybe b -> SourceInfo -> Text +yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog #{outputText sim1} #{rename "_1" mis} -read_verilog syn_#{idSim2}.v +read_verilog syn_#{outputText sim2}.v #{rename "_2" mis} read_verilog #{top}.v proc; opt_clean @@ -58,7 +58,6 @@ flatten #{top} sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{top} |] where - idSim2 = maybe "rtl" toText sim2 mis = src ^.. getSourceId -- brittany-disable-next-binding @@ -88,7 +87,7 @@ write_verilog -force #{outf} |] -- brittany-disable-next-binding -sbyConfig :: (Synthesiser a, Synthesiser b) => a -> Maybe b -> SourceInfo -> Text +sbyConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text sbyConfig sim1 sim2 (SourceInfo top _) = [st|[options] multiclock on mode prove @@ -99,13 +98,13 @@ abc pdr [script] #{readL} read -formal #{outputText sim1} -read -formal #{maybe "rtl.v" outputText sim2} +read -formal #{outputText sim2} read -formal top.v prep -top #{top} [files] #{depList} -#{maybe "rtl.v" outputText sim2} +#{outputText sim2} #{outputText sim1} top.v |] |