diff options
| author | Yann Herklotz <git@ymhg.org> | 2019-05-07 19:20:30 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@ymhg.org> | 2019-05-07 19:20:30 +0100 |
| commit | 634315880f01c65d916d53db12f92b49517fab9f (patch) | |
| tree | 13ee6cca09a7ce259fa032e90f602c855eb62836 /src/VeriFuzz/Sim/Yosys.hs | |
| parent | b073c6214dd62c9b8d30c5ec187375828c753d0e (diff) | |
| download | verismith-634315880f01c65d916d53db12f92b49517fab9f.tar.gz verismith-634315880f01c65d916d53db12f92b49517fab9f.zip | |
Use abc for verification
Diffstat (limited to 'src/VeriFuzz/Sim/Yosys.hs')
| -rw-r--r-- | src/VeriFuzz/Sim/Yosys.hs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs index 80fb5b5..656bc52 100644 --- a/src/VeriFuzz/Sim/Yosys.hs +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -58,7 +58,7 @@ runSynthYosys sim (SourceInfo _ src) = (<?> SynthFail) . liftSh $ do logCommand_ dir "yosys" $ timeout (yosysPath sim) - ["-b", "verilog -noattr", "-o", out, "-S", inp] + ["-p", "read -formal " <> inp <> "; synth; write_verilog -noattr " <> out] logger "Yosys: synthesis done" where inpf = "rtl.v" @@ -114,7 +114,7 @@ runEquiv _ sim1 sim2 srcInfo = do ^. mainModule replaceMods (synthOutput sim1) "_1" srcInfo replaceMods (maybe "rtl.v" synthOutput sim2) "_2" srcInfo - writefile "test.sby" $ sbyConfig sim1 sim2 srcInfo + writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo liftSh $ logger "Running SymbiYosys" - execute_ EquivFail dir "symbiyosys" "sby" ["-f", "test.sby"] + execute_ EquivFail dir "symbiyosys" "sby" ["proof.sby"] liftSh $ logger "SymbiYosys equivalence check passed" |