From 186bb5f37770c150bd8e601e9761211af6a9c277 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 10 Apr 2019 23:42:58 +0100 Subject: Fix the generation of modules and add initialisation --- src/VeriFuzz.hs | 21 +++-- src/VeriFuzz/Config.hs | 131 +++++++++++++------------- src/VeriFuzz/Sim/Icarus.hs | 3 +- src/VeriFuzz/Sim/Internal.hs | 2 +- src/VeriFuzz/Sim/Reduce.hs | 4 +- src/VeriFuzz/Sim/Template.hs | 2 +- src/VeriFuzz/Verilog.hs | 1 + src/VeriFuzz/Verilog/AST.hs | 2 + src/VeriFuzz/Verilog/Arbitrary.hs | 19 ++-- src/VeriFuzz/Verilog/CodeGen.hs | 43 ++++++--- src/VeriFuzz/Verilog/Gen.hs | 189 ++++++++++++++++++++++++++++---------- src/VeriFuzz/Verilog/Internal.hs | 7 +- src/VeriFuzz/Verilog/Mutate.hs | 28 ++++-- src/VeriFuzz/Verilog/Parser.hs | 6 +- 14 files changed, 289 insertions(+), 169 deletions(-) (limited to 'src') diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index e46751a..9486537 100644 --- a/src/VeriFuzz.hs +++ b/src/VeriFuzz.hs @@ -55,8 +55,7 @@ generateByteString n = do return $ randomByteString gen n [] makeSrcInfo :: ModDecl -> SourceInfo -makeSrcInfo m = - SourceInfo (m ^. modId . getIdentifier) (Verilog [m]) +makeSrcInfo m = SourceInfo (m ^. modId . getIdentifier) (Verilog [m]) -- | Draw a randomly generated DAG to a dot file and compile it to a png so it -- can be seen. @@ -107,18 +106,20 @@ checkEquivalence src dir = shellyFailDir $ do setenv "VERIFUZZ_ROOT" curr cd (fromText dir) catch_sh - (runEquiv defaultYosys defaultYosys (Just defaultVivado) src >> return True + ( runEquiv defaultYosys defaultYosys (Just defaultVivado) src + >> return True ) ((\_ -> return False) :: RunFailed -> Sh Bool) -- | Run a fuzz run and check if all of the simulators passed by checking if the -- generated Verilog files are equivalent. -runEquivalence :: Gen Verilog -- ^ Generator for the Verilog file. - -> Text -- ^ Name of the folder on each thread. - -> Text -- ^ Name of the general folder being used. - -> Bool -- ^ Keep flag. - -> Int -- ^ Used to track the recursion. - -> IO () +runEquivalence + :: Gen Verilog -- ^ Generator for the Verilog file. + -> Text -- ^ Name of the folder on each thread. + -> Text -- ^ Name of the general folder being used. + -> Bool -- ^ Keep flag. + -> Int -- ^ Used to track the recursion. + -> IO () runEquivalence gm t d k i = do m <- Hog.sample gm let srcInfo = SourceInfo "top" m @@ -129,7 +130,7 @@ runEquivalence gm t d k i = do setenv "VERIFUZZ_ROOT" curr cd (fromText "output" fromText n) catch_sh - ( runEquiv defaultYosys defaultYosys (Just defaultVivado) srcInfo + (runEquiv defaultYosys defaultYosys (Just defaultVivado) srcInfo >> echoP "Test OK" ) $ onFailure n diff --git a/src/VeriFuzz/Config.hs b/src/VeriFuzz/Config.hs index ec3fbc1..8b48995 100644 --- a/src/VeriFuzz/Config.hs +++ b/src/VeriFuzz/Config.hs @@ -34,13 +34,16 @@ module VeriFuzz.Config , ProbModItem(..) , probModItemAssign , probModItemAlways + , probModItemInst , ProbStatement(..) , probStmntBlock , probStmntNonBlock , probStmntCond , propSize , propSeed - , propDepth + , propStmntDepth + , propModDepth + , propMaxModules , parseConfigFile , parseConfig , configEncode @@ -71,6 +74,7 @@ data ProbExpr = ProbExpr { _probExprNum :: {-# UNPACK #-} !Int data ProbModItem = ProbModItem { _probModItemAssign :: {-# UNPACK #-} !Int , _probModItemAlways :: {-# UNPACK #-} !Int + , _probModItemInst :: {-# UNPACK #-} !Int } deriving (Eq, Show) @@ -86,9 +90,11 @@ data Probability = Probability { _probModItem :: {-# UNPACK #-} !ProbModItem } deriving (Eq, Show) -data Property = Property { _propSize :: {-# UNPACK #-} !Int - , _propSeed :: !(Maybe Int) - , _propDepth :: {-# UNPACK #-} !Int +data Property = Property { _propSize :: {-# UNPACK #-} !Int + , _propSeed :: !(Maybe Int) + , _propStmntDepth :: {-# UNPACK #-} !Int + , _propModDepth :: {-# UNPACK #-} !Int + , _propMaxModules :: {-# UNPACK #-} !Int } deriving (Eq, Show) @@ -112,10 +118,12 @@ defaultValue defaultValue x = Toml.dimap Just (fromMaybe x) . Toml.dioptional defaultConfig :: Config -defaultConfig = Config (Probability defModItem defStmnt defExpr) (Property 20 Nothing 3) - where defModItem = ProbModItem 5 1 - defStmnt = ProbStatement 5 5 1 - defExpr = ProbExpr 1 1 1 1 1 1 0 1 1 +defaultConfig = Config (Probability defModItem defStmnt defExpr) + (Property 20 Nothing 3 2 5) + where + defModItem = ProbModItem 5 1 1 + defStmnt = ProbStatement 5 5 1 + defExpr = ProbExpr 1 1 1 1 1 1 0 1 1 twoKey :: Toml.Piece -> Toml.Piece -> Toml.Key twoKey a b = Toml.Key (a :| [b]) @@ -126,72 +134,63 @@ int a = Toml.int . twoKey a exprCodec :: TomlCodec ProbExpr exprCodec = ProbExpr - <$> defaultValue (defProb probExprNum) - (intE "number") - .= _probExprNum - <*> defaultValue (defProb probExprId) - (intE "variable") - .= _probExprId - <*> defaultValue (defProb probExprUnOp) - (intE "unary") - .= _probExprUnOp - <*> defaultValue (defProb probExprBinOp) - (intE "binary") - .= _probExprBinOp - <*> defaultValue (defProb probExprCond) - (intE "ternary") - .= _probExprCond - <*> defaultValue (defProb probExprConcat) - (intE "concatenation") - .= _probExprConcat - <*> defaultValue (defProb probExprStr) - (intE "string") - .= _probExprStr - <*> defaultValue (defProb probExprSigned) - (intE "signed") - .= _probExprSigned - <*> defaultValue (defProb probExprUnsigned) - (intE "unsigned") - .= _probExprUnsigned - where defProb i = defaultConfig ^. configProbability . probExpr . i - intE = int "expr" + <$> defaultValue (defProb probExprNum) (intE "number") + .= _probExprNum + <*> defaultValue (defProb probExprId) (intE "variable") + .= _probExprId + <*> defaultValue (defProb probExprUnOp) (intE "unary") + .= _probExprUnOp + <*> defaultValue (defProb probExprBinOp) (intE "binary") + .= _probExprBinOp + <*> defaultValue (defProb probExprCond) (intE "ternary") + .= _probExprCond + <*> defaultValue (defProb probExprConcat) (intE "concatenation") + .= _probExprConcat + <*> defaultValue (defProb probExprStr) (intE "string") + .= _probExprStr + <*> defaultValue (defProb probExprSigned) (intE "signed") + .= _probExprSigned + <*> defaultValue (defProb probExprUnsigned) (intE "unsigned") + .= _probExprUnsigned + where + defProb i = defaultConfig ^. configProbability . probExpr . i + intE = int "expr" stmntCodec :: TomlCodec ProbStatement stmntCodec = ProbStatement - <$> defaultValue (defProb probStmntBlock) - (intS "blocking") - .= _probStmntBlock - <*> defaultValue (defProb probStmntNonBlock) - (intS "nonblocking") - .= _probStmntNonBlock - <*> defaultValue (defProb probStmntCond) - (intS "conditional") - .= _probStmntCond - where defProb i = defaultConfig ^. configProbability . probStmnt . i - intS = int "statement" + <$> defaultValue (defProb probStmntBlock) (intS "blocking") + .= _probStmntBlock + <*> defaultValue (defProb probStmntNonBlock) (intS "nonblocking") + .= _probStmntNonBlock + <*> defaultValue (defProb probStmntCond) (intS "conditional") + .= _probStmntCond + where + defProb i = defaultConfig ^. configProbability . probStmnt . i + intS = int "statement" modItemCodec :: TomlCodec ProbModItem modItemCodec = ProbModItem - <$> defaultValue (defProb probModItemAssign) - (intM "assign") - .= _probModItemAssign - <*> defaultValue (defProb probModItemAlways) - (intM "always") - .= _probModItemAlways - where defProb i = defaultConfig ^. configProbability . probModItem . i - intM = int "moditem" + <$> defaultValue (defProb probModItemAssign) (intM "assign") + .= _probModItemAssign + <*> defaultValue (defProb probModItemAlways) (intM "always") + .= _probModItemAlways + <*> defaultValue (defProb probModItemInst) (intM "instantiation") + .= _probModItemInst + where + defProb i = defaultConfig ^. configProbability . probModItem . i + intM = int "moditem" probCodec :: TomlCodec Probability probCodec = Probability - <$> defaultValue (defProb probModItem) modItemCodec - .= _probModItem - <*> defaultValue (defProb probStmnt) stmntCodec - .= _probStmnt - <*> defaultValue (defProb probExpr) exprCodec - .= _probExpr + <$> defaultValue (defProb probModItem) modItemCodec + .= _probModItem + <*> defaultValue (defProb probStmnt) stmntCodec + .= _probStmnt + <*> defaultValue (defProb probExpr) exprCodec + .= _probExpr where defProb i = defaultConfig ^. configProbability . i propCodec :: TomlCodec Property @@ -201,8 +200,12 @@ propCodec = .= _propSize <*> Toml.dioptional (Toml.int "seed") .= _propSeed - <*> defaultValue (defProp propDepth) (Toml.int "depth") - .= _propDepth + <*> defaultValue (defProp propStmntDepth) (int "statement" "depth") + .= _propStmntDepth + <*> defaultValue (defProp propModDepth) (int "module" "depth") + .= _propModDepth + <*> defaultValue (defProp propMaxModules) (int "module" "max") + .= _propMaxModules where defProp i = defaultConfig ^. configProperty . i configCodec :: TomlCodec Config diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs index 9b5138f..8876706 100644 --- a/src/VeriFuzz/Sim/Icarus.hs +++ b/src/VeriFuzz/Sim/Icarus.hs @@ -92,7 +92,8 @@ runSimIcarus sim rinfo bss = do [ Initial $ fold (addDisplay $ assignFunc (_modInPorts m) <$> bss) <> (SysTaskEnable $ Task "finish" []) - ] [] + ] + [] let newtb = instantiateMod m tb let modWithTb = Verilog [newtb, m] writefile "main.v" $ genSource modWithTb diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs index 925b155..145042a 100644 --- a/src/VeriFuzz/Sim/Internal.hs +++ b/src/VeriFuzz/Sim/Internal.hs @@ -74,7 +74,7 @@ mainModule = lens get_ set_ set_ (SourceInfo top main) v = SourceInfo top (main & getModule %~ update top v) update top v m@(ModDecl (Identifier i) _ _ _ _) | i == top = v - | otherwise = m + | otherwise = m get_ (SourceInfo top main) = head . filter (f top) $ main ^.. getModule f top (ModDecl (Identifier i) _ _ _ _) = i == top diff --git a/src/VeriFuzz/Sim/Reduce.hs b/src/VeriFuzz/Sim/Reduce.hs index 5684ed5..381a84c 100644 --- a/src/VeriFuzz/Sim/Reduce.hs +++ b/src/VeriFuzz/Sim/Reduce.hs @@ -67,8 +67,8 @@ filterExpr ids (Id i) = if i `notElem` ids then Number 1 0 else Id i filterExpr _ e = e filterDecl :: [Identifier] -> ModItem -> Bool -filterDecl ids (Decl Nothing (Port _ _ _ i)) = i `elem` ids -filterDecl _ _ = True +filterDecl ids (Decl Nothing (Port _ _ _ i) _) = i `elem` ids +filterDecl _ _ = True filterAssigns :: [Port] -> ModItem -> Bool filterAssigns out (ModCA (ContAssign i _)) = diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs index 0fc74a0..f630ea6 100644 --- a/src/VeriFuzz/Sim/Template.hs +++ b/src/VeriFuzz/Sim/Template.hs @@ -91,7 +91,7 @@ sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options] mode prove [engines] -smtbmc +smtbmc z3 [script] #{readL} diff --git a/src/VeriFuzz/Verilog.hs b/src/VeriFuzz/Verilog.hs index 752b754..19dc607 100644 --- a/src/VeriFuzz/Verilog.hs +++ b/src/VeriFuzz/Verilog.hs @@ -14,6 +14,7 @@ module VeriFuzz.Verilog ( Verilog(..) , parseVerilog , procedural + , proceduralIO , randomMod , GenVerilog(..) , genSource diff --git a/src/VeriFuzz/Verilog/AST.hs b/src/VeriFuzz/Verilog/AST.hs index 270793d..8ed0254 100644 --- a/src/VeriFuzz/Verilog/AST.hs +++ b/src/VeriFuzz/Verilog/AST.hs @@ -132,6 +132,7 @@ module VeriFuzz.Verilog.AST , traverseModItem , declDir , declPort + , declVal , ModConn(..) , modConn , modConnName @@ -432,6 +433,7 @@ data ModItem = ModCA { _modContAssign :: !ContAssign } | Always !Statement | Decl { _declDir :: !(Maybe PortDir) , _declPort :: !Port + , _declVal :: Maybe ConstExpr } | ParamDecl { _paramDecl :: NonEmpty Parameter } | LocalParamDecl { _localParamDecl :: NonEmpty LocalParam } diff --git a/src/VeriFuzz/Verilog/Arbitrary.hs b/src/VeriFuzz/Verilog/Arbitrary.hs index 40b9787..52e0d5f 100644 --- a/src/VeriFuzz/Verilog/Arbitrary.hs +++ b/src/VeriFuzz/Verilog/Arbitrary.hs @@ -137,14 +137,15 @@ expr n | n == 0 = Hog.choice $ (Id <$> arb) : exprSafeList where subexpr y = expr (n `div` y) constExpr :: Gen ConstExpr -constExpr = Hog.recursive Hog.choice - [ ConstNum <$> genPositive <*> arb - , ParamId <$> arb - ] - [ Hog.subtermM constExpr (\e -> ConstUnOp <$> arb <*> pure e) - , Hog.subtermM2 constExpr constExpr (\a b -> ConstBinOp <$> pure a <*> arb <*> pure b) - , Hog.subterm3 constExpr constExpr constExpr ConstCond - ] +constExpr = Hog.recursive + Hog.choice + [ConstNum <$> genPositive <*> arb, ParamId <$> arb] + [ Hog.subtermM constExpr (\e -> ConstUnOp <$> arb <*> pure e) + , Hog.subtermM2 constExpr + constExpr + (\a b -> ConstBinOp <$> pure a <*> arb <*> pure b) + , Hog.subterm3 constExpr constExpr constExpr ConstCond + ] instance Arb ConstExpr where arb = constExpr @@ -203,7 +204,7 @@ instance Arb ModItem where , ModInst <$> arb <*> arb <*> listOf arb , Initial <$> arb , Always <$> (EventCtrl <$> arb <*> Hog.maybe arb) - , Decl <$> pure Nothing <*> arb + , Decl <$> pure Nothing <*> arb <*> pure Nothing ] modPortGen :: Gen Port diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs index 2479d39..53af0d1 100644 --- a/src/VeriFuzz/Verilog/CodeGen.hs +++ b/src/VeriFuzz/Verilog/CodeGen.hs @@ -51,15 +51,19 @@ verilogSrc (Verilog modules) = fold $ moduleDecl <$> modules moduleDecl :: ModDecl -> Text moduleDecl (ModDecl i outP inP items ps) = "module " - <> identifier i <> params ps <> ports <> ";\n" <> modI + <> identifier i + <> params ps + <> ports + <> ";\n" + <> modI <> "endmodule\n" where ports | null outP && null inP = "" - | otherwise = "(" <> comma (modPort <$> outIn) <> ")" + | otherwise = "(" <> comma (modPort <$> outIn) <> ")" modI = fold $ moduleItem <$> items outIn = outP ++ inP - params [] = "" - params (p:pps) = "\n#(\n" <> paramList (p :| pps) <> "\n)\n" + params [] = "" + params (p : pps) = "\n#(\n" <> paramList (p :| pps) <> "\n)\n" -- | Generates a parameter list. Can only be called with a 'NonEmpty' list. paramList :: NonEmpty Parameter -> Text @@ -112,9 +116,10 @@ moduleItem (ModInst (Identifier i) (Identifier name) conn) = i <> " " <> name <> "(" <> comma (mConn <$> conn) <> ")" <> ";\n" moduleItem (Initial stat) = "initial " <> statement stat moduleItem (Always stat) = "always " <> statement stat -moduleItem (Decl dir p ) = maybe "" makePort dir <> port p <> ";\n" +moduleItem (Decl dir p ini ) = maybe "" makePort dir <> port p <> maybe "" makeIni ini <> ";\n" where makePort = (<> " ") . portDir -moduleItem (ParamDecl p) = paramList p <> ";\n" + makeIni = (" = " <>) . constExpr +moduleItem (ParamDecl p) = paramList p <> ";\n" moduleItem (LocalParamDecl p) = localParamList p <> ";\n" mConn :: ModConn -> Text @@ -144,19 +149,22 @@ expr (Func f e ) = func f <> "(" <> expr e <> ")" expr (Str t ) = "\"" <> t <> "\"" showNum :: Int -> Integer -> Text -showNum s n = "(" <> minus <> showT s <> "'h" <> T.pack (showHex (abs n) "") <> ")" +showNum s n = + "(" <> minus <> showT s <> "'h" <> T.pack (showHex (abs n) "") <> ")" where minus | signum n >= 0 = "" | otherwise = "-" constExpr :: ConstExpr -> Text -constExpr (ConstNum s n) = showNum s n -constExpr (ParamId i) = identifier i +constExpr (ConstNum s n ) = showNum s n +constExpr (ParamId i) = identifier i constExpr (ConstConcat c) = "{" <> comma (constExpr <$> c) <> "}" constExpr (ConstUnOp u e) = "(" <> unaryOp u <> constExpr e <> ")" -constExpr (ConstBinOp eRhs bin eLhs) = "(" <> constExpr eRhs <> binaryOp bin <> constExpr eLhs <> ")" -constExpr (ConstCond l t f) = "(" <> constExpr l <> " ? " <> constExpr t <> " : " <> constExpr f <> ")" -constExpr (ConstStr t ) = "\"" <> t <> "\"" +constExpr (ConstBinOp eRhs bin eLhs) = + "(" <> constExpr eRhs <> binaryOp bin <> constExpr eLhs <> ")" +constExpr (ConstCond l t f) = + "(" <> constExpr l <> " ? " <> constExpr t <> " : " <> constExpr f <> ")" +constExpr (ConstStr t) = "\"" <> t <> "\"" -- | Convert 'BinaryOperator' to 'Text'. binaryOp :: BinaryOperator -> Text @@ -239,9 +247,14 @@ statement (CondStmnt e t Nothing) = "if(" <> expr e <> ")\n" <> defMap t statement (CondStmnt e t f) = "if(" <> expr e <> ")\n" <> defMap t <> "else\n" <> defMap f statement (ForLoop a e incr stmnt) = - "for(" <> genAssign " = " a - <> "; " <> expr e <> "; " <> genAssign " = " incr - <> ")\n" <> statement stmnt + "for(" + <> genAssign " = " a + <> "; " + <> expr e + <> "; " + <> genAssign " = " incr + <> ")\n" + <> statement stmnt task :: Task -> Text task (Task name e) | null e = i diff --git a/src/VeriFuzz/Verilog/Gen.hs b/src/VeriFuzz/Verilog/Gen.hs index 6ec422d..4f3ceca 100644 --- a/src/VeriFuzz/Verilog/Gen.hs +++ b/src/VeriFuzz/Verilog/Gen.hs @@ -15,6 +15,7 @@ Various useful generators. module VeriFuzz.Verilog.Gen ( -- * Generation methods procedural + , proceduralIO , randomMod ) where @@ -38,8 +39,10 @@ import VeriFuzz.Verilog.Mutate data Context = Context { _variables :: [Port] , _parameters :: [Parameter] - , _nameCounter :: Int - , _stmntDepth :: Int + , _modules :: [ModDecl] + , _nameCounter :: {-# UNPACK #-} !Int + , _stmntDepth :: {-# UNPACK #-} !Int + , _modDepth :: {-# UNPACK #-} !Int } makeLenses ''Context @@ -77,7 +80,11 @@ randomMod inps total = do let other = drop inps ident let y = ModCA . ContAssign "y" . fold $ Id <$> drop inps ids let yport = [wire (sumSize other) "y"] - return . declareMod other $ ModDecl "test_module" yport inputs_ (x ++ [y]) [] + return . declareMod other $ ModDecl "test_module" + yport + inputs_ + (x ++ [y]) + [] where ids = toId <$> [1 .. total] end = drop inps ids @@ -89,32 +96,46 @@ gen = lift . lift constExprWithContext :: [Parameter] -> ProbExpr -> Hog.Size -> Gen ConstExpr constExprWithContext ps prob size | size == 0 = Hog.frequency - [ (prob ^. probExprNum, ConstNum <$> genPositive <*> arb) - , (if null ps then 0 else prob ^. probExprId, ParamId . view paramIdent <$> Hog.element ps) - ] + [ (prob ^. probExprNum, ConstNum <$> genPositive <*> arb) + , ( if null ps then 0 else prob ^. probExprId + , ParamId . view paramIdent <$> Hog.element ps + ) + ] | size > 0 = Hog.frequency - [ (prob ^. probExprNum, ConstNum <$> genPositive <*> arb) - , (if null ps then 0 else prob ^. probExprId, ParamId . view paramIdent <$> Hog.element ps) - , (prob ^. probExprUnOp, ConstUnOp <$> arb <*> subexpr 2) - , (prob ^. probExprBinOp, ConstBinOp <$> subexpr 2 <*> arb <*> subexpr 2) - , (prob ^. probExprCond, ConstCond <$> subexpr 3 <*> subexpr 3 <*> subexpr 3) - , (prob ^. probExprConcat, ConstConcat <$> listOf1 (subexpr 8)) - ] + [ (prob ^. probExprNum, ConstNum <$> genPositive <*> arb) + , ( if null ps then 0 else prob ^. probExprId + , ParamId . view paramIdent <$> Hog.element ps + ) + , (prob ^. probExprUnOp, ConstUnOp <$> arb <*> subexpr 2) + , ( prob ^. probExprBinOp + , ConstBinOp <$> subexpr 2 <*> arb <*> subexpr 2 + ) + , ( prob ^. probExprCond + , ConstCond <$> subexpr 3 <*> subexpr 3 <*> subexpr 3 + ) + , (prob ^. probExprConcat, ConstConcat <$> listOf1 (subexpr 8)) + ] | otherwise = constExprWithContext ps prob 0 where subexpr y = constExprWithContext ps prob $ size `div` y exprSafeList :: ProbExpr -> [(Int, Gen Expr)] -exprSafeList prob = [(prob ^. probExprNum, Number <$> genPositive <*> Hog.integral (Hog.linearFrom 0 (-100) 100))] +exprSafeList prob = + [ ( prob ^. probExprNum + , Number <$> genPositive <*> Hog.integral (Hog.linearFrom 0 (-100) 100) + ) + ] exprRecList :: ProbExpr -> (Hog.Size -> Gen Expr) -> [(Int, Gen Expr)] exprRecList prob subexpr = - [ (prob ^. probExprNum, Number <$> genPositive <*> Hog.integral (Hog.linearFrom 0 (-100) 100)) - , (prob ^. probExprConcat, Concat <$> listOf1 (subexpr 8)) - , (prob ^. probExprUnOp, UnOp <$> arb <*> subexpr 2) + [ ( prob ^. probExprNum + , Number <$> genPositive <*> Hog.integral (Hog.linearFrom 0 (-100) 100) + ) + , (prob ^. probExprConcat , Concat <$> listOf1 (subexpr 8)) + , (prob ^. probExprUnOp , UnOp <$> arb <*> subexpr 2) , (prob ^. probExprStr, Str <$> Hog.text (Hog.linear 0 100) Hog.alphaNum) - , (prob ^. probExprBinOp, BinOp <$> subexpr 2 <*> arb <*> subexpr 2) - , (prob ^. probExprCond, Cond <$> subexpr 3 <*> subexpr 3 <*> subexpr 3) - , (prob ^. probExprSigned, Func <$> pure SignedFunc <*> subexpr 2) + , (prob ^. probExprBinOp , BinOp <$> subexpr 2 <*> arb <*> subexpr 2) + , (prob ^. probExprCond , Cond <$> subexpr 3 <*> subexpr 3 <*> subexpr 3) + , (prob ^. probExprSigned , Func <$> pure SignedFunc <*> subexpr 2) , (prob ^. probExprUnsigned, Func <$> pure UnsignedFunc <*> subexpr 2) ] @@ -124,9 +145,16 @@ exprWithContext prob [] n | n == 0 = Hog.frequency $ exprSafeList prob | otherwise = exprWithContext prob [] 0 where subexpr y = exprWithContext prob [] $ n `div` y exprWithContext prob l n - | n == 0 = Hog.frequency $ (prob ^. probExprId, Id <$> Hog.element l) : exprSafeList prob - | n > 0 = Hog.frequency $ (prob ^. probExprId, Id <$> Hog.element l) : exprRecList prob subexpr - | otherwise = exprWithContext prob l 0 + | n == 0 + = Hog.frequency + $ (prob ^. probExprId, Id <$> Hog.element l) + : exprSafeList prob + | n > 0 + = Hog.frequency + $ (prob ^. probExprId, Id <$> Hog.element l) + : exprRecList prob subexpr + | otherwise + = exprWithContext prob l 0 where subexpr y = exprWithContext prob l $ n `div` y some :: StateGen a -> StateGen [a] @@ -136,7 +164,7 @@ some f = do many :: StateGen a -> StateGen [a] many f = do - amount <- gen $ Hog.int (Hog.linear 0 10) + amount <- gen $ Hog.int (Hog.linear 0 30) replicateM amount f makeIdentifier :: T.Text -> StateGen Identifier @@ -153,13 +181,10 @@ newPort pt = do variables %= (p :) return p -choose :: PortType -> Port -> Bool -choose ptype (Port a _ _ _) = ptype == a - scopedExpr :: StateGen Expr scopedExpr = do context <- get - prob <- askProbability + prob <- askProbability gen . Hog.sized . exprWithContext (prob ^. probExpr) @@ -171,7 +196,7 @@ scopedExpr = do contAssign :: StateGen ContAssign contAssign = do expr <- scopedExpr - p <- newPort Wire + p <- newPort Wire return $ ContAssign (p ^. portName) expr lvalFromPort :: Port -> LVal @@ -215,33 +240,90 @@ always = do stat <- SeqBlock <$> some statement return $ Always (EventCtrl (EPosEdge "clk") (Just stat)) +instantiate :: ModDecl -> StateGen ModItem +instantiate (ModDecl i outP inP _ _) = do + context <- get + outs <- + fmap (Id . view portName) <$> (replicateM (length outP) $ newPort Wire) + ins <- + (Id "clk" :) + . fmap (Id . view portName) + . take (length inP - 1) + <$> (Hog.shuffle $ context ^. variables) + ident <- makeIdentifier "modinst" + Hog.choice + [ return . ModInst i ident $ ModConn <$> outs <> ins + , ModInst i ident + <$> Hog.shuffle (zipWith ModConnNamed (view portName <$> outP <> inP) (outs <> ins)) + ] + +-- | Generates a module instance by also generating a new module if there are +-- not enough modules currently in the context. It keeps generating new modules +-- for every instance and for every level until either the deepest level is +-- achieved, or the maximum number of modules are reached. +-- +-- If the maximum number of levels are reached, it will always pick an instance +-- from the current context. The problem with this approach is that at the end +-- there may be many more than the max amount of modules, as the modules are +-- always set to empty when entering a new level. This is to fix recursive +-- definitions of modules, which are not defined. +-- +-- One way to fix that is to also decrement the max modules for every level, +-- depending on how many modules have already been generated. This would mean +-- there would be moments when the module cannot generate a new instance but +-- also not take a module from the current context. A fix for that may be to +-- have a default definition of a simple module that is used instead. +-- +-- Another different way to handle this would be to have a probability of taking +-- a module from a context or generating a new one. +modInst :: StateGen ModItem +modInst = do + prob <- lift ask + context <- get + let maxMods = prob ^. configProperty . propMaxModules + if length (context ^. modules) < maxMods + then do + let currMods = context ^. modules + let params = context ^. parameters + let vars = context ^. variables + modules .= [] + variables .= [] + parameters .= [] + modDepth -= 1 + chosenMod <- moduleDef Nothing + ncont <- get + let genMods = ncont ^. modules + modDepth += 1 + parameters .= params + variables .= vars + modules .= chosenMod : currMods <> genMods + instantiate chosenMod + else Hog.element (context ^. modules) >>= instantiate + -- | Generate a random module item. modItem :: StateGen ModItem modItem = do - prob <- askProbability + prob <- askProbability + context <- get let defProb i = prob ^. probModItem . i Hog.frequency [ (defProb probModItemAssign, ModCA <$> contAssign) , (defProb probModItemAlways, always) + , ( if context ^. modDepth > 0 then defProb probModItemInst else 0 + , modInst + ) ] moduleName :: Maybe Identifier -> StateGen Identifier moduleName (Just t) = return t -moduleName Nothing = gen arb - -initialBlock :: StateGen ModItem -initialBlock = do - context <- get - let l = filter (choose Reg) $ context ^.. variables . traverse - return . Initial . SeqBlock $ makeAssign <$> l - where - makeAssign p = NonBlockAssign $ Assign (lvalFromPort p) Nothing 0 +moduleName Nothing = makeIdentifier "module" constExpr :: StateGen ConstExpr constExpr = do - prob <- askProbability + prob <- askProbability context <- get - gen . Hog.sized $ constExprWithContext (context ^. parameters) (prob ^. probExpr) + gen . Hog.sized $ constExprWithContext (context ^. parameters) + (prob ^. probExpr) parameter :: StateGen Parameter parameter = do @@ -249,7 +331,7 @@ parameter = do cexpr <- constExpr let param = Parameter ident cexpr parameters %= (param :) - return $ param + return param -- | Generates a module definition randomly. It always has one output port which -- is set to @y@. The size of @y@ is the total combination of all the locally @@ -261,20 +343,27 @@ moduleDef top = do portList <- some $ newPort Wire mi <- some modItem context <- get - initBlock <- initialBlock let local = filter (`notElem` portList) $ context ^. variables let size = sum $ local ^.. traverse . portSize let clock = Port Wire False 1 "clk" let yport = Port Wire False size "y" - let comb = combineAssigns_ yport local - declareMod local . ModDecl name [yport] (clock:portList) (initBlock : mi <> [comb]) <$> many parameter + let comb = combineAssigns_ yport local + declareMod local + . ModDecl name [yport] (clock : portList) (mi <> [comb]) + <$> many parameter -- | Procedural generation method for random Verilog. Uses internal 'Reader' and -- 'State' to keep track of the current Verilog code structure. procedural :: Config -> Gen Verilog -procedural config = Verilog . (: []) <$> Hog.resize - num - (runReaderT (evalStateT (moduleDef (Just "top")) context) config) +procedural config = do + (mainMod, st) <- Hog.resize num + $ runReaderT (runStateT (moduleDef (Just "top")) context) config + return . Verilog $ mainMod : st ^. modules where - context = Context [] [] 0 $ config ^. configProperty . propDepth - num = fromIntegral $ config ^. configProperty . propSize + context = + Context [] [] [] 0 (confProp propStmntDepth) $ confProp propModDepth + num = fromIntegral $ confProp propSize + confProp i = config ^. configProperty . i + +proceduralIO :: Config -> IO Verilog +proceduralIO = Hog.sample . procedural diff --git a/src/VeriFuzz/Verilog/Internal.hs b/src/VeriFuzz/Verilog/Internal.hs index a7b0a15..d68e46c 100644 --- a/src/VeriFuzz/Verilog/Internal.hs +++ b/src/VeriFuzz/Verilog/Internal.hs @@ -33,10 +33,10 @@ import Data.Text (Text) import VeriFuzz.Verilog.AST regDecl :: Identifier -> ModItem -regDecl = Decl Nothing . Port Reg False 1 +regDecl i = Decl Nothing (Port Reg False 1 i) Nothing wireDecl :: Identifier -> ModItem -wireDecl = Decl Nothing . Port Wire False 1 +wireDecl i = Decl Nothing (Port Wire False 1 i) Nothing -- | Create an empty module. emptyMod :: ModDecl @@ -75,7 +75,8 @@ testBench = ModDecl -- ] -- , SysTaskEnable $ Task "finish" [] ] - ] [] + ] + [] addTestBench :: Verilog -> Verilog addTestBench = addModDecl testBench diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs index 2b6ab3a..e170680 100644 --- a/src/VeriFuzz/Verilog/Mutate.hs +++ b/src/VeriFuzz/Verilog/Mutate.hs @@ -124,8 +124,8 @@ 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) + 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 @@ -185,8 +185,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. @@ -206,17 +206,19 @@ 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 +275,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 diff --git a/src/VeriFuzz/Verilog/Parser.hs b/src/VeriFuzz/Verilog/Parser.hs index 8c9a986..3b07366 100644 --- a/src/VeriFuzz/Verilog/Parser.hs +++ b/src/VeriFuzz/Verilog/Parser.hs @@ -259,7 +259,7 @@ parseNetDecl pd = do range <- option 1 parseRange name <- identifier tok' SymSemi - return . Decl pd . Port t sign range $ name + return $ Decl pd (Port t sign range name) Nothing where type_ = tok KWWire $> Wire <|> tok KWReg $> Reg parsePortDir :: Parser PortDir @@ -281,8 +281,8 @@ parseModList :: Parser [Identifier] parseModList = list <|> return [] where list = parens $ commaSep identifier filterDecl :: PortDir -> ModItem -> Bool -filterDecl p (Decl (Just p') _) = p == p' -filterDecl _ _ = False +filterDecl p (Decl (Just p') _ _) = p == p' +filterDecl _ _ = False modPorts :: PortDir -> [ModItem] -> [Port] modPorts p mis = filter (filterDecl p) mis ^.. traverse . declPort -- cgit