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 +++++++++++++++++++++++-----------------------
 1 file changed, 26 insertions(+), 26 deletions(-)

(limited to 'src/VeriFuzz/Sim/Icarus.hs')

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
-- 
cgit