diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/VeriFuzz.hs | 21 | ||||
-rw-r--r-- | src/VeriFuzz/Circuit.hs | 1 | ||||
-rw-r--r-- | src/VeriFuzz/Circuit/Gen.hs | 8 | ||||
-rw-r--r-- | src/VeriFuzz/Config.hs | 175 | ||||
-rw-r--r-- | src/VeriFuzz/Internal.hs | 5 | ||||
-rw-r--r-- | src/VeriFuzz/RecursionScheme.hs | 84 | ||||
-rw-r--r-- | src/VeriFuzz/Sim/Icarus.hs | 3 | ||||
-rw-r--r-- | src/VeriFuzz/Sim/Internal.hs | 6 | ||||
-rw-r--r-- | src/VeriFuzz/Sim/Reduce.hs | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Sim/Template.hs | 2 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog.hs | 10 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/AST.hs | 336 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/CodeGen.hs | 115 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/Gen.hs | 336 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/Internal.hs | 25 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/Mutate.hs | 46 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/Parser.hs | 14 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/Preprocess.hs | 7 |
18 files changed, 770 insertions, 428 deletions
diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index ebedb0d..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 [Description 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/Circuit.hs b/src/VeriFuzz/Circuit.hs index 37e25ac..d385d32 100644 --- a/src/VeriFuzz/Circuit.hs +++ b/src/VeriFuzz/Circuit.hs @@ -43,4 +43,3 @@ fromGraph = do $ nestUpTo 5 (generateAST gr) ^.. getVerilog . traverse - . getDescription diff --git a/src/VeriFuzz/Circuit/Gen.hs b/src/VeriFuzz/Circuit/Gen.hs index 817d2f8..1e31e56 100644 --- a/src/VeriFuzz/Circuit/Gen.hs +++ b/src/VeriFuzz/Circuit/Gen.hs @@ -38,7 +38,7 @@ inputsC :: Circuit -> [Node] inputsC c = inputs (getCircuit c) genPortsAST :: (Circuit -> [Node]) -> Circuit -> [Port] -genPortsAST f c = port . frNode <$> f c where port = Port Wire False 4 +genPortsAST f c = port . frNode <$> f c where port = Port Wire False 0 4 -- | Generates the nested expression AST, so that it can then generate the -- assignment expressions. @@ -67,13 +67,13 @@ genAssignAST c = catMaybes $ genContAssignAST c <$> nodes nodes = G.labNodes gr genModuleDeclAST :: Circuit -> ModDecl -genModuleDeclAST c = ModDecl i output ports $ combineAssigns yPort a +genModuleDeclAST c = ModDecl i output ports (combineAssigns yPort a) [] where i = Identifier "gen_module" ports = genPortsAST inputsC c output = [] a = genAssignAST c - yPort = Port Wire False 90 "y" + yPort = Port Wire False 0 90 "y" generateAST :: Circuit -> Verilog -generateAST c = Verilog [Description $ genModuleDeclAST c] +generateAST c = Verilog [genModuleDeclAST c] diff --git a/src/VeriFuzz/Config.hs b/src/VeriFuzz/Config.hs index d812248..66c5aa2 100644 --- a/src/VeriFuzz/Config.hs +++ b/src/VeriFuzz/Config.hs @@ -15,17 +15,36 @@ Configuration file format and parser. module VeriFuzz.Config ( Config(..) , defaultConfig + , configProbability + , configProperty , Probability(..) - , probBlock - , probNonBlock - , probAssign - , probAlways - , probCond + , probModItem + , probStmnt + , probExpr + , ProbExpr(..) + , probExprNum + , probExprId + , probExprUnOp + , probExprBinOp + , probExprCond + , probExprConcat + , probExprStr + , probExprSigned + , probExprUnsigned + , ProbModItem(..) + , probModItemAssign + , probModItemAlways + , probModItemInst + , ProbStatement(..) + , probStmntBlock + , probStmntNonBlock + , probStmntCond + , probStmntFor , propSize , propSeed - , propDepth - , configProbability - , configProperty + , propStmntDepth + , propModDepth + , propMaxModules , parseConfigFile , parseConfig , configEncode @@ -42,29 +61,55 @@ import qualified Data.Text.IO as T (writeFile) import Toml (TomlCodec, (.=)) import qualified Toml -data Probability = Probability { _probAssign :: {-# UNPACK #-} !Int - , _probAlways :: {-# UNPACK #-} !Int - , _probBlock :: {-# UNPACK #-} !Int - , _probNonBlock :: {-# UNPACK #-} !Int - , _probCond :: {-# UNPACK #-} !Int +data ProbExpr = ProbExpr { _probExprNum :: {-# UNPACK #-} !Int + , _probExprId :: {-# UNPACK #-} !Int + , _probExprUnOp :: {-# UNPACK #-} !Int + , _probExprBinOp :: {-# UNPACK #-} !Int + , _probExprCond :: {-# UNPACK #-} !Int + , _probExprConcat :: {-# UNPACK #-} !Int + , _probExprStr :: {-# UNPACK #-} !Int + , _probExprSigned :: {-# UNPACK #-} !Int + , _probExprUnsigned :: {-# UNPACK #-} !Int + } + deriving (Eq, Show) + +data ProbModItem = ProbModItem { _probModItemAssign :: {-# UNPACK #-} !Int + , _probModItemAlways :: {-# UNPACK #-} !Int + , _probModItemInst :: {-# UNPACK #-} !Int } deriving (Eq, Show) -makeLenses ''Probability +data ProbStatement = ProbStatement { _probStmntBlock :: {-# UNPACK #-} !Int + , _probStmntNonBlock :: {-# UNPACK #-} !Int + , _probStmntCond :: {-# UNPACK #-} !Int + , _probStmntFor :: {-# UNPACK #-} !Int + } + deriving (Eq, Show) -data Property = Property { _propSize :: {-# UNPACK #-} !Int - , _propSeed :: !(Maybe Int) - , _propDepth :: {-# UNPACK #-} !Int +data Probability = Probability { _probModItem :: {-# UNPACK #-} !ProbModItem + , _probStmnt :: {-# UNPACK #-} !ProbStatement + , _probExpr :: {-# UNPACK #-} !ProbExpr + } + deriving (Eq, Show) + +data Property = Property { _propSize :: {-# UNPACK #-} !Int + , _propSeed :: !(Maybe Int) + , _propStmntDepth :: {-# UNPACK #-} !Int + , _propModDepth :: {-# UNPACK #-} !Int + , _propMaxModules :: {-# UNPACK #-} !Int } deriving (Eq, Show) -makeLenses ''Property - data Config = Config { _configProbability :: {-# UNPACK #-} !Probability , _configProperty :: {-# UNPACK #-} !Property } deriving (Eq, Show) +makeLenses ''ProbExpr +makeLenses ''ProbModItem +makeLenses ''ProbStatement +makeLenses ''Probability +makeLenses ''Property makeLenses ''Config defaultValue @@ -75,29 +120,81 @@ defaultValue defaultValue x = Toml.dimap Just (fromMaybe x) . Toml.dioptional defaultConfig :: Config -defaultConfig = Config (Probability 5 1 5 1 1) (Property 20 Nothing 3) +defaultConfig = Config (Probability defModItem defStmnt defExpr) + (Property 20 Nothing 3 2 5) + where + defModItem = ProbModItem 5 1 1 + defStmnt = ProbStatement 5 5 1 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]) +int :: Toml.Piece -> Toml.Piece -> TomlCodec Int +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" + +stmntCodec :: TomlCodec ProbStatement +stmntCodec = + ProbStatement + <$> defaultValue (defProb probStmntBlock) (intS "blocking") + .= _probStmntBlock + <*> defaultValue (defProb probStmntNonBlock) (intS "nonblocking") + .= _probStmntNonBlock + <*> defaultValue (defProb probStmntCond) (intS "conditional") + .= _probStmntCond + <*> defaultValue (defProb probStmntFor) (intS "forloop") + .= _probStmntFor + 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 + <*> defaultValue (defProb probModItemInst) (intM "instantiation") + .= _probModItemInst + where + defProb i = defaultConfig ^. configProbability . probModItem . i + intM = int "moditem" + probCodec :: TomlCodec Probability probCodec = Probability - <$> defaultValue (defProb probAssign) - (Toml.int $ twoKey "moditem" "assign") - .= _probAssign - <*> defaultValue (defProb probAlways) - (Toml.int $ twoKey "moditem" "always") - .= _probAlways - <*> defaultValue (defProb probBlock) - (Toml.int $ twoKey "statement" "blocking") - .= _probBlock - <*> defaultValue (defProb probNonBlock) - (Toml.int $ twoKey "statement" "nonblocking") - .= _probNonBlock - <*> defaultValue (defProb probNonBlock) - (Toml.int $ twoKey "statement" "conditional") - .= _probCond + <$> defaultValue (defProb probModItem) modItemCodec + .= _probModItem + <*> defaultValue (defProb probStmnt) stmntCodec + .= _probStmnt + <*> defaultValue (defProb probExpr) exprCodec + .= _probExpr where defProb i = defaultConfig ^. configProbability . i propCodec :: TomlCodec Property @@ -107,8 +204,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/Internal.hs b/src/VeriFuzz/Internal.hs index 51bb52c..22efa92 100644 --- a/src/VeriFuzz/Internal.hs +++ b/src/VeriFuzz/Internal.hs @@ -15,6 +15,7 @@ module VeriFuzz.Internal safe , showT , comma + , commaNL ) where @@ -33,3 +34,7 @@ showT = T.pack . show -- | Inserts commas between '[Text]' and except the last one. comma :: [Text] -> Text comma = T.intercalate ", " + +-- | Inserts commas and newlines between '[Text]' and except the last one. +commaNL :: [Text] -> Text +commaNL = T.intercalate ",\n" diff --git a/src/VeriFuzz/RecursionScheme.hs b/src/VeriFuzz/RecursionScheme.hs new file mode 100644 index 0000000..7d89498 --- /dev/null +++ b/src/VeriFuzz/RecursionScheme.hs @@ -0,0 +1,84 @@ +{-| +Module : VeriFuzz.RecursionScheme +Description : Recursion scheme implementation for the AST. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Recursion scheme implementation for the AST. +-} + +module VeriFuzz.RecursionScheme + ( Term(..) + , Attr(..) + , Algebra + , bottomUp + , topDown + , cata + , ana + , para + , apo + ) +where + +import Control.Arrow ((&&&), (>>>), (|||)) +import Data.Function ((&)) + +newtype Term f = In { out :: f (Term f) } + +data Attr f a = Attr + { attribute :: a + , hole :: f (Attr f a) + } + +type Algebra f a = f a -> a + +type RAlgebra f a = f (Term f, a) -> a + +type RAlgebra' f a = Term f -> f a -> a + +type CVAlgebra f a = f (Attr f a) -> a + +type Coalgebra f a = a -> f a + +type RCoalgebra f a = a -> f (Either (Term f) a) + +bottomUp :: Functor a => (Term a -> Term a) -> Term a -> Term a +bottomUp fn = cata $ In >>> fn + +topDown :: Functor a => (Term a -> Term a) -> Term a -> Term a +topDown fn = ana $ fn >>> out + +cata :: Functor f => Algebra f a -> Term f -> a +cata fn = para' $ const fn + +ana :: Functor f => Coalgebra f a -> a -> Term f +ana fn = + fn + >>> fmap (ana fn) + >>> In + +para :: Functor f => RAlgebra f a -> Term f -> a +para ralg = + out + >>> fmap (id &&& para ralg) + >>> ralg + +para' :: Functor f => RAlgebra' f a -> Term f -> a +para' ralg t = out t & fmap (para' ralg) & ralg t + +apo :: Functor f => RCoalgebra f a -> a -> Term f +apo rcoalg = + rcoalg + >>> fmap (id ||| apo rcoalg) + >>> In + +histo :: Functor f => CVAlgebra f a -> Term f -> a +histo cv = + out + >>> fmap worker + >>> cv + where + worker t = undefined diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs index 14023b7..8876706 100644 --- a/src/VeriFuzz/Sim/Icarus.hs +++ b/src/VeriFuzz/Sim/Icarus.hs @@ -93,8 +93,9 @@ runSimIcarus sim rinfo bss = do $ fold (addDisplay $ assignFunc (_modInPorts m) <$> bss) <> (SysTaskEnable $ Task "finish" []) ] + [] let newtb = instantiateMod m tb - let modWithTb = Verilog $ Description <$> [newtb, m] + let modWithTb = Verilog [newtb, m] writefile "main.v" $ genSource modWithTb runSimWithFile sim "main.v" bss where m = rinfo ^. mainModule diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs index 062035c..145042a 100644 --- a/src/VeriFuzz/Sim/Internal.hs +++ b/src/VeriFuzz/Sim/Internal.hs @@ -73,10 +73,10 @@ mainModule = lens get_ set_ where set_ (SourceInfo top main) v = SourceInfo top (main & getModule %~ update top v) - update top v m@(ModDecl (Identifier i) _ _ _) | i == top = v - | otherwise = m + update top v m@(ModDecl (Identifier i) _ _ _ _) | i == top = v + | otherwise = m get_ (SourceInfo top main) = head . filter (f top) $ main ^.. getModule - f top (ModDecl (Identifier i) _ _ _) = i == top + f top (ModDecl (Identifier i) _ _ _ _) = i == top rootPath :: Sh FilePath rootPath = do diff --git a/src/VeriFuzz/Sim/Reduce.hs b/src/VeriFuzz/Sim/Reduce.hs index 5684ed5..361df3e 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 fdf2ac0..4d3b82c 100644 --- a/src/VeriFuzz/Verilog.hs +++ b/src/VeriFuzz/Verilog.hs @@ -14,12 +14,11 @@ module VeriFuzz.Verilog ( Verilog(..) , parseVerilog , procedural + , proceduralIO , randomMod , GenVerilog(..) , genSource , getVerilog - , Description(..) - , getDescription -- * Primitives -- ** Identifier , Identifier(..) @@ -69,8 +68,6 @@ module VeriFuzz.Verilog , exprFunc , exprBody , exprStr - , exprWithContext - , traverseExpr , ConstExpr(..) , constNum , Function(..) @@ -91,7 +88,6 @@ module VeriFuzz.Verilog , statements , stmntBA , stmntNBA - , stmntCA , stmntTask , stmntSysTask , stmntCondExpr @@ -118,10 +114,6 @@ module VeriFuzz.Verilog -- * Useful Lenses and Traversals , getModule , getSourceId - -- * Arbitrary - , Arb - , arb - , genPositive ) where diff --git a/src/VeriFuzz/Verilog/AST.hs b/src/VeriFuzz/Verilog/AST.hs index 405b712..007b3b5 100644 --- a/src/VeriFuzz/Verilog/AST.hs +++ b/src/VeriFuzz/Verilog/AST.hs @@ -18,8 +18,6 @@ module VeriFuzz.Verilog.AST ( -- * Top level types Verilog(..) , getVerilog - , Description(..) - , getDescription -- * Primitives -- ** Identifier , Identifier(..) @@ -50,6 +48,7 @@ module VeriFuzz.Verilog.AST , Port(..) , portType , portSigned + , portSizeLower , portSize , portName -- * Expression @@ -69,10 +68,20 @@ module VeriFuzz.Verilog.AST , exprFunc , exprBody , exprStr - , exprWithContext - , traverseExpr , ConstExpr(..) + , constSize , constNum + , constParamId + , constConcat + , constUnOp + , constPrim + , constLhs + , constBinOp + , constRhs + , constCond + , constTrue + , constFalse + , constStr , Function(..) -- * Assignment , Assign(..) @@ -82,6 +91,13 @@ module VeriFuzz.Verilog.AST , ContAssign(..) , contAssignNetLVal , contAssignExpr + -- ** Parameters + , Parameter(..) + , paramIdent + , paramValue + , LocalParam(..) + , localParamIdent + , localParamValue -- * Statment , Statement(..) , statDelay @@ -91,26 +107,33 @@ module VeriFuzz.Verilog.AST , statements , stmntBA , stmntNBA - , stmntCA , stmntTask , stmntSysTask , stmntCondExpr , stmntCondTrue , stmntCondFalse + , forAssign + , forExpr + , forIncr + , forStmnt -- * Module , ModDecl(..) , modId , modOutPorts , modInPorts , modItems + , modParams , ModItem(..) , modContAssign , modInstId , modInstName , modInstConns + , paramDecl + , localParamDecl , traverseModItem , declDir , declPort + , declVal , ModConn(..) , modConn , modConnName @@ -118,25 +141,16 @@ module VeriFuzz.Verilog.AST -- * Useful Lenses and Traversals , getModule , getSourceId - -- * Arbitrary - , Arb - , arb - , genPositive ) where import Control.Lens -import Control.Monad (replicateM) import Data.Data import Data.Data.Lens -import Data.List.NonEmpty (toList) +import Data.List.NonEmpty (NonEmpty) import Data.String (IsString, fromString) import Data.Text (Text) -import qualified Data.Text as T import Data.Traversable (sequenceA) -import Hedgehog (Gen) -import qualified Hedgehog.Gen as Hog -import qualified Hedgehog.Range as Hog -- | Identifier in Verilog. This is just a string of characters that can either -- be lowercase and uppercase for now. This might change in the future though, @@ -199,7 +213,7 @@ data UnaryOperator = UnPlus -- ^ @+@ deriving (Eq, Show, Ord, Data) data Function = SignedFunc - | UnSignedFunc + | UnsignedFunc deriving (Eq, Show, Ord, Data) -- | Verilog expression, which can either be a primary expression, unary @@ -250,17 +264,49 @@ instance IsString Expr where instance Plated Expr where plate = uniplate -traverseExpr :: (Applicative f) => (Expr -> f Expr) -> Expr -> f Expr -traverseExpr f (Concat e ) = Concat <$> sequenceA (f <$> e) -traverseExpr f (UnOp u e ) = UnOp u <$> f e -traverseExpr f (BinOp l o r) = BinOp <$> f l <*> pure o <*> f r -traverseExpr f (Cond c l r) = Cond <$> f c <*> f l <*> f r -traverseExpr f (Func fn e ) = Func fn <$> f e -traverseExpr _ e = pure e +-- | Constant expression, which are known before simulation at compile time. +data ConstExpr = ConstNum { _constSize :: Int + , _constNum :: Integer + } + | ParamId { _constParamId :: {-# UNPACK #-} !Identifier } + | ConstConcat { _constConcat :: [ConstExpr] } + | ConstUnOp { _constUnOp :: !UnaryOperator + , _constPrim :: ConstExpr + } + | ConstBinOp { _constLhs :: ConstExpr + , _constBinOp :: !BinaryOperator + , _constRhs :: ConstExpr + } + | ConstCond { _constCond :: ConstExpr + , _constTrue :: ConstExpr + , _constFalse :: ConstExpr + } + | ConstStr { _constStr :: {-# UNPACK #-} !Text } + deriving (Eq, Show, Ord, Data) + +instance Num ConstExpr where + a + b = ConstBinOp a BinPlus b + a - b = ConstBinOp a BinMinus b + a * b = ConstBinOp a BinTimes b + negate = ConstUnOp UnMinus + abs = undefined + signum = undefined + fromInteger = ConstNum 32 . fromInteger + +instance Semigroup ConstExpr where + (ConstConcat a) <> (ConstConcat b) = ConstConcat $ a <> b + (ConstConcat a) <> b = ConstConcat $ a <> [b] + a <> (ConstConcat b) = ConstConcat $ a : b + a <> b = ConstConcat [a, b] --- | Constant expression, which are known before simulation at compilation time. -newtype ConstExpr = ConstExpr { _constNum :: Int } - deriving (Eq, Show, Ord, Data, Num) +instance Monoid ConstExpr where + mempty = ConstConcat [] + +instance IsString ConstExpr where + fromString = ConstStr . fromString + +instance Plated ConstExpr where + plate = uniplate data Task = Task { _taskName :: {-# UNPACK #-} !Identifier , _taskExpr :: [Expr] @@ -306,10 +352,11 @@ data PortType = Wire -- -- This is now implemented inside 'ModDecl' itself, which uses a list of output -- and input ports. -data Port = Port { _portType :: !PortType - , _portSigned :: !Bool - , _portSize :: {-# UNPACK #-} !Int - , _portName :: {-# UNPACK #-} !Identifier +data Port = Port { _portType :: !PortType + , _portSigned :: !Bool + , _portSizeLower :: {-# UNPACK #-} !Int + , _portSize :: {-# UNPACK #-} !Int + , _portName :: {-# UNPACK #-} !Identifier } deriving (Eq, Show, Ord, Data) -- | This is currently a type because direct module declaration should also be @@ -343,13 +390,17 @@ data Statement = TimeCtrl { _statDelay :: {-# UNPACK #-} !Delay | SeqBlock { _statements :: [Statement] } -- ^ Sequential block (@begin ... end@) | BlockAssign { _stmntBA :: !Assign } -- ^ blocking assignment (@=@) | NonBlockAssign { _stmntNBA :: !Assign } -- ^ Non blocking assignment (@<=@) - | StatCA { _stmntCA :: !ContAssign } -- ^ Statement continuous assignment. May not be correct. | TaskEnable { _stmntTask :: !Task } | SysTaskEnable { _stmntSysTask :: !Task } | CondStmnt { _stmntCondExpr :: Expr , _stmntCondTrue :: Maybe Statement , _stmntCondFalse :: Maybe Statement } + | ForLoop { _forAssign :: !Assign + , _forExpr :: Expr + , _forIncr :: !Assign + , _forStmnt :: Statement + } -- ^ Loop bounds shall be statically computable for a for loop. deriving (Eq, Show, Ord, Data) instance Semigroup Statement where @@ -361,6 +412,19 @@ instance Semigroup Statement where instance Monoid Statement where mempty = SeqBlock [] +-- | Parameter that can be assigned in blocks or modules using @parameter@. +data Parameter = Parameter { _paramIdent :: {-# UNPACK #-} !Identifier + , _paramValue :: ConstExpr + } + deriving (Eq, Show, Ord, Data) + +-- | Local parameter that can be assigned anywhere using @localparam@. It cannot +-- be changed by initialising the module. +data LocalParam = LocalParam { _localParamIdent :: {-# UNPACK #-} !Identifier + , _localParamValue :: ConstExpr + } + deriving (Eq, Show, Ord, Data) + -- | Module item which is the body of the module expression. data ModItem = ModCA { _modContAssign :: !ContAssign } | ModInst { _modInstId :: {-# UNPACK #-} !Identifier @@ -371,7 +435,10 @@ data ModItem = ModCA { _modContAssign :: !ContAssign } | Always !Statement | Decl { _declDir :: !(Maybe PortDir) , _declPort :: !Port + , _declVal :: Maybe ConstExpr } + | ParamDecl { _paramDecl :: NonEmpty Parameter } + | LocalParamDecl { _localParamDecl :: NonEmpty LocalParam } deriving (Eq, Show, Ord, Data) -- | 'module' module_identifier [list_of_ports] ';' { module_item } 'end_module' @@ -379,7 +446,9 @@ data ModDecl = ModDecl { _modId :: {-# UNPACK #-} !Identifier , _modOutPorts :: [Port] , _modInPorts :: [Port] , _modItems :: [ModItem] - } deriving (Eq, Show, Ord, Data) + , _modParams :: [Parameter] + } + deriving (Eq, Show, Ord, Data) traverseModConn :: (Applicative f) => (Expr -> f Expr) -> ModConn -> f ModConn traverseModConn f (ModConn e ) = ModConn <$> f e @@ -391,12 +460,8 @@ traverseModItem f (ModInst a b e) = ModInst a b <$> sequenceA (traverseModConn f <$> e) traverseModItem _ e = pure e --- | Description of the Verilog module. -newtype Description = Description { _getDescription :: ModDecl } - deriving (Eq, Show, Ord, Data) - -- | The complete sourcetext for the Verilog module. -newtype Verilog = Verilog { _getVerilog :: [Description] } +newtype Verilog = Verilog { _getVerilog :: [ModDecl] } deriving (Eq, Show, Ord, Data, Semigroup, Monoid) makeLenses ''Identifier @@ -412,206 +477,15 @@ makeLenses ''Assign makeLenses ''ContAssign makeLenses ''Statement makeLenses ''ModItem +makeLenses ''Parameter +makeLenses ''LocalParam makeLenses ''ModDecl -makeLenses ''Description makeLenses ''Verilog getModule :: Traversal' Verilog ModDecl -getModule = getVerilog . traverse . getDescription +getModule = getVerilog . traverse {-# INLINE getModule #-} getSourceId :: Traversal' Verilog Text getSourceId = getModule . modId . getIdentifier {-# INLINE getSourceId #-} - -listOf1 :: Gen a -> Gen [a] -listOf1 a = toList <$> Hog.nonEmpty (Hog.linear 0 100) a - -listOf :: Gen a -> Gen [a] -listOf = Hog.list (Hog.linear 0 100) - -genPositive :: Gen Int -genPositive = Hog.filter (>= 0) $ Hog.int (Hog.linear 1 99) - -integral :: Gen Integer -integral = Hog.integral (Hog.linear 0 100) - -class Arb a where - arb :: Gen a - -instance Arb Identifier where - arb = do - l <- genPositive - Identifier . T.pack <$> replicateM (l + 1) (Hog.element ['a'..'z']) - -instance Arb Delay where - arb = Delay <$> genPositive - -instance Arb Event where - arb = EId <$> arb - -instance Arb BinaryOperator where - arb = Hog.element - [ BinPlus - , BinMinus - , BinTimes - -- , BinDiv - -- , BinMod - , BinEq - , BinNEq - -- , BinCEq - -- , BinCNEq - , BinLAnd - , BinLOr - , BinLT - , BinLEq - , BinGT - , BinGEq - , BinAnd - , BinOr - , BinXor - , BinXNor - , BinXNorInv - -- , BinPower - , BinLSL - , BinLSR - , BinASL - , BinASR - ] - -instance Arb UnaryOperator where - arb = Hog.element - [ UnPlus - , UnMinus - , UnNot - , UnLNot - , UnAnd - , UnNand - , UnOr - , UnNor - , UnXor - , UnNxor - , UnNxorInv - ] - -instance Arb Function where - arb = Hog.element - [ SignedFunc - , UnSignedFunc - ] - -instance Arb Expr where - arb = Hog.sized expr - -exprSafeList :: [Gen Expr] -exprSafeList = [Number <$> genPositive <*> integral] - -exprRecList :: (Hog.Size -> Gen Expr) -> [Gen Expr] -exprRecList subexpr = - [ Number <$> genPositive <*> integral - , Concat <$> listOf1 (subexpr 8) - , UnOp - <$> arb - <*> subexpr 2 - -- , Str <$> arb - , BinOp <$> subexpr 2 <*> arb <*> subexpr 2 - , Cond <$> subexpr 3 <*> subexpr 3 <*> subexpr 3 - , Func <$> arb <*> subexpr 2 - ] - -expr :: Hog.Size -> Gen Expr -expr n | n == 0 = Hog.choice $ (Id <$> arb) : exprSafeList - | n > 0 = Hog.choice $ (Id <$> arb) : exprRecList subexpr - | otherwise = expr 0 - where subexpr y = expr (n `div` y) - -exprWithContext :: [Identifier] -> Hog.Size -> Gen Expr -exprWithContext [] n | n == 0 = Hog.choice exprSafeList - | n > 0 = Hog.choice $ exprRecList subexpr - | otherwise = exprWithContext [] 0 - where subexpr y = exprWithContext [] (n `div` y) -exprWithContext l n - | n == 0 = Hog.choice $ (Id <$> Hog.element l) : exprSafeList - | n > 0 = Hog.choice $ (Id <$> Hog.element l) : exprRecList subexpr - | otherwise = exprWithContext l 0 - where subexpr y = exprWithContext l (n `div` y) - -instance Arb Int where - arb = Hog.int (Hog.linear 0 100) - -instance Arb ConstExpr where - arb = ConstExpr <$> Hog.int (Hog.linear 0 100) - -instance Arb Task where - arb = Task <$> arb <*> listOf arb - -instance Arb LVal where - arb = Hog.choice [ RegId <$> arb - , RegExpr <$> arb <*> arb - , RegSize <$> arb <*> arb <*> arb - ] - -instance Arb PortDir where - arb = Hog.element [PortIn, PortOut, PortInOut] - -instance Arb PortType where - arb = Hog.element [Wire, Reg] - -instance Arb Port where - arb = Port <$> arb <*> arb <*> genPositive <*> arb - -instance Arb ModConn where - arb = ModConn <$> arb - -instance Arb Assign where - arb = Assign <$> arb <*> Hog.maybe arb <*> arb - -instance Arb ContAssign where - arb = ContAssign <$> arb <*> arb - -instance Arb Statement where - arb = Hog.sized statement - -statement :: Hog.Size -> Gen Statement -statement n - | n == 0 = Hog.choice - [ BlockAssign <$> arb - , NonBlockAssign <$> arb - -- , StatCA <$> arb - , TaskEnable <$> arb - , SysTaskEnable <$> arb - ] - | n > 0 = Hog.choice - [ TimeCtrl <$> arb <*> (Just <$> substat 2) - , SeqBlock <$> listOf1 (substat 4) - , BlockAssign <$> arb - , NonBlockAssign <$> arb - -- , StatCA <$> arb - , TaskEnable <$> arb - , SysTaskEnable <$> arb - ] - | otherwise = statement 0 - where substat y = statement (n `div` y) - -instance Arb ModItem where - arb = Hog.choice [ ModCA <$> arb - , ModInst <$> arb <*> arb <*> listOf arb - , Initial <$> arb - , Always <$> (EventCtrl <$> arb <*> Hog.maybe arb) - , Decl <$> pure Nothing <*> arb - ] - -modPortGen :: Gen Port -modPortGen = Port <$> arb <*> arb <*> arb <*> arb - -instance Arb ModDecl where - arb = ModDecl <$> arb <*> listOf arb <*> listOf1 modPortGen <*> listOf arb - -instance Arb Description where - arb = Description <$> arb - -instance Arb Verilog where - arb = Verilog <$> listOf1 arb - -instance Arb Bool where - arb = Hog.element [True, False] diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs index a05309f..3a8d14a 100644 --- a/src/VeriFuzz/Verilog/CodeGen.hs +++ b/src/VeriFuzz/Verilog/CodeGen.hs @@ -23,6 +23,7 @@ where import Control.Lens (view, (^.)) import Data.Foldable (fold) +import Data.List.NonEmpty (NonEmpty (..), toList) import Data.Text (Text) import qualified Data.Text as T import qualified Data.Text.IO as T @@ -44,30 +45,44 @@ defMap = maybe ";\n" statement -- | Convert the 'Verilog' type to 'Text' so that it can be rendered. verilogSrc :: Verilog -> Text -verilogSrc source = fold $ description <$> source ^. getVerilog - --- | Generate the 'Description' to 'Text'. -description :: Description -> Text -description desc = moduleDecl $ desc ^. getDescription +verilogSrc (Verilog modules) = fold $ moduleDecl <$> modules -- | Generate the 'ModDecl' for a module and convert it to 'Text'. moduleDecl :: ModDecl -> Text -moduleDecl m = +moduleDecl (ModDecl i outP inP items ps) = "module " - <> m - ^. modId - . getIdentifier + <> identifier i + <> params ps <> ports <> ";\n" <> modI <> "endmodule\n" where - ports | noIn && noOut = "" - | otherwise = "(" <> comma (modPort <$> outIn) <> ")" - modI = fold $ moduleItem <$> m ^. modItems - noOut = null $ m ^. modOutPorts - noIn = null $ m ^. modInPorts - outIn = (m ^. modOutPorts) ++ (m ^. modInPorts) + ports | null outP && null inP = "" + | otherwise = "(" <> comma (modPort <$> outIn) <> ")" + modI = fold $ moduleItem <$> items + outIn = outP ++ inP + 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 +paramList ps = "parameter " <> (commaNL . toList $ parameter <$> ps) + +-- | Generates a localparam list. Can only be called with a 'NonEmpty' list. +localParamList :: NonEmpty LocalParam -> Text +localParamList ps = "localparam " <> (commaNL . toList $ localParam <$> ps) + +-- | Generates the assignment for a 'Parameter'. +parameter :: Parameter -> Text +parameter (Parameter name val) = identifier name <> " = " <> constExpr val + +-- | Generates the assignment for a 'LocalParam'. +localParam :: LocalParam -> Text +localParam (LocalParam name val) = identifier name <> " = " <> constExpr val + +identifier :: Identifier -> Text +identifier (Identifier i) = i -- | Conversts 'Port' to 'Text' for the module list, which means it only -- generates a list of identifiers. @@ -76,13 +91,11 @@ modPort p = p ^. portName . getIdentifier -- | Generate the 'Port' description. port :: Port -> Text -port p = t <> sign <> size <> name +port (Port tp sgn low sz (Identifier name)) = t <> sign <> size <> name where - t = flip mappend " " . pType $ p ^. portType - size | p ^. portSize > 1 = "[" <> showT (p ^. portSize - 1) <> ":0] " - | otherwise = "" - name = p ^. portName . getIdentifier - sign = signed $ p ^. portSigned + t = flip mappend " " $ pType tp + size = "[" <> showT (low+sz-1) <> ":" <> showT low <> "] " + sign = signed sgn signed :: Bool -> Text signed True = "signed " @@ -101,8 +114,13 @@ 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" - where makePort = (<> " ") . portDir +moduleItem (Decl dir p ini) = + maybe "" makePort dir <> port p <> maybe "" makeIni ini <> ";\n" + where + makePort = (<> " ") . portDir + makeIni = (" = " <>) . constExpr +moduleItem (ParamDecl p) = paramList p <> ";\n" +moduleItem (LocalParamDecl p) = localParamList p <> ";\n" mConn :: ModConn -> Text mConn (ModConn c ) = expr c @@ -116,17 +134,13 @@ contAssign (ContAssign val e) = -- | Generate 'Function' to 'Text' func :: Function -> Text func SignedFunc = "$signed" -func UnSignedFunc = "$unsigned" +func UnsignedFunc = "$unsigned" -- | Generate 'Expr' to 'Text'. expr :: Expr -> Text expr (BinOp eRhs bin eLhs) = "(" <> expr eRhs <> binaryOp bin <> expr eLhs <> ")" -expr (Number s n) = - "(" <> minus <> showT s <> "'h" <> T.pack (showHex (abs n) "") <> ")" - where - minus | signum n >= 0 = "" - | otherwise = "-" +expr (Number s n) = showNum s n expr (Id i ) = i ^. getIdentifier expr (Concat c ) = "{" <> comma (expr <$> c) <> "}" expr (UnOp u e ) = "(" <> unaryOp u <> expr e <> ")" @@ -134,6 +148,24 @@ expr (Cond l t f) = "(" <> expr l <> " ? " <> expr t <> " : " <> expr f <> ")" 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) "") <> ")" + where + minus | signum n >= 0 = "" + | otherwise = "-" + +constExpr :: ConstExpr -> Text +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 <> "\"" + -- | Convert 'BinaryOperator' to 'Text'. binaryOp :: BinaryOperator -> Text binaryOp BinPlus = " + " @@ -196,9 +228,6 @@ lVal (RegSize i msb lsb) = i ^. getIdentifier <> " [" <> constExpr msb <> ":" <> constExpr lsb <> "]" lVal (RegConcat e) = "{" <> comma (expr <$> e) <> "}" -constExpr :: ConstExpr -> Text -constExpr (ConstExpr num) = showT num - pType :: PortType -> Text pType Wire = "wire" pType Reg = "reg" @@ -212,12 +241,20 @@ statement (EventCtrl e stat ) = event e <> " " <> defMap stat statement (SeqBlock s) = "begin\n" <> fold (statement <$> s) <> "end\n" statement (BlockAssign a ) = genAssign " = " a <> ";\n" statement (NonBlockAssign a ) = genAssign " <= " a <> ";\n" -statement (StatCA a ) = contAssign a statement (TaskEnable t ) = task t <> ";\n" statement (SysTaskEnable t ) = "$" <> task t <> ";\n" 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 task :: Task -> Text task (Task name e) | null e = i @@ -275,19 +312,13 @@ instance Source Port where instance Source ModDecl where genSource = moduleDecl -instance Source Description where - genSource = description - instance Source Verilog where genSource = verilogSrc +instance Source SourceInfo where + genSource (SourceInfo _ src) = genSource src + newtype GenVerilog a = GenVerilog { unGenVerilog :: a } instance (Source a) => Show (GenVerilog a) where show = T.unpack . genSource . unGenVerilog - -instance (Arb a) => Arb (GenVerilog a) where - arb = GenVerilog <$> arb - -instance Source SourceInfo where - genSource (SourceInfo _ src) = genSource src diff --git a/src/VeriFuzz/Verilog/Gen.hs b/src/VeriFuzz/Verilog/Gen.hs index 87a0a31..c325f66 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 @@ -25,9 +26,11 @@ import Control.Monad.Trans.Class (lift) import Control.Monad.Trans.Reader hiding (local) import Control.Monad.Trans.State.Lazy import Data.Foldable (fold) +import Data.List.NonEmpty (toList) import qualified Data.Text as T import Hedgehog (Gen) import qualified Hedgehog.Gen as Hog +import qualified Hedgehog.Range as Hog import VeriFuzz.Config import VeriFuzz.Internal import VeriFuzz.Verilog.AST @@ -35,8 +38,11 @@ import VeriFuzz.Verilog.Internal import VeriFuzz.Verilog.Mutate data Context = Context { _variables :: [Port] - , _nameCounter :: Int - , _stmntDepth :: Int + , _parameters :: [Parameter] + , _modules :: [ModDecl] + , _nameCounter :: {-# UNPACK #-} !Int + , _stmntDepth :: {-# UNPACK #-} !Int + , _modDepth :: {-# UNPACK #-} !Int } makeLenses ''Context @@ -48,7 +54,7 @@ toId = Identifier . ("w" <>) . T.pack . show toPort :: Identifier -> Gen Port toPort ident = do - i <- genPositive + i <- Hog.int $ Hog.linear 1 100 return $ wire i ident sumSize :: [Port] -> Int @@ -56,7 +62,7 @@ sumSize ps = sum $ ps ^.. traverse . portSize random :: [Identifier] -> (Expr -> ContAssign) -> Gen ModItem random ctx fun = do - expr <- Hog.sized (exprWithContext ctx) + expr <- Hog.sized (exprWithContext (ProbExpr 1 1 1 1 1 1 0 1 1) ctx) return . ModCA $ fun expr --randomAssigns :: [Identifier] -> [Gen ModItem] @@ -74,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 @@ -83,9 +93,136 @@ randomMod inps total = do gen :: Gen a -> StateGen a gen = lift . lift +listOf1 :: Gen a -> Gen [a] +listOf1 a = toList <$> Hog.nonEmpty (Hog.linear 0 100) a + +--listOf :: Gen a -> Gen [a] +--listOf = Hog.list (Hog.linear 0 100) + +largeNum :: Gen Int +largeNum = Hog.int Hog.linearBounded + +wireSize :: Gen Int +wireSize = Hog.int $ Hog.linear 2 200 + +binOp :: Gen BinaryOperator +binOp = + Hog.element + [ BinPlus + , BinMinus + , BinTimes + -- , BinDiv + -- , BinMod + , BinEq + , BinNEq + -- , BinCEq + -- , BinCNEq + , BinLAnd + , BinLOr + , BinLT + , BinLEq + , BinGT + , BinGEq + , BinAnd + , BinOr + , BinXor + , BinXNor + , BinXNorInv + -- , BinPower + , BinLSL + , BinLSR + , BinASL + , BinASR + ] + +unOp :: Gen UnaryOperator +unOp = + Hog.element + [ UnPlus + , UnMinus + , UnNot + , UnLNot + , UnAnd + , UnNand + , UnOr + , UnNor + , UnXor + , UnNxor + , UnNxorInv + ] + +constExprWithContext :: [Parameter] -> ProbExpr -> Hog.Size -> Gen ConstExpr +constExprWithContext ps prob size + | size == 0 = Hog.frequency + [ (prob ^. probExprNum, ConstNum <$> wireSize <*> fmap fromIntegral largeNum) + , ( if null ps then 0 else prob ^. probExprId + , ParamId . view paramIdent <$> Hog.element ps + ) + ] + | size > 0 = Hog.frequency + [ (prob ^. probExprNum, ConstNum <$> wireSize <*> fmap fromIntegral largeNum) + , ( if null ps then 0 else prob ^. probExprId + , ParamId . view paramIdent <$> Hog.element ps + ) + , (prob ^. probExprUnOp, ConstUnOp <$> unOp <*> subexpr 2) + , ( prob ^. probExprBinOp + , ConstBinOp <$> subexpr 2 <*> binOp <*> 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 <$> wireSize <*> fmap fromIntegral largeNum + ) + ] + +exprRecList :: ProbExpr -> (Hog.Size -> Gen Expr) -> [(Int, Gen Expr)] +exprRecList prob subexpr = + [ ( prob ^. probExprNum + , Number <$> wireSize <*> fmap fromIntegral largeNum + ) + , (prob ^. probExprConcat , Concat <$> listOf1 (subexpr 8)) + , (prob ^. probExprUnOp , UnOp <$> unOp <*> subexpr 2) + , (prob ^. probExprStr, Str <$> Hog.text (Hog.linear 0 100) Hog.alphaNum) + , (prob ^. probExprBinOp , BinOp <$> subexpr 2 <*> binOp <*> 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) + ] + +exprWithContext :: ProbExpr -> [Identifier] -> Hog.Size -> Gen Expr +exprWithContext prob [] n | n == 0 = Hog.frequency $ exprSafeList prob + | n > 0 = Hog.frequency $ exprRecList prob subexpr + | 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 + where subexpr y = exprWithContext prob l $ n `div` y + some :: StateGen a -> StateGen [a] some f = do - amount <- gen genPositive + amount <- gen $ Hog.int (Hog.linear 1 100) + replicateM amount f + +many :: StateGen a -> StateGen [a] +many f = do + amount <- gen $ Hog.int (Hog.linear 0 100) replicateM amount f makeIdentifier :: T.Text -> StateGen Identifier @@ -98,32 +235,28 @@ makeIdentifier prefix = do newPort :: PortType -> StateGen Port newPort pt = do ident <- makeIdentifier . T.toLower $ showT pt - p <- gen $ Port pt <$> arb <*> genPositive <*> pure ident + p <- gen $ Port pt <$> Hog.bool <*> pure 0 <*> wireSize <*> pure ident variables %= (p :) return p -choose :: PortType -> Port -> Bool -choose ptype (Port a _ _ _) = ptype == a - scopedExpr :: StateGen Expr scopedExpr = do context <- get - gen - . Hog.sized - . exprWithContext - $ context - ^.. variables - . traverse - . portName + prob <- askProbability + gen . Hog.sized . exprWithContext (prob ^. probExpr) $ vars context + where + vars cont = + (cont ^.. variables . traverse . portName) + <> (cont ^.. parameters . traverse . paramIdent) contAssign :: StateGen ContAssign contAssign = do expr <- scopedExpr - p <- newPort Wire + p <- newPort Wire return $ ContAssign (p ^. portName) expr lvalFromPort :: Port -> LVal -lvalFromPort (Port _ _ _ i) = RegId i +lvalFromPort (Port _ _ _ _ i) = RegId i probability :: Config -> Probability probability c = c ^. configProbability @@ -137,23 +270,51 @@ assignment = do lval <- lvalFromPort <$> newPort Reg return $ Assign lval Nothing expr -conditional :: StateGen Statement -conditional = do - expr <- scopedExpr +seqBlock :: StateGen Statement +seqBlock = do stmntDepth -= 1 tstat <- SeqBlock <$> some statement - fstat <- Hog.maybe $ SeqBlock <$> some statement stmntDepth += 1 - return $ CondStmnt (BinOp expr BinEq 0) (Just tstat) fstat + return tstat + +conditional :: StateGen Statement +conditional = do + expr <- scopedExpr + tstat <- seqBlock + fstat <- Hog.maybe seqBlock + return $ CondStmnt expr (Just tstat) fstat + +--constToExpr :: ConstExpr -> Expr +--constToExpr (ConstNum s n ) = Number s n +--constToExpr (ParamId i ) = Id i +--constToExpr (ConstConcat c ) = Concat $ constToExpr <$> c +--constToExpr (ConstUnOp u p ) = UnOp u (constToExpr p) +--constToExpr (ConstBinOp a b c) = BinOp (constToExpr a) b (constToExpr c) +--constToExpr (ConstCond a b c) = +-- Cond (constToExpr a) (constToExpr b) (constToExpr c) +--constToExpr (ConstStr s) = Str s + +forLoop :: StateGen Statement +forLoop = do + num <- Hog.int (Hog.linear 0 20) + var <- lvalFromPort <$> newPort Reg + stats <- seqBlock + return $ ForLoop (Assign var Nothing 0) + (BinOp (varId var) BinLT $ fromIntegral num) + (Assign var Nothing $ BinOp (varId var) BinPlus 1) + stats + where varId v = Id (v ^. regId) statement :: StateGen Statement statement = do prob <- askProbability cont <- get + let defProb i = prob ^. probStmnt . i Hog.frequency - [ (prob ^. probBlock , BlockAssign <$> assignment) - , (prob ^. probNonBlock , NonBlockAssign <$> assignment) - , (onDepth cont (prob ^. probCond), conditional) + [ (defProb probStmntBlock , BlockAssign <$> assignment) + , (defProb probStmntNonBlock , NonBlockAssign <$> assignment) + , (onDepth cont (defProb probStmntCond), conditional) + , (onDepth cont (defProb probStmntFor) , forLoop) ] where onDepth c n = if c ^. stmntDepth > 0 then n else 0 @@ -162,26 +323,98 @@ 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 - [ (prob ^. probAssign, ModCA <$> contAssign) - , (prob ^. probAlways, always) + [ (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 +moduleName Nothing = makeIdentifier "module" -initialBlock :: StateGen ModItem -initialBlock = do +constExpr :: StateGen ConstExpr +constExpr = do + prob <- askProbability context <- get - let l = filter (choose Reg) $ context ^.. variables . traverse - return . Initial . SeqBlock $ makeAssign <$> l - where - makeAssign p = NonBlockAssign $ Assign (lvalFromPort p) Nothing 0 + gen . Hog.sized $ constExprWithContext (context ^. parameters) + (prob ^. probExpr) + +parameter :: StateGen Parameter +parameter = do + ident <- makeIdentifier "param" + cexpr <- constExpr + let param = Parameter ident cexpr + parameters %= (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 @@ -191,22 +424,29 @@ moduleDef :: Maybe Identifier -> StateGen ModDecl moduleDef top = do name <- moduleName top portList <- some $ newPort Wire - mi <- some modItem + mi <- Hog.list (Hog.linear 4 100) 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 - return . declareMod local . ModDecl name [yport] (clock:portList) $ initBlock : mi <> [comb] + let clock = Port Wire False 0 1 "clk" + let yport = Port Wire False 0 size "y" + 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 . (: []) . Description <$> 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 5999a31..63072b1 100644 --- a/src/VeriFuzz/Verilog/Internal.hs +++ b/src/VeriFuzz/Verilog/Internal.hs @@ -16,7 +16,7 @@ module VeriFuzz.Verilog.Internal , emptyMod , setModName , addModPort - , addDescription + , addModDecl , testBench , addTestBench , defaultPort @@ -33,14 +33,14 @@ 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 0 1 i) Nothing wireDecl :: Identifier -> ModItem -wireDecl = Decl Nothing . Port Wire False 1 +wireDecl i = Decl Nothing (Port Wire False 0 1 i) Nothing -- | Create an empty module. emptyMod :: ModDecl -emptyMod = ModDecl "" [] [] [] +emptyMod = ModDecl "" [] [] [] [] -- | Set a module name for a module declaration. setModName :: Text -> ModDecl -> ModDecl @@ -50,8 +50,8 @@ setModName str = modId .~ Identifier str addModPort :: Port -> ModDecl -> ModDecl addModPort port = modInPorts %~ (:) port -addDescription :: Description -> Verilog -> Verilog -addDescription desc = getVerilog %~ (:) desc +addModDecl :: ModDecl -> Verilog -> Verilog +addModDecl desc = getVerilog %~ (:) desc testBench :: ModDecl testBench = ModDecl @@ -76,24 +76,25 @@ testBench = ModDecl -- , SysTaskEnable $ Task "finish" [] ] ] + [] addTestBench :: Verilog -> Verilog -addTestBench = addDescription $ Description testBench +addTestBench = addModDecl testBench defaultPort :: Identifier -> Port -defaultPort = Port Wire False 1 +defaultPort = Port Wire False 0 1 portToExpr :: Port -> Expr -portToExpr (Port _ _ _ i) = Id i +portToExpr (Port _ _ _ _ i) = Id i modName :: ModDecl -> Text modName = view $ modId . getIdentifier yPort :: Identifier -> Port -yPort = Port Wire False 90 +yPort = Port Wire False 0 90 wire :: Int -> Identifier -> Port -wire = Port Wire False +wire = Port Wire False 0 reg :: Int -> Identifier -> Port -reg = Port Reg False +reg = Port Reg False 0 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 diff --git a/src/VeriFuzz/Verilog/Parser.hs b/src/VeriFuzz/Verilog/Parser.hs index a072ce8..518bcb9 100644 --- a/src/VeriFuzz/Verilog/Parser.hs +++ b/src/VeriFuzz/Verilog/Parser.hs @@ -106,7 +106,7 @@ systemFunc s = satisfy' matchId parseFunction :: Parser Function parseFunction = systemFunc "$unsigned" - $> UnSignedFunc + $> UnsignedFunc <|> systemFunc "$signed" $> SignedFunc @@ -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 0 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 @@ -298,14 +298,12 @@ parseModDecl = do (modPorts PortOut modItem) (modPorts PortIn modItem) modItem - -parseDescription :: Parser Description -parseDescription = Description <$> parseModDecl + [] -- | Parses a 'String' into 'Verilog' by skipping any beginning whitespace -- and then parsing multiple Verilog source. parseVerilogSrc :: Parser Verilog -parseVerilogSrc = Verilog <$> many parseDescription +parseVerilogSrc = Verilog <$> many parseModDecl -- | Parse a 'String' containing verilog code. The parser currently only supports -- the subset of Verilog that is being generated randomly. diff --git a/src/VeriFuzz/Verilog/Preprocess.hs b/src/VeriFuzz/Verilog/Preprocess.hs index fead5f0..6e9305a 100644 --- a/src/VeriFuzz/Verilog/Preprocess.hs +++ b/src/VeriFuzz/Verilog/Preprocess.hs @@ -20,7 +20,9 @@ module VeriFuzz.Verilog.Preprocess ) where --- | Remove comments from code. +-- | Remove comments from code. There is no difference between @(* *)@ and +-- @/* */@, therefore in this implementation, @*/@ could close @(*@ and vice-versa, +-- This will be fixed in an upcoming version. uncomment :: FilePath -> String -> String uncomment file = uncomment' where @@ -28,6 +30,7 @@ uncomment file = uncomment' "" -> "" '/' : '/' : rest -> " " ++ removeEOL rest '/' : '*' : rest -> " " ++ remove rest + '(' : '*' : rest -> " " ++ remove rest '"' : rest -> '"' : ignoreString rest b : rest -> b : uncomment' rest @@ -43,6 +46,7 @@ uncomment file = uncomment' '\n' : rest -> '\n' : remove rest '\t' : rest -> '\t' : remove rest '*' : '/' : rest -> " " ++ uncomment' rest + '*' : ')' : rest -> " " ++ uncomment' rest _ : rest -> " " ++ remove rest removeString a = case a of @@ -105,4 +109,3 @@ ppLine env ('`' : a) = case lookup name env of a rest = drop (length name) a ppLine env (a : b) = a : ppLine env b - |