diff options
Diffstat (limited to 'src/VeriFuzz')
33 files changed, 0 insertions, 7075 deletions
diff --git a/src/VeriFuzz/Circuit.hs b/src/VeriFuzz/Circuit.hs deleted file mode 100644 index 6083c8e..0000000 --- a/src/VeriFuzz/Circuit.hs +++ /dev/null @@ -1,45 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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 VeriFuzz.Circuit.Base -import VeriFuzz.Circuit.Gen -import VeriFuzz.Circuit.Random -import VeriFuzz.Verilog.AST -import VeriFuzz.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/VeriFuzz/Circuit/Base.hs b/src/VeriFuzz/Circuit/Base.hs deleted file mode 100644 index 0bcdf39..0000000 --- a/src/VeriFuzz/Circuit/Base.hs +++ /dev/null @@ -1,44 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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/VeriFuzz/Circuit/Gen.hs b/src/VeriFuzz/Circuit/Gen.hs deleted file mode 100644 index eb7cb97..0000000 --- a/src/VeriFuzz/Circuit/Gen.hs +++ /dev/null @@ -1,79 +0,0 @@ -{-| -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 VeriFuzz.Circuit.Gen - ( generateAST - ) -where - -import Data.Graph.Inductive (LNode, Node) -import qualified Data.Graph.Inductive as G -import Data.Maybe (catMaybes) -import VeriFuzz.Circuit.Base -import VeriFuzz.Circuit.Internal -import VeriFuzz.Verilog.AST -import VeriFuzz.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/VeriFuzz/Circuit/Internal.hs b/src/VeriFuzz/Circuit/Internal.hs deleted file mode 100644 index 17e1586..0000000 --- a/src/VeriFuzz/Circuit/Internal.hs +++ /dev/null @@ -1,55 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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/VeriFuzz/Circuit/Random.hs b/src/VeriFuzz/Circuit/Random.hs deleted file mode 100644 index fdb5253..0000000 --- a/src/VeriFuzz/Circuit/Random.hs +++ /dev/null @@ -1,67 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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 VeriFuzz.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/VeriFuzz/Config.hs b/src/VeriFuzz/Config.hs deleted file mode 100644 index c986888..0000000 --- a/src/VeriFuzz/Config.hs +++ /dev/null @@ -1,511 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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_verifuzz (version) -import Shelly (toTextIgnore) -import Toml (TomlCodec, (.=)) -import qualified Toml -import VeriFuzz.Sim.Quartus -import VeriFuzz.Sim.Vivado -import VeriFuzz.Sim.XST -import VeriFuzz.Sim.Yosys - --- $conf --- --- VeriFuzz 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 @verifuzz 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 = - "VeriFuzz " - <> showVersion version - <> " (" - <> $(gitCommitDate) - <> " " - <> $(gitHash) - <> ")" diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs deleted file mode 100644 index df0ee2d..0000000 --- a/src/VeriFuzz/Fuzz.hs +++ /dev/null @@ -1,466 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.Fuzz - ( Fuzz - , 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.Trans.Class (lift) -import Control.Monad.Trans.Control (MonadBaseControl) -import Control.Monad.Trans.Maybe (runMaybeT) -import Control.Monad.Trans.Reader hiding (local) -import Control.Monad.Trans.State.Strict -import qualified Crypto.Random.DRBG as C -import Data.ByteString (ByteString) -import Data.List (nubBy, sort) -import Data.Maybe (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 VeriFuzz.Config -import VeriFuzz.Internal -import VeriFuzz.Reduce -import VeriFuzz.Report -import VeriFuzz.Result -import VeriFuzz.Sim.Icarus -import VeriFuzz.Sim.Internal -import VeriFuzz.Sim.Yosys -import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.CodeGen - -data FuzzEnv = FuzzEnv { getSynthesisers :: ![SynthTool] - , getSimulators :: ![SimTool] - , yosysInstance :: {-# UNPACK #-} !Yosys - } - deriving (Eq, Show) - -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 => Config -> Yosys -> (Config -> Fuzz Sh a) -> m a -runFuzz conf yos m = shelly $ runFuzz' conf yos m - -runFuzz' :: Monad m => Config -> Yosys -> (Config -> Fuzz m b) -> m b -runFuzz' conf yos m = runReaderT - (evalStateT (m conf) (FuzzState [] [] [])) - (FuzzEnv - ( force - $ defaultIdentitySynth - : (descriptionToSynth <$> conf ^. configSynthesisers) - ) - (force $ descriptionToSim <$> conf ^. configSimulators) - yos - ) - -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 $ do - mkdir_p f - cp_r "data" $ f </> fromText "data" - -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 - synth <- passedSynthesis --- let synthComb = --- nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth - let synthComb = - nubBy tupEq - . filter (uncurry (/=)) - $ (,) defaultIdentitySynth - <$> synth - resTimes <- liftSh $ mapM (uncurry equiv) synthComb - fuzzSynthResults .= toSynthResult synthComb resTimes - liftSh $ inspect resTimes - where - tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') - equiv 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 a b src - where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b - -simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m () -simulation src = do - synth <- passEquiv - vals <- liftIO $ generateByteString 20 - ident <- liftSh $ equiv vals defaultIdentitySynth - resTimes <- liftSh $ mapM (equiv vals) $ conv <$> synth - liftSh - . inspect - $ (\(_, r) -> bimap show (T.unpack . T.take 10 . showBS) r) - <$> (ident : resTimes) - where - conv (SynthResult _ a _ _) = a - equiv 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 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 - fails <- failEquivWithIdentity - synthFails <- failedSynthesis - _ <- liftSh $ mapM red fails - _ <- liftSh $ mapM redSynth synthFails - return () - where - red (SynthResult a b _ _) = do - make dir - pop dir $ do - s <- reduceSynth 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 -> Config -> Fuzz m FuzzReport -fuzz gen conf = do - (seed', src) <- generateSample genMethod - let size = length . lines . T.unpack $ genSource src - liftSh - . writefile "config.toml" - . encodeConfig - $ conf - & configProperty - . propSeed - ?~ seed' - (tsynth, _) <- titleRun "Synthesis" $ synthesis src - (tequiv, _) <- titleRun "Equivalence Check" $ equivalence src - (_ , _) <- titleRun "Simulation" $ simulation src - fails <- failEquivWithIdentity - synthFails <- failedSynthesis - redResult <- - whenMaybe (not $ null fails && null synthFails) - . 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) - liftSh . writefile "index.html" $ printResultReport (bname currdir) report - return report - where - seed = conf ^. configProperty . propSeed - bname = T.pack . takeBaseName . T.unpack . toTextIgnore - genMethod = 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 - 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 - -fuzzInDir - :: MonadFuzz m => FilePath -> Gen SourceInfo -> Config -> Fuzz m FuzzReport -fuzzInDir fp src conf = do - make fp - res <- pop fp $ fuzz src conf - relativeFuzzReport res - -fuzzMultiple - :: MonadFuzz m - => Int - -> Maybe FilePath - -> Gen SourceInfo - -> Config - -> Fuzz m [FuzzReport] -fuzzMultiple n fp src conf = do - x <- case fp 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 .. n] fuzzDir' - else (: []) <$> fuzzDir' (1 :: Int) - liftSh . writefile (fromText "index" <.> "html") $ printSummary - "Fuzz Summary" - results - return results - where - fuzzDir' n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src conf - seed = conf ^. configProperty . propSeed - -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 - runIdentity - . runMaybeT - . Hog.runTree - $ Hog.runGenT 30 seed gen - of - Nothing -> loop (n - 1) - Just x -> return (seed, Hog.nodeValue x) - in loop (100 :: Int) - diff --git a/src/VeriFuzz/Generate.hs b/src/VeriFuzz/Generate.hs deleted file mode 100644 index d081504..0000000 --- a/src/VeriFuzz/Generate.hs +++ /dev/null @@ -1,649 +0,0 @@ -{-| -Module : VeriFuzz.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 TemplateHaskell #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} - -module VeriFuzz.Generate - ( -- * Generation methods - procedural - , proceduralIO - , proceduralSrc - , proceduralSrcIO - , randomMod - -- ** Generate Functions - , gen - , 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.Trans.Class (lift) -import Control.Monad.Trans.Reader hiding (local) -import Control.Monad.Trans.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) -import qualified Hedgehog.Gen as Hog -import qualified Hedgehog.Range as Hog -import VeriFuzz.Config -import VeriFuzz.Internal -import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.BitVec -import VeriFuzz.Verilog.Eval -import VeriFuzz.Verilog.Internal -import VeriFuzz.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 = StateT Context (ReaderT Config Gen) - -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 :: Identifier -> Gen 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 :: [Port] -> (Expr -> ContAssign) -> Gen 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 :: [Port] -> [Port] -> [Gen ModItem] -randomOrdAssigns inp ids = snd $ foldr generate (inp, []) ids - where - generate cid (i, o) = (cid : i, random i (ContAssign (_portName cid)) : o) - -randomMod :: Int -> Int -> Gen 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 = lift $ asks probability - --- | Lifts a 'Gen' into the 'StateGen' monad. -gen :: Gen a -> StateGen a -gen = lift . lift - --- | Generates a random large number, which can also be negative. -largeNum :: Gen 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 :: Gen Int -wireSize = Hog.int $ Hog.linear 2 100 - --- | Generates a random range by using the 'wireSize' and 0 as the lower bound. -range :: Gen Range -range = Range <$> fmap fromIntegral wireSize <*> pure 0 - --- | Generate a random bit vector using 'largeNum'. -genBitVec :: Gen 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 :: Gen BinaryOperator -binOp = Hog.element - [ BinPlus - , BinMinus - , BinTimes - -- , BinDiv - -- , BinMod - , BinEq - , BinNEq - -- , BinCEq - -- , BinCNEq - , BinLAnd - , BinLOr - , BinLT - , BinLEq - , BinGT - , BinGEq - , BinAnd - , BinOr - , BinXor - , BinXNor - , BinXNorInv - -- , BinPower - , BinLSL - , BinLSR - , BinASL - , BinASR - ] - --- | Generate a random 'UnaryOperator'. -unOp :: Gen 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 :: [Parameter] -> ProbExpr -> Hog.Size -> Gen 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 :: ProbExpr -> [(Int, Gen 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 :: ProbExpr -> (Hog.Size -> Gen Expr) -> [(Int, Gen 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 :: [Parameter] -> [Port] -> Gen 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 :: ProbExpr -> [Parameter] -> [Port] -> Hog.Size -> Gen 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 <- gen $ 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 <- gen $ Port pt <$> Hog.bool <*> range <*> pure ident - contextVariables %= (fromPort p :) - return p - --- | Generates an expression from variables that are currently in scope. -scopedExpr :: StateGen Expr -scopedExpr = do - context <- get - prob <- askProbability - gen - . Hog.sized - . exprWithContext (_probExpr prob) (_contextParameters context) - $ _portsFromContext 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 (_portsFromContext context) - 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) - , ModInst i ident <$> Hog.shuffle - (zipWith ModConnNamed (_portName <$> outP <> clkPort <> inpFixed) (toE $ outs <> clkPort <> ins)) - ] - 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 <- lift 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 <- lift 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 - gen . Hog.sized $ constExprWithContext (context ^. contextParameters) - (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 <- lift ask - let (newPorts, local) = partition (`identElem` portList) $ _portsFromContext 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 $ runReaderT - (runStateT (moduleDef (Just $ Identifier top)) context) - config - return . Verilog $ mainMod : st ^. contextModules - 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/VeriFuzz/Internal.hs b/src/VeriFuzz/Internal.hs deleted file mode 100644 index c7105fc..0000000 --- a/src/VeriFuzz/Internal.hs +++ /dev/null @@ -1,49 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs deleted file mode 100644 index 61b7bba..0000000 --- a/src/VeriFuzz/Reduce.hs +++ /dev/null @@ -1,609 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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 VeriFuzz.Internal -import VeriFuzz.Result -import VeriFuzz.Sim -import VeriFuzz.Sim.Internal -import VeriFuzz.Verilog -import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.Mutate -import VeriFuzz.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) - => a - -> b - -> SourceInfo - -> m SourceInfo -reduceSynth a b = reduce synth - where - synth src' = liftSh $ do - r <- runResultT $ do - runSynth a src' - runSynth b src' - runEquiv 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/VeriFuzz/Report.hs b/src/VeriFuzz/Report.hs deleted file mode 100644 index 56fd062..0000000 --- a/src/VeriFuzz/Report.hs +++ /dev/null @@ -1,398 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -{-| -Module : VeriFuzz.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 VeriFuzz.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 VeriFuzz.Config -import VeriFuzz.Internal -import VeriFuzz.Result -import VeriFuzz.Sim -import VeriFuzz.Sim.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] - , _simResults :: ![SimResult] - , _synthStatus :: ![SynthStatus] - , _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 </> fromText "index" <.> "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/VeriFuzz/Result.hs b/src/VeriFuzz/Result.hs deleted file mode 100644 index 61b1452..0000000 --- a/src/VeriFuzz/Result.hs +++ /dev/null @@ -1,137 +0,0 @@ -{-| -Module : VeriFuzz.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 "VeriFuzz". --} - -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE UndecidableInstances #-} - -module VeriFuzz.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/VeriFuzz/Sim.hs b/src/VeriFuzz/Sim.hs deleted file mode 100644 index 92d1bc4..0000000 --- a/src/VeriFuzz/Sim.hs +++ /dev/null @@ -1,51 +0,0 @@ -{-| -Module : VeriFuzz.Sim -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 VeriFuzz.Sim - ( - -- * 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 VeriFuzz.Sim.Icarus -import VeriFuzz.Sim.Identity -import VeriFuzz.Sim.Internal -import VeriFuzz.Sim.Quartus -import VeriFuzz.Sim.Vivado -import VeriFuzz.Sim.XST -import VeriFuzz.Sim.Yosys diff --git a/src/VeriFuzz/Sim/Icarus.hs b/src/VeriFuzz/Sim/Icarus.hs deleted file mode 100644 index 9041d14..0000000 --- a/src/VeriFuzz/Sim/Icarus.hs +++ /dev/null @@ -1,188 +0,0 @@ -{-| -Module : VeriFuzz.Sim.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 VeriFuzz.Sim.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 VeriFuzz.Sim.Internal -import VeriFuzz.Sim.Template -import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.BitVec -import VeriFuzz.Verilog.CodeGen -import VeriFuzz.Verilog.Internal -import VeriFuzz.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) - => Icarus - -> b - -> SourceInfo - -> [ByteString] - -> ResultSh ByteString -runSimIc sim1 synth1 srcInfo bss = do - dir <- liftSh pwd - let top = srcInfo ^. mainModule - let inConcat = (RegConcat (Id . _portName <$> (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 (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 diff --git a/src/VeriFuzz/Sim/Identity.hs b/src/VeriFuzz/Sim/Identity.hs deleted file mode 100644 index bfa99f5..0000000 --- a/src/VeriFuzz/Sim/Identity.hs +++ /dev/null @@ -1,51 +0,0 @@ -{-| -Module : VeriFuzz.Sim.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 VeriFuzz.Sim.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 VeriFuzz.Sim.Internal -import VeriFuzz.Verilog.AST -import VeriFuzz.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/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs deleted file mode 100644 index f5351c7..0000000 --- a/src/VeriFuzz/Sim/Internal.hs +++ /dev/null @@ -1,215 +0,0 @@ -{-| -Module : VeriFuzz.Sim.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 VeriFuzz.Sim.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 VeriFuzz.Internal -import VeriFuzz.Result -import VeriFuzz.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 'VeriFuzz'. 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 "VERIFUZZ_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 - $ "VeriFuzz " - <> 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/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs deleted file mode 100644 index 254bfa5..0000000 --- a/src/VeriFuzz/Sim/Quartus.hs +++ /dev/null @@ -1,77 +0,0 @@ -{-| -Module : VeriFuzz.Sim.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 VeriFuzz.Sim.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 VeriFuzz.Sim.Internal -import VeriFuzz.Verilog.AST -import VeriFuzz.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/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs deleted file mode 100644 index 9b8ee9f..0000000 --- a/src/VeriFuzz/Sim/Template.hs +++ /dev/null @@ -1,133 +0,0 @@ -{-| -Module : VeriFuzz.Sim.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 VeriFuzz.Sim.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 VeriFuzz.Sim.Internal -import VeriFuzz.Verilog.AST -import VeriFuzz.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) => a -> b -> SourceInfo -> Text -sbyConfig 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 - . (fromText "data" </>) - . fromText - <$> deps - readL = T.intercalate "\n" $ mappend "read -formal " <$> deps - -icarusTestbench :: (Synthesiser a) => Verilog -> a -> Text -icarusTestbench t synth1 = [st| -`include "data/cells_cmos.v" -`include "data/cells_cyclone_v.v" -`include "data/cells_verific.v" -`include "data/cells_xilinx_7.v" -`include "data/cells_yosys.v" -`include "#{toTextIgnore $ synthOutput synth1}" - -#{genSource t} -|] diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs deleted file mode 100644 index 4ddb048..0000000 --- a/src/VeriFuzz/Sim/Vivado.hs +++ /dev/null @@ -1,71 +0,0 @@ -{-| -Module : VeriFuzz.Sim.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 VeriFuzz.Sim.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 VeriFuzz.Sim.Internal -import VeriFuzz.Sim.Template -import VeriFuzz.Verilog.AST -import VeriFuzz.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/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs deleted file mode 100644 index 86db667..0000000 --- a/src/VeriFuzz/Sim/XST.hs +++ /dev/null @@ -1,85 +0,0 @@ -{-| -Module : VeriFuzz.Sim.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 VeriFuzz.Sim.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 VeriFuzz.Sim.Internal -import VeriFuzz.Sim.Template -import VeriFuzz.Verilog.AST -import VeriFuzz.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/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs deleted file mode 100644 index 8c73b86..0000000 --- a/src/VeriFuzz/Sim/Yosys.hs +++ /dev/null @@ -1,127 +0,0 @@ -{-| -Module : VeriFuzz.Sim.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 VeriFuzz.Sim.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 VeriFuzz.Result -import VeriFuzz.Sim.Internal -import VeriFuzz.Sim.Template -import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.CodeGen -import VeriFuzz.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) => a -> b -> SourceInfo -> ResultSh () -runEquiv 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 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/VeriFuzz/Verilog.hs b/src/VeriFuzz/Verilog.hs deleted file mode 100644 index 4b5029c..0000000 --- a/src/VeriFuzz/Verilog.hs +++ /dev/null @@ -1,106 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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 VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.CodeGen -import VeriFuzz.Verilog.Parser -import VeriFuzz.Verilog.Quote diff --git a/src/VeriFuzz/Verilog/AST.hs b/src/VeriFuzz/Verilog/AST.hs deleted file mode 100644 index a85c365..0000000 --- a/src/VeriFuzz/Verilog/AST.hs +++ /dev/null @@ -1,583 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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 VeriFuzz.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/VeriFuzz/Verilog/BitVec.hs b/src/VeriFuzz/Verilog/BitVec.hs deleted file mode 100644 index 0cc9eb3..0000000 --- a/src/VeriFuzz/Verilog/BitVec.hs +++ /dev/null @@ -1,119 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs deleted file mode 100644 index 56e2819..0000000 --- a/src/VeriFuzz/Verilog/CodeGen.hs +++ /dev/null @@ -1,341 +0,0 @@ -{-| -Module : VeriFuzz.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 -"VeriFuzz.Verilog.AST". --} - -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE FlexibleInstances #-} - -module VeriFuzz.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 VeriFuzz.Internal hiding (comma) -import VeriFuzz.Verilog.AST -import VeriFuzz.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 . 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/VeriFuzz/Verilog/Eval.hs b/src/VeriFuzz/Verilog/Eval.hs deleted file mode 100644 index c802267..0000000 --- a/src/VeriFuzz/Verilog/Eval.hs +++ /dev/null @@ -1,119 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.Verilog.Eval - ( evaluateConst - , resize - ) -where - -import Data.Bits -import Data.Foldable (fold) -import Data.Functor.Foldable hiding (fold) -import Data.Maybe (listToMaybe) -import VeriFuzz.Verilog.AST -import VeriFuzz.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/VeriFuzz/Verilog/Internal.hs b/src/VeriFuzz/Verilog/Internal.hs deleted file mode 100644 index 42eb4e2..0000000 --- a/src/VeriFuzz/Verilog/Internal.hs +++ /dev/null @@ -1,93 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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 VeriFuzz.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/VeriFuzz/Verilog/Lex.x b/src/VeriFuzz/Verilog/Lex.x deleted file mode 100644 index cc67ecc..0000000 --- a/src/VeriFuzz/Verilog/Lex.x +++ /dev/null @@ -1,188 +0,0 @@ --- -*- haskell -*- -{ -{-# OPTIONS_GHC -w #-} -module VeriFuzz.Verilog.Lex - ( alexScanTokens - ) where - -import VeriFuzz.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/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs deleted file mode 100644 index 2e88859..0000000 --- a/src/VeriFuzz/Verilog/Mutate.hs +++ /dev/null @@ -1,397 +0,0 @@ -{-| -Module : VeriFuzz.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 "VeriFuzz.Verilog.AST" to generate more -random patterns, such as nesting wires instead of creating new ones. --} - -{-# LANGUAGE FlexibleInstances #-} - -module VeriFuzz.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 VeriFuzz.Circuit.Internal -import VeriFuzz.Internal -import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.BitVec -import VeriFuzz.Verilog.CodeGen -import VeriFuzz.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 VeriFuzz.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/VeriFuzz/Verilog/Parser.hs b/src/VeriFuzz/Verilog/Parser.hs deleted file mode 100644 index c08ebcd..0000000 --- a/src/VeriFuzz/Verilog/Parser.hs +++ /dev/null @@ -1,511 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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 VeriFuzz.Internal -import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.BitVec -import VeriFuzz.Verilog.Internal -import VeriFuzz.Verilog.Lex -import VeriFuzz.Verilog.Preprocess -import VeriFuzz.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/VeriFuzz/Verilog/Preprocess.hs b/src/VeriFuzz/Verilog/Preprocess.hs deleted file mode 100644 index c783ac5..0000000 --- a/src/VeriFuzz/Verilog/Preprocess.hs +++ /dev/null @@ -1,111 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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/VeriFuzz/Verilog/Quote.hs b/src/VeriFuzz/Verilog/Quote.hs deleted file mode 100644 index c6d3e3c..0000000 --- a/src/VeriFuzz/Verilog/Quote.hs +++ /dev/null @@ -1,50 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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 VeriFuzz.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/VeriFuzz/Verilog/Token.hs b/src/VeriFuzz/Verilog/Token.hs deleted file mode 100644 index d69f0b3..0000000 --- a/src/VeriFuzz/Verilog/Token.hs +++ /dev/null @@ -1,350 +0,0 @@ -{-| -Module : VeriFuzz.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 VeriFuzz.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) |