diff options
Diffstat (limited to 'src/Verismith')
34 files changed, 7401 insertions, 0 deletions
diff --git a/src/Verismith/Circuit.hs b/src/Verismith/Circuit.hs new file mode 100644 index 0000000..81eec12 --- /dev/null +++ b/src/Verismith/Circuit.hs @@ -0,0 +1,45 @@ +{-| +Module : Verismith.Circuit +Description : Definition of the circuit graph. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Definition of the circuit graph. +-} + +module Verismith.Circuit + ( -- * Circuit + Gate(..) + , Circuit(..) + , CNode(..) + , CEdge(..) + , fromGraph + , generateAST + , rDups + , rDupsCirc + , randomDAG + , genRandomDAG + ) +where + +import Control.Lens +import Hedgehog (Gen) +import qualified Hedgehog.Gen as Hog +import Verismith.Circuit.Base +import Verismith.Circuit.Gen +import Verismith.Circuit.Random +import Verismith.Verilog.AST +import Verismith.Verilog.Mutate + +fromGraph :: Gen ModDecl +fromGraph = do + gr <- rDupsCirc <$> Hog.resize 100 randomDAG + return + $ initMod + . head + $ nestUpTo 5 (generateAST gr) + ^.. _Wrapped + . traverse diff --git a/src/Verismith/Circuit/Base.hs b/src/Verismith/Circuit/Base.hs new file mode 100644 index 0000000..9a5ab34 --- /dev/null +++ b/src/Verismith/Circuit/Base.hs @@ -0,0 +1,44 @@ +{-| +Module : Verismith.Circuit.Base +Description : Base types for the circuit module. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Base types for the circuit module. +-} + +module Verismith.Circuit.Base + ( Gate(..) + , Circuit(..) + , CNode(..) + , CEdge(..) + ) +where + +import Data.Graph.Inductive (Gr, LEdge, LNode) +import System.Random + +-- | The types for all the gates. +data Gate = And + | Or + | Xor + deriving (Show, Eq, Enum, Bounded, Ord) + +-- | Newtype for the Circuit which implements a Graph from fgl. +newtype Circuit = Circuit { getCircuit :: Gr Gate () } + +-- | Newtype for a node in the circuit, which is an 'LNode Gate'. +newtype CNode = CNode { getCNode :: LNode Gate } + +-- | Newtype for a named edge which is empty, as it does not need a label. +newtype CEdge = CEdge { getCEdge :: LEdge () } + +instance Random Gate where + randomR (a, b) g = + case randomR (fromEnum a, fromEnum b) g of + (x, g') -> (toEnum x, g') + + random = randomR (minBound, maxBound) diff --git a/src/Verismith/Circuit/Gen.hs b/src/Verismith/Circuit/Gen.hs new file mode 100644 index 0000000..c5cb697 --- /dev/null +++ b/src/Verismith/Circuit/Gen.hs @@ -0,0 +1,79 @@ +{-| +Module : Verilog.Circuit.Gen +Description : Generate verilog from circuit. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Generate verilog from circuit. +-} + +module Verismith.Circuit.Gen + ( generateAST + ) +where + +import Data.Graph.Inductive (LNode, Node) +import qualified Data.Graph.Inductive as G +import Data.Maybe (catMaybes) +import Verismith.Circuit.Base +import Verismith.Circuit.Internal +import Verismith.Verilog.AST +import Verismith.Verilog.Mutate + +-- | Converts a 'CNode' to an 'Identifier'. +frNode :: Node -> Identifier +frNode = Identifier . fromNode + +-- | Converts a 'Gate' to a 'BinaryOperator', which should be a bijective +-- mapping. +fromGate :: Gate -> BinaryOperator +fromGate And = BinAnd +fromGate Or = BinOr +fromGate Xor = BinXor + +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 + +-- | Generates the nested expression AST, so that it can then generate the +-- assignment expressions. +genAssignExpr :: Gate -> [Node] -> Maybe Expr +genAssignExpr _ [] = Nothing +genAssignExpr _ [n ] = Just . Id $ frNode n +genAssignExpr g (n : ns) = BinOp wire oper <$> genAssignExpr g ns + where + wire = Id $ frNode n + oper = fromGate g + +-- | Generate the continuous assignment AST for a particular node. If it does +-- not have any nodes that link to it then return 'Nothing', as that means that +-- the assignment will just be empty. +genContAssignAST :: Circuit -> LNode Gate -> Maybe ModItem +genContAssignAST c (n, g) = ModCA . ContAssign name <$> genAssignExpr g nodes + where + gr = getCircuit c + nodes = G.pre gr n + name = frNode n + +genAssignAST :: Circuit -> [ModItem] +genAssignAST c = catMaybes $ genContAssignAST c <$> nodes + where + gr = getCircuit c + nodes = G.labNodes gr + +genModuleDeclAST :: Circuit -> ModDecl +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" + +generateAST :: Circuit -> Verilog +generateAST c = Verilog [genModuleDeclAST c] diff --git a/src/Verismith/Circuit/Internal.hs b/src/Verismith/Circuit/Internal.hs new file mode 100644 index 0000000..4de2252 --- /dev/null +++ b/src/Verismith/Circuit/Internal.hs @@ -0,0 +1,55 @@ +{-| +Module : Verismith.Circuit.Internal +Description : Internal helpers for generation. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Internal helpers for generation. +-} + +module Verismith.Circuit.Internal + ( fromNode + , filterGr + , only + , inputs + , outputs + ) +where + +import Data.Graph.Inductive (Graph, Node) +import qualified Data.Graph.Inductive as G +import qualified Data.Text as T + +-- | Convert an integer into a label. +-- +-- >>> fromNode 5 +-- "w5" +fromNode :: Int -> T.Text +fromNode node = T.pack $ "w" <> show node + +-- | General function which runs 'filter' over a graph. +filterGr :: (Graph gr) => gr n e -> (Node -> Bool) -> [Node] +filterGr graph f = filter f $ G.nodes graph + +-- | Takes two functions that return an 'Int', and compares there results to 0 +-- and not 0 respectively. This result is returned. +only + :: (Graph gr) + => gr n e + -> (gr n e -> Node -> Int) + -> (gr n e -> Node -> Int) + -> Node + -> Bool +only graph fun1 fun2 n = fun1 graph n == 0 && fun2 graph n /= 0 + +-- | Returns all the input nodes to a graph, which means nodes that do not have +-- an input themselves. +inputs :: (Graph gr) => gr n e -> [Node] +inputs graph = filterGr graph $ only graph G.indeg G.outdeg + +-- | Returns all the output nodes to a graph, similar to the 'inputs' function. +outputs :: (Graph gr) => gr n e -> [Node] +outputs graph = filterGr graph $ only graph G.outdeg G.indeg diff --git a/src/Verismith/Circuit/Random.hs b/src/Verismith/Circuit/Random.hs new file mode 100644 index 0000000..0eabf56 --- /dev/null +++ b/src/Verismith/Circuit/Random.hs @@ -0,0 +1,67 @@ +{-| +Module : Verismith.Circuit.Random +Description : Random generation for DAG +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Define the random generation for the directed acyclic graph. +-} + +module Verismith.Circuit.Random + ( rDups + , rDupsCirc + , randomDAG + , genRandomDAG + ) +where + +import Data.Graph.Inductive (Context) +import qualified Data.Graph.Inductive as G +import Data.Graph.Inductive.PatriciaTree (Gr) +import Data.List (nub) +import Hedgehog (Gen) +import qualified Hedgehog.Gen as Hog +import qualified Hedgehog.Range as Hog +import Verismith.Circuit.Base + +dupFolder :: (Eq a, Eq b) => Context a b -> [Context a b] -> [Context a b] +dupFolder cont ns = unique cont : ns + where unique (a, b, c, d) = (nub a, b, c, nub d) + +-- | Remove duplicates. +rDups :: (Eq a, Eq b) => Gr a b -> Gr a b +rDups g = G.buildGr $ G.ufold dupFolder [] g + +-- | Remove duplicates. +rDupsCirc :: Circuit -> Circuit +rDupsCirc = Circuit . rDups . getCircuit + +-- | Gen instance to create an arbitrary edge, where the edges are limited by +-- `n` that is passed to it. +arbitraryEdge :: Hog.Size -> Gen CEdge +arbitraryEdge n = do + x <- with $ \a -> a < n && a > 0 && a /= n - 1 + y <- with $ \a -> x < a && a < n && a > 0 + return $ CEdge (fromIntegral x, fromIntegral y, ()) + where + with = flip Hog.filter $ fromIntegral <$> Hog.resize + n + (Hog.int (Hog.linear 0 100)) + +-- | Gen instance for a random acyclic DAG. +randomDAG :: Gen Circuit -- ^ The generated graph. It uses Arbitrary to generate + -- random instances of each node +randomDAG = do + list <- Hog.list (Hog.linear 1 100) $ Hog.enum minBound maxBound + l <- Hog.list (Hog.linear 10 1000) aE + return . Circuit $ G.mkGraph (nodes list) l + where + nodes l = zip [0 .. length l - 1] l + aE = getCEdge <$> Hog.sized arbitraryEdge + +-- | Generate a random acyclic DAG with an IO instance. +genRandomDAG :: IO Circuit +genRandomDAG = Hog.sample randomDAG diff --git a/src/Verismith/Config.hs b/src/Verismith/Config.hs new file mode 100644 index 0000000..bf79683 --- /dev/null +++ b/src/Verismith/Config.hs @@ -0,0 +1,511 @@ +{-| +Module : Verismith.Config +Description : Configuration file format and parser. +Copyright : (c) 2019, Yann Herklotz +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +TOML Configuration file format and parser. +-} + +{-# LANGUAGE TemplateHaskell #-} + +module Verismith.Config + ( -- * TOML Configuration + -- $conf + Config(..) + , defaultConfig + -- ** Probabilities + , Probability(..) + -- *** Expression + , ProbExpr(..) + -- *** Module Item + , ProbModItem(..) + -- *** Statement + , ProbStatement(..) + -- ** ConfProperty + , ConfProperty(..) + -- ** Simulator Description + , SimDescription(..) + -- ** Synthesiser Description + , SynthDescription(..) + -- * Useful Lenses + , fromXST + , fromYosys + , fromVivado + , fromQuartus + , configProbability + , configProperty + , configSimulators + , configSynthesisers + , probModItem + , probStmnt + , probExpr + , probExprNum + , probExprId + , probExprRangeSelect + , probExprUnOp + , probExprBinOp + , probExprCond + , probExprConcat + , probExprStr + , probExprSigned + , probExprUnsigned + , probModItemAssign + , probModItemSeqAlways + , probModItemCombAlways + , probModItemInst + , probStmntBlock + , probStmntNonBlock + , probStmntCond + , probStmntFor + , propSampleSize + , propSampleMethod + , propSize + , propSeed + , propStmntDepth + , propModDepth + , propMaxModules + , propCombine + , propDeterminism + , propNonDeterminism + , parseConfigFile + , parseConfig + , encodeConfig + , encodeConfigFile + , versionInfo + ) +where + +import Control.Applicative (Alternative) +import Control.Lens hiding ((.=)) +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Maybe (fromMaybe) +import Data.Text (Text, pack) +import qualified Data.Text.IO as T +import Data.Version (showVersion) +import Development.GitRev +import Hedgehog.Internal.Seed (Seed) +import Paths_verismith (version) +import Shelly (toTextIgnore) +import Toml (TomlCodec, (.=)) +import qualified Toml +import Verismith.Tool.Quartus +import Verismith.Tool.Vivado +import Verismith.Tool.XST +import Verismith.Tool.Yosys + +-- $conf +-- +-- Verismith supports a TOML configuration file that can be passed using the @-c@ +-- flag or using the 'parseConfig' and 'encodeConfig' functions. The +-- configuration can then be manipulated using the lenses that are also provided +-- in this module. +-- +-- The configuration file can be used to tweak the random Verilog generation by +-- passing different probabilities to each of the syntax nodes in the AST. It +-- can also be used to specify which simulators to fuzz with which options. A +-- seed for the run can also be set, to replay a previous run using the same +-- exact generation. A default value is associated with each key in the +-- configuration file, which means that only the options that need overriding +-- can be added to the configuration. The defaults can be observed in +-- 'defaultConfig' or when running @verismith config@. +-- +-- == Configuration Sections +-- +-- There are four main configuration sections in the TOML file: +-- +-- [@probability@] The @probability@ section defines the probabilities at +-- every node in the AST. +-- +-- [@property@] Controls different properties of the generation, such as +-- adding a seed or the depth of the statements. +-- +-- [@simulator@] This is an array of tables containing descriptions of the +-- different simulators that should be used. It currently only supports +-- <http://iverilog.icarus.com/ Icarus Verilog>. +-- +-- [@synthesiser@] This is also an array of tables containing descriptions of +-- the different synthesisers that should be used. The synthesisers that are +-- currently supported are: +-- +-- - <https://www.intel.com/content/www/us/en/programmable/downloads/download-center.html Quartus> +-- - <https://www.xilinx.com/products/design-tools/ise-design-suite.html ISE Design Suite> +-- - <https://www.xilinx.com/products/design-tools/ise-design-suite.html Vivado Design Suite> +-- - <http://www.clifford.at/yosys/ Yosys Open SYnthesis Suite> + +-- | Probability of different expressions nodes. +data ProbExpr = ProbExpr { _probExprNum :: {-# UNPACK #-} !Int + -- ^ Probability of generation a number like + -- @4'ha@. This should never be set to 0, as it is used + -- as a fallback in case there are no viable + -- identifiers, such as none being in scope. + , _probExprId :: {-# UNPACK #-} !Int + -- ^ Probability of generating an identifier that is in + -- scope and of the right type. + , _probExprRangeSelect :: {-# UNPACK #-} !Int + -- ^ Probability of generating a range selection from a port. + , _probExprUnOp :: {-# UNPACK #-} !Int + -- ^ Probability of generating a unary operator. + , _probExprBinOp :: {-# UNPACK #-} !Int + -- ^ Probability of generation a binary operator. + , _probExprCond :: {-# UNPACK #-} !Int + -- ^ probability of generating a conditional ternary + -- operator. + , _probExprConcat :: {-# UNPACK #-} !Int + -- ^ Probability of generating a concatenation. + , _probExprStr :: {-# UNPACK #-} !Int + -- ^ Probability of generating a string. This is not + -- fully supported therefore currently cannot be set. + , _probExprSigned :: {-# UNPACK #-} !Int + -- ^ Probability of generating a signed function + -- @$signed(...)@. + , _probExprUnsigned :: {-# UNPACK #-} !Int + -- ^ Probability of generating an unsigned function + -- @$unsigned(...)@. + } + deriving (Eq, Show) + +-- | Probability of generating different nodes inside a module declaration. +data ProbModItem = ProbModItem { _probModItemAssign :: {-# UNPACK #-} !Int + -- ^ Probability of generating an @assign@. + , _probModItemSeqAlways :: {-# UNPACK #-} !Int + -- ^ Probability of generating a sequential @always@ block. + , _probModItemCombAlways :: {-# UNPACK #-} !Int + -- ^ Probability of generating an combinational @always@ block. + , _probModItemInst :: {-# UNPACK #-} !Int + -- ^ Probability of generating a module + -- instantiation. + } + deriving (Eq, Show) + +data ProbStatement = ProbStatement { _probStmntBlock :: {-# UNPACK #-} !Int + , _probStmntNonBlock :: {-# UNPACK #-} !Int + , _probStmntCond :: {-# UNPACK #-} !Int + , _probStmntFor :: {-# UNPACK #-} !Int + } + deriving (Eq, Show) + +data Probability = Probability { _probModItem :: {-# UNPACK #-} !ProbModItem + , _probStmnt :: {-# UNPACK #-} !ProbStatement + , _probExpr :: {-# UNPACK #-} !ProbExpr + } + deriving (Eq, Show) + +data ConfProperty = ConfProperty { _propSize :: {-# UNPACK #-} !Int + -- ^ The size of the generated Verilog. + , _propSeed :: !(Maybe Seed) + -- ^ A possible seed that could be used to + -- generate the same Verilog. + , _propStmntDepth :: {-# UNPACK #-} !Int + -- ^ The maximum statement depth that should be + -- reached. + , _propModDepth :: {-# UNPACK #-} !Int + -- ^ The maximium module depth that should be + -- reached. + , _propMaxModules :: {-# UNPACK #-} !Int + -- ^ The maximum number of modules that are + -- allowed to be created at each level. + , _propSampleMethod :: !Text + -- ^ The sampling method that should be used to + -- generate specific distributions of random + -- programs. + , _propSampleSize :: {-# UNPACK #-} !Int + -- ^ The number of samples to take for the + -- sampling method. + , _propCombine :: !Bool + -- ^ If the output should be combined into one + -- bit or not. + , _propNonDeterminism :: {-# UNPACK #-} !Int + -- ^ The frequency at which nondeterminism + -- should be generated. + , _propDeterminism :: {-# UNPACK #-} !Int + -- ^ The frequency at which determinism should + -- be generated. + } + deriving (Eq, Show) + +data Info = Info { _infoCommit :: !Text + , _infoVersion :: !Text + } + deriving (Eq, Show) + +data SimDescription = SimDescription { simName :: {-# UNPACK #-} !Text } + deriving (Eq, Show) + +data SynthDescription = SynthDescription { synthName :: {-# UNPACK #-} !Text + , synthBin :: Maybe Text + , synthDesc :: Maybe Text + , synthOut :: Maybe Text + } + deriving (Eq, Show) + +data Config = Config { _configInfo :: Info + , _configProbability :: {-# UNPACK #-} !Probability + , _configProperty :: {-# UNPACK #-} !ConfProperty + , _configSimulators :: [SimDescription] + , _configSynthesisers :: [SynthDescription] + } + deriving (Eq, Show) + +$(makeLenses ''ProbExpr) +$(makeLenses ''ProbModItem) +$(makeLenses ''ProbStatement) +$(makeLenses ''Probability) +$(makeLenses ''ConfProperty) +$(makeLenses ''Info) +$(makeLenses ''Config) + +defaultValue + :: (Alternative r, Applicative w) + => b + -> Toml.Codec r w a b + -> Toml.Codec r w a b +defaultValue x = Toml.dimap Just (fromMaybe x) . Toml.dioptional + +fromXST :: XST -> SynthDescription +fromXST (XST a b c) = + SynthDescription "xst" (toTextIgnore <$> a) (Just b) (Just $ toTextIgnore c) + +fromYosys :: Yosys -> SynthDescription +fromYosys (Yosys a b c) = SynthDescription "yosys" + (toTextIgnore <$> a) + (Just b) + (Just $ toTextIgnore c) + +fromVivado :: Vivado -> SynthDescription +fromVivado (Vivado a b c) = SynthDescription "vivado" + (toTextIgnore <$> a) + (Just b) + (Just $ toTextIgnore c) + +fromQuartus :: Quartus -> SynthDescription +fromQuartus (Quartus a b c) = SynthDescription "quartus" + (toTextIgnore <$> a) + (Just b) + (Just $ toTextIgnore c) + +defaultConfig :: Config +defaultConfig = Config + (Info (pack $(gitHash)) (pack $ showVersion version)) + (Probability defModItem defStmnt defExpr) + defProperty + [] + [fromYosys defaultYosys, fromVivado defaultVivado] + where + defModItem = + ProbModItem { _probModItemAssign = 5 + , _probModItemSeqAlways = 1 + , _probModItemCombAlways = 0 + , _probModItemInst = 1 + } + defStmnt = + ProbStatement { _probStmntBlock = 0 + , _probStmntNonBlock = 3 + , _probStmntCond = 1 + , _probStmntFor = 0 + } + defExpr = + ProbExpr { _probExprNum = 1 + , _probExprId = 5 + , _probExprRangeSelect = 5 + , _probExprUnOp = 5 + , _probExprBinOp = 5 + , _probExprCond = 5 + , _probExprConcat = 3 + , _probExprStr = 0 + , _probExprSigned = 5 + , _probExprUnsigned = 5 + } + defProperty = + ConfProperty { _propSize = 20 + , _propSeed = Nothing + , _propStmntDepth = 3 + , _propModDepth = 2 + , _propMaxModules = 5 + , _propSampleMethod = "random" + , _propSampleSize = 10 + , _propCombine = False + , _propNonDeterminism = 0 + , _propDeterminism = 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 probExprRangeSelect) (intE "rangeselect") + .= _probExprRangeSelect + <*> 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 probModItemSeqAlways) (intM "sequential") + .= _probModItemSeqAlways + <*> defaultValue (defProb probModItemCombAlways) (intM "combinational") + .= _probModItemCombAlways + <*> 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 + where defProb i = defaultConfig ^. configProbability . i + +propCodec :: TomlCodec ConfProperty +propCodec = + ConfProperty + <$> defaultValue (defProp propSize) (Toml.int "size") + .= _propSize + <*> Toml.dioptional (Toml.read "seed") + .= _propSeed + <*> defaultValue (defProp propStmntDepth) (int "statement" "depth") + .= _propStmntDepth + <*> defaultValue (defProp propModDepth) (int "module" "depth") + .= _propModDepth + <*> defaultValue (defProp propMaxModules) (int "module" "max") + .= _propMaxModules + <*> defaultValue (defProp propSampleMethod) + (Toml.text (twoKey "sample" "method")) + .= _propSampleMethod + <*> defaultValue (defProp propSampleSize) (int "sample" "size") + .= _propSampleSize + <*> defaultValue (defProp propCombine) + (Toml.bool (twoKey "output" "combine")) + .= _propCombine + <*> defaultValue (defProp propNonDeterminism) (Toml.int "nondeterminism") + .= _propNonDeterminism + <*> defaultValue (defProp propDeterminism) (Toml.int "determinism") + .= _propDeterminism + where defProp i = defaultConfig ^. configProperty . i + +simulator :: TomlCodec SimDescription +simulator = Toml.textBy pprint parseIcarus "name" + where + parseIcarus i@"icarus" = Right $ SimDescription i + parseIcarus s = Left $ "Could not match '" <> s <> "' with a simulator." + pprint (SimDescription a) = a + +synthesiser :: TomlCodec SynthDescription +synthesiser = + SynthDescription + <$> Toml.text "name" + .= synthName + <*> Toml.dioptional (Toml.text "bin") + .= synthBin + <*> Toml.dioptional (Toml.text "description") + .= synthDesc + <*> Toml.dioptional (Toml.text "output") + .= synthOut + +infoCodec :: TomlCodec Info +infoCodec = + Info + <$> defaultValue (defaultConfig ^. configInfo . infoCommit) + (Toml.text "commit") + .= _infoCommit + <*> defaultValue (defaultConfig ^. configInfo . infoVersion) + (Toml.text "version") + .= _infoVersion + +configCodec :: TomlCodec Config +configCodec = + Config + <$> defaultValue (defaultConfig ^. configInfo) + (Toml.table infoCodec "info") + .= _configInfo + <*> defaultValue (defaultConfig ^. configProbability) + (Toml.table probCodec "probability") + .= _configProbability + <*> defaultValue (defaultConfig ^. configProperty) + (Toml.table propCodec "property") + .= _configProperty + <*> defaultValue (defaultConfig ^. configSimulators) + (Toml.list simulator "simulator") + .= _configSimulators + <*> defaultValue (defaultConfig ^. configSynthesisers) + (Toml.list synthesiser "synthesiser") + .= _configSynthesisers + +parseConfigFile :: FilePath -> IO Config +parseConfigFile = Toml.decodeFile configCodec + +parseConfig :: Text -> Config +parseConfig t = case Toml.decode configCodec t of + Right c -> c + Left Toml.TrivialError -> error "Trivial error while parsing Toml config" + Left (Toml.KeyNotFound k) -> error $ "Key " ++ show k ++ " not found" + Left (Toml.TableNotFound k) -> error $ "Table " ++ show k ++ " not found" + Left (Toml.TypeMismatch k _ _) -> + error $ "Type mismatch with key " ++ show k + Left _ -> error "Config file parse error" + +encodeConfig :: Config -> Text +encodeConfig = Toml.encode configCodec + +encodeConfigFile :: FilePath -> Config -> IO () +encodeConfigFile f = T.writeFile f . encodeConfig + +versionInfo :: String +versionInfo = + "Verismith " + <> showVersion version + <> " (" + <> $(gitCommitDate) + <> " " + <> $(gitHash) + <> ")" diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs new file mode 100644 index 0000000..d14e74b --- /dev/null +++ b/src/Verismith/Fuzz.hs @@ -0,0 +1,527 @@ +{-| +Module : Verismith.Fuzz +Description : Environment to run the simulator and synthesisers in a matrix. +Copyright : (c) 2019, Yann Herklotz +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Environment to run the simulator and synthesisers in a matrix. +-} + +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TemplateHaskell #-} + +module Verismith.Fuzz + ( Fuzz (..) + , FuzzOpts (..) + , fuzz + , fuzzInDir + , fuzzMultiple + , runFuzz + , sampleSeed + -- * Helpers + , make + , pop + ) +where + +import Control.DeepSeq (force) +import Control.Exception.Lifted (finally) +import Control.Lens hiding ((<.>)) +import Control.Monad (forM, replicateM) +import Control.Monad.IO.Class +import Control.Monad.Reader +import Control.Monad.State.Strict +import Control.Monad.Trans.Control (MonadBaseControl) +import qualified Crypto.Random.DRBG as C +import Data.ByteString (ByteString) +import Data.List (nubBy, sort) +import Data.Maybe (fromMaybe, isNothing) +import Data.Text (Text) +import qualified Data.Text as T +import Data.Time +import Data.Tuple (swap) +import Hedgehog (Gen) +import qualified Hedgehog.Internal.Gen as Hog +import Hedgehog.Internal.Seed (Seed) +import qualified Hedgehog.Internal.Seed as Hog +import qualified Hedgehog.Internal.Tree as Hog +import Prelude hiding (FilePath) +import Shelly hiding (get) +import Shelly.Lifted (MonadSh, liftSh) +import System.FilePath.Posix (takeBaseName) +import Verismith.Config +import Verismith.Internal +import Verismith.Reduce +import Verismith.Report +import Verismith.Result +import Verismith.Tool.Icarus +import Verismith.Tool.Internal +import Verismith.Tool.Yosys +import Verismith.Verilog.AST +import Verismith.Verilog.CodeGen + +data FuzzOpts = FuzzOpts { _fuzzOptsOutput :: !(Maybe FilePath) + , _fuzzOptsForced :: !Bool + , _fuzzOptsKeepAll :: !Bool + , _fuzzOptsIterations :: {-# UNPACK #-} !Int + , _fuzzOptsNoSim :: !Bool + , _fuzzOptsNoEquiv :: !Bool + , _fuzzOptsNoReduction :: !Bool + , _fuzzOptsConfig :: {-# UNPACK #-} !Config + , _fuzzDataDir :: {-# UNPACK #-} !FilePath + } + deriving (Show, Eq) + +$(makeLenses ''FuzzOpts) + +defaultFuzzOpts :: FuzzOpts +defaultFuzzOpts = FuzzOpts { _fuzzOptsOutput = Nothing + , _fuzzOptsForced = False + , _fuzzOptsKeepAll = False + , _fuzzOptsIterations = 1 + , _fuzzOptsNoSim = False + , _fuzzOptsNoEquiv = False + , _fuzzOptsNoReduction = False + , _fuzzOptsConfig = defaultConfig + , _fuzzDataDir = fromText "." + } + +data FuzzEnv = FuzzEnv { _getSynthesisers :: ![SynthTool] + , _getSimulators :: ![SimTool] + , _yosysInstance :: {-# UNPACK #-} !Yosys + , _fuzzEnvOpts :: {-# UNPACK #-} !FuzzOpts + } + deriving (Eq, Show) + +$(makeLenses ''FuzzEnv) + +data FuzzState = FuzzState { _fuzzSynthResults :: ![SynthResult] + , _fuzzSimResults :: ![SimResult] + , _fuzzSynthStatus :: ![SynthStatus] + } + deriving (Eq, Show) + +$(makeLenses ''FuzzState) + +type Frequency a = [(Seed, a)] -> [(Int, Gen (Seed, a))] + +-- | The main type for the fuzzing, which contains an environment that can be +-- read from and the current state of all the results. +type Fuzz m = StateT FuzzState (ReaderT FuzzEnv m) + +type MonadFuzz m = (MonadBaseControl IO m, MonadIO m, MonadSh m) + +runFuzz :: MonadIO m => FuzzOpts -> Yosys -> Fuzz Sh a -> m a +runFuzz fo yos m = shelly $ runFuzz' fo yos m + +runFuzz' :: Monad m => FuzzOpts -> Yosys -> Fuzz m b -> m b +runFuzz' fo yos m = runReaderT + (evalStateT m (FuzzState [] [] [])) + (FuzzEnv { _getSynthesisers = ( force + $ defaultIdentitySynth + : (descriptionToSynth <$> conf ^. configSynthesisers) + ) + , _getSimulators = (force $ descriptionToSim <$> conf ^. configSimulators) + , _yosysInstance = yos + , _fuzzEnvOpts = fo + } + ) + where + conf = _fuzzOptsConfig fo + +askConfig :: Monad m => Fuzz m Config +askConfig = asks (_fuzzOptsConfig . _fuzzEnvOpts) + +askOpts :: Monad m => Fuzz m FuzzOpts +askOpts = asks _fuzzEnvOpts + +genMethod conf seed gen = + case T.toLower $ conf ^. configProperty . propSampleMethod of + "hat" -> do + logT "Using the hat function" + sv hatFreqs + "mean" -> do + logT "Using the mean function" + sv meanFreqs + "median" -> do + logT "Using the median function" + sv medianFreqs + _ -> do + logT "Using first seed" + sampleSeed seed gen + where + sv a = sampleVerilog a (conf ^. configProperty . propSampleSize) seed gen + +relativeFuzzReport :: (MonadSh m) => FuzzReport -> m FuzzReport +relativeFuzzReport fr@(FuzzReport dir _ _ _ _ _ _ _) = liftSh $ do + newPath <- relPath dir + return $ (fuzzDir .~ newPath) fr + +filterSynth :: SynthResult -> Bool +filterSynth (SynthResult _ _ (Pass _) _) = True +filterSynth _ = False + +filterSim :: SimResult -> Bool +filterSim (SimResult _ _ (Pass _) _) = True +filterSim _ = False + +filterSynthStat :: SynthStatus -> Bool +filterSynthStat (SynthStatus _ (Pass _) _) = True +filterSynthStat _ = False + +passedFuzz :: FuzzReport -> Bool +passedFuzz (FuzzReport _ synth sim synthstat _ _ _ _) = + (passedSynth + passedSim + passedSynthStat) == 0 + where + passedSynth = length $ filter (not . filterSynth) synth + passedSim = length $ filter (not . filterSim) sim + passedSynthStat = length $ filter (not . filterSynthStat) synthstat + +synthesisers :: Monad m => Fuzz m [SynthTool] +synthesisers = lift $ asks _getSynthesisers + +--simulators :: (Monad m) => Fuzz () m [SimTool] +--simulators = lift $ asks getSimulators + +--combinations :: [a] -> [b] -> [(a, b)] +--combinations l1 l2 = [ (x, y) | x <- l1, y <- l2 ] + +logT :: MonadSh m => Text -> m () +logT = liftSh . logger + +timeit :: (MonadIO m, MonadSh m) => m a -> m (NominalDiffTime, a) +timeit a = do + start <- liftIO getCurrentTime + result <- a + end <- liftIO getCurrentTime + return (diffUTCTime end start, result) + +synthesis :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () +synthesis src = do + synth <- synthesisers + resTimes <- liftSh $ mapM exec synth + fuzzSynthStatus + .= applyList (uncurry . SynthStatus <$> synth) (fmap swap resTimes) + liftSh $ inspect resTimes + where + exec a = toolRun ("synthesis with " <> toText a) . runResultT $ do + liftSh . mkdir_p . fromText $ toText a + pop (fromText $ toText a) $ runSynth a src + +passedSynthesis :: MonadSh m => Fuzz m [SynthTool] +passedSynthesis = fmap toSynth . filter passed . _fuzzSynthStatus <$> get + where + passed (SynthStatus _ (Pass _) _) = True + passed _ = False + toSynth (SynthStatus s _ _) = s + +failedSynthesis :: MonadSh m => Fuzz m [SynthTool] +failedSynthesis = fmap toSynth . filter failed . _fuzzSynthStatus <$> get + where + failed (SynthStatus _ (Fail SynthFail) _) = True + failed _ = False + toSynth (SynthStatus s _ _) = s + +make :: MonadSh m => FilePath -> m () +make f = liftSh $ mkdir_p f + +pop :: (MonadBaseControl IO m, MonadSh m) => FilePath -> m a -> m a +pop f a = do + dir <- liftSh pwd + finally (liftSh (cd f) >> a) . liftSh $ cd dir + +applyList :: [a -> b] -> [a] -> [b] +applyList a b = apply' <$> zip a b where apply' (a', b') = a' b' + +applyLots :: (a -> b -> c -> d -> e) -> [(a, b)] -> [(c, d)] -> [e] +applyLots func a b = applyList (uncurry . uncurry func <$> a) b + +toSynthResult + :: [(SynthTool, SynthTool)] + -> [(NominalDiffTime, Result Failed ())] + -> [SynthResult] +toSynthResult a b = applyLots SynthResult a $ fmap swap b + +toolRun :: (MonadIO m, MonadSh m) => Text -> m a -> m (NominalDiffTime, a) +toolRun t m = do + logT $ "Running " <> t + (diff, res) <- timeit m + logT $ "Finished " <> t <> " (" <> showT diff <> ")" + return (diff, res) + +equivalence :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () +equivalence src = do + datadir <- fmap _fuzzDataDir askOpts + synth <- passedSynthesis +-- let synthComb = +-- nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth + let synthComb = + nubBy tupEq + . filter (uncurry (/=)) + $ (,) defaultIdentitySynth + <$> synth + resTimes <- liftSh $ mapM (uncurry (equiv datadir)) synthComb + fuzzSynthResults .= toSynthResult synthComb resTimes + liftSh $ inspect resTimes + where + tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') + equiv datadir a b = + toolRun ("equivalence check for " <> toText a <> " and " <> toText b) + . runResultT + $ do make dir + pop dir $ do + liftSh $ do + cp ( fromText ".." + </> fromText (toText a) + </> synthOutput a + ) $ synthOutput a + cp ( fromText ".." + </> fromText (toText b) + </> synthOutput b + ) $ synthOutput b + writefile "rtl.v" $ genSource src + runEquiv datadir a b src + where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b + +simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m () +simulation src = do + datadir <- fmap _fuzzDataDir askOpts + synth <- passedSynthesis + vals <- liftIO $ generateByteString 20 + ident <- liftSh $ equiv datadir vals defaultIdentitySynth + resTimes <- liftSh $ mapM (equiv datadir vals) synth + liftSh + . inspect + $ (\(_, r) -> bimap show (T.unpack . T.take 10 . showBS) r) + <$> (ident : resTimes) + where + equiv datadir b a = toolRun ("simulation for " <> toText a) . runResultT $ do + make dir + pop dir $ do + liftSh $ do + cp (fromText ".." </> fromText (toText a) </> synthOutput a) + $ synthOutput a + writefile "rtl.v" $ genSource src + runSimIc datadir defaultIcarus a src b + where dir = fromText $ "simulation_" <> toText a + +-- | Generate a specific number of random bytestrings of size 256. +randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString] +randomByteString gen n bytes + | n == 0 = ranBytes : bytes + | otherwise = randomByteString newGen (n - 1) $ ranBytes : bytes + where Right (ranBytes, newGen) = C.genBytes 32 gen + +-- | generates the specific number of bytestring with a random seed. +generateByteString :: Int -> IO [ByteString] +generateByteString n = do + gen <- C.newGenIO :: IO C.CtrDRBG + return $ randomByteString gen n [] + +failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult] +failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get + where + withIdentity (SynthResult (IdentitySynth _) _ (Fail EquivFail) _) = True + withIdentity (SynthResult _ (IdentitySynth _) (Fail EquivFail) _) = True + withIdentity _ = False + +passEquiv :: (MonadSh m) => Fuzz m [SynthResult] +passEquiv = filter withIdentity . _fuzzSynthResults <$> get + where + withIdentity (SynthResult _ _ (Pass _) _) = True + withIdentity _ = False + +-- | Always reduces with respect to 'Identity'. +reduction :: (MonadSh m) => SourceInfo -> Fuzz m () +reduction src = do + datadir <- fmap _fuzzDataDir askOpts + fails <- failEquivWithIdentity + synthFails <- failedSynthesis + _ <- liftSh $ mapM (red datadir) fails + _ <- liftSh $ mapM redSynth synthFails + return () + where + red datadir (SynthResult a b _ _) = do + make dir + pop dir $ do + s <- reduceSynth datadir a b src + writefile (fromText ".." </> dir <.> "v") $ genSource s + return s + where dir = fromText $ "reduce_" <> toText a <> "_" <> toText b + redSynth a = do + make dir + pop dir $ do + s <- reduceSynthesis a src + writefile (fromText ".." </> dir <.> "v") $ genSource s + return s + where dir = fromText $ "reduce_" <> toText a + +titleRun + :: (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a) +titleRun t f = do + logT $ "### Starting " <> t <> " ###" + (diff, res) <- timeit f + logT $ "### Finished " <> t <> " (" <> showT diff <> ") ###" + return (diff, res) + +whenMaybe :: Applicative m => Bool -> m a -> m (Maybe a) +whenMaybe b x = if b then Just <$> x else pure Nothing + +getTime :: (Num n) => Maybe (n, a) -> n +getTime = maybe 0 fst + +generateSample + :: (MonadIO m, MonadSh m) + => Fuzz m (Seed, SourceInfo) + -> Fuzz m (Seed, SourceInfo) +generateSample f = do + logT "Sampling Verilog from generator" + (t, v@(s, _)) <- timeit f + logT $ "Chose " <> showT s + logT $ "Generated Verilog (" <> showT t <> ")" + return v + +verilogSize :: (Source a) => a -> Int +verilogSize = length . lines . T.unpack . genSource + +sampleVerilog + :: (MonadSh m, MonadIO m, Source a, Ord a) + => Frequency a + -> Int + -> Maybe Seed + -> Gen a + -> m (Seed, a) +sampleVerilog _ _ seed@(Just _) gen = sampleSeed seed gen +sampleVerilog freq n Nothing gen = do + res <- replicateM n $ sampleSeed Nothing gen + let sizes = fmap getSize res + let samples = fmap snd . sort $ zip sizes res + liftIO $ Hog.sample . Hog.frequency $ freq samples + where getSize (_, s) = verilogSize s + +hatFreqs :: Frequency a +hatFreqs l = zip hat (return <$> l) + where + h = length l `div` 2 + hat = (+ h) . negate . abs . (h -) <$> [1 .. length l] + +meanFreqs :: Source a => Frequency a +meanFreqs l = zip hat (return <$> l) + where + hat = calc <$> sizes + calc i = if abs (mean - i) == min_ then 1 else 0 + mean = sum sizes `div` length l + min_ = minimum $ abs . (mean -) <$> sizes + sizes = verilogSize . snd <$> l + +medianFreqs :: Frequency a +medianFreqs l = zip hat (return <$> l) + where + h = length l `div` 2 + hat = set_ <$> [1 .. length l] + set_ n = if n == h then 1 else 0 + +fuzz :: MonadFuzz m => Gen SourceInfo -> Fuzz m FuzzReport +fuzz gen = do + conf <- askConfig + opts <- askOpts + let seed = conf ^. configProperty . propSeed + (seed', src) <- generateSample $ genMethod conf seed gen + let size = length . lines . T.unpack $ genSource src + liftSh + . writefile "config.toml" + . encodeConfig + $ conf + & configProperty + . propSeed + ?~ seed' + (tsynth, _) <- titleRun "Synthesis" $ synthesis src + (tequiv, _) <- if (_fuzzOptsNoEquiv opts) + then return (0, mempty) + else titleRun "Equivalence Check" $ equivalence src + (_ , _) <- if (_fuzzOptsNoSim opts) + then return (0, mempty) + else titleRun "Simulation" $ simulation src + fails <- failEquivWithIdentity + synthFails <- failedSynthesis + redResult <- + whenMaybe (not (null fails && null synthFails) + && not (_fuzzOptsNoReduction opts)) + . titleRun "Reduction" + $ reduction src + state_ <- get + currdir <- liftSh pwd + let vi = flip view state_ + let report = FuzzReport currdir + (vi fuzzSynthResults) + (vi fuzzSimResults) + (vi fuzzSynthStatus) + size + tsynth + tequiv + (getTime redResult) + return report + +fuzzInDir :: MonadFuzz m => Gen SourceInfo -> Fuzz m FuzzReport +fuzzInDir src = do + fuzzOpts <- askOpts + let fp = fromMaybe "fuzz" $ _fuzzOptsOutput fuzzOpts + make fp + res <- pop fp $ fuzz src + liftSh $ do + writefile (fp <.> "html") $ printResultReport (bname fp) res + when (passedFuzz res && not (_fuzzOptsKeepAll fuzzOpts)) $ rm_rf fp + relativeFuzzReport res + where + bname = T.pack . takeBaseName . T.unpack . toTextIgnore + +fuzzMultiple + :: MonadFuzz m + => Gen SourceInfo + -> Fuzz m [FuzzReport] +fuzzMultiple src = do + fuzzOpts <- askOpts + let seed = (_fuzzOptsConfig fuzzOpts) ^. configProperty . propSeed + x <- case _fuzzOptsOutput fuzzOpts of + Nothing -> do + ct <- liftIO getZonedTime + return + . fromText + . T.pack + $ "output_" + <> formatTime defaultTimeLocale "%Y-%m-%d_%H-%M-%S" ct + Just f -> return f + make x + pop x $ do + results <- if isNothing seed + then forM [1 .. (_fuzzOptsIterations fuzzOpts)] fuzzDir' + else (: []) <$> fuzzDir' (1 :: Int) + liftSh . writefile (fromText "index" <.> "html") $ printSummary + "Fuzz Summary" + results + return results + where + fuzzDir' :: (Show a, MonadFuzz m) => a -> Fuzz m FuzzReport + fuzzDir' n' = local (fuzzEnvOpts . fuzzOptsOutput .~ + (Just . fromText $ "fuzz_" <> showT n')) + $ fuzzInDir src + +sampleSeed :: MonadSh m => Maybe Seed -> Gen a -> m (Seed, a) +sampleSeed s gen = + liftSh + $ let loop n = if n <= 0 + then + error + "Hedgehog.Gen.sample: too many discards, could not generate a sample" + else do + seed <- maybe Hog.random return s + case Hog.evalGen 30 seed gen of + Nothing -> + loop (n - 1) + Just x -> + pure (seed, Hog.treeValue x) + in loop (100 :: Int) diff --git a/src/Verismith/Generate.hs b/src/Verismith/Generate.hs new file mode 100644 index 0000000..8dba3fa --- /dev/null +++ b/src/Verismith/Generate.hs @@ -0,0 +1,646 @@ +{-| +Module : Verismith.Generate +Description : Various useful generators. +Copyright : (c) 2019, Yann Herklotz +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Various useful generators. +-} + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} + +module Verismith.Generate + ( -- * Generation methods + procedural + , proceduralIO + , proceduralSrc + , proceduralSrcIO + , randomMod + -- ** Generate Functions + , largeNum + , wireSize + , range + , genBitVec + , binOp + , unOp + , constExprWithContext + , exprSafeList + , exprRecList + , exprWithContext + , makeIdentifier + , nextPort + , newPort + , scopedExpr + , contAssign + , lvalFromPort + , assignment + , seqBlock + , conditional + , forLoop + , statement + , alwaysSeq + , instantiate + , modInst + , modItem + , constExpr + , parameter + , moduleDef + -- ** Helpers + , someI + , probability + , askProbability + , resizePort + , moduleName + , evalRange + , calcRange + ) +where + +import Control.Lens hiding (Context) +import Control.Monad (replicateM) +import Control.Monad.Reader +import Control.Monad.State.Strict +import Data.Foldable (fold) +import Data.Functor.Foldable (cata) +import Data.List (foldl', partition) +import qualified Data.Text as T +import Hedgehog (Gen, GenT, MonadGen) +import qualified Hedgehog as Hog +import qualified Hedgehog.Gen as Hog +import qualified Hedgehog.Range as Hog +import Verismith.Config +import Verismith.Internal +import Verismith.Verilog.AST +import Verismith.Verilog.BitVec +import Verismith.Verilog.Eval +import Verismith.Verilog.Internal +import Verismith.Verilog.Mutate + +data PortInfo = PortInfo { _portInfoPort :: {-# UNPACK #-} !Port + , _portInfoDet :: !Bool + } + +$(makeLenses ''PortInfo) + +data Context = Context { _contextVariables :: ![PortInfo] + , _contextParameters :: ![Parameter] + , _contextModules :: ![ModDecl] + , _contextNameCounter :: {-# UNPACK #-} !Int + , _contextStmntDepth :: {-# UNPACK #-} !Int + , _contextModDepth :: {-# UNPACK #-} !Int + , _contextDeterminism :: !Bool + } + +$(makeLenses ''Context) + +type StateGen = ReaderT Config (GenT (State Context)) + +fromPort :: Port -> PortInfo +fromPort p = PortInfo p True + +portsFromContext :: Traversal' Context Port +portsFromContext = contextVariables . traverse . portInfoPort + +_portsFromContext :: Context -> [Port] +_portsFromContext c = c ^.. contextVariables . traverse . portInfoPort + +toId :: Int -> Identifier +toId = Identifier . ("w" <>) . T.pack . show + +toPort :: (MonadGen m) => Identifier -> m Port +toPort ident = do + i <- range + return $ wire i ident + +sumSize :: [Port] -> Range +sumSize ps = sum $ ps ^.. traverse . portSize + +legacySafeProb = ProbExpr { _probExprNum = 1 + , _probExprId = 1 + , _probExprRangeSelect = 0 + , _probExprUnOp = 1 + , _probExprBinOp = 1 + , _probExprCond = 1 + , _probExprConcat = 0 + , _probExprStr = 0 + , _probExprSigned = 1 + , _probExprUnsigned = 1 + } + +random :: (MonadGen m) => [Port] -> (Expr -> ContAssign) -> m ModItem +random ctx fun = do + expr <- Hog.sized (exprWithContext legacySafeProb [] ctx) + return . ModCA $ fun expr + +--randomAssigns :: [Identifier] -> [Gen ModItem] +--randomAssigns ids = random ids . ContAssign <$> ids + +randomOrdAssigns :: (MonadGen m) => [Port] -> [Port] -> [m ModItem] +randomOrdAssigns inp ids = snd $ foldr generate (inp, []) ids + where + generate cid (i, o) = (cid : i, random i (ContAssign (_portName cid)) : o) + +randomMod :: (MonadGen m) => Int -> Int -> m ModDecl +randomMod inps total = do + ident <- sequence $ toPort <$> ids + x <- sequence $ randomOrdAssigns (start ident) (end ident) + let inputs_ = take inps ident + 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]) + [] + where + ids = toId <$> [1 .. total] + end = drop inps + start = take inps + +-- | Converts a 'Port' to an 'LVal' by only keeping the 'Identifier' of the +-- 'Port'. +lvalFromPort :: Port -> LVal +lvalFromPort (Port _ _ _ i) = RegId i + +-- | Returns the probability from the configuration. +probability :: Config -> Probability +probability c = c ^. configProbability + +-- | Gets the current probabilities from the 'State'. +askProbability :: StateGen Probability +askProbability = asks probability + +-- | Generates a random large number, which can also be negative. +largeNum :: (MonadGen m) => m Int +largeNum = Hog.int $ Hog.linear (-100) 100 + +-- | Generates a random size for a wire so that it is not too small and not too +-- large. +wireSize :: (MonadGen m) => m Int +wireSize = Hog.int $ Hog.linear 2 100 + +-- | Generates a random range by using the 'wireSize' and 0 as the lower bound. +range :: (MonadGen m) => m Range +range = Range <$> fmap fromIntegral wireSize <*> pure 0 + +-- | Generate a random bit vector using 'largeNum'. +genBitVec :: (MonadGen m) => m BitVec +genBitVec = fmap fromIntegral largeNum + +-- | Return a random 'BinaryOperator'. This currently excludes 'BinDiv', +-- 'BinMod' because they can take a long time to synthesis, and 'BinCEq', +-- 'BinCNEq', because these are not synthesisable. 'BinPower' is also excluded +-- because it can only be used in conjunction with base powers of 2 which is +-- currently not enforced. +binOp :: (MonadGen m) => m 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 + ] + +-- | Generate a random 'UnaryOperator'. +unOp :: (MonadGen m) => m UnaryOperator +unOp = Hog.element + [ UnPlus + , UnMinus + , UnNot + , UnLNot + , UnAnd + , UnNand + , UnOr + , UnNor + , UnXor + , UnNxor + , UnNxorInv + ] + +-- | Generate a random 'ConstExpr' by using the current context of 'Parameter'. +constExprWithContext :: (MonadGen m) => [Parameter] -> ProbExpr -> Hog.Size -> m ConstExpr +constExprWithContext ps prob size + | size == 0 = Hog.frequency + [ (prob ^. probExprNum, ConstNum <$> genBitVec) + , ( if null ps then 0 else prob ^. probExprId + , ParamId . _paramIdent <$> Hog.element ps + ) + ] + | size > 0 = Hog.frequency + [ (prob ^. probExprNum, ConstNum <$> genBitVec) + , ( if null ps then 0 else prob ^. probExprId + , ParamId . _paramIdent <$> Hog.element ps + ) + , (prob ^. probExprUnOp, ConstUnOp <$> unOp <*> subexpr 2) + , ( prob ^. probExprBinOp + , ConstBinOp <$> subexpr 2 <*> binOp <*> subexpr 2 + ) + , ( prob ^. probExprCond + , ConstCond <$> subexpr 2 <*> subexpr 2 <*> subexpr 2 + ) + , ( prob ^. probExprConcat + , ConstConcat <$> Hog.nonEmpty (Hog.linear 0 10) (subexpr 2) + ) + ] + | otherwise = constExprWithContext ps prob 0 + where subexpr y = constExprWithContext ps prob $ size `div` y + +-- | The list of safe 'Expr', meaning that these will not recurse and will end +-- the 'Expr' generation. +exprSafeList :: (MonadGen m) => ProbExpr -> [(Int, m Expr)] +exprSafeList prob = [(prob ^. probExprNum, Number <$> genBitVec)] + +-- | List of 'Expr' that have the chance to recurse and will therefore not be +-- used when the expression grows too large. +exprRecList :: (MonadGen m) => ProbExpr -> (Hog.Size -> m Expr) -> [(Int, m Expr)] +exprRecList prob subexpr = + [ (prob ^. probExprNum, Number <$> genBitVec) + , ( prob ^. probExprConcat + , Concat <$> Hog.nonEmpty (Hog.linear 0 10) (subexpr 2) + ) + , (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 2 <*> subexpr 2 <*> subexpr 2) + , (prob ^. probExprSigned , Appl <$> pure "$signed" <*> subexpr 2) + , (prob ^. probExprUnsigned, Appl <$> pure "$unsigned" <*> subexpr 2) + ] + +-- | Select a random port from a list of ports and generate a safe bit selection +-- for that port. +rangeSelect :: (MonadGen m) => [Parameter] -> [Port] -> m Expr +rangeSelect ps ports = do + p <- Hog.element ports + let s = calcRange ps (Just 32) $ _portSize p + msb <- Hog.int (Hog.constantFrom (s `div` 2) 0 (s - 1)) + lsb <- Hog.int (Hog.constantFrom (msb `div` 2) 0 msb) + return . RangeSelect (_portName p) $ Range (fromIntegral msb) + (fromIntegral lsb) + +-- | Generate a random expression from the 'Context' with a guarantee that it +-- will terminate using the list of safe 'Expr'. +exprWithContext :: (MonadGen m) => ProbExpr -> [Parameter] -> [Port] -> Hog.Size -> m Expr +exprWithContext prob ps [] n | n == 0 = Hog.frequency $ exprSafeList prob + | n > 0 = Hog.frequency $ exprRecList prob subexpr + | otherwise = exprWithContext prob ps [] 0 + where subexpr y = exprWithContext prob ps [] $ n `div` y +exprWithContext prob ps l n + | n == 0 + = Hog.frequency + $ (prob ^. probExprId, Id . _portName <$> Hog.element l) + : exprSafeList prob + | n > 0 + = Hog.frequency + $ (prob ^. probExprId , Id . _portName <$> Hog.element l) + : (prob ^. probExprRangeSelect, rangeSelect ps l) + : exprRecList prob subexpr + | otherwise + = exprWithContext prob ps l 0 + where subexpr y = exprWithContext prob ps l $ n `div` y + +-- | Runs a 'StateGen' for a random number of times, limited by an 'Int' that is +-- passed to it. +someI :: Int -> StateGen a -> StateGen [a] +someI m f = do + amount <- Hog.int (Hog.linear 1 m) + replicateM amount f + +-- | Make a new name with a prefix and the current nameCounter. The nameCounter +-- is then increased so that the label is unique. +makeIdentifier :: T.Text -> StateGen Identifier +makeIdentifier prefix = do + context <- get + let ident = Identifier $ prefix <> showT (context ^. contextNameCounter) + contextNameCounter += 1 + return ident + +getPort' :: PortType -> Identifier -> [Port] -> StateGen Port +getPort' pt i c = case filter portId c of + x : _ -> return x + [] -> newPort i pt + where portId (Port pt' _ _ i') = i == i' && pt == pt' + +-- | Makes a new 'Identifier' and then checks if the 'Port' already exists, if +-- it does the existant 'Port' is returned, otherwise a new port is created with +-- 'newPort'. This is used subsequently in all the functions to create a port, +-- in case a port with the same name was already created. This could be because +-- the generation is currently in the other branch of an if-statement. +nextPort :: PortType -> StateGen Port +nextPort pt = do + context <- get + ident <- makeIdentifier . T.toLower $ showT pt + getPort' pt ident (_portsFromContext context) + +-- | Creates a new port based on the current name counter and adds it to the +-- current context. +newPort :: Identifier -> PortType -> StateGen Port +newPort ident pt = do + p <- Port pt <$> Hog.bool <*> range <*> pure ident + variables %= (p :) + return p + +-- | Generates an expression from variables that are currently in scope. +scopedExpr :: StateGen Expr +scopedExpr = do + context <- get + prob <- askProbability + Hog.sized + . exprWithContext (_probExpr prob) (_parameters context) + $ _variables context + +-- | Generates a random continuous assignment and assigns it to a random wire +-- that is created. +contAssign :: StateGen ContAssign +contAssign = do + expr <- scopedExpr + p <- nextPort Wire + return $ ContAssign (p ^. portName) expr + +-- | Generate a random assignment and assign it to a random 'Reg'. +assignment :: StateGen Assign +assignment = do + expr <- scopedExpr + lval <- lvalFromPort <$> nextPort Reg + return $ Assign lval Nothing expr + +-- | Generate a random 'Statement' safely, by also increasing the depth counter. +seqBlock :: StateGen Statement +seqBlock = do + contextStmntDepth -= 1 + tstat <- SeqBlock <$> someI 20 statement + contextStmntDepth += 1 + return tstat + +-- | Generate a random conditional 'Statement'. The nameCounter is reset between +-- branches so that port names can be reused. This is safe because if a 'Port' +-- is not reused, it is left at 0, as all the 'Reg' are initialised to 0 at the +-- start. +conditional :: StateGen Statement +conditional = do + expr <- scopedExpr + nc <- _contextNameCounter <$> get + tstat <- seqBlock + nc' <- _contextNameCounter <$> get + contextNameCounter .= nc + fstat <- seqBlock + nc'' <- _contextNameCounter <$> get + contextNameCounter .= max nc' nc'' + return $ CondStmnt expr (Just tstat) (Just fstat) + +-- | Generate a random for loop by creating a new variable name for the counter +-- and then generating random statements in the body. +forLoop :: StateGen Statement +forLoop = do + num <- Hog.int (Hog.linear 0 20) + var <- lvalFromPort <$> nextPort Reg + ForLoop (Assign var Nothing 0) + (BinOp (varId var) BinLT $ fromIntegral num) + (Assign var Nothing $ BinOp (varId var) BinPlus 1) + <$> seqBlock + where varId v = Id (v ^. regId) + +-- | Choose a 'Statement' to generate. +statement :: StateGen Statement +statement = do + prob <- askProbability + cont <- get + let defProb i = prob ^. probStmnt . i + Hog.frequency + [ (defProb probStmntBlock , BlockAssign <$> assignment) + , (defProb probStmntNonBlock , NonBlockAssign <$> assignment) + , (onDepth cont (defProb probStmntCond), conditional) + , (onDepth cont (defProb probStmntFor) , forLoop) + ] + where onDepth c n = if c ^. contextStmntDepth > 0 then n else 0 + +-- | Generate a sequential always block which is dependent on the clock. +alwaysSeq :: StateGen ModItem +alwaysSeq = Always . EventCtrl (EPosEdge "clk") . Just <$> seqBlock + +-- | Should resize a port that connects to a module port if the latter is +-- larger. This should not cause any problems if the same net is used as input +-- multiple times, and is resized multiple times, as it should only get larger. +resizePort :: [Parameter] -> Identifier -> Range -> Port -> Port +resizePort ps i ra p@(Port t _ ri i') + | i' == i && calc ri < calc ra = (p & portSize .~ ra) + | otherwise = p + where + calc = calcRange ps $ Just 64 + +-- | Instantiate a module, where the outputs are new nets that are created, and +-- the inputs are taken from existing ports in the context. +-- +-- 1 is subtracted from the inputs for the length because the clock is not +-- counted and is assumed to be there, this should be made nicer by filtering +-- out the clock instead. I think that in general there should be a special +-- representation for the clock. +instantiate :: ModDecl -> StateGen ModItem +instantiate (ModDecl i outP inP _ _) = do + context <- get + outs <- replicateM (length outP) (nextPort Wire) + ins <- take (length inpFixed) <$> Hog.shuffle (context ^. variables) + insLit <- replicateM (length inpFixed - length ins) (Number <$> genBitVec) + mapM_ (uncurry process) . zip (ins ^.. traverse . portName) $ inpFixed ^.. traverse . portSize + ident <- makeIdentifier "modinst" + vs <- _portsFromContext <$> get + Hog.choice + [ return . ModInst i ident $ ModConn <$> (toE (outs <> clkPort <> ins) <> insLit) + , ModInst i ident <$> Hog.shuffle + (zipWith ModConnNamed (view portName <$> outP <> clkPort <> inpFixed) + (toE (outs <> clkPort <> ins) <> insLit)) + ] + where + toE ins = Id . _portName <$> ins + (inpFixed, clkPort) = partition filterFunc inP + filterFunc (Port _ _ _ n) + | n == "clk" = False + | otherwise = True + process p r = do + params <- _contextParameters <$> get + portsFromContext %= resizePort params p r + +-- | 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 <- ask + context <- get + let maxMods = prob ^. configProperty . propMaxModules + if length (_contextModules context) < maxMods + then do + let currMods = _contextModules context + let params = _contextParameters context + let vars = _contextVariables context + contextModules .= [] + contextVariables .= [] + contextParameters .= [] + contextModDepth -= 1 + chosenMod <- moduleDef Nothing + ncont <- get + let genMods = _contextModules ncont + contextModDepth += 1 + contextParameters .= params + contextVariables .= vars + contextModules .= chosenMod : currMods <> genMods + instantiate chosenMod + else Hog.element (_contextModules context) >>= instantiate + +-- | Generate a random module item. +modItem :: StateGen ModItem +modItem = do + conf <- ask + let prob = conf ^. configProbability + context <- get + let defProb i = prob ^. probModItem . i + det <- Hog.frequency [ (conf ^. configProperty . propDeterminism, return True) + , (conf ^. configProperty . propNonDeterminism, return False) ] + contextDeterminism .= det + Hog.frequency + [ (defProb probModItemAssign , ModCA <$> contAssign) + , (defProb probModItemSeqAlways, alwaysSeq) + , ( if context ^. contextModDepth > 0 then defProb probModItemInst else 0 + , modInst ) + ] + +-- | Either return the 'Identifier' that was passed to it, or generate a new +-- 'Identifier' based on the current 'contextNameCounter'. +moduleName :: Maybe Identifier -> StateGen Identifier +moduleName (Just t) = return t +moduleName Nothing = makeIdentifier "module" + +-- | Generate a random 'ConstExpr' by using the current context of 'Parameters'. +constExpr :: StateGen ConstExpr +constExpr = do + prob <- askProbability + context <- get + Hog.sized $ constExprWithContext (context ^. parameters) + (prob ^. probExpr) + +-- | Generate a random 'Parameter' and assign it to a constant expression which +-- it will be initialised to. The assumption is that this constant expression +-- should always be able to be evaluated with the current context of parameters. +parameter :: StateGen Parameter +parameter = do + ident <- makeIdentifier "param" + cexpr <- constExpr + let param = Parameter ident cexpr + contextParameters %= (param :) + return param + +-- | Evaluate a range to an integer, and cast it back to a range. +evalRange :: [Parameter] -> Int -> Range -> Range +evalRange ps n (Range l r) = Range (eval l) (eval r) + where eval = ConstNum . cata (evaluateConst ps) . resize n + +-- | Calculate a range to an int by maybe resizing the ranges to a value. +calcRange :: [Parameter] -> Maybe Int -> Range -> Int +calcRange ps i (Range l r) = eval l - eval r + 1 + where + eval a = fromIntegral . cata (evaluateConst ps) $ maybe a (`resize` a) i + +-- | Filter out a port based on it's name instead of equality of the ports. This +-- is because the ports might not be equal if the sizes are being updated. +identElem :: Port -> [Port] -> Bool +identElem p = elem (p ^. portName) . toListOf (traverse . portName) + +-- | 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 +-- defined wires, so that it correctly reflects the internal state of the +-- module. +moduleDef :: Maybe Identifier -> StateGen ModDecl +moduleDef top = do + name <- moduleName top + portList <- Hog.list (Hog.linear 4 10) $ nextPort Wire + mi <- Hog.list (Hog.linear 4 100) modItem + ps <- Hog.list (Hog.linear 0 10) parameter + context <- get + config <- ask + let (newPorts, local) = partition (`identElem` portList) $ _variables context + let + size = + evalRange (_contextParameters context) 32 + . sum + $ local + ^.. traverse + . portSize + let combine = config ^. configProperty . propCombine + let clock = Port Wire False 1 "clk" + let yport = + if combine then Port Wire False 1 "y" else Port Wire False size "y" + let comb = combineAssigns_ combine yport local + return + . declareMod local + . ModDecl name [yport] (clock : newPorts) (comb : mi) + $ ps + +-- | Procedural generation method for random Verilog. Uses internal 'Reader' and +-- 'State' to keep track of the current Verilog code structure. +procedural :: T.Text -> Config -> Gen Verilog +procedural top config = do + (mainMod, st) <- Hog.resize num $ runStateT + (Hog.distributeT (runReaderT (moduleDef (Just $ Identifier top)) config)) + context + return . Verilog $ mainMod : st ^. modules + where + context = + Context [] [] [] 0 (confProp propStmntDepth) (confProp propModDepth) True + num = fromIntegral $ confProp propSize + confProp i = config ^. configProperty . i + +-- | Samples the 'Gen' directly to generate random 'Verilog' using the 'T.Text' as +-- the name of the main module and the configuration 'Config' to influence the +-- generation. +proceduralIO :: T.Text -> Config -> IO Verilog +proceduralIO t = Hog.sample . procedural t + +-- | Given a 'T.Text' and a 'Config' will generate a 'SourceInfo' which has the +-- top module set to the right name. +proceduralSrc :: T.Text -> Config -> Gen SourceInfo +proceduralSrc t c = SourceInfo t <$> procedural t c + +-- | Sampled and wrapped into a 'SourceInfo' with the given top module name. +proceduralSrcIO :: T.Text -> Config -> IO SourceInfo +proceduralSrcIO t c = SourceInfo t <$> proceduralIO t c diff --git a/src/Verismith/Internal.hs b/src/Verismith/Internal.hs new file mode 100644 index 0000000..b47c924 --- /dev/null +++ b/src/Verismith/Internal.hs @@ -0,0 +1,49 @@ +{-| +Module : Verismith.Internal +Description : Shared high level code used in the other modules internally. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Shared high level code used in the other modules internally. +-} + +module Verismith.Internal + ( -- * Useful functions + safe + , showT + , showBS + , comma + , commaNL + ) +where + +import Data.ByteString (ByteString) +import Data.ByteString.Builder (byteStringHex, toLazyByteString) +import qualified Data.ByteString.Lazy as L +import Data.Text (Text) +import qualified Data.Text as T +import Data.Text.Encoding (decodeUtf8) + +-- | Function to show a bytestring in a hex format. +showBS :: ByteString -> Text +showBS = decodeUtf8 . L.toStrict . toLazyByteString . byteStringHex + +-- | Converts unsafe list functions in the Prelude to a safe version. +safe :: ([a] -> b) -> [a] -> Maybe b +safe _ [] = Nothing +safe f l = Just $ f l + +-- | Show function for 'Text' +showT :: (Show a) => a -> Text +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/Verismith/OptParser.hs b/src/Verismith/OptParser.hs new file mode 100644 index 0000000..a475e9a --- /dev/null +++ b/src/Verismith/OptParser.hs @@ -0,0 +1,262 @@ +module Verismith.OptParser + ( OptTool (..) + , Opts (..) + , opts + ) +where + +import Control.Applicative ((<|>)) +import Data.Text (Text) +import qualified Data.Text as T +import Options.Applicative (Mod (..), OptionFields (..), Parser (..), + ParserInfo (..), ReadM (..), (<**>)) +import qualified Options.Applicative as Opt +import Prelude hiding (FilePath (..)) +import Shelly (FilePath (..), fromText) +import Verismith.Config (SynthDescription (..), versionInfo) + +data OptTool = TYosys + | TXST + | TIcarus + +instance Show OptTool where + show TYosys = "yosys" + show TXST = "xst" + show TIcarus = "icarus" + +data Opts = Fuzz { fuzzOutput :: {-# UNPACK #-} !Text + , fuzzConfigFile :: !(Maybe FilePath) + , fuzzForced :: !Bool + , fuzzKeepAll :: !Bool + , fuzzNum :: {-# UNPACK #-} !Int + , fuzzNoSim :: !Bool + , fuzzNoEquiv :: !Bool + , fuzzNoReduction :: !Bool + } + | Generate { generateFilename :: !(Maybe FilePath) + , generateConfigFile :: !(Maybe FilePath) + } + | Parse { parseFilename :: {-# UNPACK #-} !FilePath + } + | Reduce { reduceFilename :: {-# UNPACK #-} !FilePath + , reduceTop :: {-# UNPACK #-} !Text + , reduceScript :: !(Maybe FilePath) + , reduceSynthesiserDesc :: ![SynthDescription] + , reduceRerun :: !Bool + } + | ConfigOpt { configOptWriteConfig :: !(Maybe FilePath) + , configOptConfigFile :: !(Maybe FilePath) + , configOptDoRandomise :: !Bool + } + +textOption :: Mod OptionFields String -> Parser Text +textOption = fmap T.pack . Opt.strOption + +optReader :: (String -> Maybe a) -> ReadM a +optReader f = Opt.eitherReader $ \arg -> case f arg of + Just a -> Right a + Nothing -> Left $ "Cannot parse option: " <> arg + +parseSynth :: String -> Maybe OptTool +parseSynth val | val == "yosys" = Just TYosys + | val == "xst" = Just TXST + | otherwise = Nothing + +parseSynthDesc :: String -> Maybe SynthDescription +parseSynthDesc val + | val == "yosys" = Just $ SynthDescription "yosys" Nothing Nothing Nothing + | val == "vivado" = Just $ SynthDescription "vivado" Nothing Nothing Nothing + | val == "xst" = Just $ SynthDescription "xst" Nothing Nothing Nothing + | val == "quartus" = Just + $ SynthDescription "quartus" Nothing Nothing Nothing + | val == "identity" = Just + $ SynthDescription "identity" Nothing Nothing Nothing + | otherwise = Nothing + +parseSim :: String -> Maybe OptTool +parseSim val | val == "icarus" = Just TIcarus + | otherwise = Nothing + +fuzzOpts :: Parser Opts +fuzzOpts = + Fuzz + <$> textOption + ( Opt.long "output" + <> Opt.short 'o' + <> Opt.metavar "DIR" + <> Opt.help "Output directory that the fuzz run takes place in." + <> Opt.showDefault + <> Opt.value "output") + <*> ( Opt.optional + . Opt.strOption + $ Opt.long "config" + <> Opt.short 'c' + <> Opt.metavar "FILE" + <> Opt.help "Config file for the current fuzz run.") + <*> (Opt.switch $ Opt.long "force" <> Opt.short 'f' <> Opt.help + "Overwrite the specified directory.") + <*> (Opt.switch $ Opt.long "keep" <> Opt.short 'k' <> Opt.help + "Keep all the directories.") + <*> ( Opt.option Opt.auto + $ Opt.long "num" + <> Opt.short 'n' + <> Opt.help "The number of fuzz runs that should be performed." + <> Opt.showDefault + <> Opt.value 1 + <> Opt.metavar "INT") + <*> (Opt.switch $ Opt.long "no-sim" <> Opt.help + "Do not run simulation on the output netlist.") + <*> (Opt.switch $ Opt.long "no-equiv" <> Opt.help + "Do not run an equivalence check on the output netlist.") + <*> (Opt.switch $ Opt.long "no-reduction" <> Opt.help + "Do not run reduction on a failed testcase.") + +genOpts :: Parser Opts +genOpts = + Generate + <$> ( Opt.optional + . Opt.strOption + $ Opt.long "output" + <> Opt.short 'o' + <> Opt.metavar "FILE" + <> Opt.help "Output to a verilog file instead." + ) + <*> ( Opt.optional + . Opt.strOption + $ Opt.long "config" + <> Opt.short 'c' + <> Opt.metavar "FILE" + <> Opt.help "Config file for the generation run." + ) + +parseOpts :: Parser Opts +parseOpts = Parse . fromText . T.pack <$> Opt.strArgument + (Opt.metavar "FILE" <> Opt.help "Verilog input file.") + +reduceOpts :: Parser Opts +reduceOpts = + Reduce + . fromText + . T.pack + <$> Opt.strArgument (Opt.metavar "FILE" <> Opt.help "Verilog input file.") + <*> textOption + ( Opt.short 't' + <> Opt.long "top" + <> Opt.metavar "TOP" + <> Opt.help "Name of top level module." + <> Opt.showDefault + <> Opt.value "top" + ) + <*> ( Opt.optional + . Opt.strOption + $ Opt.long "script" + <> Opt.metavar "SCRIPT" + <> Opt.help + "Script that determines if the current file is interesting, which is determined by the script returning 0." + ) + <*> ( Opt.many + . Opt.option (optReader parseSynthDesc) + $ Opt.short 's' + <> Opt.long "synth" + <> Opt.metavar "SYNTH" + <> Opt.help "Specify synthesiser to use." + ) + <*> ( Opt.switch + $ Opt.short 'r' + <> Opt.long "rerun" + <> Opt.help + "Only rerun the current synthesis file with all the synthesisers." + ) + +configOpts :: Parser Opts +configOpts = + ConfigOpt + <$> ( Opt.optional + . Opt.strOption + $ Opt.long "output" + <> Opt.short 'o' + <> Opt.metavar "FILE" + <> Opt.help "Output to a TOML Config file." + ) + <*> ( Opt.optional + . Opt.strOption + $ Opt.long "config" + <> Opt.short 'c' + <> Opt.metavar "FILE" + <> Opt.help "Config file for the current fuzz run." + ) + <*> ( Opt.switch + $ Opt.long "randomise" + <> Opt.short 'r' + <> Opt.help + "Randomise the given default config, or the default config by randomly switchin on and off options." + ) + +argparse :: Parser Opts +argparse = + Opt.hsubparser + ( Opt.command + "fuzz" + (Opt.info + fuzzOpts + (Opt.progDesc + "Run fuzzing on the specified simulators and synthesisers." + ) + ) + <> Opt.metavar "fuzz" + ) + <|> Opt.hsubparser + ( Opt.command + "generate" + (Opt.info + genOpts + (Opt.progDesc "Generate a random Verilog program.") + ) + <> Opt.metavar "generate" + ) + <|> Opt.hsubparser + ( Opt.command + "parse" + (Opt.info + parseOpts + (Opt.progDesc + "Parse a verilog file and output a pretty printed version." + ) + ) + <> Opt.metavar "parse" + ) + <|> Opt.hsubparser + ( Opt.command + "reduce" + (Opt.info + reduceOpts + (Opt.progDesc + "Reduce a Verilog file by rerunning the fuzzer on the file." + ) + ) + <> Opt.metavar "reduce" + ) + <|> Opt.hsubparser + ( Opt.command + "config" + (Opt.info + configOpts + (Opt.progDesc + "Print the current configuration of the fuzzer." + ) + ) + <> Opt.metavar "config" + ) + +version :: Parser (a -> a) +version = Opt.infoOption versionInfo $ mconcat + [Opt.long "version", Opt.short 'v', Opt.help "Show version information.", Opt.hidden] + +opts :: ParserInfo Opts +opts = Opt.info + (argparse <**> Opt.helper <**> version) + ( Opt.fullDesc + <> Opt.progDesc "Fuzz different simulators and synthesisers." + <> Opt.header + "Verismith - A hardware simulator and synthesiser Verilog fuzzer." + ) diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs new file mode 100644 index 0000000..a7ec3f8 --- /dev/null +++ b/src/Verismith/Reduce.hs @@ -0,0 +1,610 @@ +{-| +Module : Verismith.Reduce +Description : Test case reducer implementation. +Copyright : (c) 2019, Yann Herklotz +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Test case reducer implementation. +-} + +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Verismith.Reduce + ( -- $strategy + reduceWithScript + , reduceSynth + , reduceSynthesis + , reduce + , reduce_ + , Replacement(..) + , halveModules + , halveModItems + , halveStatements + , halveExpr + , halveAssigns + , findActiveWires + , clean + , cleanSourceInfo + , cleanSourceInfoAll + , removeDecl + , filterExpr + ) +where + +import Control.Lens hiding ((<.>)) +import Control.Monad (void) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Data.Foldable (foldrM) +import Data.List (nub) +import Data.List.NonEmpty (NonEmpty (..)) +import qualified Data.List.NonEmpty as NonEmpty +import Data.Maybe (mapMaybe) +import Data.Text (Text) +import Shelly ((<.>)) +import qualified Shelly +import Shelly.Lifted (MonadSh, liftSh) +import Verismith.Internal +import Verismith.Result +import Verismith.Tool +import Verismith.Tool.Internal +import Verismith.Verilog +import Verismith.Verilog.AST +import Verismith.Verilog.Mutate +import Verismith.Verilog.Parser + + +-- $strategy +-- The reduction strategy has multiple different steps. 'reduce' will run these +-- strategies one after another, starting at the most coarse grained one. The +-- supported reduction strategies are the following: +-- +-- [Modules] First of all, the reducer will try and remove all the modules +-- except the top module. +-- +-- [Module Items] Then, the module items will be reduced by using standard +-- delta debugging. Half of the module items will be removed, and both +-- versions will be tested. If both succeed, they will be divided further and +-- tested further. Finally, the shortest version will be returned. +-- +-- [Statements] Once the module items have been reduced, the statements will +-- be reduced as well. This is done using delta debugging, just like the +-- module items. +-- +-- [Expressions] Finally, the expressions themselves will be reduced. This is +-- done by splitting the top most binary expressions in half and testing each +-- half. + +-- | Replacement type that supports returning different kinds of reduced +-- replacements that could be tried. +data Replacement a = Dual a a + | Single a + | None + deriving (Show, Eq) + +type Replace a = a -> Replacement a + +instance Functor Replacement where + fmap f (Dual a b) = Dual (f a) $ f b + fmap f (Single a) = Single $ f a + fmap _ None = None + +instance Applicative Replacement where + pure = Single + (Dual a b) <*> (Dual c d) = Dual (a c) $ b d + (Dual a b) <*> (Single c) = Dual (a c) $ b c + (Single a) <*> (Dual b c) = Dual (a b) $ a c + (Single a) <*> (Single b) = Single $ a b + None <*> _ = None + _ <*> None = None + +instance Foldable Replacement where + foldMap _ None = mempty + foldMap f (Single a) = f a + foldMap f (Dual a b) = f a <> f b + +instance Traversable Replacement where + traverse _ None = pure None + traverse f (Single a) = Single <$> f a + traverse f (Dual a b) = Dual <$> f a <*> f b + +-- | Split a list in two halves. +halve :: Replace [a] +halve [] = Single [] +halve [_] = Single [] +halve l = Dual a b where (a, b) = splitAt (length l `div` 2) l + +halveNonEmpty :: Replace (NonEmpty a) +halveNonEmpty l = case NonEmpty.splitAt (length l `div` 2) l of + ([] , [] ) -> None + ([] , a : b) -> Single $ a :| b + (a : b, [] ) -> Single $ a :| b + (a : b, c : d) -> Dual (a :| b) $ c :| d + +-- | When given a Lens and a function that works on a lower replacement, it will +-- go down, apply the replacement, and return a replacement of the original +-- module. +combine :: Lens' a b -> Replace b -> Replace a +combine l f i = modify <$> f (i ^. l) where modify res = i & l .~ res + +-- | Deletes Id 'Expr' if they are not part of the current scope, and replaces +-- these by 0. +filterExpr :: [Identifier] -> Expr -> Expr +filterExpr ids (Id i) = if i `elem` ids then Id i else Number 0 +filterExpr ids (VecSelect i e) = + if i `elem` ids then VecSelect i e else Number 0 +filterExpr ids (RangeSelect i r) = + if i `elem` ids then RangeSelect i r else Number 0 +filterExpr _ e = e + +-- | Checks if a declaration is part of the current scope. If not, it returns +-- 'False', otherwise 'True', as it should be kept. +--filterDecl :: [Identifier] -> ModItem -> Bool +--filterDecl ids (Decl Nothing (Port _ _ _ i) _) = i `elem` ids +--filterDecl _ _ = True + +-- | Checks if a continuous assignment is in the current scope, if not, it +-- returns 'False'. +filterAssigns :: [Port] -> ModItem -> Bool +filterAssigns out (ModCA (ContAssign i _)) = + elem i $ out ^.. traverse . portName +filterAssigns _ _ = True + +clean :: (Mutate a) => [Identifier] -> a -> a +clean ids = mutExpr (transform $ filterExpr ids) + +cleanUndefined :: [Identifier] -> [ModItem] -> [ModItem] +cleanUndefined ids mis = clean usedWires mis + where + usedWires = mis ^.. traverse . modContAssign . contAssignNetLVal <> ids + +halveModAssign :: Replace ModDecl +halveModAssign m = cleanMod m $ modify <$> assigns (m ^. modItems) + where + assigns = halve . filter (filterAssigns $ m ^. modOutPorts) + modify l = m & modItems .~ l + +cleanMod :: ModDecl -> Replacement ModDecl -> Replacement ModDecl +cleanMod m newm = modify . change <$> newm + where + mis = m ^. modItems + modify l = m & modItems .~ l + change l = + cleanUndefined (m ^.. modInPorts . traverse . portName) + . combineAssigns (head $ m ^. modOutPorts) + . (filter (not . filterAssigns []) mis <>) + $ l + ^. modItems + +halveIndExpr :: Replace Expr +halveIndExpr (Concat l ) = Concat <$> halveNonEmpty l +halveIndExpr (BinOp e1 _ e2) = Dual e1 e2 +halveIndExpr (Cond _ e1 e2) = Dual e1 e2 +halveIndExpr (UnOp _ e ) = Single e +halveIndExpr (Appl _ e ) = Single e +halveIndExpr e = Single e + +halveModExpr :: Replace ModItem +halveModExpr (ModCA ca) = ModCA <$> combine contAssignExpr halveIndExpr ca +halveModExpr a = Single a + +-- | Remove all the undefined mod instances. +cleanModInst :: SourceInfo -> SourceInfo +cleanModInst srcInfo = srcInfo & infoSrc . _Wrapped .~ cleaned + where + validInst = srcInfo ^.. infoSrc . _Wrapped . traverse . modId + cleaned = cleanModInst' validInst <$> srcInfo ^. infoSrc . _Wrapped + +-- | Clean all the undefined module instances in a specific module using a +-- context. +cleanModInst' :: [Identifier] -> ModDecl -> ModDecl +cleanModInst' ids m = m & modItems .~ newModItem + where newModItem = filter (validModInst ids) $ m ^.. modItems . traverse + +-- | Check if a mod instance is in the current context. +validModInst :: [Identifier] -> ModItem -> Bool +validModInst ids (ModInst i _ _) = i `elem` ids +validModInst _ _ = True + +-- | Adds a 'ModDecl' to a 'SourceInfo'. +addMod :: ModDecl -> SourceInfo -> SourceInfo +addMod m srcInfo = srcInfo & infoSrc . _Wrapped %~ (m :) + +-- | Split a module declaration in half by trying to remove assign +-- statements. This is only done in the main module of the source. +halveAssigns :: Replace SourceInfo +halveAssigns = combine mainModule halveModAssign + +-- | Checks if a module item is needed in the module declaration. +relevantModItem :: ModDecl -> ModItem -> Bool +relevantModItem (ModDecl _ out _ _ _) (ModCA (ContAssign i _)) = + i `elem` fmap _portName out +relevantModItem _ Decl{} = True +relevantModItem _ _ = False + +isAssign :: Statement -> Bool +isAssign (BlockAssign _) = True +isAssign (NonBlockAssign _) = True +isAssign _ = False + +lValName :: LVal -> [Identifier] +lValName (RegId i ) = [i] +lValName (RegExpr i _) = [i] +lValName (RegSize i _) = [i] +lValName (RegConcat e) = mapMaybe getId . concat $ universe <$> e + where + getId (Id i) = Just i + getId _ = Nothing + +-- | Pretending that expr is an LVal for the case that it is in a module +-- instantiation. +exprName :: Expr -> [Identifier] +exprName (Id i ) = [i] +exprName (VecSelect i _) = [i] +exprName (RangeSelect i _) = [i] +exprName (Concat i ) = concat . NonEmpty.toList $ exprName <$> i +exprName _ = [] + +-- | Returns the only identifiers that are directly tied to an expression. This +-- is useful if one does not have to recurse deeper into the expressions. +exprId :: Expr -> Maybe Identifier +exprId (Id i ) = Just i +exprId (VecSelect i _) = Just i +exprId (RangeSelect i _) = Just i +exprId _ = Nothing + +eventId :: Event -> Maybe Identifier +eventId (EId i) = Just i +eventId (EPosEdge i) = Just i +eventId (ENegEdge i) = Just i +eventId _ = Nothing + +portToId :: Port -> Identifier +portToId (Port _ _ _ i) = i + +paramToId :: Parameter -> Identifier +paramToId (Parameter i _) = i + +isModule :: Identifier -> ModDecl -> Bool +isModule i (ModDecl n _ _ _ _) = i == n + +modInstActive :: [ModDecl] -> ModItem -> [Identifier] +modInstActive decl (ModInst n _ i) = case m of + Nothing -> [] + Just m' -> concat $ calcActive m' <$> zip i [0 ..] + where + m = safe head $ filter (isModule n) decl + calcActive (ModDecl _ o _ _ _) (ModConn e, n') | n' < length o = exprName e + | otherwise = [] + calcActive (ModDecl _ o _ _ _) (ModConnNamed i' e, _) + | i' `elem` fmap _portName o = exprName e + | otherwise = [] +modInstActive _ _ = [] + +fixModInst :: SourceInfo -> ModItem -> ModItem +fixModInst (SourceInfo _ (Verilog decl)) (ModInst n g i) = case m of + Nothing -> error "Moditem not found" + Just m' -> ModInst n g . mapMaybe (fixModInst' m') $ zip i [0 ..] + where + m = safe head $ filter (isModule n) decl + fixModInst' (ModDecl _ o i' _ _) (ModConn e, n') + | n' < length o + length i' = Just $ ModConn e + | otherwise = Nothing + fixModInst' (ModDecl _ o i'' _ _) (ModConnNamed i' e, _) + | i' `elem` fmap _portName (o <> i'') = Just $ ModConnNamed i' e + | otherwise = Nothing +fixModInst _ a = a + +findActiveWires :: Identifier -> SourceInfo -> [Identifier] +findActiveWires t src = + nub + $ assignWires + <> assignStat + <> fmap portToId i + <> fmap portToId o + <> fmap paramToId p + <> modinstwires + where + assignWires = m ^.. modItems . traverse . modContAssign . contAssignNetLVal + assignStat = + concatMap lValName + $ (allStat ^.. traverse . stmntBA . assignReg) + <> (allStat ^.. traverse . stmntNBA . assignReg) + allStat = filter isAssign . concat $ fmap universe stat + stat = + (m ^.. modItems . traverse . _Initial) + <> (m ^.. modItems . traverse . _Always) + modinstwires = + concat $ modInstActive (src ^. infoSrc . _Wrapped) <$> m ^. modItems + m@(ModDecl _ o i _ p) = src ^. aModule t + +-- | Clean a specific module. Have to be carful that the module is in the +-- 'SourceInfo', otherwise it will crash. +cleanSourceInfo :: Identifier -> SourceInfo -> SourceInfo +cleanSourceInfo t src = src & aModule t %~ clean (findActiveWires t src) + +cleanSourceInfoAll :: SourceInfo -> SourceInfo +cleanSourceInfoAll src = foldr cleanSourceInfo src allMods + where allMods = src ^.. infoSrc . _Wrapped . traverse . modId + +-- | Returns true if the text matches the name of a module. +matchesModName :: Identifier -> ModDecl -> Bool +matchesModName top (ModDecl i _ _ _ _) = top == i + +halveStatement :: Replace Statement +halveStatement (SeqBlock [s]) = halveStatement s +halveStatement (SeqBlock s) = SeqBlock <$> halve s +halveStatement (CondStmnt _ (Just s1) (Just s2)) = Dual s1 s2 +halveStatement (CondStmnt _ (Just s1) Nothing) = Single s1 +halveStatement (CondStmnt _ Nothing (Just s1)) = Single s1 +halveStatement (EventCtrl e (Just s)) = EventCtrl e . Just <$> halveStatement s +halveStatement (TimeCtrl e (Just s)) = TimeCtrl e . Just <$> halveStatement s +halveStatement a = Single a + +halveAlways :: Replace ModItem +halveAlways (Always s) = Always <$> halveStatement s +halveAlways a = Single a + +-- | Removes half the modules randomly, until it reaches a minimal amount of +-- modules. This is done by doing a binary search on the list of modules and +-- removing the instantiations from the main module body. +halveModules :: Replace SourceInfo +halveModules srcInfo@(SourceInfo top _) = + cleanSourceInfoAll + . cleanModInst + . addMod main + <$> combine (infoSrc . _Wrapped) repl srcInfo + where + repl = halve . filter (not . matchesModName (Identifier top)) + main = srcInfo ^. mainModule + +moduleBot :: SourceInfo -> Bool +moduleBot (SourceInfo _ (Verilog [] )) = True +moduleBot (SourceInfo _ (Verilog [_])) = True +moduleBot (SourceInfo _ (Verilog _ )) = False + +-- | Reducer for module items. It does a binary search on all the module items, +-- except assignments to outputs and input-output declarations. +halveModItems :: Identifier -> Replace SourceInfo +halveModItems t srcInfo = cleanSourceInfo t . addRelevant <$> src + where + repl = halve . filter (not . relevantModItem main) + relevant = filter (relevantModItem main) $ main ^. modItems + main = srcInfo ^. aModule t + src = combine (aModule t . modItems) repl srcInfo + addRelevant = aModule t . modItems %~ (relevant ++) + +modItemBot :: Identifier -> SourceInfo -> Bool +modItemBot t srcInfo | length modItemsNoDecl > 2 = False + | otherwise = True + where + modItemsNoDecl = + filter noDecl $ srcInfo ^.. aModule t . modItems . traverse + noDecl Decl{} = False + noDecl _ = True + +halveStatements :: Identifier -> Replace SourceInfo +halveStatements t m = + cleanSourceInfo t <$> combine (aModule t . modItems) halves m + where halves = traverse halveAlways + +-- | Reduce expressions by splitting them in half and keeping the half that +-- succeeds. +halveExpr :: Identifier -> Replace SourceInfo +halveExpr t = combine contexpr $ traverse halveModExpr + where + contexpr :: Lens' SourceInfo [ModItem] + contexpr = aModule t . modItems + +toIds :: [Expr] -> [Identifier] +toIds = nub . mapMaybe exprId . concatMap universe + +toIdsConst :: [ConstExpr] -> [Identifier] +toIdsConst = toIds . fmap constToExpr + +toIdsEvent :: [Event] -> [Identifier] +toIdsEvent = nub . mapMaybe eventId . concatMap universe + +allStatIds' :: Statement -> [Identifier] +allStatIds' s = nub $ assignIds <> otherExpr <> eventProcessedIds + where + assignIds = + toIds + $ (s ^.. stmntBA . assignExpr) + <> (s ^.. stmntNBA . assignExpr) + <> (s ^.. forAssign . assignExpr) + <> (s ^.. forIncr . assignExpr) + otherExpr = toIds $ (s ^.. forExpr) <> (s ^.. stmntCondExpr) + eventProcessedIds = toIdsEvent $ s ^.. statEvent + +allStatIds :: Statement -> [Identifier] +allStatIds s = nub . concat $ allStatIds' <$> universe s + +fromRange :: Range -> [ConstExpr] +fromRange r = [rangeMSB r, rangeLSB r] + +allExprIds :: ModDecl -> [Identifier] +allExprIds m = + nub + $ contAssignIds + <> modInstIds + <> modInitialIds + <> modAlwaysIds + <> modPortIds + <> modDeclIds + <> paramIds + where + contAssignIds = + toIds $ m ^.. modItems . traverse . modContAssign . contAssignExpr + modInstIds = + toIds $ m ^.. modItems . traverse . modInstConns . traverse . modExpr + modInitialIds = + nub . concatMap allStatIds $ m ^.. modItems . traverse . _Initial + modAlwaysIds = + nub . concatMap allStatIds $ m ^.. modItems . traverse . _Always + modPortIds = + nub + . concatMap (toIdsConst . fromRange) + $ m + ^.. modItems + . traverse + . declPort + . portSize + modDeclIds = toIdsConst $ m ^.. modItems . traverse . declVal . _Just + paramIds = + toIdsConst + $ (m ^.. modItems . traverse . paramDecl . traverse . paramValue) + <> ( m + ^.. modItems + . traverse + . localParamDecl + . traverse + . localParamValue + ) + +isUsedDecl :: [Identifier] -> ModItem -> Bool +isUsedDecl ids (Decl _ (Port _ _ _ i) _) = i `elem` ids +isUsedDecl _ _ = True + +isUsedParam :: [Identifier] -> Parameter -> Bool +isUsedParam ids (Parameter i _) = i `elem` ids + +isUsedPort :: [Identifier] -> Port -> Bool +isUsedPort ids (Port _ _ _ i) = i `elem` ids + +removeDecl :: SourceInfo -> SourceInfo +removeDecl src = foldr fix removed allMods + where + removeDecl' t src' = + src' + & (\a -> a & aModule t . modItems %~ filter + (isUsedDecl (used <> findActiveWires t a)) + ) + . (aModule t . modParams %~ filter (isUsedParam used)) + . (aModule t . modInPorts %~ filter (isUsedPort used)) + where used = nub $ allExprIds (src' ^. aModule t) + allMods = src ^.. infoSrc . _Wrapped . traverse . modId + fix t a = a & aModule t . modItems %~ fmap (fixModInst a) + removed = foldr removeDecl' src allMods + +defaultBot :: SourceInfo -> Bool +defaultBot = const False + +-- | Reduction using custom reduction strategies. +reduce_ + :: MonadSh m + => Text + -> Replace SourceInfo + -> (SourceInfo -> Bool) + -> (SourceInfo -> m Bool) + -> SourceInfo + -> m SourceInfo +reduce_ title repl bot eval src = do + liftSh + . Shelly.echo + $ "Reducing " + <> title + <> " (Modules: " + <> showT (length . getVerilog $ _infoSrc src) + <> ", Module items: " + <> showT + (length + (src ^.. infoSrc . _Wrapped . traverse . modItems . traverse) + ) + <> ")" + if bot src + then return src + else case repl src of + Single s -> do + red <- eval s + if red + then if cond s then recReduction s else return s + else return src + Dual l r -> do + red <- eval l + if red + then if cond l then recReduction l else return l + else do + red' <- eval r + if red' + then if cond r then recReduction r else return r + else return src + None -> return src + where + cond s = s /= src + recReduction = reduce_ title repl bot eval + +-- | Reduce an input to a minimal representation. It follows the reduction +-- strategy mentioned above. +reduce + :: MonadSh m + => (SourceInfo -> m Bool) -- ^ Failed or not. + -> SourceInfo -- ^ Input verilog source to be reduced. + -> m SourceInfo -- ^ Reduced output. +reduce eval src = + fmap removeDecl + $ red "Modules" moduleBot halveModules src + >>= redAll "Module Items" modItemBot halveModItems + >>= redAll "Statements" (const defaultBot) halveStatements + -- >>= redAll "Expressions" (const defaultBot) halveExpr + where + red s bot a = reduce_ s a bot eval + red' s bot a t = reduce_ s (a t) (bot t) eval + redAll s bot halve' src' = foldrM + (\t -> red' (s <> " (" <> getIdentifier t <> ")") bot halve' t) + src' + (src' ^.. infoSrc . _Wrapped . traverse . modId) + +runScript + :: MonadSh m => Shelly.FilePath -> Shelly.FilePath -> SourceInfo -> m Bool +runScript fp file src = do + e <- liftSh $ do + Shelly.writefile file $ genSource src + noPrint . Shelly.errExit False $ Shelly.run_ fp [] + Shelly.lastExitCode + return $ e == 0 + +-- | Reduce using a script that is passed to it +reduceWithScript + :: (MonadSh m, MonadIO m) + => Text + -> Shelly.FilePath + -> Shelly.FilePath + -> m () +reduceWithScript top script file = do + liftSh . Shelly.cp file $ file <.> "original" + srcInfo <- liftIO . parseSourceInfoFile top $ Shelly.toTextIgnore file + void $ reduce (runScript script file) srcInfo + +-- | Reduce a 'SourceInfo' using two 'Synthesiser' that are passed to it. +reduceSynth + :: (Synthesiser a, Synthesiser b, MonadSh m) + => Shelly.FilePath + -> a + -> b + -> SourceInfo + -> m SourceInfo +reduceSynth datadir a b = reduce synth + where + synth src' = liftSh $ do + r <- runResultT $ do + runSynth a src' + runSynth b src' + runEquiv datadir a b src' + return $ case r of + Fail EquivFail -> True + Fail _ -> False + Pass _ -> False + +reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo +reduceSynthesis a = reduce synth + where + synth src = liftSh $ do + r <- runResultT $ runSynth a src + return $ case r of + Fail SynthFail -> True + Fail _ -> False + Pass _ -> False diff --git a/src/Verismith/Report.hs b/src/Verismith/Report.hs new file mode 100644 index 0000000..196e891 --- /dev/null +++ b/src/Verismith/Report.hs @@ -0,0 +1,398 @@ +{-# LANGUAGE RankNTypes #-} +{-| +Module : Verismith.Report +Description : Generate a report from a fuzz run. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Generate a report from a fuzz run. +-} + +{-# LANGUAGE TemplateHaskell #-} + +module Verismith.Report + ( SynthTool(..) + , SynthStatus(..) + , SynthResult(..) + , SimResult(..) + , SimTool(..) + , FuzzReport(..) + , printResultReport + , printSummary + , synthResults + , simResults + , synthStatus + , equivTime + , fuzzDir + , fileLines + , reducTime + , synthTime + , defaultIcarusSim + , defaultVivadoSynth + , defaultYosysSynth + , defaultXSTSynth + , defaultQuartusSynth + , defaultIdentitySynth + , descriptionToSim + , descriptionToSynth + ) +where + +import Control.DeepSeq (NFData, rnf) +import Control.Lens hiding (Identity, (<.>)) +import Data.Bifunctor (bimap) +import Data.ByteString (ByteString) +import Data.Maybe (fromMaybe) +import Data.Monoid (Endo) +import Data.Text (Text) +import qualified Data.Text as T +import Data.Text.Lazy (toStrict) +import Data.Time +import Data.Vector (fromList) +import Prelude hiding (FilePath) +import Shelly (FilePath, fromText, + toTextIgnore, (<.>), (</>)) +import Statistics.Sample (meanVariance) +import Text.Blaze.Html (Html, (!)) +import Text.Blaze.Html.Renderer.Text (renderHtml) +import qualified Text.Blaze.Html5 as H +import qualified Text.Blaze.Html5.Attributes as A +import Verismith.Config +import Verismith.Internal +import Verismith.Result +import Verismith.Tool +import Verismith.Tool.Internal + +-- | Common type alias for synthesis results +type UResult = Result Failed () + +-- | Commont type alias for simulation results +type BResult = Result Failed ByteString + +data SynthTool = XSTSynth {-# UNPACK #-} !XST + | VivadoSynth {-# UNPACK #-} !Vivado + | YosysSynth {-# UNPACK #-} !Yosys + | QuartusSynth {-# UNPACK #-} !Quartus + | IdentitySynth {-# UNPACK #-} !Identity + deriving (Eq) + +instance NFData SynthTool where + rnf (XSTSynth a) = rnf a + rnf (VivadoSynth a) = rnf a + rnf (YosysSynth a) = rnf a + rnf (QuartusSynth a) = rnf a + rnf (IdentitySynth a) = rnf a + +instance Show SynthTool where + show (XSTSynth xst) = show xst + show (VivadoSynth vivado) = show vivado + show (YosysSynth yosys) = show yosys + show (QuartusSynth quartus) = show quartus + show (IdentitySynth identity) = show identity + +instance Tool SynthTool where + toText (XSTSynth xst) = toText xst + toText (VivadoSynth vivado) = toText vivado + toText (YosysSynth yosys) = toText yosys + toText (QuartusSynth quartus) = toText quartus + toText (IdentitySynth identity) = toText identity + +instance Synthesiser SynthTool where + runSynth (XSTSynth xst) = runSynth xst + runSynth (VivadoSynth vivado) = runSynth vivado + runSynth (YosysSynth yosys) = runSynth yosys + runSynth (QuartusSynth quartus) = runSynth quartus + runSynth (IdentitySynth identity) = runSynth identity + + synthOutput (XSTSynth xst) = synthOutput xst + synthOutput (VivadoSynth vivado) = synthOutput vivado + synthOutput (YosysSynth yosys) = synthOutput yosys + synthOutput (QuartusSynth quartus) = synthOutput quartus + synthOutput (IdentitySynth identity) = synthOutput identity + + setSynthOutput (YosysSynth yosys) = YosysSynth . setSynthOutput yosys + setSynthOutput (XSTSynth xst) = XSTSynth . setSynthOutput xst + setSynthOutput (VivadoSynth vivado) = VivadoSynth . setSynthOutput vivado + setSynthOutput (QuartusSynth quartus) = QuartusSynth . setSynthOutput quartus + setSynthOutput (IdentitySynth identity) = IdentitySynth . setSynthOutput identity + +defaultYosysSynth :: SynthTool +defaultYosysSynth = YosysSynth defaultYosys + +defaultQuartusSynth :: SynthTool +defaultQuartusSynth = QuartusSynth defaultQuartus + +defaultVivadoSynth :: SynthTool +defaultVivadoSynth = VivadoSynth defaultVivado + +defaultXSTSynth :: SynthTool +defaultXSTSynth = XSTSynth defaultXST + +defaultIdentitySynth :: SynthTool +defaultIdentitySynth = IdentitySynth defaultIdentity + +newtype SimTool = IcarusSim Icarus + deriving (Eq) + +instance NFData SimTool where + rnf (IcarusSim a) = rnf a + +instance Tool SimTool where + toText (IcarusSim icarus) = toText icarus + +instance Simulator SimTool where + runSim (IcarusSim icarus) = runSim icarus + runSimWithFile (IcarusSim icarus) = runSimWithFile icarus + +instance Show SimTool where + show (IcarusSim icarus) = show icarus + +defaultIcarusSim :: SimTool +defaultIcarusSim = IcarusSim defaultIcarus + +-- | The results from running a tool through a simulator. It can either fail or +-- return a result, which is most likely a 'ByteString'. +data SimResult = SimResult !SynthTool !SimTool !BResult !NominalDiffTime + deriving (Eq) + +instance Show SimResult where + show (SimResult synth sim r d) = show synth <> ", " <> show sim <> ": " <> show (bimap show (T.unpack . showBS) r) <> " (" <> show d <> ")" + +getSimResult :: SimResult -> UResult +getSimResult (SimResult _ _ (Pass _) _) = Pass () +getSimResult (SimResult _ _ (Fail b) _) = Fail b + +-- | The results of comparing the synthesised outputs of two files using a +-- formal equivalence checker. This will either return a failure or an output +-- which is most likely '()'. +data SynthResult = SynthResult !SynthTool !SynthTool !UResult !NominalDiffTime + deriving (Eq) + +instance Show SynthResult where + show (SynthResult synth synth2 r d) = show synth <> ", " <> show synth2 <> ": " <> show r <> " (" <> show d <> ")" + +getSynthResult :: SynthResult -> UResult +getSynthResult (SynthResult _ _ a _) = a + +-- | The status of the synthesis using a simulator. This will be checked before +-- attempting to run the equivalence checks on the simulator, as that would be +-- unnecessary otherwise. +data SynthStatus = SynthStatus !SynthTool !UResult !NominalDiffTime + deriving (Eq) + +getSynthStatus :: SynthStatus -> UResult +getSynthStatus (SynthStatus _ a _) = a + +instance Show SynthStatus where + show (SynthStatus synth r d) = "synthesis " <> show synth <> ": " <> show r <> " (" <> show d <> ")" + +-- | The complete state that will be used during fuzzing, which contains the +-- results from all the operations. +data FuzzReport = FuzzReport { _fuzzDir :: !FilePath + , _synthResults :: ![SynthResult] -- ^ Results of the equivalence check. + , _simResults :: ![SimResult] -- ^ Results of the simulation. + , _synthStatus :: ![SynthStatus] -- ^ Results of the synthesis step. + , _fileLines :: {-# UNPACK #-} !Int + , _synthTime :: !NominalDiffTime + , _equivTime :: !NominalDiffTime + , _reducTime :: !NominalDiffTime + } + deriving (Eq, Show) + +$(makeLenses ''FuzzReport) + +descriptionToSim :: SimDescription -> SimTool +descriptionToSim (SimDescription "icarus") = defaultIcarusSim +descriptionToSim s = + error $ "Could not find implementation for simulator '" <> show s <> "'" + +-- | Convert a description to a synthesiser. +descriptionToSynth :: SynthDescription -> SynthTool +descriptionToSynth (SynthDescription "yosys" bin desc out) = + YosysSynth + . Yosys (fromText <$> bin) (fromMaybe (yosysDesc defaultYosys) desc) + $ maybe (yosysOutput defaultYosys) fromText out +descriptionToSynth (SynthDescription "vivado" bin desc out) = + VivadoSynth + . Vivado (fromText <$> bin) (fromMaybe (vivadoDesc defaultVivado) desc) + $ maybe (vivadoOutput defaultVivado) fromText out +descriptionToSynth (SynthDescription "xst" bin desc out) = + XSTSynth + . XST (fromText <$> bin) (fromMaybe (xstDesc defaultXST) desc) + $ maybe (xstOutput defaultXST) fromText out +descriptionToSynth (SynthDescription "quartus" bin desc out) = + QuartusSynth + . Quartus (fromText <$> bin) + (fromMaybe (quartusDesc defaultQuartus) desc) + $ maybe (quartusOutput defaultQuartus) fromText out +descriptionToSynth (SynthDescription "identity" _ desc out) = + IdentitySynth + . Identity (fromMaybe (identityDesc defaultIdentity) desc) + $ maybe (identityOutput defaultIdentity) fromText out +descriptionToSynth s = + error $ "Could not find implementation for synthesiser '" <> show s <> "'" + +status :: Result Failed () -> Html +status (Pass _ ) = H.td ! A.class_ "is-success" $ "Passed" +status (Fail EmptyFail ) = H.td ! A.class_ "is-danger" $ "Failed" +status (Fail EquivFail ) = H.td ! A.class_ "is-danger" $ "Equivalence failed" +status (Fail SimFail ) = H.td ! A.class_ "is-danger" $ "Simulation failed" +status (Fail SynthFail ) = H.td ! A.class_ "is-danger" $ "Synthesis failed" +status (Fail EquivError ) = H.td ! A.class_ "is-danger" $ "Equivalence error" +status (Fail TimeoutError) = H.td ! A.class_ "is-warning" $ "Time out" + +synthStatusHtml :: SynthStatus -> Html +synthStatusHtml (SynthStatus synth res diff) = H.tr $ do + H.td . H.toHtml $ toText synth + status res + H.td . H.toHtml $ showT diff + +synthResultHtml :: SynthResult -> Html +synthResultHtml (SynthResult synth1 synth2 res diff) = H.tr $ do + H.td . H.toHtml $ toText synth1 + H.td . H.toHtml $ toText synth2 + status res + H.td . H.toHtml $ showT diff + +resultHead :: Text -> Html +resultHead name = H.head $ do + H.title $ "Fuzz Report - " <> H.toHtml name + H.meta ! A.name "viewport" ! A.content "width=device-width, initial-scale=1" + H.meta ! A.charset "utf8" + H.link + ! A.rel "stylesheet" + ! A.href + "https://cdnjs.cloudflare.com/ajax/libs/bulma/0.7.4/css/bulma.min.css" + +resultReport :: Text -> FuzzReport -> Html +resultReport name (FuzzReport _ synth _ stat _ _ _ _) = H.docTypeHtml $ do + resultHead name + H.body + . (H.section ! A.class_ "section") + . (H.div ! A.class_ "container") + $ do + H.h1 ! A.class_ "title is-1" $ "Fuzz Report - " <> H.toHtml name + H.h2 ! A.class_ "title is-2" $ "Synthesis" + H.table ! A.class_ "table" $ do + H.thead + . H.toHtml + $ ( H.tr + . H.toHtml + $ [H.th "Tool", H.th "Status", H.th "Run time"] + ) + H.tbody . H.toHtml $ fmap synthStatusHtml stat + H.h2 ! A.class_ "title is-2" $ "Equivalence Check" + H.table ! A.class_ "table" $ do + H.thead + . H.toHtml + $ ( H.tr + . H.toHtml + $ [ H.th "First tool" + , H.th "Second tool" + , H.th "Status" + , H.th "Run time" + ] + ) + H.tbody . H.toHtml $ fmap synthResultHtml synth + +resultStatus :: Result a b -> Html +resultStatus (Pass _) = H.td ! A.class_ "is-success" $ "Passed" +resultStatus (Fail _) = H.td ! A.class_ "is-danger" $ "Failed" + +fuzzStats + :: (Real a1, Traversable t) + => ((a1 -> Const (Endo [a1]) a1) -> a2 -> Const (Endo [a1]) a2) + -> t a2 + -> (Double, Double) +fuzzStats sel fr = meanVariance converted + where converted = fromList . fmap realToFrac $ fr ^.. traverse . sel + +fuzzStatus :: Text -> FuzzReport -> Html +fuzzStatus name (FuzzReport dir s1 s2 s3 sz t1 t2 t3) = H.tr $ do + H.td + . ( H.a + ! A.href + ( H.textValue + $ toTextIgnore (dir <.> "html") + ) + ) + $ H.toHtml name + resultStatus + $ mconcat (fmap getSynthResult s1) + <> mconcat (fmap getSimResult s2) + <> mconcat (fmap getSynthStatus s3) + H.td . H.string $ show sz + H.td . H.string $ show t1 + H.td . H.string $ show t2 + H.td . H.string $ show t3 + +summary :: Text -> [FuzzReport] -> Html +summary name fuzz = H.docTypeHtml $ do + resultHead name + H.body + . (H.section ! A.class_ "section") + . (H.div ! A.class_ "container") + $ do + H.h1 ! A.class_ "title is-1" $ "FuzzReport - " <> H.toHtml name + H.table ! A.class_ "table" $ do + H.thead . H.tr $ H.toHtml + [ H.th "Name" + , H.th "Status" + , H.th "Size (loc)" + , H.th "Synthesis time" + , H.th "Equivalence check time" + , H.th "Reduction time" + ] + H.tbody + . H.toHtml + . fmap + (\(i, r) -> + fuzzStatus ("Fuzz " <> showT (i :: Int)) r + ) + $ zip [1 ..] fuzz + H.tfoot . H.toHtml $ do + H.tr $ H.toHtml + [ H.td $ H.strong "Total" + , H.td mempty + , H.td + . H.string + . show + . sum + $ fuzz + ^.. traverse + . fileLines + , sumUp synthTime + , sumUp equivTime + , sumUp reducTime + ] + H.tr $ H.toHtml + [ H.td $ H.strong "Mean" + , H.td mempty + , fst $ bimap d2I d2I $ fuzzStats fileLines fuzz + , fst $ meanVar synthTime + , fst $ meanVar equivTime + , fst $ meanVar reducTime + ] + H.tr $ H.toHtml + [ H.td $ H.strong "Variance" + , H.td mempty + , snd $ bimap d2I d2I $ fuzzStats fileLines fuzz + , snd $ meanVar synthTime + , snd $ meanVar equivTime + , snd $ meanVar reducTime + ] + where + sumUp s = showHtml . sum $ fuzz ^.. traverse . s + meanVar s = bimap d2T d2T $ fuzzStats s fuzz + showHtml = H.td . H.string . show + d2T = showHtml . (realToFrac :: Double -> NominalDiffTime) + d2I = H.td . H.string . show + +printResultReport :: Text -> FuzzReport -> Text +printResultReport t f = toStrict . renderHtml $ resultReport t f + +printSummary :: Text -> [FuzzReport] -> Text +printSummary t f = toStrict . renderHtml $ summary t f diff --git a/src/Verismith/Result.hs b/src/Verismith/Result.hs new file mode 100644 index 0000000..d8efd2f --- /dev/null +++ b/src/Verismith/Result.hs @@ -0,0 +1,137 @@ +{-| +Module : Verismith.Result +Description : Result monadic type. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Result monadic type. This is nearly equivalent to the transformers 'Error' type, +but to have more control this is reimplemented with the instances that are +needed in "Verismith". +-} + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Verismith.Result + ( Result(..) + , ResultT(..) + , (<?>) + , annotate + ) +where + +import Control.Monad.Base +import Control.Monad.IO.Class +import Control.Monad.Trans.Class +import Control.Monad.Trans.Control +import Data.Bifunctor (Bifunctor (..)) +import Shelly (RunFailed (..), Sh, catch_sh) +import Shelly.Lifted (MonadSh, liftSh) + +-- | Result type which is equivalent to 'Either' or 'Error'. This is +-- reimplemented so that there is full control over the 'Monad' definition and +-- definition of a 'Monad' transformer 'ResultT'. +data Result a b = Fail a + | Pass b + deriving (Eq, Show) + +instance Semigroup (Result a b) where + Pass _ <> a = a + a <> _ = a + +instance (Monoid b) => Monoid (Result a b) where + mempty = Pass mempty + +instance Functor (Result a) where + fmap f (Pass a) = Pass $ f a + fmap _ (Fail b) = Fail b + +instance Applicative (Result a) where + pure = Pass + Fail e <*> _ = Fail e + Pass f <*> r = fmap f r + +instance Monad (Result a) where + Pass a >>= f = f a + Fail b >>= _ = Fail b + +instance MonadBase (Result a) (Result a) where + liftBase = id + +instance Bifunctor Result where + bimap a _ (Fail c) = Fail $ a c + bimap _ b (Pass c) = Pass $ b c + +-- | The transformer for the 'Result' type. This +newtype ResultT a m b = ResultT { runResultT :: m (Result a b) } + +instance Functor f => Functor (ResultT a f) where + fmap f = ResultT . fmap (fmap f) . runResultT + +instance Monad m => Applicative (ResultT a m) where + pure = ResultT . pure . pure + f <*> a = ResultT $ do + f' <- runResultT f + case f' of + Fail e -> return (Fail e) + Pass k -> do + a' <- runResultT a + case a' of + Fail e -> return (Fail e) + Pass v -> return (Pass $ k v) + +instance Monad m => Monad (ResultT a m) where + a >>= b = ResultT $ do + m <- runResultT a + case m of + Fail e -> return (Fail e) + Pass p -> runResultT (b p) + +instance (MonadSh m, Monoid a) => MonadSh (ResultT a m) where + liftSh s = + ResultT + . liftSh + . catch_sh (Pass <$> s) + $ (const (Fail <$> return mempty) :: RunFailed -> Sh (Result a b)) + +instance MonadIO m => MonadIO (ResultT a m) where + liftIO s = ResultT $ Pass <$> liftIO s + +instance MonadBase b m => MonadBase b (ResultT a m) where + liftBase = liftBaseDefault + +instance MonadTrans (ResultT e) where + lift m = ResultT $ Pass <$> m + +instance MonadTransControl (ResultT a) where + type StT (ResultT a) b = Result a b + liftWith f = ResultT $ return <$> f runResultT + restoreT = ResultT + {-# INLINABLE liftWith #-} + {-# INLINABLE restoreT #-} + +instance MonadBaseControl IO m => MonadBaseControl IO (ResultT a m) where + type StM (ResultT a m) b = ComposeSt (ResultT a) m b + liftBaseWith = defaultLiftBaseWith + restoreM = defaultRestoreM + {-# INLINABLE liftBaseWith #-} + {-# INLINABLE restoreM #-} + +infix 0 <?> + +(<?>) :: (Monad m, Monoid a) => ResultT a m b -> a -> ResultT a m b +m <?> b = ResultT $ do + a <- runResultT m + case a of + Pass a' -> return $ Pass a' + Fail a' -> return . Fail $ a' <> b + +annotate :: (Monad m, Monoid a) => a -> ResultT a m b -> ResultT a m b +annotate = flip (<?>) diff --git a/src/Verismith/Tool.hs b/src/Verismith/Tool.hs new file mode 100644 index 0000000..7e41180 --- /dev/null +++ b/src/Verismith/Tool.hs @@ -0,0 +1,51 @@ +{-| +Module : Verismith.Tool +Description : Simulator implementations. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Simulator implementations. +-} + +module Verismith.Tool + ( + -- * Simulators + -- ** Icarus + Icarus(..) + , defaultIcarus + -- * Synthesisers + -- ** Yosys + , Yosys(..) + , defaultYosys + -- ** Vivado + , Vivado(..) + , defaultVivado + -- ** XST + , XST(..) + , defaultXST + -- ** Quartus + , Quartus(..) + , defaultQuartus + -- ** Identity + , Identity(..) + , defaultIdentity + -- * Equivalence + , runEquiv + -- * Simulation + , runSim + -- * Synthesis + , runSynth + , logger + ) +where + +import Verismith.Tool.Icarus +import Verismith.Tool.Identity +import Verismith.Tool.Internal +import Verismith.Tool.Quartus +import Verismith.Tool.Vivado +import Verismith.Tool.XST +import Verismith.Tool.Yosys diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs new file mode 100644 index 0000000..9d4281f --- /dev/null +++ b/src/Verismith/Tool/Icarus.hs @@ -0,0 +1,191 @@ +{-| +Module : Verismith.Tool.Icarus +Description : Icarus verilog module. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Icarus verilog module. +-} + +module Verismith.Tool.Icarus + ( Icarus(..) + , defaultIcarus + , runSimIc + ) +where + +import Control.DeepSeq (NFData, rnf, rwhnf) +import Control.Lens +import Control.Monad (void) +import Crypto.Hash (Digest, hash) +import Crypto.Hash.Algorithms (SHA256) +import Data.Binary (encode) +import Data.Bits +import qualified Data.ByteArray as BA (convert) +import Data.ByteString (ByteString) +import qualified Data.ByteString as B +import Data.ByteString.Lazy (toStrict) +import qualified Data.ByteString.Lazy as L (ByteString) +import Data.Char (digitToInt) +import Data.Foldable (fold) +import Data.List (transpose) +import Data.Maybe (listToMaybe) +import Data.Text (Text) +import qualified Data.Text as T +import Numeric (readInt) +import Prelude hiding (FilePath) +import Shelly +import Shelly.Lifted (liftSh) +import Verismith.Tool.Internal +import Verismith.Tool.Template +import Verismith.Verilog.AST +import Verismith.Verilog.BitVec +import Verismith.Verilog.CodeGen +import Verismith.Verilog.Internal +import Verismith.Verilog.Mutate + +data Icarus = Icarus { icarusPath :: FilePath + , vvpPath :: FilePath + } + deriving (Eq) + +instance Show Icarus where + show _ = "iverilog" + +instance Tool Icarus where + toText _ = "iverilog" + +instance Simulator Icarus where + runSim = runSimIcarus + runSimWithFile = runSimIcarusWithFile + +instance NFData Icarus where + rnf = rwhnf + +defaultIcarus :: Icarus +defaultIcarus = Icarus "iverilog" "vvp" + +addDisplay :: [Statement] -> [Statement] +addDisplay s = concat $ transpose + [ s + , replicate l $ TimeCtrl 1 Nothing + , replicate l . SysTaskEnable $ Task "display" ["%b", Id "y"] + ] + where l = length s + +assignFunc :: [Port] -> ByteString -> Statement +assignFunc inp bs = + NonBlockAssign + . Assign conc Nothing + . Number + . BitVec (B.length bs * 8) + $ bsToI bs + where conc = RegConcat (portToExpr <$> inp) + +convert :: Text -> ByteString +convert = + toStrict + . (encode :: Integer -> L.ByteString) + . maybe 0 fst + . listToMaybe + . readInt 2 (`elem` ("01" :: String)) digitToInt + . T.unpack + +mask :: Text -> Text +mask = T.replace "x" "0" + +callback :: ByteString -> Text -> ByteString +callback b t = b <> convert (mask t) + +runSimIcarus :: Icarus -> SourceInfo -> [ByteString] -> ResultSh ByteString +runSimIcarus sim rinfo bss = do + let tb = ModDecl + "main" + [] + [] + [ Initial + $ fold (addDisplay $ assignFunc (_modInPorts m) <$> bss) + <> (SysTaskEnable $ Task "finish" []) + ] + [] + let newtb = instantiateMod m tb + let modWithTb = Verilog [newtb, m] + liftSh . writefile "main.v" $ genSource modWithTb + annotate SimFail $ runSimWithFile sim "main.v" bss + where m = rinfo ^. mainModule + +runSimIcarusWithFile + :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString +runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do + dir <- pwd + logCommand_ dir "icarus" + $ run (icarusPath sim) ["-o", "main", toTextIgnore f] + B.take 8 . BA.convert . (hash :: ByteString -> Digest SHA256) <$> logCommand + dir + "vvp" + (runFoldLines (mempty :: ByteString) callback (vvpPath sim) ["main"]) + +fromBytes :: ByteString -> Integer +fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b + +runSimIc + :: (Synthesiser b) + => FilePath + -> Icarus + -> b + -> SourceInfo + -> [ByteString] + -> ResultSh ByteString +runSimIc datadir sim1 synth1 srcInfo bss = do + dir <- liftSh pwd + let top = srcInfo ^. mainModule + let inConcat = (RegConcat . filter filterClk $ (Id . fromPort <$> (top ^. modInPorts))) + let + tb = instantiateMod top $ ModDecl + "testbench" + [] + [] + [ Initial + $ fold + [ BlockAssign (Assign "clk" Nothing 0) + , BlockAssign (Assign inConcat Nothing 0) + ] + <> fold + ( (\r -> TimeCtrl + 10 + (Just $ BlockAssign (Assign inConcat Nothing r)) + ) + . fromInteger + . fromBytes + <$> bss + ) + <> (SysTaskEnable $ Task "finish" []) + , Always . TimeCtrl 5 . Just $ BlockAssign + (Assign "clk" Nothing (UnOp UnNot (Id "clk"))) + , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task + "strobe" + ["%b", Id "y"] + ] + [] + + liftSh . writefile "testbench.v" $ icarusTestbench datadir (Verilog [tb]) synth1 + liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"] + liftSh + $ B.take 8 + . BA.convert + . (hash :: ByteString -> Digest SHA256) + <$> logCommand + dir + "vvp" + (runFoldLines (mempty :: ByteString) + callback + (vvpPath sim1) + ["main"] + ) + where + exe dir name e = void . errExit False . logCommand dir name . timeout e + filterClk (Id "clk") = False + filterClk (Id _) = True diff --git a/src/Verismith/Tool/Identity.hs b/src/Verismith/Tool/Identity.hs new file mode 100644 index 0000000..93b05d5 --- /dev/null +++ b/src/Verismith/Tool/Identity.hs @@ -0,0 +1,51 @@ +{-| +Module : Verismith.Tool.Identity +Description : The identity simulator and synthesiser. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +The identity simulator and synthesiser. +-} + +module Verismith.Tool.Identity + ( Identity(..) + , defaultIdentity + ) +where + +import Control.DeepSeq (NFData, rnf, rwhnf) +import Data.Text (Text, unpack) +import Prelude hiding (FilePath) +import Shelly (FilePath) +import Shelly.Lifted (writefile) +import Verismith.Tool.Internal +import Verismith.Verilog.AST +import Verismith.Verilog.CodeGen + +data Identity = Identity { identityDesc :: {-# UNPACK #-} !Text + , identityOutput :: {-# UNPACK #-} !FilePath + } + deriving (Eq) + +instance Tool Identity where + toText (Identity d _) = d + +instance Show Identity where + show t = unpack $ toText t + +instance Synthesiser Identity where + runSynth = runSynthIdentity + synthOutput = identityOutput + setSynthOutput (Identity a _) = Identity a + +instance NFData Identity where + rnf = rwhnf + +runSynthIdentity :: Identity -> SourceInfo -> ResultSh () +runSynthIdentity (Identity _ out) = writefile out . genSource + +defaultIdentity :: Identity +defaultIdentity = Identity "identity" "syn_identity.v" diff --git a/src/Verismith/Tool/Internal.hs b/src/Verismith/Tool/Internal.hs new file mode 100644 index 0000000..c2e3a0c --- /dev/null +++ b/src/Verismith/Tool/Internal.hs @@ -0,0 +1,215 @@ +{-| +Module : Verismith.Tool.Internal +Description : Class of the simulator. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Class of the simulator and the synthesize tool. +-} + +{-# LANGUAGE DeriveFunctor #-} + +module Verismith.Tool.Internal + ( ResultSh + , resultSh + , Tool(..) + , Simulator(..) + , Synthesiser(..) + , Failed(..) + , renameSource + , checkPresent + , checkPresentModules + , replace + , replaceMods + , rootPath + , timeout + , timeout_ + , bsToI + , noPrint + , logger + , logCommand + , logCommand_ + , execute + , execute_ + , (<?>) + , annotate + ) +where + +import Control.Lens +import Control.Monad (forM, void) +import Control.Monad.Catch (throwM) +import Data.Bits (shiftL) +import Data.ByteString (ByteString) +import qualified Data.ByteString as B +import Data.Maybe (catMaybes) +import Data.Text (Text) +import qualified Data.Text as T +import Data.Time.Format (defaultTimeLocale, formatTime) +import Data.Time.LocalTime (getZonedTime) +import Prelude hiding (FilePath) +import Shelly +import Shelly.Lifted (MonadSh, liftSh) +import System.FilePath.Posix (takeBaseName) +import Verismith.Internal +import Verismith.Result +import Verismith.Verilog.AST + +-- | Tool class. +class Tool a where + toText :: a -> Text + +-- | Simulation type class. +class Tool a => Simulator a where + runSim :: a -- ^ Simulator instance + -> SourceInfo -- ^ Run information + -> [ByteString] -- ^ Inputs to simulate + -> ResultSh ByteString -- ^ Returns the value of the hash at the output of the testbench. + runSimWithFile :: a + -> FilePath + -> [ByteString] + -> ResultSh ByteString + +data Failed = EmptyFail + | EquivFail + | EquivError + | SimFail + | SynthFail + | TimeoutError + deriving (Eq, Show) + +instance Semigroup Failed where + EmptyFail <> a = a + b <> _ = b + +instance Monoid Failed where + mempty = EmptyFail + +-- | Synthesiser type class. +class Tool a => Synthesiser a where + runSynth :: a -- ^ Synthesiser tool instance + -> SourceInfo -- ^ Run information + -> ResultSh () -- ^ does not return any values + synthOutput :: a -> FilePath + setSynthOutput :: a -> FilePath -> a + +renameSource :: (Synthesiser a) => a -> SourceInfo -> SourceInfo +renameSource a src = + src & infoSrc . _Wrapped . traverse . modId . _Wrapped %~ (<> toText a) + +-- | Type synonym for a 'ResultT' that will be used throughout 'Verismith'. This +-- has instances for 'MonadSh' and 'MonadIO' if the 'Monad' it is parametrised +-- with also has those instances. +type ResultSh = ResultT Failed Sh + +resultSh :: ResultSh a -> Sh a +resultSh s = do + result <- runResultT s + case result of + Fail e -> throwM . RunFailed "" [] 1 $ showT e + Pass s' -> return s' + +checkPresent :: FilePath -> Text -> Sh (Maybe Text) +checkPresent fp t = do + errExit False $ run_ "grep" [t, toTextIgnore fp] + i <- lastExitCode + if i == 0 then return $ Just t else return Nothing + +-- | Checks what modules are present in the synthesised output, as some modules +-- may have been inlined. This could be improved if the parser worked properly. +checkPresentModules :: FilePath -> SourceInfo -> Sh [Text] +checkPresentModules fp (SourceInfo _ src) = do + vals <- forM (src ^.. _Wrapped . traverse . modId . _Wrapped) + $ checkPresent fp + return $ catMaybes vals + +-- | Uses sed to replace a string in a text file. +replace :: FilePath -> Text -> Text -> Sh () +replace fp t1 t2 = do + errExit False . noPrint $ run_ + "sed" + ["-i", "s/" <> t1 <> "/" <> t2 <> "/g", toTextIgnore fp] + +-- | This is used because rename only renames the definitions of modules of +-- course, so instead this just searches and replaces all the module names. This +-- should find all the instantiations and definitions. This could again be made +-- much simpler if the parser works. +replaceMods :: FilePath -> Text -> SourceInfo -> Sh () +replaceMods fp t (SourceInfo _ src) = + void + . forM (src ^.. _Wrapped . traverse . modId . _Wrapped) + $ (\a -> replace fp a (a <> t)) + +rootPath :: Sh FilePath +rootPath = do + current <- pwd + maybe current fromText <$> get_env "VERISMITH_ROOT" + +timeout :: FilePath -> [Text] -> Sh Text +timeout = command1 "timeout" ["300"] . toTextIgnore +{-# INLINE timeout #-} + +timeout_ :: FilePath -> [Text] -> Sh () +timeout_ = command1_ "timeout" ["300"] . toTextIgnore +{-# INLINE timeout_ #-} + +-- | Helper function to convert bytestrings to integers +bsToI :: ByteString -> Integer +bsToI = B.foldl' (\i b -> (i `shiftL` 8) + fromIntegral b) 0 +{-# INLINE bsToI #-} + +noPrint :: Sh a -> Sh a +noPrint = print_stdout False . print_stderr False +{-# INLINE noPrint #-} + +logger :: Text -> Sh () +logger t = do + fn <- pwd + currentTime <- liftIO getZonedTime + echo + $ "Verismith " + <> T.pack (formatTime defaultTimeLocale "%H:%M:%S " currentTime) + <> bname fn + <> " - " + <> t + where bname = T.pack . takeBaseName . T.unpack . toTextIgnore + +logCommand :: FilePath -> Text -> Sh a -> Sh a +logCommand fp name = log_stderr_with (l "_stderr.log") + . log_stdout_with (l ".log") + where + l s t = appendFile (file s) (T.unpack t) >> appendFile (file s) "\n" + file s = T.unpack (toTextIgnore $ fp </> fromText name) <> s + +logCommand_ :: FilePath -> Text -> Sh a -> Sh () +logCommand_ fp name = void . logCommand fp name + +execute + :: (MonadSh m, Monad m) + => Failed + -> FilePath + -> Text + -> FilePath + -> [Text] + -> ResultT Failed m Text +execute f dir name e cs = do + (res, exitCode) <- liftSh $ do + res <- errExit False . logCommand dir name $ timeout e cs + (,) res <$> lastExitCode + case exitCode of + 0 -> ResultT . return $ Pass res + 124 -> ResultT . return $ Fail TimeoutError + _ -> ResultT . return $ Fail f + +execute_ + :: (MonadSh m, Monad m) + => Failed + -> FilePath + -> Text + -> FilePath + -> [Text] + -> ResultT Failed m () +execute_ a b c d = void . execute a b c d diff --git a/src/Verismith/Tool/Quartus.hs b/src/Verismith/Tool/Quartus.hs new file mode 100644 index 0000000..109d46c --- /dev/null +++ b/src/Verismith/Tool/Quartus.hs @@ -0,0 +1,77 @@ +{-| +Module : Verismith.Tool.Quartus +Description : Quartus synthesiser implementation. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Quartus synthesiser implementation. +-} + +module Verismith.Tool.Quartus + ( Quartus(..) + , defaultQuartus + ) +where + +import Control.DeepSeq (NFData, rnf, rwhnf) +import Data.Text (Text, unpack) +import Prelude hiding (FilePath) +import Shelly +import Shelly.Lifted (liftSh) +import Verismith.Tool.Internal +import Verismith.Verilog.AST +import Verismith.Verilog.CodeGen + +data Quartus = Quartus { quartusBin :: !(Maybe FilePath) + , quartusDesc :: {-# UNPACK #-} !Text + , quartusOutput :: {-# UNPACK #-} !FilePath + } + deriving (Eq) + +instance Tool Quartus where + toText (Quartus _ t _) = t + +instance Show Quartus where + show t = unpack $ toText t + +instance Synthesiser Quartus where + runSynth = runSynthQuartus + synthOutput = quartusOutput + setSynthOutput (Quartus a b _) = Quartus a b + +instance NFData Quartus where + rnf = rwhnf + +defaultQuartus :: Quartus +defaultQuartus = Quartus Nothing "quartus" "syn_quartus.v" + +runSynthQuartus :: Quartus -> SourceInfo -> ResultSh () +runSynthQuartus sim (SourceInfo top src) = do + dir <- liftSh pwd + let ex = execute_ SynthFail dir "quartus" + liftSh . writefile inpf $ genSource src + liftSh . noPrint $ run_ + "sed" + [ "-i" + , "s/^module/(* multstyle = \"logic\" *) module/;" + , toTextIgnore inpf + ] + ex (exec "quartus_map") + [top, "--source=" <> toTextIgnore inpf, "--family=Cyclone V"] + ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"] + ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"] + liftSh $ do + cp (fromText "simulation/vcs" </> fromText top <.> "vo") + $ synthOutput sim + run_ + "sed" + [ "-ri" + , "s,^// DATE.*,,; s,^tri1 (.*);,wire \\1 = 1;,; /^\\/\\/ +synopsys/ d;" + , toTextIgnore $ synthOutput sim + ] + where + inpf = "rtl.v" + exec s = maybe (fromText s) (</> fromText s) $ quartusBin sim diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs new file mode 100644 index 0000000..d02daf8 --- /dev/null +++ b/src/Verismith/Tool/Template.hs @@ -0,0 +1,135 @@ +{-| +Module : Verismith.Tool.Template +Description : Template file for different configuration files +Copyright : (c) 2019, Yann Herklotz +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Template file for different configuration files. +-} + +{-# LANGUAGE QuasiQuotes #-} + +module Verismith.Tool.Template + ( yosysSatConfig + , yosysSimConfig + , xstSynthConfig + , vivadoSynthConfig + , sbyConfig + , icarusTestbench + ) +where + +import Control.Lens ((^..)) +import Data.Text (Text) +import qualified Data.Text as T +import Prelude hiding (FilePath) +import Shelly +import Text.Shakespeare.Text (st) +import Verismith.Tool.Internal +import Verismith.Verilog.AST +import Verismith.Verilog.CodeGen + +rename :: Text -> [Text] -> Text +rename end entries = + T.intercalate "\n" + $ flip mappend end + . mappend "rename " + . doubleName + <$> entries +{-# INLINE rename #-} + +doubleName :: Text -> Text +doubleName n = n <> " " <> n +{-# INLINE doubleName #-} + +outputText :: Synthesiser a => a -> Text +outputText = toTextIgnore . synthOutput + +-- brittany-disable-next-binding +yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text +yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog #{outputText sim1} +#{rename "_1" mis} +read_verilog syn_#{outputText sim2}.v +#{rename "_2" mis} +read_verilog #{top}.v +proc; opt_clean +flatten #{top} +sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{top} +|] + where + mis = src ^.. getSourceId + +-- brittany-disable-next-binding +yosysSimConfig :: Text +yosysSimConfig = [st|read_verilog rtl.v; proc;; +rename mod mod_rtl +|] + +-- brittany-disable-next-binding +xstSynthConfig :: Text -> Text +xstSynthConfig top = [st|run +-ifn #{top}.prj -ofn #{top} -p artix7 -top #{top} +-iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO +-fsm_extract YES -fsm_encoding Auto +-change_error_to_warning "HDLCompiler:226 HDLCompiler:1832" +|] + +-- brittany-disable-next-binding +vivadoSynthConfig :: Text -> Text -> Text +vivadoSynthConfig top outf = [st| +# CRITICAL WARNING: [Synth 8-5821] Potential divide by zero +set_msg_config -id {Synth 8-5821} -new_severity {WARNING} + +read_verilog rtl.v +synth_design -part xc7k70t -top #{top} +write_verilog -force #{outf} +|] + +-- brittany-disable-next-binding +sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> Text +sbyConfig datadir sim1 sim2 (SourceInfo top _) = [st|[options] +multiclock on +mode prove + +[engines] +abc pdr + +[script] +#{readL} +read -formal #{outputText sim1} +read -formal #{outputText sim2} +read -formal top.v +prep -top #{top} + +[files] +#{depList} +#{outputText sim2} +#{outputText sim1} +top.v +|] + where + deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v", "cells_yosys.v"] + depList = + T.intercalate "\n" + $ toTextIgnore + . (datadir </> fromText "data" </>) + . fromText + <$> deps + readL = T.intercalate "\n" $ mappend "read -formal " <$> deps + +icarusTestbench :: (Synthesiser a) => FilePath -> Verilog -> a -> Text +icarusTestbench datadir t synth1 = [st| +`include "#{ddir}/data/cells_cmos.v" +`include "#{ddir}/data/cells_cyclone_v.v" +`include "#{ddir}/data/cells_verific.v" +`include "#{ddir}/data/cells_xilinx_7.v" +`include "#{ddir}/data/cells_yosys.v" +`include "#{toTextIgnore $ synthOutput synth1}" + +#{genSource t} +|] + where + ddir = toTextIgnore datadir diff --git a/src/Verismith/Tool/Vivado.hs b/src/Verismith/Tool/Vivado.hs new file mode 100644 index 0000000..272311e --- /dev/null +++ b/src/Verismith/Tool/Vivado.hs @@ -0,0 +1,71 @@ +{-| +Module : Verismith.Tool.Vivado +Description : Vivado Synthesiser implementation. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Vivado Synthesiser implementation. +-} + +module Verismith.Tool.Vivado + ( Vivado(..) + , defaultVivado + ) +where + +import Control.DeepSeq (NFData, rnf, rwhnf) +import Data.Text (Text, unpack) +import Prelude hiding (FilePath) +import Shelly +import Shelly.Lifted (liftSh) +import Verismith.Tool.Internal +import Verismith.Tool.Template +import Verismith.Verilog.AST +import Verismith.Verilog.CodeGen + +data Vivado = Vivado { vivadoBin :: !(Maybe FilePath) + , vivadoDesc :: {-# UNPACK #-} !Text + , vivadoOutput :: {-# UNPACK #-} !FilePath + } + deriving (Eq) + +instance Tool Vivado where + toText (Vivado _ t _) = t + +instance Show Vivado where + show t = unpack $ toText t + +instance Synthesiser Vivado where + runSynth = runSynthVivado + synthOutput = vivadoOutput + setSynthOutput (Vivado a b _) = Vivado a b + +instance NFData Vivado where + rnf = rwhnf + +defaultVivado :: Vivado +defaultVivado = Vivado Nothing "vivado" "syn_vivado.v" + +runSynthVivado :: Vivado -> SourceInfo -> ResultSh () +runSynthVivado sim (SourceInfo top src) = do + dir <- liftSh pwd + liftSh $ do + writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput + sim + writefile "rtl.v" $ genSource src + run_ + "sed" + [ "s/^module/(* use_dsp48=\"no\" *) (* use_dsp=\"no\" *) module/;" + , "-i" + , "rtl.v" + ] + let exec_ n = execute_ + SynthFail + dir + "vivado" + (maybe (fromText n) (</> fromText n) $ vivadoBin sim) + exec_ "vivado" ["-mode", "batch", "-source", toTextIgnore vivadoTcl] + where vivadoTcl = fromText ("vivado_" <> top) <.> "tcl" diff --git a/src/Verismith/Tool/XST.hs b/src/Verismith/Tool/XST.hs new file mode 100644 index 0000000..c713e0b --- /dev/null +++ b/src/Verismith/Tool/XST.hs @@ -0,0 +1,85 @@ +{-| +Module : Verismith.Tool.XST +Description : XST (ise) simulator implementation. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +XST (ise) simulator implementation. +-} + +{-# LANGUAGE QuasiQuotes #-} + +module Verismith.Tool.XST + ( XST(..) + , defaultXST + ) +where + +import Control.DeepSeq (NFData, rnf, rwhnf) +import Data.Text (Text, unpack) +import Prelude hiding (FilePath) +import Shelly +import Shelly.Lifted (liftSh) +import Text.Shakespeare.Text (st) +import Verismith.Tool.Internal +import Verismith.Tool.Template +import Verismith.Verilog.AST +import Verismith.Verilog.CodeGen + +data XST = XST { xstBin :: !(Maybe FilePath) + , xstDesc :: {-# UNPACK #-} !Text + , xstOutput :: {-# UNPACK #-} !FilePath + } + deriving (Eq) + +instance Tool XST where + toText (XST _ t _) = t + +instance Show XST where + show t = unpack $ toText t + +instance Synthesiser XST where + runSynth = runSynthXST + synthOutput = xstOutput + setSynthOutput (XST a b _) = XST a b + +instance NFData XST where + rnf = rwhnf + +defaultXST :: XST +defaultXST = XST Nothing "xst" "syn_xst.v" + +runSynthXST :: XST -> SourceInfo -> ResultSh () +runSynthXST sim (SourceInfo top src) = do + dir <- liftSh pwd + let exec n = execute_ + SynthFail + dir + "xst" + (maybe (fromText n) (</> fromText n) $ xstBin sim) + liftSh $ do + writefile xstFile $ xstSynthConfig top + writefile prjFile [st|verilog work "rtl.v"|] + writefile "rtl.v" $ genSource src + exec "xst" ["-ifn", toTextIgnore xstFile] + exec + "netgen" + [ "-w" + , "-ofmt" + , "verilog" + , toTextIgnore $ modFile <.> "ngc" + , toTextIgnore $ synthOutput sim + ] + liftSh . noPrint $ run_ + "sed" + [ "-i" + , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;" + , toTextIgnore $ synthOutput sim + ] + where + modFile = fromText top + xstFile = modFile <.> "xst" + prjFile = modFile <.> "prj" diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs new file mode 100644 index 0000000..afbffe9 --- /dev/null +++ b/src/Verismith/Tool/Yosys.hs @@ -0,0 +1,127 @@ +{-| +Module : Verismith.Tool.Yosys +Description : Yosys simulator implementation. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Yosys simulator implementation. +-} + +{-# LANGUAGE QuasiQuotes #-} + +module Verismith.Tool.Yosys + ( Yosys(..) + , defaultYosys + , runEquiv + , runEquivYosys + ) +where + +import Control.DeepSeq (NFData, rnf, rwhnf) +import Control.Lens +import Control.Monad (void) +import Data.Text (Text, unpack) +import Prelude hiding (FilePath) +import Shelly +import Shelly.Lifted (liftSh) +import Text.Shakespeare.Text (st) +import Verismith.Result +import Verismith.Tool.Internal +import Verismith.Tool.Template +import Verismith.Verilog.AST +import Verismith.Verilog.CodeGen +import Verismith.Verilog.Mutate + +data Yosys = Yosys { yosysBin :: !(Maybe FilePath) + , yosysDesc :: {-# UNPACK #-} !Text + , yosysOutput :: {-# UNPACK #-} !FilePath + } + deriving (Eq) + +instance Tool Yosys where + toText (Yosys _ t _) = t + +instance Show Yosys where + show t = unpack $ toText t + +instance Synthesiser Yosys where + runSynth = runSynthYosys + synthOutput = yosysOutput + setSynthOutput (Yosys a b _) = Yosys a b + +instance NFData Yosys where + rnf = rwhnf + +defaultYosys :: Yosys +defaultYosys = Yosys Nothing "yosys" "syn_yosys.v" + +yosysPath :: Yosys -> FilePath +yosysPath sim = maybe (fromText "yosys") (</> fromText "yosys") $ yosysBin sim + +runSynthYosys :: Yosys -> SourceInfo -> ResultSh () +runSynthYosys sim (SourceInfo _ src) = do + dir <- liftSh $ do + dir' <- pwd + writefile inpf $ genSource src + return dir' + execute_ + SynthFail + dir + "yosys" + (yosysPath sim) + [ "-p" + , "read_verilog " <> inp <> "; synth; write_verilog -noattr " <> out + ] + where + inpf = "rtl.v" + inp = toTextIgnore inpf + out = toTextIgnore $ synthOutput sim + +runEquivYosys + :: (Synthesiser a, Synthesiser b) + => Yosys + -> a + -> b + -> SourceInfo + -> ResultSh () +runEquivYosys yosys sim1 sim2 srcInfo = do + liftSh $ do + writefile "top.v" + . genSource + . initMod + . makeTop 2 + $ srcInfo + ^. mainModule + writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo + runSynth sim1 srcInfo + runSynth sim2 srcInfo + liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile] + where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|] + +runEquiv + :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> ResultSh () +runEquiv datadir sim1 sim2 srcInfo = do + dir <- liftSh pwd + liftSh $ do + writefile "top.v" + . genSource + . initMod + . makeTopAssert + $ srcInfo + ^. mainModule + replaceMods (synthOutput sim1) "_1" srcInfo + replaceMods (synthOutput sim2) "_2" srcInfo + writefile "proof.sby" $ sbyConfig datadir sim1 sim2 srcInfo + e <- liftSh $ do + exe dir "symbiyosys" "sby" ["-f", "proof.sby"] + lastExitCode + case e of + 0 -> ResultT . return $ Pass () + 2 -> ResultT . return $ Fail EquivFail + 124 -> ResultT . return $ Fail TimeoutError + _ -> ResultT . return $ Fail EquivError + where + exe dir name e = void . errExit False . logCommand dir name . timeout e diff --git a/src/Verismith/Verilog.hs b/src/Verismith/Verilog.hs new file mode 100644 index 0000000..f3d9e85 --- /dev/null +++ b/src/Verismith/Verilog.hs @@ -0,0 +1,106 @@ +{-| +Module : Verismith.Verilog +Description : Verilog implementation with random generation and mutations. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Verilog implementation with random generation and mutations. +-} + +{-# LANGUAGE QuasiQuotes #-} + +module Verismith.Verilog + ( SourceInfo(..) + , Verilog(..) + , parseVerilog + , GenVerilog(..) + , genSource + -- * Primitives + -- ** Identifier + , Identifier(..) + -- ** Control + , Delay(..) + , Event(..) + -- ** Operators + , BinaryOperator(..) + , UnaryOperator(..) + -- ** Task + , Task(..) + , taskName + , taskExpr + -- ** Left hand side value + , LVal(..) + , regId + , regExprId + , regExpr + , regSizeId + , regSizeRange + , regConc + -- ** Ports + , PortDir(..) + , PortType(..) + , Port(..) + , portType + , portSigned + , portSize + , portName + -- * Expression + , Expr(..) + , ConstExpr(..) + , constToExpr + , exprToConst + , constNum + -- * Assignment + , Assign(..) + , assignReg + , assignDelay + , assignExpr + , ContAssign(..) + , contAssignNetLVal + , contAssignExpr + -- * Statment + , Statement(..) + , statDelay + , statDStat + , statEvent + , statEStat + , statements + , stmntBA + , stmntNBA + , stmntTask + , stmntSysTask + , stmntCondExpr + , stmntCondTrue + , stmntCondFalse + -- * Module + , ModDecl(..) + , modId + , modOutPorts + , modInPorts + , modItems + , ModItem(..) + , modContAssign + , modInstId + , modInstName + , modInstConns + , traverseModItem + , declDir + , declPort + , ModConn(..) + , modConnName + , modExpr + -- * Useful Lenses and Traversals + , getModule + , getSourceId + -- * Quote + , verilog + ) +where + +import Verismith.Verilog.AST +import Verismith.Verilog.CodeGen +import Verismith.Verilog.Parser +import Verismith.Verilog.Quote diff --git a/src/Verismith/Verilog/AST.hs b/src/Verismith/Verilog/AST.hs new file mode 100644 index 0000000..699d87a --- /dev/null +++ b/src/Verismith/Verilog/AST.hs @@ -0,0 +1,583 @@ +{-| +Module : Verismith.Verilog.AST +Description : Definition of the Verilog AST types. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Poratbility : POSIX + +Defines the types to build a Verilog AST. +-} + +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} + +module Verismith.Verilog.AST + ( -- * Top level types + SourceInfo(..) + , infoTop + , infoSrc + , Verilog(..) + -- * Primitives + -- ** Identifier + , Identifier(..) + -- ** Control + , Delay(..) + , Event(..) + -- ** Operators + , BinaryOperator(..) + , UnaryOperator(..) + -- ** Task + , Task(..) + , taskName + , taskExpr + -- ** Left hand side value + , LVal(..) + , regId + , regExprId + , regExpr + , regSizeId + , regSizeRange + , regConc + -- ** Ports + , PortDir(..) + , PortType(..) + , Port(..) + , portType + , portSigned + , portSize + , portName + -- * Expression + , Expr(..) + , ConstExpr(..) + , ConstExprF(..) + , constToExpr + , exprToConst + , Range(..) + , constNum + , constParamId + , constConcat + , constUnOp + , constPrim + , constLhs + , constBinOp + , constRhs + , constCond + , constTrue + , constFalse + , constStr + -- * Assignment + , Assign(..) + , assignReg + , assignDelay + , assignExpr + , ContAssign(..) + , contAssignNetLVal + , contAssignExpr + -- ** Parameters + , Parameter(..) + , paramIdent + , paramValue + , LocalParam(..) + , localParamIdent + , localParamValue + -- * Statment + , Statement(..) + , statDelay + , statDStat + , statEvent + , statEStat + , statements + , stmntBA + , stmntNBA + , stmntTask + , stmntSysTask + , stmntCondExpr + , stmntCondTrue + , stmntCondFalse + , forAssign + , forExpr + , forIncr + , forStmnt + -- * Module + , ModDecl(..) + , modId + , modOutPorts + , modInPorts + , modItems + , modParams + , ModItem(..) + , modContAssign + , modInstId + , modInstName + , modInstConns + , _Initial + , _Always + , paramDecl + , localParamDecl + , traverseModItem + , declDir + , declPort + , declVal + , ModConn(..) + , modConnName + , modExpr + -- * Useful Lenses and Traversals + , aModule + , getModule + , getSourceId + , mainModule + ) +where + +import Control.DeepSeq (NFData) +import Control.Lens hiding ((<|)) +import Data.Data +import Data.Data.Lens +import Data.Functor.Foldable.TH (makeBaseFunctor) +import Data.List.NonEmpty (NonEmpty (..), (<|)) +import Data.String (IsString, fromString) +import Data.Text (Text, pack) +import Data.Traversable (sequenceA) +import GHC.Generics (Generic) +import Verismith.Verilog.BitVec + +-- | 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, +-- as Verilog supports many more characters in Identifiers. +newtype Identifier = Identifier { getIdentifier :: Text } + deriving (Eq, Show, Ord, Data, Generic, NFData) + +instance IsString Identifier where + fromString = Identifier . pack + +instance Semigroup Identifier where + Identifier a <> Identifier b = Identifier $ a <> b + +instance Monoid Identifier where + mempty = Identifier mempty + +-- | Verilog syntax for adding a delay, which is represented as @#num@. +newtype Delay = Delay { _getDelay :: Int } + deriving (Eq, Show, Ord, Data, Generic, NFData) + +instance Num Delay where + Delay a + Delay b = Delay $ a + b + Delay a - Delay b = Delay $ a - b + Delay a * Delay b = Delay $ a * b + negate (Delay a) = Delay $ negate a + abs (Delay a) = Delay $ abs a + signum (Delay a) = Delay $ signum a + fromInteger = Delay . fromInteger + +-- | Verilog syntax for an event, such as @\@x@, which is used for always blocks +data Event = EId {-# UNPACK #-} !Identifier + | EExpr !Expr + | EAll + | EPosEdge {-# UNPACK #-} !Identifier + | ENegEdge {-# UNPACK #-} !Identifier + | EOr !Event !Event + | EComb !Event !Event + deriving (Eq, Show, Ord, Data, Generic, NFData) + +instance Plated Event where + plate = uniplate + +-- | Binary operators that are currently supported in the verilog generation. +data BinaryOperator = 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 -- ^ @>>>@ + deriving (Eq, Show, Ord, Data, Generic, NFData) + +-- | Unary operators that are currently supported by the generator. +data UnaryOperator = UnPlus -- ^ @+@ + | UnMinus -- ^ @-@ + | UnLNot -- ^ @!@ + | UnNot -- ^ @~@ + | UnAnd -- ^ @&@ + | UnNand -- ^ @~&@ + | UnOr -- ^ @|@ + | UnNor -- ^ @~|@ + | UnXor -- ^ @^@ + | UnNxor -- ^ @~^@ + | UnNxorInv -- ^ @^~@ + deriving (Eq, Show, Ord, Data, Generic, NFData) + +-- | Verilog expression, which can either be a primary expression, unary +-- expression, binary operator expression or a conditional expression. +data Expr = Number {-# UNPACK #-} !BitVec + -- ^ Number implementation containing the size and the value itself + | Id {-# UNPACK #-} !Identifier + | VecSelect {-# UNPACK #-} !Identifier !Expr + | RangeSelect {-# UNPACK #-} !Identifier !Range + -- ^ Symbols + | Concat !(NonEmpty Expr) + -- ^ Bit-wise concatenation of expressions represented by braces. + | UnOp !UnaryOperator !Expr + | BinOp !Expr !BinaryOperator !Expr + | Cond !Expr !Expr !Expr + | Appl !Identifier !Expr + | Str {-# UNPACK #-} !Text + deriving (Eq, Show, Ord, Data, Generic, NFData) + +instance Num Expr where + a + b = BinOp a BinPlus b + a - b = BinOp a BinMinus b + a * b = BinOp a BinTimes b + negate = UnOp UnMinus + abs = undefined + signum = undefined + fromInteger = Number . fromInteger + +instance Semigroup Expr where + (Concat a) <> (Concat b) = Concat $ a <> b + (Concat a) <> b = Concat $ a <> (b :| []) + a <> (Concat b) = Concat $ a <| b + a <> b = Concat $ a <| b :| [] + +instance Monoid Expr where + mempty = Number 0 + +instance IsString Expr where + fromString = Str . fromString + +instance Plated Expr where + plate = uniplate + +-- | Constant expression, which are known before simulation at compile time. +data ConstExpr = ConstNum { _constNum :: {-# UNPACK #-} !BitVec } + | ParamId { _constParamId :: {-# UNPACK #-} !Identifier } + | ConstConcat { _constConcat :: !(NonEmpty 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, Generic, NFData) + +constToExpr :: ConstExpr -> Expr +constToExpr (ConstNum a ) = Number a +constToExpr (ParamId a ) = Id a +constToExpr (ConstConcat a ) = Concat $ fmap constToExpr a +constToExpr (ConstUnOp a b ) = UnOp a $ constToExpr b +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 a) = Str a + +exprToConst :: Expr -> ConstExpr +exprToConst (Number a ) = ConstNum a +exprToConst (Id a ) = ParamId a +exprToConst (Concat a ) = ConstConcat $ fmap exprToConst a +exprToConst (UnOp a b ) = ConstUnOp a $ exprToConst b +exprToConst (BinOp a b c) = ConstBinOp (exprToConst a) b $ exprToConst c +exprToConst (Cond a b c) = + ConstCond (exprToConst a) (exprToConst b) $ exprToConst c +exprToConst (Str a) = ConstStr a +exprToConst _ = error "Not a constant expression" + +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 . 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 :| [] + +instance Monoid ConstExpr where + mempty = ConstNum 0 + +instance IsString ConstExpr where + fromString = ConstStr . fromString + +instance Plated ConstExpr where + plate = uniplate + +data Task = Task { _taskName :: {-# UNPACK #-} !Identifier + , _taskExpr :: [Expr] + } deriving (Eq, Show, Ord, Data, Generic, NFData) + +-- | Type that represents the left hand side of an assignment, which can be a +-- concatenation such as in: +-- +-- @ +-- {a, b, c} = 32'h94238; +-- @ +data LVal = RegId { _regId :: {-# UNPACK #-} !Identifier } + | RegExpr { _regExprId :: {-# UNPACK #-} !Identifier + , _regExpr :: !Expr + } + | RegSize { _regSizeId :: {-# UNPACK #-} !Identifier + , _regSizeRange :: {-# UNPACK #-} !Range + } + | RegConcat { _regConc :: [Expr] } + deriving (Eq, Show, Ord, Data, Generic, NFData) + +instance IsString LVal where + fromString = RegId . fromString + +-- | Different port direction that are supported in Verilog. +data PortDir = PortIn -- ^ Input direction for port (@input@). + | PortOut -- ^ Output direction for port (@output@). + | PortInOut -- ^ Inout direction for port (@inout@). + deriving (Eq, Show, Ord, Data, Generic, NFData) + +-- | Currently, only @wire@ and @reg@ are supported, as the other net types are +-- not that common and not a priority. +data PortType = Wire + | Reg + deriving (Eq, Show, Ord, Data, Generic, NFData) + +-- | Range that can be associated with any port or left hand side. Contains the +-- msb and lsb bits as 'ConstExpr'. This means that they can be generated using +-- parameters, which can in turn be changed at synthesis time. +data Range = Range { rangeMSB :: !ConstExpr + , rangeLSB :: !ConstExpr + } + deriving (Eq, Show, Ord, Data, Generic, NFData) + +instance Num Range where + (Range s1 a) + (Range s2 b) = Range (s1 + s2) $ a + b + (Range s1 a) - (Range s2 b) = Range (s1 - s2) . max 0 $ a - b + (Range s1 a) * (Range s2 b) = Range (s1 * s2) $ a * b + negate = undefined + abs = id + signum _ = 1 + fromInteger = flip Range 0 . fromInteger . (-) 1 + +-- | Port declaration. It contains information about the type of the port, the +-- size, and the port name. It used to also contain information about if it was +-- an input or output port. However, this is not always necessary and was more +-- cumbersome than useful, as a lot of ports can be declared without input and +-- output port. +-- +-- 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 #-} !Range + , _portName :: {-# UNPACK #-} !Identifier + } deriving (Eq, Show, Ord, Data, Generic, NFData) + +-- | This is currently a type because direct module declaration should also be +-- added: +-- +-- @ +-- mod a(.y(y1), .x1(x11), .x2(x22)); +-- @ +data ModConn = ModConn { _modExpr :: !Expr } + | ModConnNamed { _modConnName :: {-# UNPACK #-} !Identifier + , _modExpr :: !Expr + } + deriving (Eq, Show, Ord, Data, Generic, NFData) + +data Assign = Assign { _assignReg :: !LVal + , _assignDelay :: !(Maybe Delay) + , _assignExpr :: !Expr + } deriving (Eq, Show, Ord, Data, Generic, NFData) + +data ContAssign = ContAssign { _contAssignNetLVal :: {-# UNPACK #-} !Identifier + , _contAssignExpr :: !Expr + } deriving (Eq, Show, Ord, Data, Generic, NFData) + +-- | Statements in Verilog. +data Statement = TimeCtrl { _statDelay :: {-# UNPACK #-} !Delay + , _statDStat :: Maybe Statement + } -- ^ Time control (@#NUM@) + | EventCtrl { _statEvent :: !Event + , _statEStat :: Maybe Statement + } + | SeqBlock { _statements :: [Statement] } -- ^ Sequential block (@begin ... end@) + | BlockAssign { _stmntBA :: !Assign } -- ^ blocking assignment (@=@) + | NonBlockAssign { _stmntNBA :: !Assign } -- ^ Non blocking assignment (@<=@) + | 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, Generic, NFData) + +instance Plated Statement where + plate = uniplate + +instance Semigroup Statement where + (SeqBlock a) <> (SeqBlock b) = SeqBlock $ a <> b + (SeqBlock a) <> b = SeqBlock $ a <> [b] + a <> (SeqBlock b) = SeqBlock $ a : b + a <> b = SeqBlock [a, b] + +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, Generic, NFData) + +-- | 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, Generic, NFData) + +-- | Module item which is the body of the module expression. +data ModItem = ModCA { _modContAssign :: !ContAssign } + | ModInst { _modInstId :: {-# UNPACK #-} !Identifier + , _modInstName :: {-# UNPACK #-} !Identifier + , _modInstConns :: [ModConn] + } + | Initial !Statement + | Always !Statement + | Decl { _declDir :: !(Maybe PortDir) + , _declPort :: !Port + , _declVal :: Maybe ConstExpr + } + | ParamDecl { _paramDecl :: NonEmpty Parameter } + | LocalParamDecl { _localParamDecl :: NonEmpty LocalParam } + deriving (Eq, Show, Ord, Data, Generic, NFData) + +-- | 'module' module_identifier [list_of_ports] ';' { module_item } 'end_module' +data ModDecl = ModDecl { _modId :: {-# UNPACK #-} !Identifier + , _modOutPorts :: ![Port] + , _modInPorts :: ![Port] + , _modItems :: ![ModItem] + , _modParams :: ![Parameter] + } + deriving (Eq, Show, Ord, Data, Generic, NFData) + +traverseModConn :: (Applicative f) => (Expr -> f Expr) -> ModConn -> f ModConn +traverseModConn f (ModConn e ) = ModConn <$> f e +traverseModConn f (ModConnNamed a e) = ModConnNamed a <$> f e + +traverseModItem :: (Applicative f) => (Expr -> f Expr) -> ModItem -> f ModItem +traverseModItem f (ModCA (ContAssign a e)) = ModCA . ContAssign a <$> f e +traverseModItem f (ModInst a b e) = + ModInst a b <$> sequenceA (traverseModConn f <$> e) +traverseModItem _ e = pure e + +-- | The complete sourcetext for the Verilog module. +newtype Verilog = Verilog { getVerilog :: [ModDecl] } + deriving (Eq, Show, Ord, Data, Generic, NFData) + +instance Semigroup Verilog where + Verilog a <> Verilog b = Verilog $ a <> b + +instance Monoid Verilog where + mempty = Verilog mempty + +data SourceInfo = SourceInfo { _infoTop :: {-# UNPACK #-} !Text + , _infoSrc :: !Verilog + } + deriving (Eq, Show, Ord, Data, Generic, NFData) + +$(makeLenses ''Expr) +$(makeLenses ''ConstExpr) +$(makeLenses ''Task) +$(makeLenses ''LVal) +$(makeLenses ''PortType) +$(makeLenses ''Port) +$(makeLenses ''ModConn) +$(makeLenses ''Assign) +$(makeLenses ''ContAssign) +$(makeLenses ''Statement) +$(makeLenses ''ModItem) +$(makeLenses ''Parameter) +$(makeLenses ''LocalParam) +$(makeLenses ''ModDecl) +$(makeLenses ''SourceInfo) +$(makeWrapped ''Verilog) +$(makeWrapped ''Identifier) +$(makeWrapped ''Delay) +$(makePrisms ''ModItem) + +$(makeBaseFunctor ''Event) +$(makeBaseFunctor ''Expr) +$(makeBaseFunctor ''ConstExpr) + +getModule :: Traversal' Verilog ModDecl +getModule = _Wrapped . traverse +{-# INLINE getModule #-} + +getSourceId :: Traversal' Verilog Text +getSourceId = getModule . modId . _Wrapped +{-# INLINE getSourceId #-} + +-- | May need to change this to Traversal to be safe. For now it will fail when +-- the main has not been properly set with. +aModule :: Identifier -> Lens' SourceInfo ModDecl +aModule t = lens get_ set_ + where + set_ (SourceInfo top main) v = + SourceInfo top (main & getModule %~ update (getIdentifier t) v) + update top v m@(ModDecl (Identifier i) _ _ _ _) | i == top = v + | otherwise = m + get_ (SourceInfo _ main) = + head . filter (f $ getIdentifier t) $ main ^.. getModule + f top (ModDecl (Identifier i) _ _ _ _) = i == top + + +-- | May need to change this to Traversal to be safe. For now it will fail when +-- the main has not been properly set with. +mainModule :: Lens' SourceInfo ModDecl +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 + get_ (SourceInfo top main) = head . filter (f top) $ main ^.. getModule + f top (ModDecl (Identifier i) _ _ _ _) = i == top diff --git a/src/Verismith/Verilog/BitVec.hs b/src/Verismith/Verilog/BitVec.hs new file mode 100644 index 0000000..bc594a3 --- /dev/null +++ b/src/Verismith/Verilog/BitVec.hs @@ -0,0 +1,119 @@ +{-| +Module : Verismith.Verilog.BitVec +Description : Unsigned BitVec implementation. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Unsigned BitVec implementation. +-} + +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} + +module Verismith.Verilog.BitVec + ( BitVecF(..) + , BitVec + , bitVec + , select + ) +where + +import Control.DeepSeq (NFData) +import Data.Bits +import Data.Data +import Data.Ratio +import GHC.Generics (Generic) + +-- | Bit Vector that stores the bits in an arbitrary container together with the +-- size. +data BitVecF a = BitVec { width :: {-# UNPACK #-} !Int + , value :: !a + } + deriving (Show, Eq, Ord, Data, Functor, Foldable, Traversable, Generic, NFData) + +-- | Specialisation of the above with Integer, so that infinitely large bit +-- vectors can be stored. +type BitVec = BitVecF Integer + +instance (Enum a) => Enum (BitVecF a) where + toEnum i = BitVec (width' $ fromIntegral i) $ toEnum i + fromEnum (BitVec _ v) = fromEnum v + +instance (Num a, Bits a) => Num (BitVecF a) where + BitVec w1 v1 + BitVec w2 v2 = bitVec (max w1 w2) (v1 + v2) + BitVec w1 v1 - BitVec w2 v2 = bitVec (max w1 w2) (v1 - v2) + BitVec w1 v1 * BitVec w2 v2 = bitVec (max w1 w2) (v1 * v2) + abs = id + signum (BitVec _ v) = if v == 0 then bitVec 1 0 else bitVec 1 1 + fromInteger i = bitVec (width' i) $ fromInteger i + +instance (Integral a, Bits a) => Real (BitVecF a) where + toRational (BitVec _ n) = fromIntegral n % 1 + +instance (Integral a, Bits a) => Integral (BitVecF a) where + quotRem (BitVec w1 v1) (BitVec w2 v2) = both (BitVec $ max w1 w2) $ quotRem v1 v2 + toInteger (BitVec _ v) = toInteger v + +instance (Num a, Bits a) => Bits (BitVecF a) where + BitVec w1 v1 .&. BitVec w2 v2 = bitVec (max w1 w2) (v1 .&. v2) + BitVec w1 v1 .|. BitVec w2 v2 = bitVec (max w1 w2) (v1 .|. v2) + BitVec w1 v1 `xor` BitVec w2 v2 = bitVec (max w1 w2) (v1 `xor` v2) + complement (BitVec w v) = bitVec w $ complement v + shift (BitVec w v) i = bitVec w $ shift v i + rotate = rotateBitVec + bit i = fromInteger $ bit i + testBit (BitVec _ v) = testBit v + bitSize (BitVec w _) = w + bitSizeMaybe (BitVec w _) = Just w + isSigned _ = False + popCount (BitVec _ v) = popCount v + +instance (Num a, Bits a) => FiniteBits (BitVecF a) where + finiteBitSize (BitVec w _) = w + +instance Bits a => Semigroup (BitVecF a) where + (BitVec w1 v1) <> (BitVec w2 v2) = BitVec (w1 + w2) (shiftL v1 w2 .|. v2) + +instance Bits a => Monoid (BitVecF a) where + mempty = BitVec 0 zeroBits + +-- | BitVecF construction, given width and value. +bitVec :: (Num a, Bits a) => Int -> a -> BitVecF a +bitVec w v = BitVec w' $ v .&. ((2 ^ w') - 1) where w' = max w 0 + +-- | Bit selection. LSB is 0. +select + :: (Integral a, Bits a, Integral b, Bits b) + => BitVecF a + -> (BitVecF b, BitVecF b) + -> BitVecF a +select (BitVec _ v) (msb, lsb) = + bitVec (from $ msb - lsb + 1) . shiftR (fromIntegral v) $ from lsb + where from = fromIntegral . value + +-- | Rotate bits in a 'BitVec'. +rotateBitVec :: (Num a, Bits a) => BitVecF a -> Int -> BitVecF a +rotateBitVec b@(BitVec s _) n | n >= 0 = iterate rotateL1 b !! n + | otherwise = iterate rotateR1 b !! abs n + where + rotateR1 n' = testBits 0 (s - 1) n' .|. shiftR n' 1 + rotateL1 n' = testBits (s - 1) 0 n' .|. shiftL n' 1 + testBits a b' n' = if testBit n' a then bit b' else zeroBits + +width' :: Integer -> Int +width' a | a == 0 = 1 + | otherwise = width'' a + where + width'' a' | a' == 0 = 0 + | a' == -1 = 1 + | otherwise = 1 + width'' (shiftR a' 1) + +both :: (a -> b) -> (a, a) -> (b, b) +both f (a, b) = (f a, f b) diff --git a/src/Verismith/Verilog/CodeGen.hs b/src/Verismith/Verilog/CodeGen.hs new file mode 100644 index 0000000..842394d --- /dev/null +++ b/src/Verismith/Verilog/CodeGen.hs @@ -0,0 +1,341 @@ +{-| +Module : Verismith.Verilog.CodeGen +Description : Code generation for Verilog AST. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +This module generates the code from the Verilog AST defined in +"Verismith.Verilog.AST". +-} + +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} + +module Verismith.Verilog.CodeGen + ( -- * Code Generation + GenVerilog(..) + , Source(..) + , render + ) +where + +import Data.Data (Data) +import Data.List.NonEmpty (NonEmpty (..), toList) +import Data.Text (Text) +import qualified Data.Text as T +import Data.Text.Prettyprint.Doc +import Numeric (showHex) +import Verismith.Internal hiding (comma) +import Verismith.Verilog.AST +import Verismith.Verilog.BitVec + +-- | 'Source' class which determines that source code is able to be generated +-- from the data structure using 'genSource'. This will be stored in 'Text' and +-- can then be processed further. +class Source a where + genSource :: a -> Text + +-- | Map a 'Maybe Statement' to 'Text'. If it is 'Just statement', the generated +-- statements are returned. If it is 'Nothing', then @;\n@ is returned. +defMap :: Maybe Statement -> Doc a +defMap = maybe semi statement + +-- | Convert the 'Verilog' type to 'Text' so that it can be rendered. +verilogSrc :: Verilog -> Doc a +verilogSrc (Verilog modules) = vsep . ("// -*- mode: verilog -*-" :) . punctuate line $ moduleDecl <$> modules + +-- | Generate the 'ModDecl' for a module and convert it to 'Text'. +moduleDecl :: ModDecl -> Doc a +moduleDecl (ModDecl i outP inP items ps) = vsep + [ sep ["module" <+> identifier i, params ps, ports <> semi] + , indent 2 modI + , "endmodule" + ] + where + ports + | null outP && null inP = "" + | otherwise = parens . align . sep . punctuate comma $ modPort <$> outIn + modI = vsep $ moduleItem <$> items + outIn = outP ++ inP + params [] = "" + params (p : pps) = hcat ["#", paramList (p :| pps)] + +-- | Generates a parameter list. Can only be called with a 'NonEmpty' list. +paramList :: NonEmpty Parameter -> Doc a +paramList ps = tupled . toList $ parameter <$> ps + +-- | Generates a localparam list. Can only be called with a 'NonEmpty' list. +localParamList :: NonEmpty LocalParam -> Doc a +localParamList ps = tupled . toList $ localParam <$> ps + +-- | Generates the assignment for a 'Parameter'. +parameter :: Parameter -> Doc a +parameter (Parameter name val) = + hsep ["parameter", identifier name, "=", constExpr val] + +-- | Generates the assignment for a 'LocalParam'. +localParam :: LocalParam -> Doc a +localParam (LocalParam name val) = + hsep ["localparameter", identifier name, "=", constExpr val] + +identifier :: Identifier -> Doc a +identifier (Identifier i) = pretty i + +-- | Conversts 'Port' to 'Text' for the module list, which means it only +-- generates a list of identifiers. +modPort :: Port -> Doc a +modPort (Port _ _ _ i) = identifier i + +-- | Generate the 'Port' description. +port :: Port -> Doc a +port (Port tp sgn r name) = hsep [t, sign, range r, identifier name] + where + t = pType tp + sign = signed sgn + +range :: Range -> Doc a +range (Range msb lsb) = brackets $ hcat [constExpr msb, colon, constExpr lsb] + +signed :: Bool -> Doc a +signed True = "signed" +signed _ = mempty + +-- | Convert the 'PortDir' type to 'Text'. +portDir :: PortDir -> Doc a +portDir PortIn = "input" +portDir PortOut = "output" +portDir PortInOut = "inout" + +-- | Generate a 'ModItem'. +moduleItem :: ModItem -> Doc a +moduleItem (ModCA ca ) = contAssign ca +moduleItem (ModInst i name conn) = hsep + [ identifier i + , identifier name + , parens . hsep $ punctuate comma (mConn <$> conn) + , semi + ] +moduleItem (Initial stat ) = nest 2 $ vsep ["initial", statement stat] +moduleItem (Always stat ) = nest 2 $ vsep ["always", statement stat] +moduleItem (Decl dir p ini) = hsep + [maybe mempty makePort dir, port p, maybe mempty makeIni ini, semi] + where + makePort = portDir + makeIni = ("=" <+>) . constExpr +moduleItem (ParamDecl p) = hcat [paramList p, semi] +moduleItem (LocalParamDecl p) = hcat [localParamList p, semi] + +mConn :: ModConn -> Doc a +mConn (ModConn c ) = expr c +mConn (ModConnNamed n c) = hcat [dot, identifier n, parens $ expr c] + +-- | Generate continuous assignment +contAssign :: ContAssign -> Doc a +contAssign (ContAssign val e) = + hsep ["assign", identifier val, "=", align $ expr e, semi] + +-- | Generate 'Expr' to 'Text'. +expr :: Expr -> Doc a +expr (BinOp eRhs bin eLhs) = parens $ hsep [expr eRhs, binaryOp bin, expr eLhs] +expr (Number b ) = showNum b +expr (Id i ) = identifier i +expr (VecSelect i e ) = hcat [identifier i, brackets $ expr e] +expr (RangeSelect i r ) = hcat [identifier i, range r] +expr (Concat c) = braces . nest 4 . sep . punctuate comma $ toList (expr <$> c) +expr (UnOp u e ) = parens $ hcat [unaryOp u, expr e] +expr (Cond l t f) = + parens . nest 4 $ sep [expr l <+> "?", hsep [expr t, colon, expr f]] +expr (Appl f e) = hcat [identifier f, parens $ expr e] +expr (Str t ) = dquotes $ pretty t + +showNum :: BitVec -> Doc a +showNum (BitVec s n) = parens + $ hcat [minus, pretty $ showT s, "'h", pretty $ T.pack (showHex (abs n) "")] + where + minus | signum n >= 0 = mempty + | otherwise = "-" + +constExpr :: ConstExpr -> Doc a +constExpr (ConstNum b) = showNum b +constExpr (ParamId i) = identifier i +constExpr (ConstConcat c) = + braces . hsep . punctuate comma $ toList (constExpr <$> c) +constExpr (ConstUnOp u e) = parens $ hcat [unaryOp u, constExpr e] +constExpr (ConstBinOp eRhs bin eLhs) = + parens $ hsep [constExpr eRhs, binaryOp bin, constExpr eLhs] +constExpr (ConstCond l t f) = + parens $ hsep [constExpr l, "?", constExpr t, colon, constExpr f] +constExpr (ConstStr t) = dquotes $ pretty t + +-- | Convert 'BinaryOperator' to 'Text'. +binaryOp :: BinaryOperator -> Doc a +binaryOp BinPlus = "+" +binaryOp BinMinus = "-" +binaryOp BinTimes = "*" +binaryOp BinDiv = "/" +binaryOp BinMod = "%" +binaryOp BinEq = "==" +binaryOp BinNEq = "!=" +binaryOp BinCEq = "===" +binaryOp BinCNEq = "!==" +binaryOp BinLAnd = "&&" +binaryOp BinLOr = "||" +binaryOp BinLT = "<" +binaryOp BinLEq = "<=" +binaryOp BinGT = ">" +binaryOp BinGEq = ">=" +binaryOp BinAnd = "&" +binaryOp BinOr = "|" +binaryOp BinXor = "^" +binaryOp BinXNor = "^~" +binaryOp BinXNorInv = "~^" +binaryOp BinPower = "**" +binaryOp BinLSL = "<<" +binaryOp BinLSR = ">>" +binaryOp BinASL = "<<<" +binaryOp BinASR = ">>>" + +-- | Convert 'UnaryOperator' to 'Text'. +unaryOp :: UnaryOperator -> Doc a +unaryOp UnPlus = "+" +unaryOp UnMinus = "-" +unaryOp UnLNot = "!" +unaryOp UnNot = "~" +unaryOp UnAnd = "&" +unaryOp UnNand = "~&" +unaryOp UnOr = "|" +unaryOp UnNor = "~|" +unaryOp UnXor = "^" +unaryOp UnNxor = "~^" +unaryOp UnNxorInv = "^~" + +event :: Event -> Doc a +event a = hcat ["@", parens $ eventRec a] + +-- | Generate verilog code for an 'Event'. +eventRec :: Event -> Doc a +eventRec (EId i) = identifier i +eventRec (EExpr e) = expr e +eventRec EAll = "*" +eventRec (EPosEdge i) = hsep ["posedge", identifier i] +eventRec (ENegEdge i) = hsep ["negedge", identifier i] +eventRec (EOr a b ) = hsep [eventRec a, "or", eventRec b] +eventRec (EComb a b ) = hsep $ punctuate comma [eventRec a, eventRec b] + +-- | Generates verilog code for a 'Delay'. +delay :: Delay -> Doc a +delay (Delay i) = "#" <> pretty i + +-- | Generate the verilog code for an 'LVal'. +lVal :: LVal -> Doc a +lVal (RegId i ) = identifier i +lVal (RegExpr i e) = hsep [identifier i, expr e] +lVal (RegSize i r) = hsep [identifier i, range r] +lVal (RegConcat e) = braces . hsep $ punctuate comma (expr <$> e) + +pType :: PortType -> Doc a +pType Wire = "wire" +pType Reg = "reg" + +genAssign :: Text -> Assign -> Doc a +genAssign op (Assign r d e) = + hsep [lVal r, pretty op, maybe mempty delay d, expr e] + +statement :: Statement -> Doc a +statement (TimeCtrl d stat) = hsep [delay d, defMap stat] +statement (EventCtrl e stat) = hsep [event e, defMap stat] +statement (SeqBlock s) = + vsep ["begin", indent 2 . vsep $ statement <$> s, "end"] +statement (BlockAssign a) = hcat [genAssign "=" a, semi] +statement (NonBlockAssign a) = hcat [genAssign "<=" a, semi] +statement (TaskEnable t) = hcat [task t, semi] +statement (SysTaskEnable t) = hcat ["$", task t, semi] +statement (CondStmnt e t Nothing) = + vsep [hsep ["if", parens $ expr e], indent 2 $ defMap t] +statement (CondStmnt e t f) = vsep + [ hsep ["if", parens $ expr e] + , indent 2 $ defMap t + , "else" + , indent 2 $ defMap f + ] +statement (ForLoop a e incr stmnt) = vsep + [ hsep + [ "for" + , parens . hsep $ punctuate + semi + [genAssign "=" a, expr e, genAssign "=" incr] + ] + , indent 2 $ statement stmnt + ] + +task :: Task -> Doc a +task (Task i e) + | null e = identifier i + | otherwise = hsep + [identifier i, parens . hsep $ punctuate comma (expr <$> e)] + +-- | Render the 'Text' to 'IO'. This is equivalent to 'putStrLn'. +render :: (Source a) => a -> IO () +render = print . genSource + +-- Instances + +instance Source Identifier where + genSource = showT . identifier + +instance Source Task where + genSource = showT . task + +instance Source Statement where + genSource = showT . statement + +instance Source PortType where + genSource = showT . pType + +instance Source ConstExpr where + genSource = showT . constExpr + +instance Source LVal where + genSource = showT . lVal + +instance Source Delay where + genSource = showT . delay + +instance Source Event where + genSource = showT . event + +instance Source UnaryOperator where + genSource = showT . unaryOp + +instance Source Expr where + genSource = showT . expr + +instance Source ContAssign where + genSource = showT . contAssign + +instance Source ModItem where + genSource = showT . moduleItem + +instance Source PortDir where + genSource = showT . portDir + +instance Source Port where + genSource = showT . port + +instance Source ModDecl where + genSource = showT . moduleDecl + +instance Source Verilog where + genSource = showT . verilogSrc + +instance Source SourceInfo where + genSource (SourceInfo _ src) = genSource src + +newtype GenVerilog a = GenVerilog { unGenVerilog :: a } + deriving (Eq, Ord, Data) + +instance (Source a) => Show (GenVerilog a) where + show = T.unpack . genSource . unGenVerilog diff --git a/src/Verismith/Verilog/Eval.hs b/src/Verismith/Verilog/Eval.hs new file mode 100644 index 0000000..cbc2563 --- /dev/null +++ b/src/Verismith/Verilog/Eval.hs @@ -0,0 +1,119 @@ +{-| +Module : Verismith.Verilog.Eval +Description : Evaluation of Verilog expressions and statements. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Evaluation of Verilog expressions and statements. +-} + +module Verismith.Verilog.Eval + ( evaluateConst + , resize + ) +where + +import Data.Bits +import Data.Foldable (fold) +import Data.Functor.Foldable hiding (fold) +import Data.Maybe (listToMaybe) +import Verismith.Verilog.AST +import Verismith.Verilog.BitVec + +type Bindings = [Parameter] + +paramIdent_ :: Parameter -> Identifier +paramIdent_ (Parameter i _) = i + +paramValue_ :: Parameter -> ConstExpr +paramValue_ (Parameter _ v) = v + +applyUnary :: (Num a, FiniteBits a) => UnaryOperator -> a -> a +applyUnary UnPlus a = a +applyUnary UnMinus a = negate a +applyUnary UnLNot a | a == 0 = 0 + | otherwise = 1 +applyUnary UnNot a = complement a +applyUnary UnAnd a | finiteBitSize a == popCount a = 1 + | otherwise = 0 +applyUnary UnNand a | finiteBitSize a == popCount a = 0 + | otherwise = 1 +applyUnary UnOr a | popCount a == 0 = 0 + | otherwise = 1 +applyUnary UnNor a | popCount a == 0 = 1 + | otherwise = 0 +applyUnary UnXor a | popCount a `mod` 2 == 0 = 0 + | otherwise = 1 +applyUnary UnNxor a | popCount a `mod` 2 == 0 = 1 + | otherwise = 0 +applyUnary UnNxorInv a | popCount a `mod` 2 == 0 = 1 + | otherwise = 0 + +compXor :: Bits c => c -> c -> c +compXor a = complement . xor a + +toIntegral :: Num p => (t1 -> t2 -> Bool) -> t1 -> t2 -> p +toIntegral a b c = if a b c then 1 else 0 + +toInt :: (Integral a, Num t1) => (t2 -> t1 -> t3) -> t2 -> a -> t3 +toInt a b c = a b $ fromIntegral c + +applyBinary :: (Integral a, Bits a) => BinaryOperator -> a -> a -> a +applyBinary BinPlus = (+) +applyBinary BinMinus = (-) +applyBinary BinTimes = (*) +applyBinary BinDiv = quot +applyBinary BinMod = rem +applyBinary BinEq = toIntegral (==) +applyBinary BinNEq = toIntegral (/=) +applyBinary BinCEq = toIntegral (==) +applyBinary BinCNEq = toIntegral (/=) +applyBinary BinLAnd = undefined +applyBinary BinLOr = undefined +applyBinary BinLT = toIntegral (<) +applyBinary BinLEq = toIntegral (<=) +applyBinary BinGT = toIntegral (>) +applyBinary BinGEq = toIntegral (>=) +applyBinary BinAnd = (.&.) +applyBinary BinOr = (.|.) +applyBinary BinXor = xor +applyBinary BinXNor = compXor +applyBinary BinXNorInv = compXor +applyBinary BinPower = undefined +applyBinary BinLSL = toInt shiftL +applyBinary BinLSR = toInt shiftR +applyBinary BinASL = toInt shiftL +applyBinary BinASR = toInt shiftR + +-- | Evaluates a 'ConstExpr' using a context of 'Bindings' as input. +evaluateConst :: Bindings -> ConstExprF BitVec -> BitVec +evaluateConst _ (ConstNumF b) = b +evaluateConst p (ParamIdF i) = + cata (evaluateConst p) . maybe 0 paramValue_ . listToMaybe $ filter + ((== i) . paramIdent_) + p +evaluateConst _ (ConstConcatF c ) = fold c +evaluateConst _ (ConstUnOpF unop c ) = applyUnary unop c +evaluateConst _ (ConstBinOpF a binop b) = applyBinary binop a b +evaluateConst _ (ConstCondF a b c) = if a > 0 then b else c +evaluateConst _ (ConstStrF _ ) = 0 + +-- | Apply a function to all the bitvectors. Would be fixed by having a +-- 'Functor' instance for a polymorphic 'ConstExpr'. +applyBitVec :: (BitVec -> BitVec) -> ConstExpr -> ConstExpr +applyBitVec f (ConstNum b ) = ConstNum $ f b +applyBitVec f (ConstConcat c ) = ConstConcat $ fmap (applyBitVec f) c +applyBitVec f (ConstUnOp unop c) = ConstUnOp unop $ applyBitVec f c +applyBitVec f (ConstBinOp a binop b) = + ConstBinOp (applyBitVec f a) binop (applyBitVec f b) +applyBitVec f (ConstCond a b c) = ConstCond (abv a) (abv b) (abv c) + where abv = applyBitVec f +applyBitVec _ a = a + +-- | This probably could be implemented using some recursion scheme in the +-- future. It would also be fixed by having a polymorphic expression type. +resize :: Int -> ConstExpr -> ConstExpr +resize n = applyBitVec (resize' n) where resize' n' (BitVec _ a) = BitVec n' a diff --git a/src/Verismith/Verilog/Internal.hs b/src/Verismith/Verilog/Internal.hs new file mode 100644 index 0000000..b3bf07a --- /dev/null +++ b/src/Verismith/Verilog/Internal.hs @@ -0,0 +1,93 @@ +{-| +Module : Verismith.Verilog.Internal +Description : Defaults and common functions. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Defaults and common functions. +-} + +module Verismith.Verilog.Internal + ( regDecl + , wireDecl + , emptyMod + , setModName + , addModPort + , addModDecl + , testBench + , addTestBench + , defaultPort + , portToExpr + , modName + , yPort + , wire + , reg + ) +where + +import Control.Lens +import Data.Text (Text) +import Verismith.Verilog.AST + +regDecl :: Identifier -> ModItem +regDecl i = Decl Nothing (Port Reg False (Range 1 0) i) Nothing + +wireDecl :: Identifier -> ModItem +wireDecl i = Decl Nothing (Port Wire False (Range 1 0) i) Nothing + +-- | Create an empty module. +emptyMod :: ModDecl +emptyMod = ModDecl "" [] [] [] [] + +-- | Set a module name for a module declaration. +setModName :: Text -> ModDecl -> ModDecl +setModName str = modId .~ Identifier str + +-- | Add a input port to the module declaration. +addModPort :: Port -> ModDecl -> ModDecl +addModPort port = modInPorts %~ (:) port + +addModDecl :: ModDecl -> Verilog -> Verilog +addModDecl desc = _Wrapped %~ (:) desc + +testBench :: ModDecl +testBench = ModDecl + "main" + [] + [] + [ regDecl "a" + , regDecl "b" + , wireDecl "c" + , ModInst "and" + "and_gate" + [ModConn $ Id "c", ModConn $ Id "a", ModConn $ Id "b"] + , Initial $ SeqBlock + [ BlockAssign . Assign (RegId "a") Nothing $ Number 1 + , BlockAssign . Assign (RegId "b") Nothing $ Number 1 + ] + ] + [] + +addTestBench :: Verilog -> Verilog +addTestBench = addModDecl testBench + +defaultPort :: Identifier -> Port +defaultPort = Port Wire False (Range 1 0) + +portToExpr :: Port -> Expr +portToExpr (Port _ _ _ i) = Id i + +modName :: ModDecl -> Text +modName = getIdentifier . view modId + +yPort :: Identifier -> Port +yPort = Port Wire False (Range 90 0) + +wire :: Range -> Identifier -> Port +wire = Port Wire False + +reg :: Range -> Identifier -> Port +reg = Port Reg False diff --git a/src/Verismith/Verilog/Lex.x b/src/Verismith/Verilog/Lex.x new file mode 100644 index 0000000..9892714 --- /dev/null +++ b/src/Verismith/Verilog/Lex.x @@ -0,0 +1,188 @@ +-- -*- haskell -*- +{ +{-# OPTIONS_GHC -w #-} +module Verismith.Verilog.Lex + ( alexScanTokens + ) where + +import Verismith.Verilog.Token + +} + +%wrapper "posn" + +-- Numbers + +$nonZeroDecimalDigit = [1-9] +$decimalDigit = [0-9] +@binaryDigit = [0-1] +@octalDigit = [0-7] +@hexDigit = [0-9a-fA-F] + +@decimalBase = "'" [dD] +@binaryBase = "'" [bB] +@octalBase = "'" [oO] +@hexBase = "'" [hH] + +@binaryValue = @binaryDigit ("_" | @binaryDigit)* +@octalValue = @octalDigit ("_" | @octalDigit)* +@hexValue = @hexDigit ("_" | @hexDigit)* + +@unsignedNumber = $decimalDigit ("_" | $decimalDigit)* + +@size = @unsignedNumber + +@decimalNumber + = @unsignedNumber + | @size? @decimalBase @unsignedNumber + +@binaryNumber = @size? @binaryBase @binaryValue +@octalNumber = @size? @octalBase @octalValue +@hexNumber = @size? @hexBase @hexValue + +-- $exp = [eE] +-- $sign = [\+\-] +-- @realNumber = unsignedNumber "." unsignedNumber | unsignedNumber ( "." unsignedNumber)? exp sign? unsignedNumber +@number = @decimalNumber | @octalNumber | @binaryNumber | @hexNumber + +-- Strings + +@string = \" [^\r\n]* \" + +-- Identifiers + +@escapedIdentifier = "\" ($printable # $white)+ $white +@simpleIdentifier = [a-zA-Z_] [a-zA-Z0-9_\$]* +@systemIdentifier = "$" [a-zA-Z0-9_\$]+ + + +tokens :- + + "always" { tok KWAlways } + "assign" { tok KWAssign } + "begin" { tok KWBegin } + "case" { tok KWCase } + "default" { tok KWDefault } + "else" { tok KWElse } + "end" { tok KWEnd } + "endcase" { tok KWEndcase } + "endmodule" { tok KWEndmodule } + "for" { tok KWFor } + "if" { tok KWIf } + "initial" { tok KWInitial } + "inout" { tok KWInout } + "input" { tok KWInput } + "integer" { tok KWInteger } + "localparam" { tok KWLocalparam } + "module" { tok KWModule } + "negedge" { tok KWNegedge } + "or" { tok KWOr } + "output" { tok KWOutput } + "parameter" { tok KWParameter } + "posedge" { tok KWPosedge } + "reg" { tok KWReg } + "wire" { tok KWWire } + "signed" { tok KWSigned } + + @simpleIdentifier { tok IdSimple } + @escapedIdentifier { tok IdEscaped } + @systemIdentifier { tok IdSystem } + + @number { tok LitNumber } + @string { tok LitString } + + "(" { tok SymParenL } + ")" { tok SymParenR } + "[" { tok SymBrackL } + "]" { tok SymBrackR } + "{" { tok SymBraceL } + "}" { tok SymBraceR } + "~" { tok SymTildy } + "!" { tok SymBang } + "@" { tok SymAt } + "#" { tok SymPound } + "%" { tok SymPercent } + "^" { tok SymHat } + "&" { tok SymAmp } + "|" { tok SymBar } + "*" { tok SymAster } + "." { tok SymDot } + "," { tok SymComma } + ":" { tok SymColon } + ";" { tok SymSemi } + "=" { tok SymEq } + "<" { tok SymLt } + ">" { tok SymGt } + "+" { tok SymPlus } + "-" { tok SymDash } + "?" { tok SymQuestion } + "/" { tok SymSlash } + "$" { tok SymDollar } + "'" { tok SymSQuote } + + "~&" { tok SymTildyAmp } + "~|" { tok SymTildyBar } + "~^" { tok SymTildyHat } + "^~" { tok SymHatTildy } + "==" { tok SymEqEq } + "!=" { tok SymBangEq } + "&&" { tok SymAmpAmp } + "||" { tok SymBarBar } + "**" { tok SymAsterAster } + "<=" { tok SymLtEq } + ">=" { tok SymGtEq } + ">>" { tok SymGtGt } + "<<" { tok SymLtLt } + "++" { tok SymPlusPlus } + "--" { tok SymDashDash } + "+=" { tok SymPlusEq } + "-=" { tok SymDashEq } + "*=" { tok SymAsterEq } + "/=" { tok SymSlashEq } + "%=" { tok SymPercentEq } + "&=" { tok SymAmpEq } + "|=" { tok SymBarEq } + "^=" { tok SymHatEq } + "+:" { tok SymPlusColon } + "-:" { tok SymDashColon } + "::" { tok SymColonColon } + ".*" { tok SymDotAster } + "->" { tok SymDashGt } + ":=" { tok SymColonEq } + ":/" { tok SymColonSlash } + "##" { tok SymPoundPound } + "[*" { tok SymBrackLAster } + "[=" { tok SymBrackLEq } + "=>" { tok SymEqGt } + "@*" { tok SymAtAster } + "(*" { tok SymParenLAster } + "*)" { tok SymAsterParenR } + "*>" { tok SymAsterGt } + + "===" { tok SymEqEqEq } + "!==" { tok SymBangEqEq } + "=?=" { tok SymEqQuestionEq } + "!?=" { tok SymBangQuestionEq } + ">>>" { tok SymGtGtGt } + "<<<" { tok SymLtLtLt } + "<<=" { tok SymLtLtEq } + ">>=" { tok SymGtGtEq } + "|->" { tok SymBarDashGt } + "|=>" { tok SymBarEqGt } + "[->" { tok SymBrackLDashGt } + "@@(" { tok SymAtAtParenL } + "(*)" { tok SymParenLAsterParenR } + "->>" { tok SymDashGtGt } + "&&&" { tok SymAmpAmpAmp } + + "<<<=" { tok SymLtLtLtEq } + ">>>=" { tok SymGtGtGtEq } + + $white ; + + . { tok Unknown } + +{ +tok :: TokenName -> AlexPosn -> String -> Token +tok t (AlexPn _ l c) s = Token t s $ Position "" l c +} diff --git a/src/Verismith/Verilog/Mutate.hs b/src/Verismith/Verilog/Mutate.hs new file mode 100644 index 0000000..44a502a --- /dev/null +++ b/src/Verismith/Verilog/Mutate.hs @@ -0,0 +1,397 @@ +{-| +Module : Verismith.Verilog.Mutate +Description : Functions to mutate the Verilog AST. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Functions to mutate the Verilog AST from "Verismith.Verilog.AST" to generate more +random patterns, such as nesting wires instead of creating new ones. +-} + +{-# LANGUAGE FlexibleInstances #-} + +module Verismith.Verilog.Mutate + ( Mutate(..) + , inPort + , findAssign + , idTrans + , replace + , nestId + , nestSource + , nestUpTo + , allVars + , instantiateMod + , instantiateMod_ + , instantiateModSpec_ + , filterChar + , initMod + , makeIdFrom + , makeTop + , makeTopAssert + , simplify + , removeId + , combineAssigns + , combineAssigns_ + , declareMod + ) +where + +import Control.Lens +import Data.Foldable (fold) +import Data.Maybe (catMaybes, fromMaybe) +import Data.Text (Text) +import qualified Data.Text as T +import Verismith.Circuit.Internal +import Verismith.Internal +import Verismith.Verilog.AST +import Verismith.Verilog.BitVec +import Verismith.Verilog.CodeGen +import Verismith.Verilog.Internal + +class Mutate a where + mutExpr :: (Expr -> Expr) -> a -> a + +instance Mutate Identifier where + mutExpr _ = id + +instance Mutate Delay where + mutExpr _ = id + +instance Mutate Event where + mutExpr f (EExpr e) = EExpr $ f e + mutExpr _ a = a + +instance Mutate BinaryOperator where + mutExpr _ = id + +instance Mutate UnaryOperator where + mutExpr _ = id + +instance Mutate Expr where + mutExpr f = f + +instance Mutate ConstExpr where + mutExpr _ = id + +instance Mutate Task where + mutExpr f (Task i e) = Task i $ fmap f e + +instance Mutate LVal where + mutExpr f (RegExpr a e) = RegExpr a $ f e + mutExpr _ a = a + +instance Mutate PortDir where + mutExpr _ = id + +instance Mutate PortType where + mutExpr _ = id + +instance Mutate Range where + mutExpr _ = id + +instance Mutate Port where + mutExpr _ = id + +instance Mutate ModConn where + mutExpr f (ModConn e) = ModConn $ f e + mutExpr f (ModConnNamed a e) = ModConnNamed a $ f e + +instance Mutate Assign where + mutExpr f (Assign a b c) = Assign a b $ f c + +instance Mutate ContAssign where + mutExpr f (ContAssign a e) = ContAssign a $ f e + +instance Mutate Statement where + mutExpr f (TimeCtrl d s) = TimeCtrl d $ mutExpr f <$> s + mutExpr f (EventCtrl e s) = EventCtrl e $ mutExpr f <$> s + mutExpr f (SeqBlock s) = SeqBlock $ mutExpr f <$> s + mutExpr f (BlockAssign a) = BlockAssign $ mutExpr f a + mutExpr f (NonBlockAssign a) = NonBlockAssign $ mutExpr f a + mutExpr f (TaskEnable a) = TaskEnable $ mutExpr f a + mutExpr f (SysTaskEnable a) = SysTaskEnable $ mutExpr f a + mutExpr f (CondStmnt a b c) = CondStmnt (f a) (mutExpr f <$> b) $ mutExpr f <$> c + mutExpr f (ForLoop a1 e a2 s) = ForLoop (mutExpr f a1) (f e) (mutExpr f a2) $ mutExpr f s + +instance Mutate Parameter where + mutExpr _ = id + +instance Mutate LocalParam where + mutExpr _ = id + +instance Mutate ModItem where + mutExpr f (ModCA (ContAssign a e)) = ModCA . ContAssign a $ f e + mutExpr f (ModInst a b conns) = ModInst a b $ mutExpr f conns + mutExpr f (Initial s) = Initial $ mutExpr f s + mutExpr f (Always s) = Always $ mutExpr f s + mutExpr _ d@Decl{} = d + mutExpr _ p@ParamDecl{} = p + mutExpr _ l@LocalParamDecl{} = l + +instance Mutate ModDecl where + mutExpr f (ModDecl a b c d e) = ModDecl (mutExpr f a) (mutExpr f b) (mutExpr f c) (mutExpr f d) (mutExpr f e) + +instance Mutate Verilog where + mutExpr f (Verilog a) = Verilog $ mutExpr f a + +instance Mutate SourceInfo where + mutExpr f (SourceInfo a b) = SourceInfo a $ mutExpr f b + +instance Mutate a => Mutate [a] where + mutExpr f a = mutExpr f <$> a + +instance Mutate a => Mutate (Maybe a) where + mutExpr f a = mutExpr f <$> a + +instance Mutate a => Mutate (GenVerilog a) where + mutExpr f (GenVerilog a) = GenVerilog $ mutExpr f a + +-- | Return if the 'Identifier' is in a 'ModDecl'. +inPort :: Identifier -> ModDecl -> Bool +inPort i m = inInput + where + inInput = + any (\a -> a ^. portName == i) $ m ^. modInPorts ++ m ^. modOutPorts + +-- | Find the last assignment of a specific wire/reg to an expression, and +-- returns that expression. +findAssign :: Identifier -> [ModItem] -> Maybe Expr +findAssign i items = safe last . catMaybes $ isAssign <$> items + where + isAssign (ModCA (ContAssign val expr)) | val == i = Just expr + | otherwise = Nothing + isAssign _ = Nothing + +-- | Transforms an expression by replacing an Identifier with an +-- expression. This is used inside 'transformOf' and 'traverseExpr' to replace +-- the 'Identifier' recursively. +idTrans :: Identifier -> Expr -> Expr -> Expr +idTrans i expr (Id id') | id' == i = expr + | otherwise = Id id' +idTrans _ _ e = e + +-- | Replaces the identifier recursively in an expression. +replace :: Identifier -> Expr -> Expr -> Expr +replace = (transform .) . idTrans + +-- | Nest expressions for a specific 'Identifier'. If the 'Identifier' is not +-- found, the AST is not changed. +-- +-- This could be improved by instead of only using the last assignment to the +-- wire that one finds, to use the assignment to the wire before the current +-- expression. This would require a different approach though. +nestId :: Identifier -> ModDecl -> ModDecl +nestId i m + | not $ inPort i m + = let expr = fromMaybe def . findAssign i $ m ^. modItems + in m & get %~ replace i expr + | otherwise + = m + where + get = modItems . traverse . modContAssign . contAssignExpr + def = Id i + +-- | Replaces an identifier by a expression in all the module declaration. +nestSource :: Identifier -> Verilog -> Verilog +nestSource i src = src & getModule %~ nestId i + +-- | Nest variables in the format @w[0-9]*@ up to a certain number. +nestUpTo :: Int -> Verilog -> Verilog +nestUpTo i src = + foldl (flip nestSource) src $ Identifier . fromNode <$> [1 .. i] + +allVars :: ModDecl -> [Identifier] +allVars m = + (m ^.. modOutPorts . traverse . portName) + <> (m ^.. modInPorts . traverse . portName) + +-- $setup +-- >>> import Verismith.Verilog.CodeGen +-- >>> let m = (ModDecl (Identifier "m") [Port Wire False 5 (Identifier "y")] [Port Wire False 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 +-- @reg@. +-- +-- >>> render $ instantiateMod m main +-- module main; +-- wire [(3'h4):(1'h0)] y; +-- reg [(3'h4):(1'h0)] x; +-- m m1(y, x); +-- endmodule +-- <BLANKLINE> +-- <BLANKLINE> +instantiateMod :: ModDecl -> ModDecl -> ModDecl +instantiateMod m main = main & modItems %~ ((out ++ regIn ++ [inst]) ++) + where + 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) + $ main + ^.. modItems + . traverse + . modInstId + conns = ModConn . Id <$> allVars m + +-- | Instantiate without adding wire declarations. It also does not count the +-- current instantiations of the same module. +-- +-- >>> GenVerilog $ instantiateMod_ m +-- m m(y, x); +-- <BLANKLINE> +instantiateMod_ :: ModDecl -> ModItem +instantiateMod_ m = ModInst (m ^. modId) (m ^. modId) conns + where + conns = + ModConn + . Id + <$> (m ^.. modOutPorts . traverse . portName) + ++ (m ^.. modInPorts . traverse . portName) + +-- | Instantiate without adding wire declarations. It also does not count the +-- current instantiations of the same module. +-- +-- >>> GenVerilog $ instantiateModSpec_ "_" m +-- m m(.y(y), .x(x)); +-- <BLANKLINE> +instantiateModSpec_ :: Text -> ModDecl -> ModItem +instantiateModSpec_ outChar m = ModInst (m ^. modId) (m ^. modId) conns + where + conns = zipWith ModConnNamed ids (Id <$> instIds) + ids = filterChar outChar (name modOutPorts) <> name modInPorts + instIds = name modOutPorts <> name modInPorts + name v = m ^.. v . traverse . portName + +filterChar :: Text -> [Identifier] -> [Identifier] +filterChar t ids = + ids & traverse . _Wrapped %~ (\x -> fromMaybe x . safe head $ T.splitOn t x) + +-- | Initialise all the inputs and outputs to a module. +-- +-- >>> GenVerilog $ initMod m +-- module m(y, x); +-- output wire [(3'h4):(1'h0)] y; +-- input wire [(3'h4):(1'h0)] x; +-- endmodule +-- <BLANKLINE> +-- <BLANKLINE> +initMod :: ModDecl -> ModDecl +initMod m = m & modItems %~ ((out ++ inp) ++) + where + 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. +makeIdFrom :: (Show a) => a -> Identifier -> Identifier +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 [] + where + ys = yPort . flip makeIdFrom "y" <$> [1 .. i] + modIt = instantiateModSpec_ "_" . modN <$> [1 .. i] + modN n = + m & modId %~ makeIdFrom n & modOutPorts .~ [yPort (makeIdFrom n "y")] + +-- | Make a top module with an assert that requires @y_1@ to always be equal to +-- @y_2@, which can then be proven using a formal verification tool. +makeTopAssert :: ModDecl -> ModDecl +makeTopAssert = (modItems %~ (++ [assert])) . makeTop 2 + where + assert = Always . EventCtrl e . Just $ SeqBlock + [TaskEnable $ Task "assert" [BinOp (Id "y_1") BinEq (Id "y_2")]] + e = EPosEdge "clk" + +-- | 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 %~ (fmap decl ports ++)) + where + decl p@(Port Reg _ _ _) = Decl Nothing p (Just 0) + decl 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 +-- no more changes were made to the expression. +-- +-- >>> GenVerilog . simplify $ (Id "x") + 0 +-- x +-- +-- >>> GenVerilog . simplify $ (Id "y") + (Id "x") +-- (y + x) +simplify :: Expr -> Expr +simplify (BinOp (Number (BitVec _ 1)) BinAnd e) = e +simplify (BinOp e BinAnd (Number (BitVec _ 1))) = e +simplify (BinOp (Number (BitVec _ 0)) BinAnd _) = Number 0 +simplify (BinOp _ BinAnd (Number (BitVec _ 0))) = Number 0 +simplify (BinOp e BinPlus (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinPlus e) = e +simplify (BinOp e BinMinus (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinMinus e) = e +simplify (BinOp e BinTimes (Number (BitVec _ 1))) = e +simplify (BinOp (Number (BitVec _ 1)) BinTimes e) = e +simplify (BinOp _ BinTimes (Number (BitVec _ 0))) = Number 0 +simplify (BinOp (Number (BitVec _ 0)) BinTimes _) = Number 0 +simplify (BinOp e BinOr (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinOr e) = e +simplify (BinOp e BinLSL (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinLSL e) = e +simplify (BinOp e BinLSR (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinLSR e) = e +simplify (BinOp e BinASL (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinASL e) = e +simplify (BinOp e BinASR (Number (BitVec _ 0))) = e +simplify (BinOp (Number (BitVec _ 0)) BinASR e) = e +simplify (UnOp UnPlus e) = e +simplify e = e + +-- | Remove all 'Identifier' that do not appeare in the input list from an +-- 'Expr'. The identifier will be replaced by @1'b0@, which can then later be +-- simplified further. +-- +-- >>> GenVerilog . removeId ["x"] $ Id "x" + Id "y" +-- (x + (1'h0)) +removeId :: [Identifier] -> Expr -> Expr +removeId i = transform trans + where + trans (Id ident) | ident `notElem` i = Number 0 + | otherwise = Id ident + trans e = e + +combineAssigns :: Port -> [ModItem] -> [ModItem] +combineAssigns p a = + a + <> [ ModCA + . ContAssign (p ^. portName) + . UnOp UnXor + . fold + $ Id + <$> assigns + ] + where assigns = a ^.. traverse . modContAssign . contAssignNetLVal + +combineAssigns_ :: Bool -> Port -> [Port] -> ModItem +combineAssigns_ comb p ps = + ModCA + . ContAssign (p ^. portName) + . (if comb then UnOp UnXor else id) + . fold + $ Id + <$> ps + ^.. traverse + . portName diff --git a/src/Verismith/Verilog/Parser.hs b/src/Verismith/Verilog/Parser.hs new file mode 100644 index 0000000..a6eaf24 --- /dev/null +++ b/src/Verismith/Verilog/Parser.hs @@ -0,0 +1,511 @@ +{-| +Module : Verismith.Verilog.Parser +Description : Minimal Verilog parser to reconstruct the AST. +Copyright : (c) 2019, Yann Herklotz +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Minimal Verilog parser to reconstruct the AST. This parser does not support the +whole Verilog syntax, as the AST does not support it either. +-} + +module Verismith.Verilog.Parser + ( -- * Parser + parseVerilog + , parseVerilogFile + , parseSourceInfoFile + -- ** Internal parsers + , parseEvent + , parseStatement + , parseModItem + , parseModDecl + , Parser + ) +where + +import Control.Lens +import Control.Monad (void) +import Data.Bifunctor (bimap) +import Data.Bits +import Data.Functor (($>)) +import Data.Functor.Identity (Identity) +import Data.List (isInfixOf, isPrefixOf, null) +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Text.IO as T +import Text.Parsec hiding (satisfy) +import Text.Parsec.Expr +import Verismith.Internal +import Verismith.Verilog.AST +import Verismith.Verilog.BitVec +import Verismith.Verilog.Internal +import Verismith.Verilog.Lex +import Verismith.Verilog.Preprocess +import Verismith.Verilog.Token + +type Parser = Parsec [Token] () + +type ParseOperator = Operator [Token] () Identity + +data Decimal = Decimal Int Integer + +instance Num Decimal where + (Decimal sa na) + (Decimal sb nb) = Decimal (max sa sb) (na + nb) + (Decimal sa na) - (Decimal sb nb) = Decimal (max sa sb) (na - nb) + (Decimal sa na) * (Decimal sb nb) = Decimal (max sa sb) (na * nb) + negate (Decimal s n) = Decimal s $ negate n + abs (Decimal s n) = Decimal s $ abs n + signum (Decimal s n) = Decimal s $ signum n + fromInteger = Decimal 32 . fromInteger + +-- | This parser succeeds whenever the given predicate returns true when called +-- with parsed `Token`. Same as 'Text.Parsec.Char.satisfy'. +satisfy :: (Token -> Bool) -> Parser TokenName +satisfy f = tokenPrim show nextPos tokeq + where + tokeq :: Token -> Maybe TokenName + tokeq t@(Token t' _ _) = if f t then Just t' else Nothing + +satisfy' :: (Token -> Maybe a) -> Parser a +satisfy' = tokenPrim show nextPos + +nextPos :: SourcePos -> Token -> [Token] -> SourcePos +nextPos pos _ (Token _ _ (Position _ l c) : _) = + setSourceColumn (setSourceLine pos l) c +nextPos pos _ [] = pos + +-- | Parses given `TokenName`. +tok :: TokenName -> Parser TokenName +tok t = satisfy (\(Token t' _ _) -> t' == t) <?> show t + +-- | Parse without returning the `TokenName`. +tok' :: TokenName -> Parser () +tok' p = void $ tok p + +parens :: Parser a -> Parser a +parens = between (tok SymParenL) (tok SymParenR) + +brackets :: Parser a -> Parser a +brackets = between (tok SymBrackL) (tok SymBrackR) + +braces :: Parser a -> Parser a +braces = between (tok SymBraceL) (tok SymBraceR) + +sBinOp :: BinaryOperator -> Expr -> Expr -> Expr +sBinOp = sOp BinOp where sOp f b a = f a b + +parseExpr' :: Parser Expr +parseExpr' = buildExpressionParser parseTable parseTerm <?> "expr" + +decToExpr :: Decimal -> Expr +decToExpr (Decimal s n) = Number $ bitVec s n + +-- | Parse a Number depending on if it is in a hex or decimal form. Octal and +-- binary are not supported yet. +parseNum :: Parser Expr +parseNum = decToExpr <$> number + +parseVar :: Parser Expr +parseVar = Id <$> identifier + +parseVecSelect :: Parser Expr +parseVecSelect = do + i <- identifier + expr <- brackets parseExpr + return $ VecSelect i expr + +parseRangeSelect :: Parser Expr +parseRangeSelect = do + i <- identifier + range <- parseRange + return $ RangeSelect i range + +systemFunc :: Parser String +systemFunc = satisfy' matchId + where + matchId (Token IdSystem s _) = Just s + matchId _ = Nothing + +parseFun :: Parser Expr +parseFun = do + f <- systemFunc + expr <- parens parseExpr + return $ Appl (Identifier $ T.pack f) expr + +parserNonEmpty :: [a] -> Parser (NonEmpty a) +parserNonEmpty (a : b) = return $ a :| b +parserNonEmpty [] = fail "Concatenation cannot be empty." + +parseTerm :: Parser Expr +parseTerm = + parens parseExpr + <|> (Concat <$> (braces (commaSep parseExpr) >>= parserNonEmpty)) + <|> parseFun + <|> parseNum + <|> try parseVecSelect + <|> try parseRangeSelect + <|> parseVar + <?> "simple expr" + +-- | Parses the ternary conditional operator. It will behave in a right +-- associative way. +parseCond :: Expr -> Parser Expr +parseCond e = do + tok' SymQuestion + expr <- parseExpr + tok' SymColon + Cond e expr <$> parseExpr + +parseExpr :: Parser Expr +parseExpr = do + e <- parseExpr' + option e . try $ parseCond e + +parseConstExpr :: Parser ConstExpr +parseConstExpr = fmap exprToConst parseExpr + +-- | Table of binary and unary operators that encode the right precedence for +-- each. +parseTable :: [[ParseOperator Expr]] +parseTable = + [ [prefix SymBang (UnOp UnLNot), prefix SymTildy (UnOp UnNot)] + , [ prefix SymAmp (UnOp UnAnd) + , prefix SymBar (UnOp UnOr) + , prefix SymTildyAmp (UnOp UnNand) + , prefix SymTildyBar (UnOp UnNor) + , prefix SymHat (UnOp UnXor) + , prefix SymTildyHat (UnOp UnNxor) + , prefix SymHatTildy (UnOp UnNxorInv) + ] + , [prefix SymPlus (UnOp UnPlus), prefix SymDash (UnOp UnMinus)] + , [binary SymAsterAster (sBinOp BinPower) AssocRight] + , [ binary SymAster (sBinOp BinTimes) AssocLeft + , binary SymSlash (sBinOp BinDiv) AssocLeft + , binary SymPercent (sBinOp BinMod) AssocLeft + ] + , [ binary SymPlus (sBinOp BinPlus) AssocLeft + , binary SymDash (sBinOp BinPlus) AssocLeft + ] + , [ binary SymLtLt (sBinOp BinLSL) AssocLeft + , binary SymGtGt (sBinOp BinLSR) AssocLeft + ] + , [ binary SymLtLtLt (sBinOp BinASL) AssocLeft + , binary SymGtGtGt (sBinOp BinASR) AssocLeft + ] + , [ binary SymLt (sBinOp BinLT) AssocNone + , binary SymGt (sBinOp BinGT) AssocNone + , binary SymLtEq (sBinOp BinLEq) AssocNone + , binary SymGtEq (sBinOp BinLEq) AssocNone + ] + , [ binary SymEqEq (sBinOp BinEq) AssocNone + , binary SymBangEq (sBinOp BinNEq) AssocNone + ] + , [ binary SymEqEqEq (sBinOp BinEq) AssocNone + , binary SymBangEqEq (sBinOp BinNEq) AssocNone + ] + , [binary SymAmp (sBinOp BinAnd) AssocLeft] + , [ binary SymHat (sBinOp BinXor) AssocLeft + , binary SymHatTildy (sBinOp BinXNor) AssocLeft + , binary SymTildyHat (sBinOp BinXNorInv) AssocLeft + ] + , [binary SymBar (sBinOp BinOr) AssocLeft] + , [binary SymAmpAmp (sBinOp BinLAnd) AssocLeft] + , [binary SymBarBar (sBinOp BinLOr) AssocLeft] + ] + +binary :: TokenName -> (a -> a -> a) -> Assoc -> ParseOperator a +binary name fun = Infix ((tok name <?> "binary") >> return fun) + +prefix :: TokenName -> (a -> a) -> ParseOperator a +prefix name fun = Prefix ((tok name <?> "prefix") >> return fun) + +commaSep :: Parser a -> Parser [a] +commaSep = flip sepBy $ tok SymComma + +parseContAssign :: Parser ContAssign +parseContAssign = do + var <- tok KWAssign *> identifier + expr <- tok SymEq *> parseExpr + tok' SymSemi + return $ ContAssign var expr + +numLit :: Parser String +numLit = satisfy' matchId + where + matchId (Token LitNumber s _) = Just s + matchId _ = Nothing + +number :: Parser Decimal +number = number' <$> numLit + where + number' :: String -> Decimal + number' a | all (`elem` ['0' .. '9']) a = fromInteger $ read a + | head a == '\'' = fromInteger $ f a + | "'" `isInfixOf` a = Decimal (read w) (f b) + | otherwise = error $ "Invalid number format: " ++ a + where + w = takeWhile (/= '\'') a + b = dropWhile (/= '\'') a + f a' + | "'d" `isPrefixOf` a' = read $ drop 2 a' + | "'h" `isPrefixOf` a' = read $ "0x" ++ drop 2 a' + | "'b" `isPrefixOf` a' = foldl + (\n b' -> shiftL n 1 .|. (if b' == '1' then 1 else 0)) + 0 + (drop 2 a') + | otherwise = error $ "Invalid number format: " ++ a' + +-- toInteger' :: Decimal -> Integer +-- toInteger' (Decimal _ n) = n + +toInt' :: Decimal -> Int +toInt' (Decimal _ n) = fromInteger n + +-- | Parse a range and return the total size. As it is inclusive, 1 has to be +-- added to the difference. +parseRange :: Parser Range +parseRange = do + rangeH <- tok SymBrackL *> parseConstExpr + rangeL <- tok SymColon *> parseConstExpr + tok' SymBrackR + return $ Range rangeH rangeL + +strId :: Parser String +strId = satisfy' matchId + where + matchId (Token IdSimple s _) = Just s + matchId (Token IdEscaped s _) = Just s + matchId _ = Nothing + +identifier :: Parser Identifier +identifier = Identifier . T.pack <$> strId + +parseNetDecl :: Maybe PortDir -> Parser ModItem +parseNetDecl pd = do + t <- option Wire type_ + sign <- option False (tok KWSigned $> True) + range <- option 1 parseRange + name <- identifier + i <- option Nothing (fmap Just (tok' SymEq *> parseConstExpr)) + tok' SymSemi + return $ Decl pd (Port t sign range name) i + where type_ = tok KWWire $> Wire <|> tok KWReg $> Reg + +parsePortDir :: Parser PortDir +parsePortDir = + tok KWOutput + $> PortOut + <|> tok KWInput + $> PortIn + <|> tok KWInout + $> PortInOut + +parseDecl :: Parser ModItem +parseDecl = (Just <$> parsePortDir >>= parseNetDecl) <|> parseNetDecl Nothing + +parseConditional :: Parser Statement +parseConditional = do + expr <- tok' KWIf *> parens parseExpr + true <- maybeEmptyStatement + false <- option Nothing (tok' KWElse *> maybeEmptyStatement) + return $ CondStmnt expr true false + +parseLVal :: Parser LVal +parseLVal = fmap RegConcat (braces $ commaSep parseExpr) <|> ident + where + ident = do + i <- identifier + (try (ex i) <|> try (sz i) <|> return (RegId i)) + ex i = do + e <- tok' SymBrackL *> parseExpr + tok' SymBrackR + return $ RegExpr i e + sz i = RegSize i <$> parseRange + +parseDelay :: Parser Delay +parseDelay = Delay . toInt' <$> (tok' SymPound *> number) + +parseAssign :: TokenName -> Parser Assign +parseAssign t = do + lval <- parseLVal + tok' t + delay <- option Nothing (fmap Just parseDelay) + expr <- parseExpr + return $ Assign lval delay expr + +parseLoop :: Parser Statement +parseLoop = do + a <- tok' KWFor *> tok' SymParenL *> parseAssign SymEq + expr <- tok' SymSemi *> parseExpr + incr <- tok' SymSemi *> parseAssign SymEq + tok' SymParenR + statement <- parseStatement + return $ ForLoop a expr incr statement + +eventList :: TokenName -> Parser [Event] +eventList t = do + l <- sepBy parseEvent' (tok t) + if null l then fail "Could not parse list" else return l + +parseEvent :: Parser Event +parseEvent = + tok' SymAtAster + $> EAll + <|> try (tok' SymAt *> tok' SymParenLAsterParenR $> EAll) + <|> try + ( tok' SymAt + *> tok' SymParenL + *> tok' SymAster + *> tok' SymParenR + $> EAll + ) + <|> try (tok' SymAt *> parens parseEvent') + <|> try (tok' SymAt *> parens (foldr1 EOr <$> eventList KWOr)) + <|> try (tok' SymAt *> parens (foldr1 EComb <$> eventList SymComma)) + +parseEvent' :: Parser Event +parseEvent' = + try (tok' KWPosedge *> fmap EPosEdge identifier) + <|> try (tok' KWNegedge *> fmap ENegEdge identifier) + <|> try (fmap EId identifier) + <|> try (fmap EExpr parseExpr) + +parseEventCtrl :: Parser Statement +parseEventCtrl = do + event <- parseEvent + statement <- option Nothing maybeEmptyStatement + return $ EventCtrl event statement + +parseDelayCtrl :: Parser Statement +parseDelayCtrl = do + delay <- parseDelay + statement <- option Nothing maybeEmptyStatement + return $ TimeCtrl delay statement + +parseBlocking :: Parser Statement +parseBlocking = do + a <- parseAssign SymEq + tok' SymSemi + return $ BlockAssign a + +parseNonBlocking :: Parser Statement +parseNonBlocking = do + a <- parseAssign SymLtEq + tok' SymSemi + return $ NonBlockAssign a + +parseSeq :: Parser Statement +parseSeq = do + seq' <- tok' KWBegin *> many parseStatement + tok' KWEnd + return $ SeqBlock seq' + +parseStatement :: Parser Statement +parseStatement = + parseSeq + <|> parseConditional + <|> parseLoop + <|> parseEventCtrl + <|> parseDelayCtrl + <|> try parseBlocking + <|> parseNonBlocking + +maybeEmptyStatement :: Parser (Maybe Statement) +maybeEmptyStatement = + (tok' SymSemi >> return Nothing) <|> (Just <$> parseStatement) + +parseAlways :: Parser ModItem +parseAlways = tok' KWAlways *> (Always <$> parseStatement) + +parseInitial :: Parser ModItem +parseInitial = tok' KWInitial *> (Initial <$> parseStatement) + +namedModConn :: Parser ModConn +namedModConn = do + target <- tok' SymDot *> identifier + expr <- parens parseExpr + return $ ModConnNamed target expr + +parseModConn :: Parser ModConn +parseModConn = try (fmap ModConn parseExpr) <|> namedModConn + +parseModInst :: Parser ModItem +parseModInst = do + m <- identifier + name <- identifier + modconns <- parens (commaSep parseModConn) + tok' SymSemi + return $ ModInst m name modconns + +parseModItem :: Parser ModItem +parseModItem = + try (ModCA <$> parseContAssign) + <|> try parseDecl + <|> parseAlways + <|> parseInitial + <|> parseModInst + +parseModList :: Parser [Identifier] +parseModList = list <|> return [] where list = parens $ commaSep identifier + +filterDecl :: PortDir -> ModItem -> Bool +filterDecl p (Decl (Just p') _ _) = p == p' +filterDecl _ _ = False + +modPorts :: PortDir -> [ModItem] -> [Port] +modPorts p mis = filter (filterDecl p) mis ^.. traverse . declPort + +parseParam :: Parser Parameter +parseParam = do + i <- tok' KWParameter *> identifier + expr <- tok' SymEq *> parseConstExpr + return $ Parameter i expr + +parseParams :: Parser [Parameter] +parseParams = tok' SymPound *> parens (commaSep parseParam) + +parseModDecl :: Parser ModDecl +parseModDecl = do + name <- tok KWModule *> identifier + paramList <- option [] $ try parseParams + _ <- fmap defaultPort <$> parseModList + tok' SymSemi + modItem <- option [] . try $ many1 parseModItem + tok' KWEndmodule + return $ ModDecl name + (modPorts PortOut modItem) + (modPorts PortIn modItem) + modItem + paramList + +-- | Parses a 'String' into 'Verilog' by skipping any beginning whitespace +-- and then parsing multiple Verilog source. +parseVerilogSrc :: Parser Verilog +parseVerilogSrc = Verilog <$> many parseModDecl + +-- | Parse a 'String' containing verilog code. The parser currently only supports +-- the subset of Verilog that is being generated randomly. +parseVerilog + :: Text -- ^ Name of parsed object. + -> Text -- ^ Content to be parsed. + -> Either Text Verilog -- ^ Returns 'String' with error + -- message if parse fails. +parseVerilog s = + bimap showT id + . parse parseVerilogSrc (T.unpack s) + . alexScanTokens + . preprocess [] (T.unpack s) + . T.unpack + +parseVerilogFile :: Text -> IO Verilog +parseVerilogFile file = do + src <- T.readFile $ T.unpack file + case parseVerilog file src of + Left s -> error $ T.unpack s + Right r -> return r + +parseSourceInfoFile :: Text -> Text -> IO SourceInfo +parseSourceInfoFile top = fmap (SourceInfo top) . parseVerilogFile diff --git a/src/Verismith/Verilog/Preprocess.hs b/src/Verismith/Verilog/Preprocess.hs new file mode 100644 index 0000000..91356f1 --- /dev/null +++ b/src/Verismith/Verilog/Preprocess.hs @@ -0,0 +1,111 @@ +{-| +Module : Verismith.Verilog.Preprocess +Description : Simple preprocessor for `define and comments. +Copyright : (c) 2011-2015 Tom Hawkins, 2019 Yann Herklotz +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Simple preprocessor for `define and comments. + +The code is from https://github.com/tomahawkins/verilog. + +Edits to the original code are warning fixes and formatting changes. +-} + +module Verismith.Verilog.Preprocess + ( uncomment + , preprocess + ) +where + +-- | 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 + uncomment' a = case a of + "" -> "" + '/' : '/' : rest -> " " ++ removeEOL rest + '/' : '*' : rest -> " " ++ remove rest + '(' : '*' : rest -> " " ++ remove rest + '"' : rest -> '"' : ignoreString rest + b : rest -> b : uncomment' rest + + removeEOL a = case a of + "" -> "" + '\n' : rest -> '\n' : uncomment' rest + '\t' : rest -> '\t' : removeEOL rest + _ : rest -> ' ' : removeEOL rest + + remove a = case a of + "" -> error $ "File ended without closing comment (*/): " ++ file + '"' : rest -> removeString rest + '\n' : rest -> '\n' : remove rest + '\t' : rest -> '\t' : remove rest + '*' : '/' : rest -> " " ++ uncomment' rest + '*' : ')' : rest -> " " ++ uncomment' rest + _ : rest -> " " ++ remove rest + + removeString a = case a of + "" -> error $ "File ended without closing string: " ++ file + '"' : rest -> " " ++ remove rest + '\\' : '"' : rest -> " " ++ removeString rest + '\n' : rest -> '\n' : removeString rest + '\t' : rest -> '\t' : removeString rest + _ : rest -> ' ' : removeString rest + + ignoreString a = case a of + "" -> error $ "File ended without closing string: " ++ file + '"' : rest -> '"' : uncomment' rest + '\\' : '"' : rest -> "\\\"" ++ ignoreString rest + b : rest -> b : ignoreString rest + +-- | A simple `define preprocessor. +preprocess :: [(String, String)] -> FilePath -> String -> String +preprocess env file content = unlines $ pp True [] env $ lines $ uncomment + file + content + where + pp :: Bool -> [Bool] -> [(String, String)] -> [String] -> [String] + pp _ _ _ [] = [] + pp on stack env_ (a : rest) = case words a of + "`define" : name : value -> + "" + : pp + on + stack + (if on + then (name, ppLine env_ $ unwords value) : env_ + else env_ + ) + rest + "`ifdef" : name : _ -> + "" : pp (on && elem name (map fst env_)) (on : stack) env_ rest + "`ifndef" : name : _ -> + "" : pp (on && notElem name (map fst env_)) (on : stack) env_ rest + "`else" : _ + | not $ null stack + -> "" : pp (head stack && not on) stack env_ rest + | otherwise + -> error $ "`else without associated `ifdef/`ifndef: " ++ file + "`endif" : _ + | not $ null stack + -> "" : pp (head stack) (tail stack) env_ rest + | otherwise + -> error $ "`endif without associated `ifdef/`ifndef: " ++ file + _ -> (if on then ppLine env_ a else "") : pp on stack env_ rest + +ppLine :: [(String, String)] -> String -> String +ppLine _ "" = "" +ppLine env ('`' : a) = case lookup name env of + Just value -> value ++ ppLine env rest + Nothing -> error $ "Undefined macro: `" ++ name ++ " Env: " ++ show env + where + name = takeWhile + (flip elem $ ['A' .. 'Z'] ++ ['a' .. 'z'] ++ ['0' .. '9'] ++ ['_']) + a + rest = drop (length name) a +ppLine env (a : b) = a : ppLine env b diff --git a/src/Verismith/Verilog/Quote.hs b/src/Verismith/Verilog/Quote.hs new file mode 100644 index 0000000..879b8fd --- /dev/null +++ b/src/Verismith/Verilog/Quote.hs @@ -0,0 +1,50 @@ +{-| +Module : Verismith.Verilog.Quote +Description : QuasiQuotation for verilog code in Haskell. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +QuasiQuotation for verilog code in Haskell. +-} + +{-# LANGUAGE TemplateHaskell #-} + +module Verismith.Verilog.Quote + ( verilog + ) +where + +import Data.Data +import qualified Data.Text as T +import qualified Language.Haskell.TH as TH +import Language.Haskell.TH.Quote +import Language.Haskell.TH.Syntax +import Verismith.Verilog.Parser + +liftDataWithText :: Data a => a -> Q Exp +liftDataWithText = dataToExpQ $ fmap liftText . cast + +liftText :: T.Text -> Q Exp +liftText txt = AppE (VarE 'T.pack) <$> lift (T.unpack txt) + +-- | Quasiquoter for verilog, so that verilog can be written inline and be +-- parsed to an AST at compile time. +verilog :: QuasiQuoter +verilog = QuasiQuoter + { quoteExp = quoteVerilog + , quotePat = undefined + , quoteType = undefined + , quoteDec = undefined + } + +quoteVerilog :: String -> TH.Q TH.Exp +quoteVerilog s = do + loc <- TH.location + let pos = T.pack $ TH.loc_filename loc + v <- case parseVerilog pos (T.pack s) of + Right e -> return e + Left e -> fail $ show e + liftDataWithText v diff --git a/src/Verismith/Verilog/Token.hs b/src/Verismith/Verilog/Token.hs new file mode 100644 index 0000000..b303e18 --- /dev/null +++ b/src/Verismith/Verilog/Token.hs @@ -0,0 +1,350 @@ +{-| +Module : Verismith.Verilog.Token +Description : Tokens for Verilog parsing. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX + +Tokens for Verilog parsing. +-} + +module Verismith.Verilog.Token + ( Token(..) + , TokenName(..) + , Position(..) + , tokenString + ) +where + +import Text.Printf + +tokenString :: Token -> String +tokenString (Token _ s _) = s + +data Position = Position String Int Int deriving Eq + +instance Show Position where + show (Position f l c) = printf "%s:%d:%d" f l c + +data Token = Token TokenName String Position deriving (Show, Eq) + +data TokenName + = KWAlias + | KWAlways + | KWAlwaysComb + | KWAlwaysFf + | KWAlwaysLatch + | KWAnd + | KWAssert + | KWAssign + | KWAssume + | KWAutomatic + | KWBefore + | KWBegin + | KWBind + | KWBins + | KWBinsof + | KWBit + | KWBreak + | KWBuf + | KWBufif0 + | KWBufif1 + | KWByte + | KWCase + | KWCasex + | KWCasez + | KWCell + | KWChandle + | KWClass + | KWClocking + | KWCmos + | KWConfig + | KWConst + | KWConstraint + | KWContext + | KWContinue + | KWCover + | KWCovergroup + | KWCoverpoint + | KWCross + | KWDeassign + | KWDefault + | KWDefparam + | KWDesign + | KWDisable + | KWDist + | KWDo + | KWEdge + | KWElse + | KWEnd + | KWEndcase + | KWEndclass + | KWEndclocking + | KWEndconfig + | KWEndfunction + | KWEndgenerate + | KWEndgroup + | KWEndinterface + | KWEndmodule + | KWEndpackage + | KWEndprimitive + | KWEndprogram + | KWEndproperty + | KWEndspecify + | KWEndsequence + | KWEndtable + | KWEndtask + | KWEnum + | KWEvent + | KWExpect + | KWExport + | KWExtends + | KWExtern + | KWFinal + | KWFirstMatch + | KWFor + | KWForce + | KWForeach + | KWForever + | KWFork + | KWForkjoin + | KWFunction + | KWFunctionPrototype + | KWGenerate + | KWGenvar + | KWHighz0 + | KWHighz1 + | KWIf + | KWIff + | KWIfnone + | KWIgnoreBins + | KWIllegalBins + | KWImport + | KWIncdir + | KWInclude + | KWInitial + | KWInout + | KWInput + | KWInside + | KWInstance + | KWInt + | KWInteger + | KWInterface + | KWIntersect + | KWJoin + | KWJoinAny + | KWJoinNone + | KWLarge + | KWLiblist + | KWLibrary + | KWLocal + | KWLocalparam + | KWLogic + | KWLongint + | KWMacromodule + | KWMatches + | KWMedium + | KWModport + | KWModule + | KWNand + | KWNegedge + | KWNew + | KWNmos + | KWNor + | KWNoshowcancelled + | KWNot + | KWNotif0 + | KWNotif1 + | KWNull + | KWOption + | KWOr + | KWOutput + | KWPackage + | KWPacked + | KWParameter + | KWPathpulseDollar + | KWPmos + | KWPosedge + | KWPrimitive + | KWPriority + | KWProgram + | KWProperty + | KWProtected + | KWPull0 + | KWPull1 + | KWPulldown + | KWPullup + | KWPulsestyleOnevent + | KWPulsestyleOndetect + | KWPure + | KWRand + | KWRandc + | KWRandcase + | KWRandsequence + | KWRcmos + | KWReal + | KWRealtime + | KWRef + | KWReg + | KWRelease + | KWRepeat + | KWReturn + | KWRnmos + | KWRpmos + | KWRtran + | KWRtranif0 + | KWRtranif1 + | KWScalared + | KWSequence + | KWShortint + | KWShortreal + | KWShowcancelled + | KWSigned + | KWSmall + | KWSolve + | KWSpecify + | KWSpecparam + | KWStatic + | KWStrength0 + | KWStrength1 + | KWString + | KWStrong0 + | KWStrong1 + | KWStruct + | KWSuper + | KWSupply0 + | KWSupply1 + | KWTable + | KWTagged + | KWTask + | KWThis + | KWThroughout + | KWTime + | KWTimeprecision + | KWTimeunit + | KWTran + | KWTranif0 + | KWTranif1 + | KWTri + | KWTri0 + | KWTri1 + | KWTriand + | KWTrior + | KWTrireg + | KWType + | KWTypedef + | KWTypeOption + | KWUnion + | KWUnique + | KWUnsigned + | KWUse + | KWVar + | KWVectored + | KWVirtual + | KWVoid + | KWWait + | KWWaitOrder + | KWWand + | KWWeak0 + | KWWeak1 + | KWWhile + | KWWildcard + | KWWire + | KWWith + | KWWithin + | KWWor + | KWXnor + | KWXor + | IdSimple + | IdEscaped + | IdSystem + | LitNumberUnsigned + | LitNumber + | LitString + | SymParenL + | SymParenR + | SymBrackL + | SymBrackR + | SymBraceL + | SymBraceR + | SymTildy + | SymBang + | SymAt + | SymPound + | SymPercent + | SymHat + | SymAmp + | SymBar + | SymAster + | SymDot + | SymComma + | SymColon + | SymSemi + | SymEq + | SymLt + | SymGt + | SymPlus + | SymDash + | SymQuestion + | SymSlash + | SymDollar + | SymSQuote + | SymTildyAmp + | SymTildyBar + | SymTildyHat + | SymHatTildy + | SymEqEq + | SymBangEq + | SymAmpAmp + | SymBarBar + | SymAsterAster + | SymLtEq + | SymGtEq + | SymGtGt + | SymLtLt + | SymPlusPlus + | SymDashDash + | SymPlusEq + | SymDashEq + | SymAsterEq + | SymSlashEq + | SymPercentEq + | SymAmpEq + | SymBarEq + | SymHatEq + | SymPlusColon + | SymDashColon + | SymColonColon + | SymDotAster + | SymDashGt + | SymColonEq + | SymColonSlash + | SymPoundPound + | SymBrackLAster + | SymBrackLEq + | SymEqGt + | SymAtAster + | SymParenLAster + | SymAsterParenR + | SymAsterGt + | SymEqEqEq + | SymBangEqEq + | SymEqQuestionEq + | SymBangQuestionEq + | SymGtGtGt + | SymLtLtLt + | SymLtLtEq + | SymGtGtEq + | SymBarDashGt + | SymBarEqGt + | SymBrackLDashGt + | SymAtAtParenL + | SymParenLAsterParenR + | SymDashGtGt + | SymAmpAmpAmp + | SymLtLtLtEq + | SymGtGtGtEq + | Unknown + deriving (Show, Eq) |