From 5fe3cbc3ba41cb7bfd9f4be737b0c5bc94d7e24a Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@ymhg.org>
Date: Mon, 13 May 2019 16:31:46 +0100
Subject: Remove Maybe from equivalence check

---
 src/VeriFuzz/Fuzz.hs         |  2 +-
 src/VeriFuzz/Sim/Template.hs | 11 +++++------
 src/VeriFuzz/Sim/Yosys.hs    | 26 ++++++++++----------------
 3 files changed, 16 insertions(+), 23 deletions(-)

(limited to 'src/VeriFuzz')

diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs
index 77f728a..8408fbb 100644
--- a/src/VeriFuzz/Fuzz.hs
+++ b/src/VeriFuzz/Fuzz.hs
@@ -155,7 +155,7 @@ equivalence src = do
                 cp (fromText ".." </> fromText (toText b) </> synthOutput b)
                     $ synthOutput b
                 writefile "rtl.v" $ genSource src
-            runEquiv a (Just b) src
+            runEquiv a b src
         where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b
 
 fuzz :: MonadFuzz m => Gen SourceInfo -> Config -> Fuzz m FuzzReport
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
 |]
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs
index c432afe..07125df 100644
--- a/src/VeriFuzz/Sim/Yosys.hs
+++ b/src/VeriFuzz/Sim/Yosys.hs
@@ -75,16 +75,11 @@ runSynthYosys sim (SourceInfo _ src) = (<?> SynthFail) . liftSh $ do
     inp  = toTextIgnore inpf
     out  = toTextIgnore $ synthOutput sim
 
-runMaybeSynth :: (Synthesiser a) => Maybe a -> SourceInfo -> ResultSh ()
-runMaybeSynth (Just sim) srcInfo = runSynth sim srcInfo
-runMaybeSynth Nothing (SourceInfo _ src) =
-    liftSh . writefile "rtl.v" $ genSource src
-
 runEquivYosys
     :: (Synthesiser a, Synthesiser b)
     => Yosys
     -> a
-    -> Maybe b
+    -> b
     -> SourceInfo
     -> ResultSh ()
 runEquivYosys yosys sim1 sim2 srcInfo = do
@@ -97,21 +92,20 @@ runEquivYosys yosys sim1 sim2 srcInfo = do
             ^. mainModule
         writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
     runSynth sim1 srcInfo
-    runMaybeSynth sim2 srcInfo
+    runSynth sim2 srcInfo
     liftSh $ do
         logger "Yosys: equivalence check"
         run_ (yosysPath yosys) [toTextIgnore checkFile]
         logger "Yosys: equivalence done"
   where
     checkFile =
-        fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|]
+        fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]
 
-runEquiv
-    :: (Synthesiser a, Synthesiser b)
-    => a
-    -> Maybe b
-    -> SourceInfo
-    -> ResultSh ()
+runEquiv :: (Synthesiser a, Synthesiser b)
+         => a
+         -> b
+         -> SourceInfo
+         -> ResultSh ()
 runEquiv sim1 sim2 srcInfo = do
     dir <- liftSh pwd
     liftSh $ do
@@ -121,8 +115,8 @@ runEquiv sim1 sim2 srcInfo = do
             .  makeTopAssert
             $  srcInfo
             ^. mainModule
-        replaceMods (synthOutput sim1)               "_1" srcInfo
-        replaceMods (maybe "rtl.v" synthOutput sim2) "_2" srcInfo
+        replaceMods (synthOutput sim1) "_1" srcInfo
+        replaceMods (synthOutput sim2) "_2" srcInfo
         writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo
     liftSh $ logger "Running SymbiYosys"
     execute_ EquivFail dir "symbiyosys" "sby" ["proof.sby"]
-- 
cgit