diff options
author | Yann Herklotz <ymherklotz@gmail.com> | 2019-01-20 17:46:56 +0000 |
---|---|---|
committer | Yann Herklotz <ymherklotz@gmail.com> | 2019-01-20 17:46:56 +0000 |
commit | 3e37e75f804cbf6b5ce04a427888fb0f0859660a (patch) | |
tree | e0602c9777a36ad677009031cc8edaa5fefc22cd /src/VeriFuzz/Verilog/Mutate.hs | |
parent | 8a70b3fa892aaa095aa423609bfadaecea44c655 (diff) | |
download | verismith-3e37e75f804cbf6b5ce04a427888fb0f0859660a.tar.gz verismith-3e37e75f804cbf6b5ce04a427888fb0f0859660a.zip |
[Fix #22] Fix SAT solver equivalence checking
Diffstat (limited to 'src/VeriFuzz/Verilog/Mutate.hs')
-rw-r--r-- | src/VeriFuzz/Verilog/Mutate.hs | 24 |
1 files changed, 23 insertions, 1 deletions
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 |