Use abc for verification

3 files changed, 6 insertions, 8 deletions

diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
index c26b888..a11fbd3 100644
--- a/src/VeriFuzz/Sim/Internal.hs
+++ b/src/VeriFuzz/Sim/Internal.hs
@@ -51,7 +51,6 @@ import           Prelude               hiding (FilePath)
 import           Shelly
 import           Shelly.Lifted         (MonadSh, liftSh)
 import           System.FilePath.Posix (takeBaseName)
-import           VeriFuzz.Internal
 import           VeriFuzz.Result
 import           VeriFuzz.Verilog.AST
 
@@ -154,9 +153,8 @@ logger t = do
     fn          <- pwd
     currentTime <- liftIO getZonedTime
     echo
-        $  "VeriFuzz ["
-        <> T.pack (formatTime defaultTimeLocale "%Y-%m-%d %H:%M:%S" currentTime)
-        <> "] "
+        $  "VeriFuzz "
+        <> T.pack (formatTime defaultTimeLocale "%H:%M:%S " currentTime)
         <> bname fn
         <> " - "
         <> t
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
index f6e5a1e..1085eba 100644
--- a/src/VeriFuzz/Sim/Template.hs
+++ b/src/VeriFuzz/Sim/Template.hs
@@ -94,7 +94,7 @@ multiclock on
 mode prove
 
 [engines]
-smtbmc z3
+abc pdr
 
 [script]
 #{readL}
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"