From e9e6efa72cbb21acbad196425ae03c1e321574bc Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 17 May 2021 23:10:26 +0100
Subject: Add full example of EMI testing

---
 src/Verismith/EMI.hs      | 75 +++++++++++++++++++++++++++++++++++++++++++++++
 src/Verismith/Generate.hs | 27 +++++++++++++++--
 verismith.cabal           |  1 +
 3 files changed, 101 insertions(+), 2 deletions(-)

diff --git a/src/Verismith/EMI.hs b/src/Verismith/EMI.hs
index 937a037..a96496e 100644
--- a/src/Verismith/EMI.hs
+++ b/src/Verismith/EMI.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE QuasiQuotes #-}
+
 -- |
 -- Module      : Verismith.EMI
 -- Description : Definition of the circuit graph.
@@ -9,3 +11,76 @@
 --
 -- Equivalence modulo inputs (EMI) testing.  This file should get an existing design, and spit out a
 -- modified design that is equivalent under some specific values of the extra inputs.
+module Verismith.EMI
+  ( genEMI,
+  )
+where
+
+import Control.Lens hiding (Context)
+import Control.Monad (replicateM)
+import Control.Monad.Reader
+import Control.Monad.State.Strict
+import Data.Text (Text)
+import qualified Data.Text as T
+import Hedgehog (Gen, GenT, MonadGen)
+import qualified Hedgehog as Hog
+import qualified Hedgehog.Gen as Hog
+import qualified Hedgehog.Range as Hog
+import Data.Maybe (fromMaybe)
+import Verismith.Config
+import Verismith.Internal
+import Verismith.Verilog.AST
+import Verismith.Verilog.BitVec
+import Verismith.Verilog.Eval
+import Verismith.Verilog.Internal
+import Verismith.Verilog.Mutate
+import Verismith.Generate
+
+import Verismith.Verilog.CodeGen
+import Verismith.Verilog.Quote
+import qualified Data.Text.IO as T
+
+newPort' :: Identifier -> StateGen a Port
+newPort' ident = do
+  let p = Port Wire False (Range 1 1) ident
+  emiContext . _Just . emiNewInputs %= (p :)
+  return p
+
+statementEMI :: Statement a -> StateGen a (Statement a)
+statementEMI (SeqBlock s) = do
+  s' <- statement
+  n <- newPort' "x"
+  let s'' = CondStmnt (Id "x") (Just s') Nothing
+  return $ SeqBlock (s'' : s)
+statementEMI (EventCtrl e (Just s)) = EventCtrl e . Just <$> (statementEMI s)
+statementEMI s = return s
+
+moditemEMI :: ModItem a -> StateGen a (ModItem a)
+moditemEMI (Always s) = Always <$> statementEMI s
+moditemEMI m = return m
+
+genEMI :: (ModDecl a) -> StateGen a (ModDecl a)
+genEMI (ModDecl mid outp inp itms params) = do
+  itms' <- traverse moditemEMI itms
+  return (ModDecl mid outp inp itms' params)
+
+-- | Procedural generation method for random Verilog. Uses internal 'Reader' and
+-- 'State' to keep track of the current Verilog code structure.
+proceduralEMI :: ModDecl a -> Config -> Gen (ModDecl a)
+proceduralEMI moddecl config = do
+  (mainMod, st) <-
+    Hog.resize num $
+      runStateT
+        (Hog.distributeT (runReaderT (genEMI moddecl) config))
+        context
+  let mainMod' = mainMod & modInPorts %~ (++ (st ^. emiContext . _Just . emiNewInputs))
+  return mainMod'
+  where
+    context =
+      Context [] [] [] [] [] [] 0 (confProp propStmntDepth) (confProp propModDepth) True
+        (Just (EMIContext []))
+    num = fromIntegral $ confProp propSize
+    confProp i = config ^. configProperty . i
+
+proceduralEMIIO :: ModDecl () -> Config -> IO (ModDecl ())
+proceduralEMIIO t = Hog.sample . proceduralEMI t
diff --git a/src/Verismith/Generate.hs b/src/Verismith/Generate.hs
index ecf96e3..44c53c1 100644
--- a/src/Verismith/Generate.hs
+++ b/src/Verismith/Generate.hs
@@ -20,6 +20,23 @@ module Verismith.Generate
     proceduralSrcIO,
     randomMod,
 
+    -- ** Data types
+    EMIContext(..),
+    emiNewInputs,
+    Context(..),
+    wires,
+    nonblocking,
+    blocking,
+    outofscope,
+    parameters,
+    modules,
+    nameCounter,
+    stmntDepth,
+    modDepth,
+    determinism,
+    emiContext,
+    StateGen(..),
+
     -- ** Generate Functions
     largeNum,
     wireSize,
@@ -87,6 +104,11 @@ import Verismith.Verilog.Eval
 import Verismith.Verilog.Internal
 import Verismith.Verilog.Mutate
 
+data EMIContext = EMIContext { _emiNewInputs :: [Port]
+                             }
+
+makeLenses ''EMIContext
+
 data Context a
   = Context
       { _wires :: [Port],
@@ -98,7 +120,8 @@ data Context a
         _nameCounter :: {-# UNPACK #-} !Int,
         _stmntDepth :: {-# UNPACK #-} !Int,
         _modDepth :: {-# UNPACK #-} !Int,
-        _determinism :: !Bool
+        _determinism :: !Bool,
+        _emiContext :: !(Maybe EMIContext)
       }
 
 makeLenses ''Context
@@ -744,7 +767,7 @@ procedural top config = do
   return . Verilog $ mainMod : st ^. modules
   where
     context =
-      Context [] [] [] [] [] [] 0 (confProp propStmntDepth) (confProp propModDepth) True
+      Context [] [] [] [] [] [] 0 (confProp propStmntDepth) (confProp propModDepth) True Nothing
     num = fromIntegral $ confProp propSize
     confProp i = config ^. configProperty . i
 
diff --git a/verismith.cabal b/verismith.cabal
index 35369b0..d10d28c 100644
--- a/verismith.cabal
+++ b/verismith.cabal
@@ -42,6 +42,7 @@ library
                  , Verismith.Circuit.Random
                  , Verismith.Config
                  , Verismith.CounterEg
+                 , Verismith.EMI
                  , Verismith.Fuzz
                  , Verismith.Generate
                  , Verismith.Internal
-- 
cgit