From 634315880f01c65d916d53db12f92b49517fab9f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 7 May 2019 19:20:30 +0100 Subject: Use abc for verification --- src/VeriFuzz/Sim/Yosys.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/VeriFuzz/Sim/Yosys.hs') 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" -- cgit