support cycle delay range in sequence expressions

CHANGELOG.md

@@ -6,6 +6,7 @@
   `'1`, `'x`) via `--exclude UnbasedUniszed`
 * Added support for enumerated type ranges (e.g., `enum { X[3:5] }`)
 * Added support for the SystemVerilog `edge` event
+* Added support for cycle delay ranges in assertion sequence expressions
 * Added support for passing through DPI imports and exports
 * Added support for passing through functions with output ports
 

src/Convert/Traverse.hs

@@ -300,13 +300,13 @@ traverseAssertionExprsM mapper = assertionMapper
             e' <- mapper e
             s' <- seqExprMapper s
             return $ SeqExprThroughout e' s'
-        seqExprMapper (SeqExprDelay ms e s) = do
+        seqExprMapper (SeqExprDelay ms r s) = do
             ms' <- case ms of
                 Nothing -> return Nothing
                 Just x -> seqExprMapper x >>= return . Just
-            e' <- mapper e
+            r' <- mapBothM mapper r
             s' <- seqExprMapper s
-            return $ SeqExprDelay ms' e' s'
+            return $ SeqExprDelay ms' r' s'
         seqExprMapper (SeqExprFirstMatch s items) = do
             s' <- seqExprMapper s
             items' <- mapM seqMatchItemMapper items

src/Language/SystemVerilog/AST/Expr.hs

@@ -15,6 +15,7 @@ module Language.SystemVerilog.AST.Expr
     , DimsFn (..)
     , DimFn (..)
     , showAssignment
+    , showRange
     , showRanges
     , ParamBinding
     , showParams

src/Language/SystemVerilog/AST/Stmt.hs

@@ -29,7 +29,7 @@ import Text.Printf (printf)
 import Language.SystemVerilog.AST.ShowHelp (commas, indent, unlines', showPad, showBlock)
 import Language.SystemVerilog.AST.Attr (Attr)
 import Language.SystemVerilog.AST.Decl (Decl)
-import Language.SystemVerilog.AST.Expr (Expr(Call, Ident, Nil), Args(..))
+import Language.SystemVerilog.AST.Expr (Expr(Call, Ident, Nil), Args(..), Range, showRange)
 import Language.SystemVerilog.AST.LHS (LHS)
 import Language.SystemVerilog.AST.Op (AsgnOp(AsgnOpEq))
 import Language.SystemVerilog.AST.Type (Identifier)
@@ -224,7 +224,7 @@ data SeqExpr
     | SeqExprIntersect  SeqExpr SeqExpr
     | SeqExprThroughout Expr    SeqExpr
     | SeqExprWithin     SeqExpr SeqExpr
-    | SeqExprDelay (Maybe SeqExpr) Expr SeqExpr
+    | SeqExprDelay (Maybe SeqExpr) Range SeqExpr
     | SeqExprFirstMatch SeqExpr [SeqMatchItem]
     deriving Eq
 instance Show SeqExpr where
@@ -234,9 +234,14 @@ instance Show SeqExpr where
     show (SeqExprIntersect  a b) = printf "(%s %s %s)" (show a) "intersect"  (show b)
     show (SeqExprThroughout a b) = printf "(%s %s %s)" (show a) "throughout" (show b)
     show (SeqExprWithin     a b) = printf "(%s %s %s)" (show a) "within"     (show b)
-    show (SeqExprDelay   me e s) = printf "%s##%s %s" (maybe "" showPad me) (show e) (show s)
+    show (SeqExprDelay   me r s) = printf "%s##%s %s" (maybe "" showPad me) (showCycleDelayRange r) (show s)
     show (SeqExprFirstMatch e a) = printf "first_match(%s, %s)" (show e) (commas $ map show a)
 
+showCycleDelayRange :: Range -> String
+showCycleDelayRange (Nil, e) = printf "(%s)" (show e)
+showCycleDelayRange (e, Nil) = printf "[%s:$]" (show e)
+showCycleDelayRange r = showRange r
+
 type AssertionItem = (Identifier, Assertion)
 
 data Assertion

src/Language/SystemVerilog/Parser/Parse.y

@@ -790,8 +790,8 @@ SeqExprParens :: { SeqExpr }
   | SeqExpr "intersect"  SeqExpr { SeqExprIntersect  $1 $3 }
   | Expr    "throughout" SeqExpr { SeqExprThroughout $1 $3 }
   | SeqExpr "within"     SeqExpr { SeqExprWithin     $1 $3 }
-  | SeqExpr "##" Number  SeqExpr { SeqExprDelay (Just $1) (Number $3) $4 }
-  |         "##" Number  SeqExpr { SeqExprDelay (Nothing) (Number $2) $3 }
+  | SeqExpr "##" CycleDelayRange SeqExpr { SeqExprDelay (Just $1) $3 $4 }
+  |         "##" CycleDelayRange SeqExpr { SeqExprDelay (Nothing) $2 $3 }
   | "first_match" "(" SeqExpr SeqMatchItems ")" { SeqExprFirstMatch $3 $4 }
 SeqMatchItems :: { [SeqMatchItem] }
   : "," SeqMatchItem               { [$2] }
@@ -800,6 +800,16 @@ SeqMatchItem :: { SeqMatchItem }
   : ForStepAssignment   { SeqMatchAsgn $1 }
   | Identifier CallArgs { SeqMatchCall $1 $2 }
 
+CycleDelayRange :: { Range }
+  : Range { $1 }
+  | Number       { (Nil, Number $1) }
+  | Identifier   { (Nil, Ident  $1) }
+  | "(" Expr ")" { (Nil,        $2) }
+  | "[" "+" "]"  { (RawNum 1, Nil) }
+  | "[" "*" "]"  { (RawNum 0, Nil) }
+  | "[*"    "]"  { (RawNum 0, Nil) }
+  | "[" Expr ":" "$" "]" { ($2, Nil) }
+
 ActionBlock :: { ActionBlock }
   : Stmt %prec NoElse { ActionBlock $1 Null }
   |      "else" Stmt  { ActionBlock Null $2 }

test/nosim/assert.sv

@@ -49,6 +49,15 @@ module top;
         1 and 1 or 1 intersect 1 throughout 1 within 1);
     assert property (@(posedge clk) 1 ##1 1);
     assert property (@(posedge clk) ##1 1);
+    localparam C = 1;
+    assert property (@(posedge clk) ##C 1);
+    assert property (@(posedge clk) ##(C + 1) 1);
+    assert property (@(posedge clk) ##[C:1] 1);
+    assert property (@(posedge clk) ##[+] 1);
+    assert property (@(posedge clk) ##[*] 1);
+    assert property (@(posedge clk) ##[ *] 1);
+
     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)));
 endmodule