diff options
Diffstat (limited to 'src/VeriFuzz/Verilog/Mutate.hs')
| -rw-r--r-- | src/VeriFuzz/Verilog/Mutate.hs | 46 |
1 files changed, 29 insertions, 17 deletions
diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs index 03ee1d0..536ebef 100644 --- a/src/VeriFuzz/Verilog/Mutate.hs +++ b/src/VeriFuzz/Verilog/Mutate.hs @@ -72,7 +72,7 @@ idTrans _ _ e = e -- | Replaces the identifier recursively in an expression. replace :: Identifier -> Expr -> Expr -> Expr -replace = (transformOf traverseExpr .) . idTrans +replace = (transform .) . idTrans -- | Nest expressions for a specific 'Identifier'. If the 'Identifier' is not -- found, the AST is not changed. @@ -107,8 +107,8 @@ allVars m = -- $setup -- >>> import VeriFuzz.Verilog.CodeGen --- >>> let m = (ModDecl (Identifier "m") [Port Wire False 5 (Identifier "y")] [Port Wire False 5 "x"] []) --- >>> let main = (ModDecl "main" [] [] []) +-- >>> let m = (ModDecl (Identifier "m") [Port Wire False 0 5 (Identifier "y")] [Port Wire False 0 5 "x"] [] []) +-- >>> let main = (ModDecl "main" [] [] [] []) -- | Add a Module Instantiation using 'ModInst' from the first module passed to -- it to the body of the second module. It first has to make all the inputs into @@ -124,11 +124,14 @@ allVars m = instantiateMod :: ModDecl -> ModDecl -> ModDecl 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 + out = Decl Nothing <$> m ^. modOutPorts <*> pure Nothing + regIn = + Decl Nothing + <$> (m ^. modInPorts & traverse . portType .~ Reg) + <*> pure Nothing + inst = ModInst (m ^. modId) + (m ^. modId <> (Identifier . showT $ count + 1)) + conns count = length . filter (== m ^. modId) @@ -185,8 +188,8 @@ filterChar t ids = initMod :: ModDecl -> ModDecl initMod m = m & modItems %~ ((out ++ inp) ++) where - out = Decl (Just PortOut) <$> (m ^. modOutPorts) - inp = Decl (Just PortIn) <$> (m ^. modInPorts) + out = Decl (Just PortOut) <$> (m ^. modOutPorts) <*> pure Nothing + inp = Decl (Just PortIn) <$> (m ^. modInPorts) <*> pure Nothing -- | Make an 'Identifier' from and existing Identifier and an object with a -- 'Show' instance to make it unique. @@ -196,7 +199,7 @@ makeIdFrom a i = (i <>) . Identifier . ("_" <>) $ showT a -- | Make top level module for equivalence verification. Also takes in how many -- modules to instantiate. makeTop :: Int -> ModDecl -> ModDecl -makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt +makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt [] where ys = yPort . flip makeIdFrom "y" <$> [1 .. i] modIt = instantiateModSpec_ "_" . modN <$> [1 .. i] @@ -206,17 +209,20 @@ makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt -- | 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])) . makeTop - 2 +makeTopAssert = (modItems %~ (++ [assert])) . makeTop 2 where assert = Always . EventCtrl e . Just $ SeqBlock [TaskEnable $ Task "assert" [BinOp (Id "y_1") BinEq (Id "y_2")]] - e = EPosEdge "clk" + e = EPosEdge "clk" --- | Provide declarations for all the ports that are passed to it. +-- | Provide declarations for all the ports that are passed to it. If they are +-- registers, it should assign them to 0. declareMod :: [Port] -> ModDecl -> ModDecl declareMod ports = initMod . (modItems %~ (decl ++)) - where decl = Decl Nothing <$> ports + where + decl = declf <$> ports + declf p@(Port Reg _ _ _ _) = Decl Nothing p (Just 0) + declf p = Decl Nothing p Nothing -- | Simplify an 'Expr' by using constants to remove 'BinaryOperator' and -- simplify expressions. To make this work effectively, it should be run until @@ -273,4 +279,10 @@ combineAssigns p a = combineAssigns_ :: Port -> [Port] -> ModItem combineAssigns_ p ps = - ModCA . ContAssign (p ^. portName) . fold $ Id <$> ps ^.. traverse . portName + ModCA + . ContAssign (p ^. portName) + . fold + $ Id + <$> ps + ^.. traverse + . portName |