aboutsummaryrefslogtreecommitdiffstats
path: root/src/Verismith/Verilog
diff options
context:
space:
mode:
Diffstat (limited to 'src/Verismith/Verilog')
-rw-r--r--src/Verismith/Verilog/AST.hs4
-rw-r--r--src/Verismith/Verilog/CodeGen.hs30
-rw-r--r--src/Verismith/Verilog/Internal.hs18
-rw-r--r--src/Verismith/Verilog/Mutate.hs42
-rw-r--r--src/Verismith/Verilog/Parser.hs44
-rw-r--r--src/Verismith/Verilog/Quote.hs3
6 files changed, 71 insertions, 70 deletions
diff --git a/src/Verismith/Verilog/AST.hs b/src/Verismith/Verilog/AST.hs
index 9a71022..74c3cfb 100644
--- a/src/Verismith/Verilog/AST.hs
+++ b/src/Verismith/Verilog/AST.hs
@@ -364,7 +364,7 @@ instance Num Range where
-- 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
+-- This is now implemented inside '(ModDecl ann)' itself, which uses a list of output
-- and input ports.
data Port = Port
{ _portType :: !PortType
@@ -547,7 +547,7 @@ 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 a -> f (ModItem a)
+traverseModItem :: (Applicative f) => (Expr -> f Expr) -> (ModItem ann) -> f (ModItem ann)
traverseModItem f (ModCA (ContAssign a e)) = ModCA . ContAssign a <$> f e
traverseModItem f (ModInst a b e) =
ModInst a b <$> sequenceA (traverseModConn f <$> e)
diff --git a/src/Verismith/Verilog/CodeGen.hs b/src/Verismith/Verilog/CodeGen.hs
index 8dd8f28..f8fce80 100644
--- a/src/Verismith/Verilog/CodeGen.hs
+++ b/src/Verismith/Verilog/CodeGen.hs
@@ -38,17 +38,17 @@ import Verismith.Verilog.BitVec
class Source a where
genSource :: a -> Text
--- | Map a 'Maybe Statement' to 'Text'. If it is 'Just statement', the generated
+-- | Map a 'Maybe (Statement ann)' 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 (Statement ann) -> Doc a
defMap = maybe semi statement
--- | Convert the 'Verilog' type to 'Text' so that it can be rendered.
-verilogSrc :: Verilog -> Doc a
+-- | Convert the 'Verilog ann' type to 'Text' so that it can be rendered.
+verilogSrc :: (Verilog ann) -> 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
+-- | Generate the 'ModDecl ann' for a module and convert it to 'Text'.
+moduleDecl :: ModDecl ann -> Doc a
moduleDecl (ModDecl i outP inP items ps) = vsep
[ sep ["module" <+> identifier i, params ps, ports <> semi]
, indent 2 modI
@@ -110,8 +110,8 @@ portDir PortIn = "input"
portDir PortOut = "output"
portDir PortInOut = "inout"
--- | Generate a 'ModItem'.
-moduleItem :: ModItem -> Doc a
+-- | Generate a '(ModItem ann)'.
+moduleItem :: (ModItem ann) -> Doc a
moduleItem (ModCA ca ) = contAssign ca
moduleItem (ModInst i name conn) = (<> semi) $ hsep
[ identifier i
@@ -248,11 +248,11 @@ caseType CaseStandard = "case"
caseType CaseX = "casex"
caseType CaseZ = "casez"
-casePair :: CasePair -> Doc a
+casePair :: (CasePair ann) -> Doc a
casePair (CasePair e s) =
vsep [hsep [expr e, colon], indent 2 $ statement s]
-statement :: Statement -> Doc a
+statement :: Statement ann -> Doc a
statement (TimeCtrl d stat) = hsep [delay d, defMap stat]
statement (EventCtrl e stat) = hsep [event e, defMap stat]
statement (SeqBlock s) =
@@ -302,7 +302,7 @@ instance Source Identifier where
instance Source Task where
genSource = showT . task
-instance Source Statement where
+instance Source (Statement ann) where
genSource = showT . statement
instance Source PortType where
@@ -329,7 +329,7 @@ instance Source Expr where
instance Source ContAssign where
genSource = showT . contAssign
-instance Source ModItem where
+instance Source (ModItem ann) where
genSource = showT . moduleItem
instance Source PortDir where
@@ -338,13 +338,13 @@ instance Source PortDir where
instance Source Port where
genSource = showT . port
-instance Source ModDecl where
+instance Source (ModDecl ann) where
genSource = showT . moduleDecl
-instance Source Verilog where
+instance Source (Verilog ann) where
genSource = showT . verilogSrc
-instance Source SourceInfo where
+instance Source (SourceInfo ann) where
genSource (SourceInfo _ src) = genSource src
newtype GenVerilog a = GenVerilog { unGenVerilog :: a }
diff --git a/src/Verismith/Verilog/Internal.hs b/src/Verismith/Verilog/Internal.hs
index 0644d95..0ebc626 100644
--- a/src/Verismith/Verilog/Internal.hs
+++ b/src/Verismith/Verilog/Internal.hs
@@ -32,28 +32,28 @@ import Control.Lens
import Data.Text (Text)
import Verismith.Verilog.AST
-regDecl :: Identifier -> ModItem
+regDecl :: Identifier -> (ModItem ann)
regDecl i = Decl Nothing (Port Reg False (Range 1 0) i) Nothing
-wireDecl :: Identifier -> ModItem
+wireDecl :: Identifier -> (ModItem ann)
wireDecl i = Decl Nothing (Port Wire False (Range 1 0) i) Nothing
-- | Create an empty module.
-emptyMod :: ModDecl
+emptyMod :: (ModDecl ann)
emptyMod = ModDecl "" [] [] [] []
-- | Set a module name for a module declaration.
-setModName :: Text -> ModDecl -> ModDecl
+setModName :: Text -> (ModDecl ann) -> (ModDecl ann)
setModName str = modId .~ Identifier str
-- | Add a input port to the module declaration.
-addModPort :: Port -> ModDecl -> ModDecl
+addModPort :: Port -> (ModDecl ann) -> (ModDecl ann)
addModPort port = modInPorts %~ (:) port
-addModDecl :: ModDecl -> Verilog -> Verilog
+addModDecl :: (ModDecl ann) -> (Verilog ann) -> (Verilog ann)
addModDecl desc = _Wrapped %~ (:) desc
-testBench :: ModDecl
+testBench :: (ModDecl ann)
testBench = ModDecl
"main"
[]
@@ -71,7 +71,7 @@ testBench = ModDecl
]
[]
-addTestBench :: Verilog -> Verilog
+addTestBench :: (Verilog ann) -> (Verilog ann)
addTestBench = addModDecl testBench
defaultPort :: Identifier -> Port
@@ -80,7 +80,7 @@ defaultPort = Port Wire False (Range 1 0)
portToExpr :: Port -> Expr
portToExpr (Port _ _ _ i) = Id i
-modName :: ModDecl -> Text
+modName :: (ModDecl ann) -> Text
modName = getIdentifier . view modId
yPort :: Identifier -> Port
diff --git a/src/Verismith/Verilog/Mutate.hs b/src/Verismith/Verilog/Mutate.hs
index e80437f..260d759 100644
--- a/src/Verismith/Verilog/Mutate.hs
+++ b/src/Verismith/Verilog/Mutate.hs
@@ -106,7 +106,7 @@ instance Mutate Assign where
instance Mutate ContAssign where
mutExpr f (ContAssign a e) = ContAssign a $ f e
-instance Mutate Statement where
+instance Mutate (Statement ann) 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
@@ -123,7 +123,7 @@ instance Mutate Parameter where
instance Mutate LocalParam where
mutExpr _ = id
-instance Mutate ModItem where
+instance Mutate (ModItem ann) 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
@@ -132,13 +132,13 @@ instance Mutate ModItem where
mutExpr _ p@ParamDecl{} = p
mutExpr _ l@LocalParamDecl{} = l
-instance Mutate ModDecl where
+instance Mutate (ModDecl ann) 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
+instance Mutate (Verilog ann) where
mutExpr f (Verilog a) = Verilog $ mutExpr f a
-instance Mutate SourceInfo where
+instance Mutate (SourceInfo ann) where
mutExpr f (SourceInfo a b) = SourceInfo a $ mutExpr f b
instance Mutate a => Mutate [a] where
@@ -150,8 +150,8 @@ instance Mutate a => Mutate (Maybe a) where
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
+-- | Return if the 'Identifier' is in a '(ModDecl ann)'.
+inPort :: Identifier -> (ModDecl ann) -> Bool
inPort i m = inInput
where
inInput =
@@ -159,7 +159,7 @@ inPort i m = inInput
-- | Find the last assignment of a specific wire/reg to an expression, and
-- returns that expression.
-findAssign :: Identifier -> [ModItem] -> Maybe Expr
+findAssign :: Identifier -> [ModItem ann] -> Maybe Expr
findAssign i items = safe last . catMaybes $ isAssign <$> items
where
isAssign (ModCA (ContAssign val expr)) | val == i = Just expr
@@ -184,7 +184,7 @@ replace = (transform .) . idTrans
-- 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 :: Identifier -> (ModDecl ann) -> (ModDecl ann)
nestId i m
| not $ inPort i m
= let expr = fromMaybe def . findAssign i $ m ^. modItems
@@ -196,15 +196,15 @@ nestId i m
def = Id i
-- | Replaces an identifier by a expression in all the module declaration.
-nestSource :: Identifier -> Verilog -> Verilog
+nestSource :: Identifier -> (Verilog ann) -> (Verilog ann)
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 :: Int -> (Verilog ann) -> (Verilog ann)
nestUpTo i src =
foldl (flip nestSource) src $ Identifier . fromNode <$> [1 .. i]
-allVars :: ModDecl -> [Identifier]
+allVars :: (ModDecl ann) -> [Identifier]
allVars m =
(m ^.. modOutPorts . traverse . portName)
<> (m ^.. modInPorts . traverse . portName)
@@ -226,7 +226,7 @@ allVars m =
-- endmodule
-- <BLANKLINE>
-- <BLANKLINE>
-instantiateMod :: ModDecl -> ModDecl -> ModDecl
+instantiateMod :: (ModDecl ann) -> (ModDecl ann) -> (ModDecl ann)
instantiateMod m main = main & modItems %~ ((out ++ regIn ++ [inst]) ++)
where
out = Decl Nothing <$> m ^. modOutPorts <*> pure Nothing
@@ -252,7 +252,7 @@ instantiateMod m main = main & modItems %~ ((out ++ regIn ++ [inst]) ++)
-- >>> GenVerilog $ instantiateMod_ m
-- m m(y, x);
-- <BLANKLINE>
-instantiateMod_ :: ModDecl -> ModItem
+instantiateMod_ :: (ModDecl ann) -> (ModItem ann)
instantiateMod_ m = ModInst (m ^. modId) (m ^. modId) conns
where
conns =
@@ -267,7 +267,7 @@ instantiateMod_ m = ModInst (m ^. modId) (m ^. modId) conns
-- >>> GenVerilog $ instantiateModSpec_ "_" m
-- m m(.y(y), .x(x));
-- <BLANKLINE>
-instantiateModSpec_ :: Text -> ModDecl -> ModItem
+instantiateModSpec_ :: Text -> (ModDecl ann) -> (ModItem ann)
instantiateModSpec_ outChar m = ModInst (m ^. modId) (m ^. modId) conns
where
conns = zipWith ModConnNamed ids (Id <$> instIds)
@@ -288,7 +288,7 @@ filterChar t ids =
-- endmodule
-- <BLANKLINE>
-- <BLANKLINE>
-initMod :: ModDecl -> ModDecl
+initMod :: (ModDecl ann) -> (ModDecl ann)
initMod m = m & modItems %~ ((out ++ inp) ++)
where
out = Decl (Just PortOut) <$> (m ^. modOutPorts) <*> pure Nothing
@@ -301,7 +301,7 @@ makeIdFrom a i = (i <>) . Identifier . ("_" <>) $ showT a
-- | Make top level module for equivalence verification. Also takes in how many
-- modules to instantiate.
-makeTop :: Int -> ModDecl -> ModDecl
+makeTop :: Int -> (ModDecl ann) -> (ModDecl ann)
makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt []
where
ys = yPort . flip makeIdFrom "y" <$> [1 .. i]
@@ -311,7 +311,7 @@ makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt []
-- | Make a top module with an assert that requires @y_1@ to always be equal to
-- @y_2@, which can then be proven using a formal verification tool.
-makeTopAssert :: ModDecl -> ModDecl
+makeTopAssert :: (ModDecl ann) -> (ModDecl ann)
makeTopAssert = (modItems %~ (++ [assert])) . makeTop 2
where
assert = Always . EventCtrl e . Just $ SeqBlock
@@ -320,7 +320,7 @@ makeTopAssert = (modItems %~ (++ [assert])) . makeTop 2
-- | 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 :: [Port] -> (ModDecl ann) -> (ModDecl ann)
declareMod ports = initMod . (modItems %~ (fmap decl ports ++))
where
decl p@(Port Reg _ _ _) = Decl Nothing p (Just 0)
@@ -374,7 +374,7 @@ removeId i = transform trans
| otherwise = Id ident
trans e = e
-combineAssigns :: Port -> [ModItem] -> [ModItem]
+combineAssigns :: Port -> [ModItem ann] -> [ModItem ann]
combineAssigns p a =
a
<> [ ModCA
@@ -386,7 +386,7 @@ combineAssigns p a =
]
where assigns = a ^.. traverse . modContAssign . contAssignNetLVal
-combineAssigns_ :: Bool -> Port -> [Port] -> ModItem
+combineAssigns_ :: Bool -> Port -> [Port] -> (ModItem ann)
combineAssigns_ comb p ps =
ModCA
. ContAssign (p ^. portName)
diff --git a/src/Verismith/Verilog/Parser.hs b/src/Verismith/Verilog/Parser.hs
index a6eaf24..70dc973 100644
--- a/src/Verismith/Verilog/Parser.hs
+++ b/src/Verismith/Verilog/Parser.hs
@@ -283,7 +283,7 @@ strId = satisfy' matchId
identifier :: Parser Identifier
identifier = Identifier . T.pack <$> strId
-parseNetDecl :: Maybe PortDir -> Parser ModItem
+parseNetDecl :: Maybe PortDir -> Parser (ModItem ann)
parseNetDecl pd = do
t <- option Wire type_
sign <- option False (tok KWSigned $> True)
@@ -303,10 +303,10 @@ parsePortDir =
<|> tok KWInout
$> PortInOut
-parseDecl :: Parser ModItem
+parseDecl :: Parser (ModItem ann)
parseDecl = (Just <$> parsePortDir >>= parseNetDecl) <|> parseNetDecl Nothing
-parseConditional :: Parser Statement
+parseConditional :: Parser (Statement ann)
parseConditional = do
expr <- tok' KWIf *> parens parseExpr
true <- maybeEmptyStatement
@@ -336,7 +336,7 @@ parseAssign t = do
expr <- parseExpr
return $ Assign lval delay expr
-parseLoop :: Parser Statement
+parseLoop :: Parser (Statement ann)
parseLoop = do
a <- tok' KWFor *> tok' SymParenL *> parseAssign SymEq
expr <- tok' SymSemi *> parseExpr
@@ -373,37 +373,37 @@ parseEvent' =
<|> try (fmap EId identifier)
<|> try (fmap EExpr parseExpr)
-parseEventCtrl :: Parser Statement
+parseEventCtrl :: Parser (Statement ann)
parseEventCtrl = do
event <- parseEvent
statement <- option Nothing maybeEmptyStatement
return $ EventCtrl event statement
-parseDelayCtrl :: Parser Statement
+parseDelayCtrl :: Parser (Statement ann)
parseDelayCtrl = do
delay <- parseDelay
statement <- option Nothing maybeEmptyStatement
return $ TimeCtrl delay statement
-parseBlocking :: Parser Statement
+parseBlocking :: Parser (Statement ann)
parseBlocking = do
a <- parseAssign SymEq
tok' SymSemi
return $ BlockAssign a
-parseNonBlocking :: Parser Statement
+parseNonBlocking :: Parser (Statement ann)
parseNonBlocking = do
a <- parseAssign SymLtEq
tok' SymSemi
return $ NonBlockAssign a
-parseSeq :: Parser Statement
+parseSeq :: Parser (Statement ann)
parseSeq = do
seq' <- tok' KWBegin *> many parseStatement
tok' KWEnd
return $ SeqBlock seq'
-parseStatement :: Parser Statement
+parseStatement :: Parser (Statement ann)
parseStatement =
parseSeq
<|> parseConditional
@@ -413,14 +413,14 @@ parseStatement =
<|> try parseBlocking
<|> parseNonBlocking
-maybeEmptyStatement :: Parser (Maybe Statement)
+maybeEmptyStatement :: Parser (Maybe (Statement ann))
maybeEmptyStatement =
(tok' SymSemi >> return Nothing) <|> (Just <$> parseStatement)
-parseAlways :: Parser ModItem
+parseAlways :: Parser (ModItem ann)
parseAlways = tok' KWAlways *> (Always <$> parseStatement)
-parseInitial :: Parser ModItem
+parseInitial :: Parser (ModItem ann)
parseInitial = tok' KWInitial *> (Initial <$> parseStatement)
namedModConn :: Parser ModConn
@@ -432,7 +432,7 @@ namedModConn = do
parseModConn :: Parser ModConn
parseModConn = try (fmap ModConn parseExpr) <|> namedModConn
-parseModInst :: Parser ModItem
+parseModInst :: Parser (ModItem ann)
parseModInst = do
m <- identifier
name <- identifier
@@ -440,7 +440,7 @@ parseModInst = do
tok' SymSemi
return $ ModInst m name modconns
-parseModItem :: Parser ModItem
+parseModItem :: Parser (ModItem ann)
parseModItem =
try (ModCA <$> parseContAssign)
<|> try parseDecl
@@ -451,11 +451,11 @@ parseModItem =
parseModList :: Parser [Identifier]
parseModList = list <|> return [] where list = parens $ commaSep identifier
-filterDecl :: PortDir -> ModItem -> Bool
+filterDecl :: PortDir -> (ModItem ann) -> Bool
filterDecl p (Decl (Just p') _ _) = p == p'
filterDecl _ _ = False
-modPorts :: PortDir -> [ModItem] -> [Port]
+modPorts :: PortDir -> [ModItem ann] -> [Port]
modPorts p mis = filter (filterDecl p) mis ^.. traverse . declPort
parseParam :: Parser Parameter
@@ -467,7 +467,7 @@ parseParam = do
parseParams :: Parser [Parameter]
parseParams = tok' SymPound *> parens (commaSep parseParam)
-parseModDecl :: Parser ModDecl
+parseModDecl :: Parser (ModDecl ann)
parseModDecl = do
name <- tok KWModule *> identifier
paramList <- option [] $ try parseParams
@@ -483,7 +483,7 @@ parseModDecl = do
-- | Parses a 'String' into 'Verilog' by skipping any beginning whitespace
-- and then parsing multiple Verilog source.
-parseVerilogSrc :: Parser Verilog
+parseVerilogSrc :: Parser (Verilog ann)
parseVerilogSrc = Verilog <$> many parseModDecl
-- | Parse a 'String' containing verilog code. The parser currently only supports
@@ -491,7 +491,7 @@ parseVerilogSrc = Verilog <$> many parseModDecl
parseVerilog
:: Text -- ^ Name of parsed object.
-> Text -- ^ Content to be parsed.
- -> Either Text Verilog -- ^ Returns 'String' with error
+ -> Either Text (Verilog ann) -- ^ Returns 'String' with error
-- message if parse fails.
parseVerilog s =
bimap showT id
@@ -500,12 +500,12 @@ parseVerilog s =
. preprocess [] (T.unpack s)
. T.unpack
-parseVerilogFile :: Text -> IO Verilog
+parseVerilogFile :: Text -> IO (Verilog ann)
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 :: Text -> Text -> IO (SourceInfo ann)
parseSourceInfoFile top = fmap (SourceInfo top) . parseVerilogFile
diff --git a/src/Verismith/Verilog/Quote.hs b/src/Verismith/Verilog/Quote.hs
index 879b8fd..5e1e5dc 100644
--- a/src/Verismith/Verilog/Quote.hs
+++ b/src/Verismith/Verilog/Quote.hs
@@ -23,6 +23,7 @@ import qualified Language.Haskell.TH as TH
import Language.Haskell.TH.Quote
import Language.Haskell.TH.Syntax
import Verismith.Verilog.Parser
+import Verismith.Verilog.AST (Verilog)
liftDataWithText :: Data a => a -> Q Exp
liftDataWithText = dataToExpQ $ fmap liftText . cast
@@ -47,4 +48,4 @@ quoteVerilog s = do
v <- case parseVerilog pos (T.pack s) of
Right e -> return e
Left e -> fail $ show e
- liftDataWithText v
+ liftDataWithText (v :: Verilog ())
generated by cgit (git 2.34.1) at 2024-06-03 03:18:16 +0000