From 3e37e75f804cbf6b5ce04a427888fb0f0859660a Mon Sep 17 00:00:00 2001
From: Yann Herklotz <ymherklotz@gmail.com>
Date: Sun, 20 Jan 2019 17:46:56 +0000
Subject: [Fix #22] Fix SAT solver equivalence checking

---
 src/VeriFuzz/Verilog/AST.hs     | 12 ++++++++++--
 src/VeriFuzz/Verilog/CodeGen.hs |  8 +++++++-
 src/VeriFuzz/Verilog/Mutate.hs  | 24 +++++++++++++++++++++++-
 3 files changed, 40 insertions(+), 4 deletions(-)

(limited to 'src/VeriFuzz')

diff --git a/src/VeriFuzz/Verilog/AST.hs b/src/VeriFuzz/Verilog/AST.hs
index 1b2cb19..b02da1b 100644
--- a/src/VeriFuzz/Verilog/AST.hs
+++ b/src/VeriFuzz/Verilog/AST.hs
@@ -104,6 +104,8 @@ module VeriFuzz.Verilog.AST
   , declPort
   , ModConn(..)
   , modConn
+  , modConnName
+  , modExpr
   )
 where
 
@@ -398,11 +400,17 @@ instance QC.Arbitrary Port where
 -- @
 -- mod a(.y(y1), .x1(x11), .x2(x22));
 -- @
-newtype ModConn = ModConn { _modConn :: Expr }
-                deriving (Eq, Show, QC.Arbitrary)
+data ModConn = ModConn { _modConn :: Expr }
+             | ModConnNamed { _modConnName :: Identifier
+                            , _modExpr     :: Expr
+                            }
+             deriving (Eq, Show)
 
 makeLenses ''ModConn
 
+instance QC.Arbitrary ModConn where
+  arbitrary = ModConn <$> QC.arbitrary
+
 data Assign = Assign { _assignReg   :: LVal
                      , _assignDelay :: Maybe Delay
                      , _assignExpr  :: Expr
diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs
index 0b7f422..8b574c2 100644
--- a/src/VeriFuzz/Verilog/CodeGen.hs
+++ b/src/VeriFuzz/Verilog/CodeGen.hs
@@ -86,12 +86,18 @@ genPortDir PortInOut = "inout"
 genModuleItem :: ModItem -> Text
 genModuleItem (ModCA ca) = genContAssign ca
 genModuleItem (ModInst (Identifier i) (Identifier name) conn) =
-  i <> " " <> name <> "(" <> comma (genExpr . _modConn <$> conn) <> ")" <> ";\n"
+  i <> " " <> name <> "(" <> comma (genModConn <$> conn) <> ")" <> ";\n"
 genModuleItem (Initial stat ) = "initial " <> genStmnt stat
 genModuleItem (Always  stat ) = "always " <> genStmnt stat
 genModuleItem (Decl dir port) = maybe "" makePort dir <> genPort port <> ";\n"
   where makePort = (<> " ") . genPortDir
 
+genModConn :: ModConn -> Text
+genModConn (ModConn c) =
+  genExpr c
+genModConn (ModConnNamed n c) =
+  "." <> n ^. getIdentifier <> "(" <> genExpr c <> ")"
+
 -- | Generate continuous assignment
 genContAssign :: ContAssign -> Text
 genContAssign (ContAssign val e) = "assign " <> name <> " = " <> expr <> ";\n"
diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs
index 0e68419..4b58de7 100644
--- a/src/VeriFuzz/Verilog/Mutate.hs
+++ b/src/VeriFuzz/Verilog/Mutate.hs
@@ -15,6 +15,9 @@ module VeriFuzz.Verilog.Mutate where
 
 import           Control.Lens
 import           Data.Maybe               (catMaybes, fromMaybe)
+import           Data.Maybe               (fromMaybe)
+import           Data.Text                (Text)
+import qualified Data.Text                as T
 import           VeriFuzz.Internal.Gen
 import           VeriFuzz.Internal.Shared
 import           VeriFuzz.Verilog.AST
@@ -111,6 +114,25 @@ instantiateMod_ m = ModInst (m ^. modId) (m ^. modId) conns
       <$> (m ^.. modOutPorts . traverse . portName)
       ++  (m ^.. modInPorts . traverse . portName)
 
+-- | Instantiate without adding wire declarations. It also does not count the
+-- current instantiations of the same module.
+--
+-- >>> render $ instantiateModSpec_ "_" m
+-- m m(.y(y), .x(x));
+-- <BLANKLINE>
+instantiateModSpec_ :: Text -> ModDecl -> ModItem
+instantiateModSpec_ outChar m = ModInst (m ^. modId) (m ^. modId) conns
+ where
+  conns =
+    zipWith ModConnNamed ids (Id <$> instIds)
+  ids = (filterChar outChar $ name modOutPorts) ++ (name modInPorts)
+  instIds = (name modOutPorts) ++ (name modInPorts)
+  name v = m ^.. v . traverse . portName
+
+filterChar :: Text -> [Identifier] -> [Identifier]
+filterChar t ids =
+  ids & traverse . getIdentifier %~ (\x -> fromMaybe x . safe head $ T.splitOn t x)
+
 -- | Initialise all the inputs and outputs to a module.
 --
 -- >>> render $ initMod m
@@ -134,7 +156,7 @@ makeTop :: Int -> ModDecl -> ModDecl
 makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt
  where
   ys    = Port Wire 90 . flip makeIdFrom "y" <$> [1 .. i]
-  modIt = instantiateMod_ . modN <$> [1 .. i]
+  modIt = instantiateModSpec_ "_" . modN <$> [1 .. i]
   modN n = m & modId %~ makeIdFrom n & modOutPorts .~ [Port Wire 90 (makeIdFrom n "y")]
 
 makeTopAssert :: ModDecl -> ModDecl
-- 
cgit