diff options
Diffstat (limited to 'src/VeriFuzz/Mutate.hs')
| -rw-r--r-- | src/VeriFuzz/Mutate.hs | 37 |
1 files changed, 28 insertions, 9 deletions
diff --git a/src/VeriFuzz/Mutate.hs b/src/VeriFuzz/Mutate.hs index 7092cbf..3052322 100644 --- a/src/VeriFuzz/Mutate.hs +++ b/src/VeriFuzz/Mutate.hs @@ -23,7 +23,9 @@ import VeriFuzz.Internal -- | Return if the 'Identifier' is in a 'ModDecl'. inPort :: Identifier -> ModDecl -> Bool inPort i m = inInput - where inInput = any (\a -> a ^. portName == i) $ m ^. modInPorts ++ m ^. modOutPorts + where + inInput = + any (\a -> a ^. portName == i) $ m ^. modInPorts ++ m ^. modOutPorts -- | Find the last assignment of a specific wire/reg to an expression, and -- returns that expression. @@ -55,7 +57,8 @@ replace = (transformOf traverseExpr .) . idTrans nestId :: Identifier -> ModDecl -> ModDecl nestId i m | not $ inPort i m - = let expr = fromMaybe def . findAssign i $ m ^. modItems in m & get %~ replace i expr + = let expr = fromMaybe def . findAssign i $ m ^. modItems + in m & get %~ replace i expr | otherwise = m where @@ -68,10 +71,13 @@ nestSource i src = src & getVerilogSrc . traverse . getDescription %~ nestId i -- | Nest variables in the format @w[0-9]*@ up to a certain number. nestUpTo :: Int -> VerilogSrc -> VerilogSrc -nestUpTo i src = foldl (flip nestSource) src $ Identifier . fromNode <$> [1 .. i] +nestUpTo i src = + foldl (flip nestSource) src $ Identifier . fromNode <$> [1 .. i] allVars :: ModDecl -> [Identifier] -allVars m = (m ^.. modOutPorts . traverse . portName) <> (m ^.. modInPorts . traverse . portName) +allVars m = + (m ^.. modOutPorts . traverse . portName) + <> (m ^.. modInPorts . traverse . portName) -- $setup -- >>> import VeriFuzz.CodeGen @@ -94,8 +100,16 @@ instantiateMod m main = main & modItems %~ ((out ++ regIn ++ [inst]) ++) where out = Decl Nothing <$> m ^. modOutPorts regIn = Decl Nothing <$> (m ^. modInPorts & traverse . portType .~ Reg) - inst = ModInst (m ^. modId) (m ^. modId <> (Identifier . showT $ count + 1)) conns - count = length . filter (== m ^. modId) $ main ^.. modItems . traverse . modInstId + inst = ModInst (m ^. modId) + (m ^. modId <> (Identifier . showT $ count + 1)) + conns + count = + length + . filter (== m ^. modId) + $ main + ^.. modItems + . traverse + . modInstId conns = ModConn . Id <$> allVars m -- | Instantiate without adding wire declarations. It also does not count the @@ -129,7 +143,10 @@ instantiateModSpec_ outChar m = ModInst (m ^. modId) (m ^. modId) conns filterChar :: Text -> [Identifier] -> [Identifier] filterChar t ids = - ids & traverse . getIdentifier %~ (\x -> fromMaybe x . safe head $ T.splitOn t x) + ids + & traverse + . getIdentifier + %~ (\x -> fromMaybe x . safe head $ T.splitOn t x) -- | Initialise all the inputs and outputs to a module. -- @@ -157,12 +174,14 @@ makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt where ys = yPort . flip makeIdFrom "y" <$> [1 .. i] modIt = instantiateModSpec_ "_" . modN <$> [1 .. i] - modN n = m & modId %~ makeIdFrom n & modOutPorts .~ [yPort (makeIdFrom n "y")] + modN n = + m & modId %~ makeIdFrom n & modOutPorts .~ [yPort (makeIdFrom n "y")] -- | Make a top module with an assert that requires @y_1@ to always be equal to -- @y_2@, which can then be proven using a formal verification tool. makeTopAssert :: ModDecl -> ModDecl -makeTopAssert = (modItems %~ (++ [assert])) . (modInPorts %~ addClk) . makeTop 2 +makeTopAssert = (modItems %~ (++ [assert])) . (modInPorts %~ addClk) . makeTop + 2 where assert = Always . EventCtrl e . Just $ SeqBlock [TaskEnable $ Task "assert" [BinOp (Id "y_1") BinEq (Id "y_2")]] |