Add part of the simulator implementation

3 files changed, 104 insertions, 5 deletions

diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs
index dadae90..3aeb0e0 100644
--- a/src/VeriFuzz/Fuzz.hs
+++ b/src/VeriFuzz/Fuzz.hs
@@ -211,6 +211,44 @@ equivalence src = do
                       runEquiv a b src
         where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b
 
+simulation :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m ()
+simulation src = do
+    synth <- passEquiv
+--    let synthComb =
+--            nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth
+    let synthComb =
+            nubBy tupEq
+                .   filter (uncurry (/=))
+                $   (,) defaultIdentitySynth
+                <$> synth
+    resTimes <- liftSh $ mapM (uncurry equiv) synthComb
+    fuzzSynthResults .= toSynthResult synthComb resTimes
+    liftSh $ inspect resTimes
+  where
+    tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a')
+    equiv a b =
+        toolRun ("equivalence check for " <> toText a <> " and " <> toText b)
+            . runResultT
+            $ do
+                  make dir
+                  pop dir $ do
+                      liftSh $ do
+                          cp
+                                  (   fromText ".."
+                                  </> fromText (toText a)
+                                  </> synthOutput a
+                                  )
+                              $ synthOutput a
+                          cp
+                                  (   fromText ".."
+                                  </> fromText (toText b)
+                                  </> synthOutput b
+                                  )
+                              $ synthOutput b
+                          writefile "rtl.v" $ genSource src
+                      runEquiv a b src
+        where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b
+
 failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult]
 failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get
   where
@@ -218,6 +256,12 @@ failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get
     withIdentity (SynthResult _ (IdentitySynth _) (Fail EquivFail) _) = True
     withIdentity _                                                    = False
 
+passEquiv :: (MonadSh m) => Fuzz m [SynthResult]
+passEquiv = filter withIdentity . _fuzzSynthResults <$> get
+  where
+    withIdentity (SynthResult _ _ (Pass _) _) = True
+    withIdentity _                            = False
+
 -- | Always reduces with respect to 'Identity'.
 reduction :: (MonadSh m) => SourceInfo -> Fuzz m ()
 reduction src = do
@@ -320,6 +364,7 @@ fuzz gen conf = do
         ?~ seed'
     (tsynth, _) <- titleRun "Synthesis" $ synthesis src
     (tequiv, _) <- titleRun "Equivalence Check" $ equivalence src
+    (tsim, _) <- titleRun "Equivalence Check" $ simulation src
     fails       <- failEquivWithIdentity
     synthFails  <- failedSynthesis
     redResult   <-
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}
+|]