[Fix #26] Add support for SymbiYosys

2 files changed, 10 insertions, 4 deletions

diff --git a/src/VeriFuzz/Simulator/Internal/Template.hs b/src/VeriFuzz/Simulator/Internal/Template.hs
index 4b9cc4e..109c679 100644
--- a/src/VeriFuzz/Simulator/Internal/Template.hs
+++ b/src/VeriFuzz/Simulator/Internal/Template.hs
@@ -65,9 +65,9 @@ smtbmc
 
 [script]
 #{readL}
-read syn_#{toText sim1}.v
+read -formal syn_#{toText sim1}.v
 rename #{mi} #{mi}_1
-read syn_#{maybe "rtl" toText sim2}.v
+read -formal syn_#{maybe "rtl" toText sim2}.v
 rename #{mi} #{mi}_2
 read -formal top.v
 prep -top #{mi}
@@ -87,4 +87,4 @@ top.v
         .   ((bd </> fromText "data") </>)
         .   fromText
         <$> deps
-    readL = T.intercalate "\n" $ mappend "read " <$> deps
+    readL = T.intercalate "\n" $ mappend "read -formal " <$> deps
diff --git a/src/VeriFuzz/Simulator/Yosys.hs b/src/VeriFuzz/Simulator/Yosys.hs
index ec5a284..286a132 100644
--- a/src/VeriFuzz/Simulator/Yosys.hs
+++ b/src/VeriFuzz/Simulator/Yosys.hs
@@ -65,8 +65,14 @@ runEquivYosys yosys sim1 sim2 m = do
   runSynth sim1 m $ fromText [st|syn_#{toText sim1}.v|]
   runMaybeSynth sim2 m
   run_ (yosysPath yosys) [toTextIgnore checkFile]
-  where checkFile = fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|]
+  where
+    checkFile = fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|]
 
 runEquiv :: (Synthesize a, Synthesize b) => Yosys -> a -> Maybe b -> ModDecl -> Sh ()
 runEquiv yosys sim1 sim2 m = do
+  root <- rootPath
   writefile "top.v" . genSource . initMod $ makeTopAssert m
+  writefile "test.sby" $ sbyConfig root sim1 sim2 m
+  runSynth sim1 m $ fromText [st|syn_#{toText sim1}.v|]
+  runMaybeSynth sim2 m
+  run_ "sby" ["test.sby"]