parser support for not, strong, weak, nexttime, and s_nexttime

CHANGELOG.md

 ## Unreleased
 
+### New Features
+
+* Added parsing support for `not`, `strong`, `weak`, `nexttime`, and
+  `s_nexttime` in assertion property expressions
+
 ### Bug Fixes
 
 * Fixed `--write path/to/dir/` with directives like `` `default_nettype ``

src/Convert/Traverse.hs

@@ -111,6 +111,7 @@ module Convert.Traverse
 ) where
 
 import Data.Bitraversable (bimapM)
+import Data.Functor ((<&>))
 import Data.Functor.Identity (Identity, runIdentity)
 import Control.Monad ((>=>))
 import Control.Monad.Writer.Strict
@@ -344,6 +345,16 @@ traversePropExprExprsM mapper (PropExprIff p1 p2) = do
     p1' <- traversePropExprExprsM mapper p1
     p2' <- traversePropExprExprsM mapper p2
     return $ PropExprIff p1' p2'
+traversePropExprExprsM mapper (PropExprNeg pe) =
+    traversePropExprExprsM mapper pe <&> PropExprNeg
+traversePropExprExprsM mapper (PropExprStrong se) =
+    traverseSeqExprExprsM mapper se <&> PropExprStrong
+traversePropExprExprsM mapper (PropExprWeak se) =
+    traverseSeqExprExprsM mapper se <&> PropExprWeak
+traversePropExprExprsM mapper (PropExprNextTime strong index prop) = do
+    index' <- mapper index
+    prop' <- traversePropExprExprsM mapper prop
+    return $ PropExprNextTime strong index' prop'
 
 seqExprHelper :: Monad m => MapperM m Expr
     -> (SeqExpr -> SeqExpr -> SeqExpr)

src/Language/SystemVerilog/AST/Stmt.hs

@@ -235,6 +235,10 @@ data PropExpr
     | PropExprFollowsO  SeqExpr PropExpr
     | PropExprFollowsNO SeqExpr PropExpr
     | PropExprIff PropExpr PropExpr
+    | PropExprNeg    PropExpr
+    | PropExprStrong SeqExpr
+    | PropExprWeak   SeqExpr
+    | PropExprNextTime Bool Expr PropExpr
     deriving Eq
 instance Show PropExpr where
     show (PropExpr se) = show se
@@ -243,6 +247,14 @@ instance Show PropExpr where
     show (PropExprFollowsO  a b) = printf "(%s #-# %s)" (show a) (show b)
     show (PropExprFollowsNO a b) = printf "(%s #=# %s)" (show a) (show b)
     show (PropExprIff a b) = printf "(%s iff %s)" (show a) (show b)
+    show (PropExprNeg    pe) = printf    "not (%s)" (show pe)
+    show (PropExprStrong se) = printf "strong (%s)" (show se)
+    show (PropExprWeak   se) = printf   "weak (%s)" (show se)
+    show (PropExprNextTime strong index prop) =
+        printf "%s%s (%s)" kwStr indexStr (show prop)
+        where
+            kwStr = (if strong then "s_" else "") ++ "nexttime"
+            indexStr = if index == Nil then "" else printf " [%s]" (show index)
 data SeqMatchItem
     = SeqMatchAsgn (LHS, AsgnOp, Expr)
     | SeqMatchCall Identifier Args

src/Language/SystemVerilog/Parser/Parse.y

@@ -413,6 +413,7 @@ time               { Token Lit_time        _ _ }
 %right "iff"
 %left "or" ","
 %left "and"
+%nonassoc "not" "nexttime" "s_nexttime"
 %left "intersect"
 %left "within"
 %right "throughout"
@@ -794,6 +795,13 @@ PropExprParens :: { PropExpr }
   | SeqExpr "#-#" PropExpr { PropExprFollowsO  $1 $3 }
   | SeqExpr "#=#" PropExpr { PropExprFollowsNO $1 $3 }
   | PropExpr "iff" PropExpr { PropExprIff $1 $3 }
+  | "not" PropExpr { PropExprNeg $2 }
+  | "strong" "(" SeqExpr ")" { PropExprStrong $3 }
+  | "weak"   "(" SeqExpr ")" { PropExprWeak   $3 }
+  | "nexttime"                PropExpr { PropExprNextTime False Nil $2 }
+  | "nexttime"   "[" Expr "]" PropExpr { PropExprNextTime False $3  $5 }
+  | "s_nexttime"              PropExpr { PropExprNextTime True  Nil $2 }
+  | "s_nexttime" "[" Expr "]" PropExpr { PropExprNextTime True  $3  $5 }
 SeqExpr :: { SeqExpr }
   : Expr { SeqExpr $1 }
   | SeqExprParens { $1 }

test/nosim/assert.sv

@@ -47,6 +47,11 @@ module top;
         (1 |-> (1 |=> (1 #-# (1 #=# (1 iff 1))))));
     assert property (@(posedge clk)
         1 and 1 or 1 intersect 1 throughout 1 within 1);
+    assert property (@(posedge clk) not (strong(1) iff weak(1)));
+    assert property (@(posedge clk) nexttime (1 iff 1));
+    assert property (@(posedge clk) nexttime [0] (1 iff 1));
+    assert property (@(posedge clk) s_nexttime (1 iff 1));
+    assert property (@(posedge clk) s_nexttime [0] (1 iff 1));
     assert property (@(posedge clk) 1 ##1 1);
     assert property (@(posedge clk) ##1 1);
     localparam C = 1;