From 238ef567f11c0f07f6b9834ef2199117485ba273 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 21 May 2019 15:24:45 +0100
Subject: Remove logging from within tools

---
 src/VeriFuzz/Sim/Icarus.hs  |  2 --
 src/VeriFuzz/Sim/Quartus.hs |  5 +----
 src/VeriFuzz/Sim/Vivado.hs  |  2 --
 src/VeriFuzz/Sim/XST.hs     | 17 ++++++-----------
 src/VeriFuzz/Sim/Yosys.hs   | 10 ++--------
 5 files changed, 9 insertions(+), 27 deletions(-)

(limited to 'src/VeriFuzz/Sim')

diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs
index 423d51b..6c5751a 100644
--- a/src/VeriFuzz/Sim/Icarus.hs
+++ b/src/VeriFuzz/Sim/Icarus.hs
@@ -117,10 +117,8 @@ runSimIcarusWithFile
     :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString
 runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do
     dir <- pwd
-    logger "Icarus: Compile"
     logCommand_ dir "icarus"
         $ run (icarusPath sim) ["-o", "main", toTextIgnore f]
-    logger "Icarus: Run"
     B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logCommand
         dir
         "vvp"
diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs
index ece00eb..4007004 100644
--- a/src/VeriFuzz/Sim/Quartus.hs
+++ b/src/VeriFuzz/Sim/Quartus.hs
@@ -52,9 +52,7 @@ runSynthQuartus :: Quartus -> SourceInfo -> ResultSh ()
 runSynthQuartus sim (SourceInfo top src) = do
     dir <- liftSh pwd
     let ex = execute_ SynthFail dir "quartus"
-    liftSh $ do
-        writefile inpf $ genSource src
-        logger "Running Quartus synthesis"
+    liftSh . writefile inpf $ genSource src
     ex (exec "quartus_map")
        [top, "--source=" <> toTextIgnore inpf, "--family=Cyclone V"]
     ex (exec "quartus_fit") [top, "--part=5CGTFD9E5F35C7N"]
@@ -68,7 +66,6 @@ runSynthQuartus sim (SourceInfo top src) = do
             , "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;"
             , toTextIgnore $ synthOutput sim
             ]
-        logger "Quartus synthesis done"
   where
     inpf = "rtl.v"
     exec s = maybe (fromText s) (</> fromText s) $ quartusBin sim
diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs
index ee67a78..9f48188 100644
--- a/src/VeriFuzz/Sim/Vivado.hs
+++ b/src/VeriFuzz/Sim/Vivado.hs
@@ -57,12 +57,10 @@ runSynthVivado sim (SourceInfo top src) = do
             sim
         writefile "rtl.v" $ genSource src
         run_ "sed" ["s/^module/(* use_dsp=\"no\" *) module/;", "-i", "rtl.v"]
-        logger "Vivado: run"
     let exec_ n = execute_
             SynthFail
             dir
             "vivado"
             (maybe (fromText n) (</> fromText n) $ vivadoBin sim)
     exec_ "vivado" ["-mode", "batch", "-source", toTextIgnore vivadoTcl]
-    liftSh $ logger "Vivado: done"
     where vivadoTcl = fromText ("vivado_" <> top) <.> "tcl"
diff --git a/src/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs
index 11be094..71a4e1b 100644
--- a/src/VeriFuzz/Sim/XST.hs
+++ b/src/VeriFuzz/Sim/XST.hs
@@ -64,9 +64,7 @@ runSynthXST sim (SourceInfo top src) = do
         writefile xstFile $ xstSynthConfig top
         writefile prjFile [st|verilog work "rtl.v"|]
         writefile "rtl.v" $ genSource src
-        logger "XST: run"
     exec "xst" ["-ifn", toTextIgnore xstFile]
-    liftSh $ logger "XST: netgen"
     exec
         "netgen"
         [ "-w"
@@ -75,15 +73,12 @@ runSynthXST sim (SourceInfo top src) = do
         , toTextIgnore $ modFile <.> "ngc"
         , toTextIgnore $ synthOutput sim
         ]
-    liftSh $ do
-        logger "XST: clean"
-        noPrint $ run_
-            "sed"
-            [ "-i"
-            , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;"
-            , toTextIgnore $ synthOutput sim
-            ]
-        logger "XST: done"
+    liftSh . noPrint $ run_
+        "sed"
+        [ "-i"
+        , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;"
+        , toTextIgnore $ synthOutput sim
+        ]
   where
     modFile = fromText top
     xstFile = modFile <.> "xst"
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs
index 3081a65..472af1f 100644
--- a/src/VeriFuzz/Sim/Yosys.hs
+++ b/src/VeriFuzz/Sim/Yosys.hs
@@ -65,13 +65,11 @@ runSynthYosys :: Yosys -> SourceInfo -> ResultSh ()
 runSynthYosys sim (SourceInfo _ src) = (<?> SynthFail) . liftSh $ do
     dir <- pwd
     writefile inpf $ genSource src
-    logger "Yosys: synthesis"
     logCommand_ dir "yosys" $ timeout
         (yosysPath sim)
         [ "-p"
         , "read -formal " <> inp <> "; synth; write_verilog -noattr " <> out
         ]
-    logger "Yosys: synthesis done"
   where
     inpf = "rtl.v"
     inp  = toTextIgnore inpf
@@ -95,10 +93,7 @@ runEquivYosys yosys sim1 sim2 srcInfo = do
         writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
     runSynth sim1 srcInfo
     runSynth sim2 srcInfo
-    liftSh $ do
-        logger "Yosys: equivalence check"
-        run_ (yosysPath yosys) [toTextIgnore checkFile]
-        logger "Yosys: equivalence done"
+    liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile]
     where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]
 
 runEquiv
@@ -115,12 +110,11 @@ runEquiv sim1 sim2 srcInfo = do
         replaceMods (synthOutput sim1) "_1" srcInfo
         replaceMods (synthOutput sim2) "_2" srcInfo
         writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo
-    liftSh $ logger "Running SymbiYosys"
     e <- liftSh $ do
         exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
         lastExitCode
     case e of
-        0   -> liftSh $ logger "SymbiYosys equivalence check passed"
+        0   -> ResultT . return $ Pass ()
         2   -> ResultT . return $ Fail EquivFail
         124 -> ResultT . return $ Fail TimeoutError
         _   -> ResultT . return $ Fail EquivError
-- 
cgit 


From e4181b3f672040c2478d00ce4c9cd9b0c2cde473 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 25 May 2019 21:10:45 +0100
Subject: Add timeout error to synthesisers

---
 src/VeriFuzz/Sim/Internal.hs | 21 ++++++++++++++-------
 src/VeriFuzz/Sim/Yosys.hs    | 11 ++++++-----
 2 files changed, 20 insertions(+), 12 deletions(-)

(limited to 'src/VeriFuzz/Sim')

diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
index 5c58e1a..d35ad86 100644
--- a/src/VeriFuzz/Sim/Internal.hs
+++ b/src/VeriFuzz/Sim/Internal.hs
@@ -188,21 +188,28 @@ logCommand_ :: FilePath -> Text -> Sh a -> Sh ()
 logCommand_ fp name = void . logCommand fp name
 
 execute
-    :: (MonadSh m, Monad m, Monoid a)
-    => a
+    :: (MonadSh m, Monad m)
+    => Failed
     -> FilePath
     -> Text
     -> FilePath
     -> [Text]
-    -> ResultT a m Text
-execute f dir name e = annotate f . liftSh . logCommand dir name . timeout e
+    -> ResultT Failed m Text
+execute f dir name e cs = do
+    (res, exitCode) <- liftSh $ do
+        res <- errExit False . logCommand dir name $ timeout e cs
+        (,) res <$> lastExitCode
+    case exitCode of
+        0   -> ResultT . return $ Pass res
+        124 -> ResultT . return $ Fail TimeoutError
+        _   -> ResultT . return $ Fail f
 
 execute_
-    :: (MonadSh m, Monad m, Monoid a)
-    => a
+    :: (MonadSh m, Monad m)
+    => Failed
     -> FilePath
     -> Text
     -> FilePath
     -> [Text]
-    -> ResultT a m ()
+    -> ResultT Failed m ()
 execute_ a b c d = void . execute a b c d
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs
index 472af1f..3729a1e 100644
--- a/src/VeriFuzz/Sim/Yosys.hs
+++ b/src/VeriFuzz/Sim/Yosys.hs
@@ -62,11 +62,12 @@ yosysPath :: Yosys -> FilePath
 yosysPath sim = maybe (fromText "yosys") (</> fromText "yosys") $ yosysBin sim
 
 runSynthYosys :: Yosys -> SourceInfo -> ResultSh ()
-runSynthYosys sim (SourceInfo _ src) = (<?> SynthFail) . liftSh $ do
-    dir <- pwd
-    writefile inpf $ genSource src
-    logCommand_ dir "yosys" $ timeout
-        (yosysPath sim)
+runSynthYosys sim (SourceInfo _ src) = do
+    dir <- liftSh $ do
+        dir' <- pwd
+        writefile inpf $ genSource src
+        return dir'
+    execute_ SynthFail dir "yosys" (yosysPath sim)
         [ "-p"
         , "read -formal " <> inp <> "; synth; write_verilog -noattr " <> out
         ]
-- 
cgit 


From 87b0f99853072ad1b17b380726b3807f6f4f91d4 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 26 May 2019 16:25:40 +0100
Subject: Add changes to work with older Vivado

---
 src/VeriFuzz/Sim/Vivado.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/VeriFuzz/Sim')

diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs
index 9f48188..90eed2d 100644
--- a/src/VeriFuzz/Sim/Vivado.hs
+++ b/src/VeriFuzz/Sim/Vivado.hs
@@ -56,7 +56,7 @@ runSynthVivado sim (SourceInfo top src) = do
         writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput
             sim
         writefile "rtl.v" $ genSource src
-        run_ "sed" ["s/^module/(* use_dsp=\"no\" *) module/;", "-i", "rtl.v"]
+        run_ "sed" ["s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;", "-i", "rtl.v"]
     let exec_ n = execute_
             SynthFail
             dir
-- 
cgit 


From 12a74a1841ffb5842af029ffcce77c3e765e00f8 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 2 Jun 2019 12:54:35 +0100
Subject: Add fix to synthesise correctly with Quartus without MAC

---
 src/VeriFuzz/Sim/Quartus.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/VeriFuzz/Sim')

diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs
index 4007004..a099495 100644
--- a/src/VeriFuzz/Sim/Quartus.hs
+++ b/src/VeriFuzz/Sim/Quartus.hs
@@ -53,9 +53,10 @@ runSynthQuartus sim (SourceInfo top src) = do
     dir <- liftSh pwd
     let ex = execute_ SynthFail dir "quartus"
     liftSh . writefile inpf $ genSource src
+    liftSh . noPrint $ run_ "sed" ["-i", "s/^module/(* multstyle = \"logic\" *) module/;", toTextIgnore inpf]
     ex (exec "quartus_map")
        [top, "--source=" <> toTextIgnore inpf, "--family=Cyclone V"]
-    ex (exec "quartus_fit") [top, "--part=5CGTFD9E5F35C7N"]
+    ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"]
     ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"]
     liftSh $ do
         cp (fromText "simulation/vcs" </> fromText top <.> "vo")
-- 
cgit 


From 720fa7a822a077458cf0b29e9dcdc754a881e8bd Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 5 Jun 2019 13:52:20 +0100
Subject: Format all files

---
 src/VeriFuzz/Sim/Quartus.hs | 7 ++++++-
 src/VeriFuzz/Sim/Vivado.hs  | 7 ++++++-
 src/VeriFuzz/Sim/Yosys.hs   | 6 +++++-
 3 files changed, 17 insertions(+), 3 deletions(-)

(limited to 'src/VeriFuzz/Sim')

diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs
index a099495..4217abb 100644
--- a/src/VeriFuzz/Sim/Quartus.hs
+++ b/src/VeriFuzz/Sim/Quartus.hs
@@ -53,7 +53,12 @@ runSynthQuartus sim (SourceInfo top src) = do
     dir <- liftSh pwd
     let ex = execute_ SynthFail dir "quartus"
     liftSh . writefile inpf $ genSource src
-    liftSh . noPrint $ run_ "sed" ["-i", "s/^module/(* multstyle = \"logic\" *) module/;", toTextIgnore inpf]
+    liftSh . noPrint $ run_
+        "sed"
+        [ "-i"
+        , "s/^module/(* multstyle = \"logic\" *) module/;"
+        , toTextIgnore inpf
+        ]
     ex (exec "quartus_map")
        [top, "--source=" <> toTextIgnore inpf, "--family=Cyclone V"]
     ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"]
diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs
index 90eed2d..a4feb07 100644
--- a/src/VeriFuzz/Sim/Vivado.hs
+++ b/src/VeriFuzz/Sim/Vivado.hs
@@ -56,7 +56,12 @@ runSynthVivado sim (SourceInfo top src) = do
         writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput
             sim
         writefile "rtl.v" $ genSource src
-        run_ "sed" ["s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;", "-i", "rtl.v"]
+        run_
+            "sed"
+            [ "s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;"
+            , "-i"
+            , "rtl.v"
+            ]
     let exec_ n = execute_
             SynthFail
             dir
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs
index 3729a1e..02a00d5 100644
--- a/src/VeriFuzz/Sim/Yosys.hs
+++ b/src/VeriFuzz/Sim/Yosys.hs
@@ -67,7 +67,11 @@ runSynthYosys sim (SourceInfo _ src) = do
         dir' <- pwd
         writefile inpf $ genSource src
         return dir'
-    execute_ SynthFail dir "yosys" (yosysPath sim)
+    execute_
+        SynthFail
+        dir
+        "yosys"
+        (yosysPath sim)
         [ "-p"
         , "read -formal " <> inp <> "; synth; write_verilog -noattr " <> out
         ]
-- 
cgit 


From a3cf56b7e2edef87181c534dea099a884ac99306 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 17 Jun 2019 16:13:00 +0100
Subject: Add part of the simulator implementation

---
 src/VeriFuzz/Sim/Icarus.hs   | 40 ++++++++++++++++++++++++++++++++++++++++
 src/VeriFuzz/Sim/Template.hs | 24 +++++++++++++++++++-----
 2 files changed, 59 insertions(+), 5 deletions(-)

(limited to 'src/VeriFuzz/Sim')

diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs
index 6c5751a..6df2cf7 100644
--- a/src/VeriFuzz/Sim/Icarus.hs
+++ b/src/VeriFuzz/Sim/Icarus.hs
@@ -123,3 +123,43 @@ runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do
         dir
         "vvp"
         (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"])
+
+runSimIc
+    :: (Synthesiser a) => a -> SourceInfo -> [ByteString] -> ResultSh ByteString
+runSimIc sim1 srcInfo bss = do
+    dir <- liftSh pwd
+    let top = srcInfo ^. mainModule
+    let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts)))
+    let tb = ModDecl
+             "testbench"
+             []
+             []
+             [ Initial
+               $ fold [ BlockAssign (Assign "clk" Nothing 0)
+                      , BlockAssign (Assign  inConcat Nothing 0)
+                      ]
+               <> (SysTaskEnable $ Task "finish" [])
+             , Always . TimeCtrl 5 $ BlockAssign (Assign "clk" Nothing (UnNot (Id "clk")))
+             , Always . EventCtrl (EPosEdge "clk") $ SysTaskEnable $ Task "strobe" ["%b", Id "y"]
+             ]
+             []
+    liftSh $ do
+        writefile "top.v"
+            .  genSource
+            .  initMod
+            .  makeTopAssert
+            $  srcInfo
+            ^. mainModule
+        replaceMods (synthOutput sim1) "_1" srcInfo
+        replaceMods (synthOutput sim2) "_2" srcInfo
+        writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo
+    e <- liftSh $ do
+        exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
+        lastExitCode
+    case e of
+        0   -> ResultT . return $ Pass ()
+        2   -> ResultT . return $ Fail EquivFail
+        124 -> ResultT . return $ Fail TimeoutError
+        _   -> ResultT . return $ Fail EquivError
+  where
+    exe dir name e = void . errExit False . logCommand dir name . timeout e
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
index 4aa07f6..913b220 100644
--- a/src/VeriFuzz/Sim/Template.hs
+++ b/src/VeriFuzz/Sim/Template.hs
@@ -18,17 +18,19 @@ module VeriFuzz.Sim.Template
     , xstSynthConfig
     , vivadoSynthConfig
     , sbyConfig
+    , icarusTestbench
     )
 where
 
-import           Control.Lens          ((^..))
-import           Data.Text             (Text)
-import qualified Data.Text             as T
-import           Prelude               hiding (FilePath)
+import           Control.Lens             ((^..))
+import           Data.Text                (Text)
+import qualified Data.Text                as T
+import           Prelude                  hiding (FilePath)
 import           Shelly
-import           Text.Shakespeare.Text (st)
+import           Text.Shakespeare.Text    (st)
 import           VeriFuzz.Sim.Internal
 import           VeriFuzz.Verilog.AST
+import           VeriFuzz.Verilog.CodeGen
 
 rename :: Text -> [Text] -> Text
 rename end entries =
@@ -117,3 +119,15 @@ top.v
         .   fromText
         <$> deps
     readL = T.intercalate "\n" $ mappend "read -formal " <$> deps
+
+icarusTestbench :: (Synthesiser a) => Verilog -> a -> Text
+icarusTestbench t synth1 = [st|
+`include "data/cells_cmos.v"
+`include "data/cells_cyclone_v.v"
+`include "data/cells_verific.v"
+`include "data/cells_xilinx_7.v"
+`include "data/cells_yosys.v"
+`include "#{synthOutput synth1}"
+
+#{genSource t}
+|]
-- 
cgit 


From 24cf9ce5bf673615ebe36f5ab5d0ff7685dfada6 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 25 Jun 2019 22:32:21 +0100
Subject: Add back the simulation

---
 src/VeriFuzz/Sim/Icarus.hs   | 52 ++++++++++++++++++++++----------------------
 src/VeriFuzz/Sim/Template.hs |  2 +-
 2 files changed, 27 insertions(+), 27 deletions(-)

(limited to 'src/VeriFuzz/Sim')

diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs
index 6df2cf7..a5a3227 100644
--- a/src/VeriFuzz/Sim/Icarus.hs
+++ b/src/VeriFuzz/Sim/Icarus.hs
@@ -13,18 +13,21 @@ Icarus verilog module.
 module VeriFuzz.Sim.Icarus
     ( Icarus(..)
     , defaultIcarus
+    , runSimIc
     )
 where
 
 import           Control.DeepSeq           (NFData, rnf, rwhnf)
 import           Control.Lens
+import           Control.Monad             (void)
 import           Crypto.Hash               (Digest, hash)
 import           Crypto.Hash.Algorithms    (SHA256)
-import           Data.Binary               (encode)
+import           Data.Binary               (decode, encode)
+import           Data.Bits
 import qualified Data.ByteArray            as BA (convert)
 import           Data.ByteString           (ByteString)
 import qualified Data.ByteString           as B
-import           Data.ByteString.Lazy      (toStrict)
+import           Data.ByteString.Lazy      (fromStrict, toStrict)
 import qualified Data.ByteString.Lazy      as L (ByteString)
 import           Data.Char                 (digitToInt)
 import           Data.Foldable             (fold)
@@ -37,6 +40,7 @@ import           Prelude                   hiding (FilePath)
 import           Shelly
 import           Shelly.Lifted             (liftSh)
 import           VeriFuzz.Sim.Internal
+import           VeriFuzz.Sim.Template
 import           VeriFuzz.Verilog.AST
 import           VeriFuzz.Verilog.BitVec
 import           VeriFuzz.Verilog.CodeGen
@@ -124,13 +128,18 @@ runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do
         "vvp"
         (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"])
 
+fromBytes :: ByteString -> Integer
+fromBytes = B.foldl' f 0
+  where
+    f a b = a `shiftL` 8 .|. fromIntegral b
+
 runSimIc
-    :: (Synthesiser a) => a -> SourceInfo -> [ByteString] -> ResultSh ByteString
-runSimIc sim1 srcInfo bss = do
+    :: (Synthesiser b) => Icarus -> b -> SourceInfo -> [ByteString] -> ResultSh ByteString
+runSimIc sim1 synth1 srcInfo bss = do
     dir <- liftSh pwd
     let top = srcInfo ^. mainModule
     let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts)))
-    let tb = ModDecl
+    let tb = instantiateMod top $ ModDecl
              "testbench"
              []
              []
@@ -138,28 +147,19 @@ runSimIc sim1 srcInfo bss = do
                $ fold [ BlockAssign (Assign "clk" Nothing 0)
                       , BlockAssign (Assign  inConcat Nothing 0)
                       ]
-               <> (SysTaskEnable $ Task "finish" [])
-             , Always . TimeCtrl 5 $ BlockAssign (Assign "clk" Nothing (UnNot (Id "clk")))
-             , Always . EventCtrl (EPosEdge "clk") $ SysTaskEnable $ Task "strobe" ["%b", Id "y"]
+                 <> fold ((\r -> TimeCtrl 10 (Just $ BlockAssign (Assign inConcat Nothing r)))
+                     . fromInteger . fromBytes <$> bss)
+                 <> (SysTaskEnable $ Task "finish" [])
+             , Always . TimeCtrl 5 . Just $ BlockAssign (Assign "clk" Nothing (UnOp UnNot (Id "clk")))
+             , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task "strobe" ["%b", Id "y"]
              ]
              []
-    liftSh $ do
-        writefile "top.v"
-            .  genSource
-            .  initMod
-            .  makeTopAssert
-            $  srcInfo
-            ^. mainModule
-        replaceMods (synthOutput sim1) "_1" srcInfo
-        replaceMods (synthOutput sim2) "_2" srcInfo
-        writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo
-    e <- liftSh $ do
-        exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
-        lastExitCode
-    case e of
-        0   -> ResultT . return $ Pass ()
-        2   -> ResultT . return $ Fail EquivFail
-        124 -> ResultT . return $ Fail TimeoutError
-        _   -> ResultT . return $ Fail EquivError
+
+    liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1
+    liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"]
+    liftSh $ B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logCommand
+        dir
+        "vvp"
+        (runFoldLines (mempty :: ByteString) callback (vvpPath sim1) ["main"])
   where
     exe dir name e = void . errExit False . logCommand dir name . timeout e
diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs
index 913b220..3be6558 100644
--- a/src/VeriFuzz/Sim/Template.hs
+++ b/src/VeriFuzz/Sim/Template.hs
@@ -127,7 +127,7 @@ icarusTestbench t synth1 = [st|
 `include "data/cells_verific.v"
 `include "data/cells_xilinx_7.v"
 `include "data/cells_yosys.v"
-`include "#{synthOutput synth1}"
+`include "#{toTextIgnore $ synthOutput synth1}"
 
 #{genSource t}
 |]
-- 
cgit 


From bb697f8bc7b593e5aabb43505f686e6503b7726f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 29 Jun 2019 20:21:43 +0100
Subject: Fix pedantic warnings

---
 src/VeriFuzz/Sim/Icarus.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/VeriFuzz/Sim')

diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs
index a5a3227..7f90814 100644
--- a/src/VeriFuzz/Sim/Icarus.hs
+++ b/src/VeriFuzz/Sim/Icarus.hs
@@ -22,12 +22,12 @@ import           Control.Lens
 import           Control.Monad             (void)
 import           Crypto.Hash               (Digest, hash)
 import           Crypto.Hash.Algorithms    (SHA256)
-import           Data.Binary               (decode, encode)
+import           Data.Binary               (encode)
 import           Data.Bits
 import qualified Data.ByteArray            as BA (convert)
 import           Data.ByteString           (ByteString)
 import qualified Data.ByteString           as B
-import           Data.ByteString.Lazy      (fromStrict, toStrict)
+import           Data.ByteString.Lazy      (toStrict)
 import qualified Data.ByteString.Lazy      as L (ByteString)
 import           Data.Char                 (digitToInt)
 import           Data.Foldable             (fold)
-- 
cgit 


From d32f4cc45bc8c0670fb788b1fcd4c2f2b15fa094 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 29 Jun 2019 20:33:59 +0100
Subject: Format files

---
 src/VeriFuzz/Sim/Icarus.hs   | 116 +++++++++++++++++++++++++++----------------
 src/VeriFuzz/Sim/Identity.hs |  15 ++++--
 src/VeriFuzz/Sim/Internal.hs |  32 +++++++-----
 src/VeriFuzz/Sim/Quartus.hs  |  13 +++--
 src/VeriFuzz/Sim/Vivado.hs   |  13 +++--
 src/VeriFuzz/Sim/XST.hs      |  15 ++++--
 src/VeriFuzz/Sim/Yosys.hs    |  17 ++++---
 7 files changed, 141 insertions(+), 80 deletions(-)

(limited to 'src/VeriFuzz/Sim')

diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs
index 7f90814..8e62136 100644
--- a/src/VeriFuzz/Sim/Icarus.hs
+++ b/src/VeriFuzz/Sim/Icarus.hs
@@ -17,28 +17,35 @@ module VeriFuzz.Sim.Icarus
     )
 where
 
-import           Control.DeepSeq           (NFData, rnf, rwhnf)
+import           Control.DeepSeq                ( NFData
+                                                , rnf
+                                                , rwhnf
+                                                )
 import           Control.Lens
-import           Control.Monad             (void)
-import           Crypto.Hash               (Digest, hash)
-import           Crypto.Hash.Algorithms    (SHA256)
-import           Data.Binary               (encode)
+import           Control.Monad                  ( void )
+import           Crypto.Hash                    ( Digest
+                                                , hash
+                                                )
+import           Crypto.Hash.Algorithms         ( SHA256 )
+import           Data.Binary                    ( encode )
 import           Data.Bits
-import qualified Data.ByteArray            as BA (convert)
-import           Data.ByteString           (ByteString)
-import qualified Data.ByteString           as B
-import           Data.ByteString.Lazy      (toStrict)
-import qualified Data.ByteString.Lazy      as L (ByteString)
-import           Data.Char                 (digitToInt)
-import           Data.Foldable             (fold)
-import           Data.List                 (transpose)
-import           Data.Maybe                (listToMaybe)
-import           Data.Text                 (Text)
-import qualified Data.Text                 as T
-import           Numeric                   (readInt)
-import           Prelude                   hiding (FilePath)
+import qualified Data.ByteArray                as BA
+                                                ( convert )
+import           Data.ByteString                ( ByteString )
+import qualified Data.ByteString               as B
+import           Data.ByteString.Lazy           ( toStrict )
+import qualified Data.ByteString.Lazy          as L
+                                                ( ByteString )
+import           Data.Char                      ( digitToInt )
+import           Data.Foldable                  ( fold )
+import           Data.List                      ( transpose )
+import           Data.Maybe                     ( listToMaybe )
+import           Data.Text                      ( Text )
+import qualified Data.Text                     as T
+import           Numeric                        ( readInt )
+import           Prelude                 hiding ( FilePath )
 import           Shelly
-import           Shelly.Lifted             (liftSh)
+import           Shelly.Lifted                  ( liftSh )
 import           VeriFuzz.Sim.Internal
 import           VeriFuzz.Sim.Template
 import           VeriFuzz.Verilog.AST
@@ -129,37 +136,60 @@ runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do
         (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"])
 
 fromBytes :: ByteString -> Integer
-fromBytes = B.foldl' f 0
-  where
-    f a b = a `shiftL` 8 .|. fromIntegral b
+fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b
 
 runSimIc
-    :: (Synthesiser b) => Icarus -> b -> SourceInfo -> [ByteString] -> ResultSh ByteString
+    :: (Synthesiser b)
+    => Icarus
+    -> b
+    -> SourceInfo
+    -> [ByteString]
+    -> ResultSh ByteString
 runSimIc sim1 synth1 srcInfo bss = do
     dir <- liftSh pwd
-    let top = srcInfo ^. mainModule
+    let top      = srcInfo ^. mainModule
     let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts)))
-    let tb = instantiateMod top $ ModDecl
-             "testbench"
-             []
-             []
-             [ Initial
-               $ fold [ BlockAssign (Assign "clk" Nothing 0)
-                      , BlockAssign (Assign  inConcat Nothing 0)
-                      ]
-                 <> fold ((\r -> TimeCtrl 10 (Just $ BlockAssign (Assign inConcat Nothing r)))
-                     . fromInteger . fromBytes <$> bss)
-                 <> (SysTaskEnable $ Task "finish" [])
-             , Always . TimeCtrl 5 . Just $ BlockAssign (Assign "clk" Nothing (UnOp UnNot (Id "clk")))
-             , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task "strobe" ["%b", Id "y"]
-             ]
-             []
+    let
+        tb = instantiateMod top $ ModDecl
+            "testbench"
+            []
+            []
+            [ Initial
+            $  fold
+                   [ BlockAssign (Assign "clk" Nothing 0)
+                   , BlockAssign (Assign inConcat Nothing 0)
+                   ]
+            <> fold
+                   (   (\r -> TimeCtrl
+                           10
+                           (Just $ BlockAssign (Assign inConcat Nothing r))
+                       )
+                   .   fromInteger
+                   .   fromBytes
+                   <$> bss
+                   )
+            <> (SysTaskEnable $ Task "finish" [])
+            , Always . TimeCtrl 5 . Just $ BlockAssign
+                (Assign "clk" Nothing (UnOp UnNot (Id "clk")))
+            , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task
+                "strobe"
+                ["%b", Id "y"]
+            ]
+            []
 
     liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1
     liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"]
-    liftSh $ B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logCommand
-        dir
-        "vvp"
-        (runFoldLines (mempty :: ByteString) callback (vvpPath sim1) ["main"])
+    liftSh
+        $   B.take 8
+        .   BA.convert
+        .   (hash :: ByteString -> Digest SHA256)
+        <$> logCommand
+                dir
+                "vvp"
+                (runFoldLines (mempty :: ByteString)
+                              callback
+                              (vvpPath sim1)
+                              ["main"]
+                )
   where
     exe dir name e = void . errExit False . logCommand dir name . timeout e
diff --git a/src/VeriFuzz/Sim/Identity.hs b/src/VeriFuzz/Sim/Identity.hs
index bfded0b..95b4097 100644
--- a/src/VeriFuzz/Sim/Identity.hs
+++ b/src/VeriFuzz/Sim/Identity.hs
@@ -16,11 +16,16 @@ module VeriFuzz.Sim.Identity
     )
 where
 
-import           Control.DeepSeq          (NFData, rnf, rwhnf)
-import           Data.Text                (Text, unpack)
-import           Prelude                  hiding (FilePath)
-import           Shelly                   (FilePath)
-import           Shelly.Lifted            (writefile)
+import           Control.DeepSeq                ( NFData
+                                                , rnf
+                                                , rwhnf
+                                                )
+import           Data.Text                      ( Text
+                                                , unpack
+                                                )
+import           Prelude                 hiding ( FilePath )
+import           Shelly                         ( FilePath )
+import           Shelly.Lifted                  ( writefile )
 import           VeriFuzz.Sim.Internal
 import           VeriFuzz.Verilog.AST
 import           VeriFuzz.Verilog.CodeGen
diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs
index d35ad86..a05a96f 100644
--- a/src/VeriFuzz/Sim/Internal.hs
+++ b/src/VeriFuzz/Sim/Internal.hs
@@ -40,20 +40,26 @@ module VeriFuzz.Sim.Internal
 where
 
 import           Control.Lens
-import           Control.Monad         (forM, void)
-import           Control.Monad.Catch   (throwM)
-import           Data.Bits             (shiftL)
-import           Data.ByteString       (ByteString)
-import qualified Data.ByteString       as B
-import           Data.Maybe            (catMaybes)
-import           Data.Text             (Text)
-import qualified Data.Text             as T
-import           Data.Time.Format      (defaultTimeLocale, formatTime)
-import           Data.Time.LocalTime   (getZonedTime)
-import           Prelude               hiding (FilePath)
+import           Control.Monad                  ( forM
+                                                , void
+                                                )
+import           Control.Monad.Catch            ( throwM )
+import           Data.Bits                      ( shiftL )
+import           Data.ByteString                ( ByteString )
+import qualified Data.ByteString               as B
+import           Data.Maybe                     ( catMaybes )
+import           Data.Text                      ( Text )
+import qualified Data.Text                     as T
+import           Data.Time.Format               ( defaultTimeLocale
+                                                , formatTime
+                                                )
+import           Data.Time.LocalTime            ( getZonedTime )
+import           Prelude                 hiding ( FilePath )
 import           Shelly
-import           Shelly.Lifted         (MonadSh, liftSh)
-import           System.FilePath.Posix (takeBaseName)
+import           Shelly.Lifted                  ( MonadSh
+                                                , liftSh
+                                                )
+import           System.FilePath.Posix          ( takeBaseName )
 import           VeriFuzz.Internal
 import           VeriFuzz.Result
 import           VeriFuzz.Verilog.AST
diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs
index 4217abb..e0fbba5 100644
--- a/src/VeriFuzz/Sim/Quartus.hs
+++ b/src/VeriFuzz/Sim/Quartus.hs
@@ -16,11 +16,16 @@ module VeriFuzz.Sim.Quartus
     )
 where
 
-import           Control.DeepSeq          (NFData, rnf, rwhnf)
-import           Data.Text                (Text, unpack)
-import           Prelude                  hiding (FilePath)
+import           Control.DeepSeq                ( NFData
+                                                , rnf
+                                                , rwhnf
+                                                )
+import           Data.Text                      ( Text
+                                                , unpack
+                                                )
+import           Prelude                 hiding ( FilePath )
 import           Shelly
-import           Shelly.Lifted            (liftSh)
+import           Shelly.Lifted                  ( liftSh )
 import           VeriFuzz.Sim.Internal
 import           VeriFuzz.Verilog.AST
 import           VeriFuzz.Verilog.CodeGen
diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs
index a4feb07..8697a0f 100644
--- a/src/VeriFuzz/Sim/Vivado.hs
+++ b/src/VeriFuzz/Sim/Vivado.hs
@@ -16,11 +16,16 @@ module VeriFuzz.Sim.Vivado
     )
 where
 
-import           Control.DeepSeq          (NFData, rnf, rwhnf)
-import           Data.Text                (Text, unpack)
-import           Prelude                  hiding (FilePath)
+import           Control.DeepSeq                ( NFData
+                                                , rnf
+                                                , rwhnf
+                                                )
+import           Data.Text                      ( Text
+                                                , unpack
+                                                )
+import           Prelude                 hiding ( FilePath )
 import           Shelly
-import           Shelly.Lifted            (liftSh)
+import           Shelly.Lifted                  ( liftSh )
 import           VeriFuzz.Sim.Internal
 import           VeriFuzz.Sim.Template
 import           VeriFuzz.Verilog.AST
diff --git a/src/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs
index 71a4e1b..f5faae5 100644
--- a/src/VeriFuzz/Sim/XST.hs
+++ b/src/VeriFuzz/Sim/XST.hs
@@ -18,12 +18,17 @@ module VeriFuzz.Sim.XST
     )
 where
 
-import           Control.DeepSeq          (NFData, rnf, rwhnf)
-import           Data.Text                (Text, unpack)
-import           Prelude                  hiding (FilePath)
+import           Control.DeepSeq                ( NFData
+                                                , rnf
+                                                , rwhnf
+                                                )
+import           Data.Text                      ( Text
+                                                , unpack
+                                                )
+import           Prelude                 hiding ( FilePath )
 import           Shelly
-import           Shelly.Lifted            (liftSh)
-import           Text.Shakespeare.Text    (st)
+import           Shelly.Lifted                  ( liftSh )
+import           Text.Shakespeare.Text          ( st )
 import           VeriFuzz.Sim.Internal
 import           VeriFuzz.Sim.Template
 import           VeriFuzz.Verilog.AST
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs
index 02a00d5..8f9d4a7 100644
--- a/src/VeriFuzz/Sim/Yosys.hs
+++ b/src/VeriFuzz/Sim/Yosys.hs
@@ -20,14 +20,19 @@ module VeriFuzz.Sim.Yosys
     )
 where
 
-import           Control.DeepSeq          (NFData, rnf, rwhnf)
+import           Control.DeepSeq                ( NFData
+                                                , rnf
+                                                , rwhnf
+                                                )
 import           Control.Lens
-import           Control.Monad            (void)
-import           Data.Text                (Text, unpack)
-import           Prelude                  hiding (FilePath)
+import           Control.Monad                  ( void )
+import           Data.Text                      ( Text
+                                                , unpack
+                                                )
+import           Prelude                 hiding ( FilePath )
 import           Shelly
-import           Shelly.Lifted            (liftSh)
-import           Text.Shakespeare.Text    (st)
+import           Shelly.Lifted                  ( liftSh )
+import           Text.Shakespeare.Text          ( st )
 import           VeriFuzz.Result
 import           VeriFuzz.Sim.Internal
 import           VeriFuzz.Sim.Template
-- 
cgit