From 11a5d0479d269eb3572db3e9f312a261b8ffcc46 Mon Sep 17 00:00:00 2001 From: Zachary Snow Date: Sun, 7 May 2023 16:45:06 -0400 Subject: [PATCH] support for sequence and property declarations --- CHANGELOG.md | 1 + src/Convert/Assertion.hs | 10 +- src/Convert/Traverse.hs | 159 +++++++++++-------- src/Language/SystemVerilog/AST/ModuleItem.hs | 21 ++- src/Language/SystemVerilog/AST/Stmt.hs | 3 - src/Language/SystemVerilog/Parser/Parse.y | 16 +- test/nosim/assert.sv | 8 + 7 files changed, 132 insertions(+), 86 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b04c19..a367893 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,7 @@ ### New Features * `string` data type is now dropped from parameters and localparams +* Added support for passing through `sequence` and `property` declarations ### Other Enhancements diff --git a/src/Convert/Assertion.hs b/src/Convert/Assertion.hs index 61890ac..46f7e2e 100644 --- a/src/Convert/Assertion.hs +++ b/src/Convert/Assertion.hs @@ -13,11 +13,11 @@ convert :: [AST] -> [AST] convert = map $ traverseDescriptions $ traverseModuleItems convertModuleItem convertModuleItem :: ModuleItem -> ModuleItem -convertModuleItem (AssertionItem item) = - Generate $ - map (GenModuleItem . MIPackageItem . Decl . CommentDecl) $ - "removed an assertion item" : - (lines $ show $ AssertionItem item) +convertModuleItem item@AssertionItem{} = + Generate $ map toItem comments + where + toItem = GenModuleItem . MIPackageItem . Decl . CommentDecl + comments = "removed an assertion item" : (lines $ show item) convertModuleItem other = traverseStmts (traverseNestedStmts convertStmt) other diff --git a/src/Convert/Traverse.hs b/src/Convert/Traverse.hs index 247dea5..b4c6943 100644 --- a/src/Convert/Traverse.hs +++ b/src/Convert/Traverse.hs @@ -282,75 +282,89 @@ traverseAssertionStmtsM mapper = assertionMapper assertionMapper (Cover e stmt) = mapper stmt >>= return . Cover e +traverseSeqExprExprsM :: Monad m => MapperM m Expr -> MapperM m SeqExpr +traverseSeqExprExprsM mapper (SeqExpr e) = + mapper e >>= return . SeqExpr +traverseSeqExprExprsM mapper (SeqExprAnd s1 s2) = + seqExprHelper mapper SeqExprAnd s1 s2 +traverseSeqExprExprsM mapper (SeqExprOr s1 s2) = + seqExprHelper mapper SeqExprOr s1 s2 +traverseSeqExprExprsM mapper (SeqExprIntersect s1 s2) = + seqExprHelper mapper SeqExprIntersect s1 s2 +traverseSeqExprExprsM mapper (SeqExprWithin s1 s2) = + seqExprHelper mapper SeqExprWithin s1 s2 +traverseSeqExprExprsM mapper (SeqExprThroughout e s) = do + e' <- mapper e + s' <- traverseSeqExprExprsM mapper s + return $ SeqExprThroughout e' s' +traverseSeqExprExprsM mapper (SeqExprDelay ms r s) = do + ms' <- case ms of + Nothing -> return Nothing + Just x -> traverseSeqExprExprsM mapper x >>= return . Just + r' <- mapBothM mapper r + s' <- traverseSeqExprExprsM mapper s + return $ SeqExprDelay ms' r' s' +traverseSeqExprExprsM mapper (SeqExprFirstMatch s items) = do + s' <- traverseSeqExprExprsM mapper s + items' <- mapM (traverseSeqMatchItemExprsM mapper) items + return $ SeqExprFirstMatch s' items' + +traverseSeqMatchItemExprsM :: Monad m => MapperM m Expr -> MapperM m SeqMatchItem +traverseSeqMatchItemExprsM mapper (SeqMatchAsgn (a, b, c)) = do + c' <- mapper c + return $ SeqMatchAsgn (a, b, c') +traverseSeqMatchItemExprsM mapper (SeqMatchCall x (Args l p)) = do + l' <- mapM mapper l + pes <- mapM mapper $ map snd p + let p' = zip (map fst p) pes + return $ SeqMatchCall x (Args l' p') + +traversePropertySpecExprsM :: Monad m => MapperM m Expr -> MapperM m PropertySpec +traversePropertySpecExprsM mapper (PropertySpec mv e pe) = do + mv' <- mapM (traverseEventExprsM mapper) mv + e' <- mapper e + pe' <- traversePropExprExprsM mapper pe + return $ PropertySpec mv' e' pe' + +traversePropExprExprsM :: Monad m => MapperM m Expr -> MapperM m PropExpr +traversePropExprExprsM mapper (PropExpr se) = + traverseSeqExprExprsM mapper se >>= return . PropExpr +traversePropExprExprsM mapper (PropExprImpliesO se pe) = + propExprHelper mapper PropExprImpliesO se pe +traversePropExprExprsM mapper (PropExprImpliesNO se pe) = + propExprHelper mapper PropExprImpliesNO se pe +traversePropExprExprsM mapper (PropExprFollowsO se pe) = + propExprHelper mapper PropExprFollowsO se pe +traversePropExprExprsM mapper (PropExprFollowsNO se pe) = + propExprHelper mapper PropExprFollowsNO se pe +traversePropExprExprsM mapper (PropExprIff p1 p2) = do + p1' <- traversePropExprExprsM mapper p1 + p2' <- traversePropExprExprsM mapper p2 + return $ PropExprIff p1' p2' + +seqExprHelper :: Monad m => MapperM m Expr + -> (SeqExpr -> SeqExpr -> SeqExpr) + -> SeqExpr -> SeqExpr -> m SeqExpr +seqExprHelper mapper constructor s1 s2 = do + s1' <- traverseSeqExprExprsM mapper s1 + s2' <- traverseSeqExprExprsM mapper s2 + return $ constructor s1' s2' + +propExprHelper :: Monad m => MapperM m Expr + -> (SeqExpr -> PropExpr -> PropExpr) + -> SeqExpr -> PropExpr -> m PropExpr +propExprHelper mapper constructor se pe = do + se' <- traverseSeqExprExprsM mapper se + pe' <- traversePropExprExprsM mapper pe + return $ constructor se' pe' + -- Note that this does not include the expressions without the statements of the -- actions associated with the assertions. traverseAssertionExprsM :: Monad m => MapperM m Expr -> MapperM m Assertion traverseAssertionExprsM mapper = assertionMapper where - seqExprMapper (SeqExpr e) = - mapper e >>= return . SeqExpr - seqExprMapper (SeqExprAnd s1 s2) = - ssMapper SeqExprAnd s1 s2 - seqExprMapper (SeqExprOr s1 s2) = - ssMapper SeqExprOr s1 s2 - seqExprMapper (SeqExprIntersect s1 s2) = - ssMapper SeqExprIntersect s1 s2 - seqExprMapper (SeqExprWithin s1 s2) = - ssMapper SeqExprWithin s1 s2 - seqExprMapper (SeqExprThroughout e s) = do - e' <- mapper e - s' <- seqExprMapper s - return $ SeqExprThroughout e' s' - seqExprMapper (SeqExprDelay ms r s) = do - ms' <- case ms of - Nothing -> return Nothing - Just x -> seqExprMapper x >>= return . Just - r' <- mapBothM mapper r - s' <- seqExprMapper s - return $ SeqExprDelay ms' r' s' - seqExprMapper (SeqExprFirstMatch s items) = do - s' <- seqExprMapper s - items' <- mapM seqMatchItemMapper items - return $ SeqExprFirstMatch s' items' - seqMatchItemMapper (SeqMatchAsgn (a, b, c)) = do - c' <- mapper c - return $ SeqMatchAsgn (a, b, c') - seqMatchItemMapper (SeqMatchCall x (Args l p)) = do - l' <- mapM mapper l - pes <- mapM mapper $ map snd p - let p' = zip (map fst p) pes - return $ SeqMatchCall x (Args l' p') - ppMapper constructor p1 p2 = do - p1' <- propExprMapper p1 - p2' <- propExprMapper p2 - return $ constructor p1' p2' - ssMapper constructor s1 s2 = do - s1' <- seqExprMapper s1 - s2' <- seqExprMapper s2 - return $ constructor s1' s2' - spMapper constructor se pe = do - se' <- seqExprMapper se - pe' <- propExprMapper pe - return $ constructor se' pe' - propExprMapper (PropExpr se) = - seqExprMapper se >>= return . PropExpr - propExprMapper (PropExprImpliesO se pe) = - spMapper PropExprImpliesO se pe - propExprMapper (PropExprImpliesNO se pe) = - spMapper PropExprImpliesNO se pe - propExprMapper (PropExprFollowsO se pe) = - spMapper PropExprFollowsO se pe - propExprMapper (PropExprFollowsNO se pe) = - spMapper PropExprFollowsNO se pe - propExprMapper (PropExprIff p1 p2) = - ppMapper PropExprIff p1 p2 - propSpecMapper (PropertySpec mv e pe) = do - mv' <- mapM (traverseEventExprsM mapper) mv - e' <- mapper e - pe' <- propExprMapper pe - return $ PropertySpec mv' e' pe' assertionExprMapper (Concurrent e) = - propSpecMapper e >>= return . Concurrent + traversePropertySpecExprsM mapper e >>= return . Concurrent assertionExprMapper (Immediate d e) = mapper e >>= return . Immediate d assertionMapper (Assert e ab) = do @@ -604,16 +618,23 @@ traverseNodesM exprMapper declMapper typeMapper lhsMapper stmtMapper = return $ MIPackageItem item' moduleItemMapper (MIPackageItem (DPIExport spec alias kw name)) = return $ MIPackageItem $ DPIExport spec alias kw name - moduleItemMapper (AssertionItem (mx, a)) = do - a' <- traverseAssertionStmtsM stmtMapper a - a'' <- traverseAssertionExprsM exprMapper a' - return $ AssertionItem (mx, a'') + moduleItemMapper (AssertionItem item) = + assertionItemMapper item >>= return . AssertionItem moduleItemMapper (ElabTask severity (Args pnArgs kwArgs)) = do pnArgs' <- mapM exprMapper pnArgs kwArgs' <- fmap (zip kwNames) $ mapM exprMapper kwExprs return $ ElabTask severity $ Args pnArgs' kwArgs' where (kwNames, kwExprs) = unzip kwArgs + assertionItemMapper (MIAssertion mx a) = do + a' <- traverseAssertionStmtsM stmtMapper a + a'' <- traverseAssertionExprsM exprMapper a' + return $ MIAssertion mx a'' + assertionItemMapper (PropertyDecl x p) = + traversePropertySpecExprsM exprMapper p >>= return . PropertyDecl x + assertionItemMapper (SequenceDecl x e) = + traverseSeqExprExprsM exprMapper e >>= return . SequenceDecl x + genItemMapper = traverseGenItemExprsM exprMapper modportDeclMapper (dir, ident, e) = do @@ -736,11 +757,11 @@ traverseLHSsM mapper = traverseModuleItemLHSsM (NInputGate kw d x lhs exprs) = do lhs' <- mapper lhs return $ NInputGate kw d x lhs' exprs - traverseModuleItemLHSsM (AssertionItem (mx, a)) = do + traverseModuleItemLHSsM (AssertionItem (MIAssertion mx a)) = do converted <- traverseNestedStmtsM (traverseStmtLHSsM mapper) (Assertion a) return $ case converted of - Assertion a' -> AssertionItem (mx, a') + Assertion a' -> AssertionItem $ MIAssertion mx a' _ -> error $ "redirected AssertionItem traverse failed: " ++ show converted traverseModuleItemLHSsM (Generate items) = do diff --git a/src/Language/SystemVerilog/AST/ModuleItem.hs b/src/Language/SystemVerilog/AST/ModuleItem.hs index 1632968..1c69b14 100644 --- a/src/Language/SystemVerilog/AST/ModuleItem.hs +++ b/src/Language/SystemVerilog/AST/ModuleItem.hs @@ -15,6 +15,7 @@ module Language.SystemVerilog.AST.ModuleItem , NOutputGateKW (..) , AssignOption (..) , Severity (..) + , AssertionItem (..) ) where import Data.List (intercalate) @@ -28,7 +29,7 @@ import Language.SystemVerilog.AST.Description (PackageItem) import Language.SystemVerilog.AST.Expr (Expr(Nil), pattern Ident, Range, showRanges, ParamBinding, showParams, Args) import Language.SystemVerilog.AST.GenItem (GenItem) import Language.SystemVerilog.AST.LHS (LHS) -import Language.SystemVerilog.AST.Stmt (Stmt, AssertionItem, Timing(Delay)) +import Language.SystemVerilog.AST.Stmt (Stmt, Assertion, Timing(Delay), PropertySpec, SeqExpr) import Language.SystemVerilog.AST.Type (Identifier, Strength0, Strength1) data ModuleItem @@ -65,10 +66,7 @@ instance Show ModuleItem where showGate kw d x $ show lhs : map show exprs show (NOutputGate kw d x lhss expr) = showGate kw d x $ (map show lhss) ++ [show expr] - show (AssertionItem (x, a)) = - if null x - then show a - else printf "%s : %s" x (show a) + show (AssertionItem i) = show i show (Instance m params i rs ports) = if null params then printf "%s %s%s%s;" m i rsStr (showPorts ports) @@ -164,3 +162,16 @@ instance Show Severity where show SeverityWarning = "$warning" show SeverityError = "$error" show SeverityFatal = "$fatal" + +data AssertionItem + = MIAssertion Identifier Assertion + | PropertyDecl Identifier PropertySpec + | SequenceDecl Identifier SeqExpr + deriving Eq + +instance Show AssertionItem where + show (MIAssertion x a) + | null x = show a + | otherwise = printf "%s : %s" x (show a) + show (PropertyDecl x p) = printf "property %s;\n%s\nendproperty" x (indent $ show p) + show (SequenceDecl x e) = printf "sequence %s;\n%s\nendsequence" x (indent $ show e) diff --git a/src/Language/SystemVerilog/AST/Stmt.hs b/src/Language/SystemVerilog/AST/Stmt.hs index 00b6d4c..aa85577 100644 --- a/src/Language/SystemVerilog/AST/Stmt.hs +++ b/src/Language/SystemVerilog/AST/Stmt.hs @@ -17,7 +17,6 @@ module Language.SystemVerilog.AST.Stmt , PropExpr (..) , SeqMatchItem (..) , SeqExpr (..) - , AssertionItem , Assertion (..) , AssertionKind(..) , Deferral (..) @@ -266,8 +265,6 @@ showCycleDelayRange (Nil, e) = printf "(%s)" (show e) showCycleDelayRange (e, Nil) = printf "[%s:$]" (show e) showCycleDelayRange r = showRange r -type AssertionItem = (Identifier, Assertion) - data Assertion = Assert AssertionKind ActionBlock | Assume AssertionKind ActionBlock diff --git a/src/Language/SystemVerilog/Parser/Parse.y b/src/Language/SystemVerilog/Parser/Parse.y index 113a383..9849d0a 100644 --- a/src/Language/SystemVerilog/Parser/Parse.y +++ b/src/Language/SystemVerilog/Parser/Parse.y @@ -726,6 +726,14 @@ AssignOption :: { AssignOption } AssertionItem :: { AssertionItem } : ConcurrentAssertionItem { $1 } | DeferredImmediateAssertionItem { $1 } + | SequenceDecl { $1 } + | PropertyDecl { $1 } + +SequenceDecl :: { AssertionItem } + : "sequence" Identifier ";" SeqExpr opt(";") "endsequence" StrTag {% checkTag $2 $7 $ SequenceDecl $2 $4 } + +PropertyDecl :: { AssertionItem } + : "property" Identifier ";" PropertySpec opt(";") "endproperty" StrTag {% checkTag $2 $7 $ PropertyDecl $2 $4 } -- for Stmt, for now ProceduralAssertionStatement :: { Assertion } @@ -737,12 +745,12 @@ ImmediateAssertionStatement :: { Assertion } | DeferredImmediateAssertionStatement { $1 } DeferredImmediateAssertionItem :: { AssertionItem } - : Identifier ":" DeferredImmediateAssertionStatement { ($1, $3) } - | DeferredImmediateAssertionStatement { ("", $1) } + : Identifier ":" DeferredImmediateAssertionStatement { MIAssertion $1 $3 } + | DeferredImmediateAssertionStatement { MIAssertion "" $1 } ConcurrentAssertionItem :: { AssertionItem } - : Identifier ":" ConcurrentAssertionStatement { ($1, $3) } - | ConcurrentAssertionStatement { ("", $1) } + : Identifier ":" ConcurrentAssertionStatement { MIAssertion $1 $3 } + | ConcurrentAssertionStatement { MIAssertion "" $1 } ConcurrentAssertionStatement :: { Assertion } : "assert" "property" "(" PropertySpec ")" ActionBlock { Assert (Concurrent $4) $6 } diff --git a/test/nosim/assert.sv b/test/nosim/assert.sv index 55215e8..c9a4c2e 100644 --- a/test/nosim/assert.sv +++ b/test/nosim/assert.sv @@ -60,4 +60,12 @@ module top; integer x; // TODO: The assignment below should only be allowed in a property decleration. assert property (@(posedge clk) first_match(1, x++, $display("a", clk), $display("b", clk))); + + sequence some_sequence; + 1 and 1; + endsequence + property some_property; + @(edge clk) some_sequence iff 1; + endproperty + assert property (some_property); endmodule