From feaf70849a93c60379104a6b4c1e7ee05afab340 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 19 May 2021 22:13:22 +0100
Subject: Add new simulation for EMI

---
 src/Verismith/Fuzz.hs        | 46 ++++++++++++++++++------------
 src/Verismith/Tool/Icarus.hs | 67 +++++++++++++++++++++++++++++++++++++++++---
 2 files changed, 91 insertions(+), 22 deletions(-)

diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs
index 42c667e..c2c30a9 100644
--- a/src/Verismith/Fuzz.hs
+++ b/src/Verismith/Fuzz.hs
@@ -324,10 +324,6 @@ equivalence src = do
       where
         dir = fromText $ "equiv_" <> toText a <> "_" <> toText b
 
-equivalenceEMI :: (MonadBaseControl IO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m ()
-equivalenceEMI src = do
-  datadir <- fmap _fuzzDataDir askOpts
-
 simulation :: (MonadIO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m ()
 simulation src = do
   datadir <- fmap _fuzzDataDir askOpts
@@ -365,6 +361,31 @@ simulation src = do
       where
         dir = fromText $ "countereg_sim_" <> toText a
 
+simulationEMI :: (MonadIO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m ()
+simulationEMI src = do
+  datadir <- fmap _fuzzDataDir askOpts
+  synth <- passedSynthesis
+  counterEgs <- failEquivWithIdentityCE
+  vals <- liftIO $ generateByteString Nothing 32 20
+  ident <- liftSh $ sim datadir vals Nothing defaultIdentitySynth
+  resTimes <- liftSh $ mapM (sim datadir vals (justPass $ snd ident)) synth
+  fuzzSimResults .= toSimResult defaultIcarusSim vals synth resTimes
+  liftSh
+    . inspect
+    $ (\(_, r) -> bimap show (T.unpack . T.take 10 . showBS) r)
+      <$> (ident : resTimes)
+  where
+    sim datadir b i a = toolRun ("simulation for " <> toText a) . runResultT $ do
+      make dir
+      pop dir $ do
+        liftSh $ do
+          cp (fromText ".." </> fromText (toText a) </> synthOutput a) $
+            synthOutput a
+          writefile "rtl.v" $ genSource src
+        runSimIc datadir defaultIcarus a src b i
+      where
+        dir = fromText $ "countereg_sim_" <> toText a
+
 failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult]
 failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get
   where
@@ -610,24 +631,13 @@ fuzzEMI gen = do
       . propSeed
         ?~ seed'
   (tsynth, _) <- titleRun "Synthesis" $ synthesis src
-  (tequiv, _) <-
-    if (_fuzzOptsNoEquiv opts)
-      then return (0, mempty)
-      else titleRun "Equivalence Check" $ equivalenceEMI src
   (_, _) <-
     if (_fuzzOptsNoSim opts)
       then return (0, mempty)
-      else titleRun "Simulation" $ simulation src
+      else titleRun "Simulation" $ simulationEMI src
   fails <- failEquivWithIdentity
   failedSim <- failedSimulations
   synthFails <- failedSynthesis
-  redResult <-
-    whenMaybe
-      ( not (null failedSim && null fails && null synthFails)
-          && not (_fuzzOptsNoReduction opts)
-      )
-      . titleRun "Reduction"
-      $ reduction src
   state_ <- get
   currdir <- liftSh pwd
   let vi = flip view state_
@@ -639,6 +649,6 @@ fuzzEMI gen = do
           (vi fuzzSynthStatus)
           size
           tsynth
-          tequiv
-          (getTime redResult)
+          0
+          0
   return report
diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs
index 8504640..da387dc 100644
--- a/src/Verismith/Tool/Icarus.hs
+++ b/src/Verismith/Tool/Icarus.hs
@@ -12,6 +12,7 @@ module Verismith.Tool.Icarus
   ( Icarus (..),
     defaultIcarus,
     runSimIc,
+    runSimIcEMI,
     runSimIcEC,
   )
 where
@@ -175,6 +176,45 @@ tbModule bss top =
   where
     inConcat = (RegConcat . filter (/= (Id "clk")) $ (Id . fromPort <$> (top ^. modInPorts)))
 
+tbModule' :: [Identifier] -> [ByteString] -> (ModDecl ann) -> (Verilog ann)
+tbModule' ids bss top =
+  Verilog
+    [ instantiateMod top $
+        ModDecl
+          "testbench"
+          []
+          []
+          [ Initial $
+              fold
+                [ BlockAssign (Assign "clk" Nothing 0),
+                  BlockAssign (Assign inConcat Nothing 0),
+                  BlockAssign (Assign inIds Nothing 0)
+                ]
+                <> fold
+                  ( ( \r ->
+                        TimeCtrl
+                          10
+                          (Just $ BlockAssign (Assign inConcat Nothing r))
+                    )
+                      . fromInteger
+                      . fromBytes <$> bss
+                  )
+                <> (TimeCtrl 10 . Just . 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"]
+          ]
+          []
+    ]
+  where
+    inConcat = (RegConcat
+                . filter (flip notElem $ fmap Id ids)
+                . filter (/= (Id "clk"))
+                $ (Id . fromPort <$> (top ^. modInPorts)))
+    inIds = RegConcat $ fmap Id ids
+
 counterTestBench :: CounterEg -> (ModDecl ann) -> (Verilog ann)
 counterTestBench (CounterEg _ states) m = tbModule filtered m
   where
@@ -230,16 +270,35 @@ runSimIc ::
   -- | Synthesis tool to be tested.
   b ->
   -- | Original generated program to test.
-  (SourceInfo ann) ->
+  SourceInfo ann ->
   -- | Test vectors to be passed as inputs to the generated Verilog.
   [ByteString] ->
-  -- | What the correct output should be. If
-  -- 'Nothing' is passed, then just return 'Pass
-  -- ByteString' with the answer.
+  -- | What the correct output should be. If 'Nothing' is passed, then just return 'Pass ByteString'
+  -- with the answer.
   Maybe ByteString ->
   ResultSh ByteString
 runSimIc = runSimIc' tbModule
 
+runSimIcEMI ::
+  (Synthesiser b, Show ann) =>
+  -- | EMI Ids
+  [Identifier] ->
+  -- | Data directory.
+  FilePath ->
+  -- | Icarus simulator.
+  Icarus ->
+  -- | Synthesis tool to be tested.
+  b ->
+  -- | Original generated program to test.
+  SourceInfo ann ->
+  -- | Test vectors to be passed as inputs to the generated Verilog.
+  [ByteString] ->
+  -- | What the correct output should be. If 'Nothing' is passed, then just return 'Pass ByteString'
+  -- with the answer.
+  Maybe ByteString ->
+  ResultSh ByteString
+runSimIcEMI ids = runSimIc' (tbModule' ids)
+
 runSimIcEC ::
   (Synthesiser b, Show ann) =>
   FilePath ->
-- 
cgit