support for deferred immediate assertion statements

src/Convert/Traverse.hs

@@ -345,10 +345,10 @@ traverseAssertionExprsM mapper = assertionMapper
             e' <- mapper e
             pe' <- propExprMapper pe
             return $ PropertySpec ms e' pe'
-        assertionExprMapper (Left e) =
-            propSpecMapper e >>= return . Left
-        assertionExprMapper (Right e) =
-            mapper e >>= return . Right
+        assertionExprMapper (Concurrent e) =
+            propSpecMapper e >>= return . Concurrent
+        assertionExprMapper (Immediate d e) =
+            mapper e >>= return . Immediate d
         assertionMapper (Assert e ab) = do
             e' <- assertionExprMapper e
             return $ Assert e' ab
@@ -389,10 +389,10 @@ traverseStmtLHSsM mapper = stmtMapper
             s2' <- senseMapper s2
             return $ SenseOr s1' s2'
         senseMapper (SenseStar       ) = return SenseStar
-        assertionExprMapper (Left (PropertySpec (Just sense) me pe)) = do
+        assertionExprMapper (Concurrent (PropertySpec (Just sense) me pe)) = do
             sense' <- senseMapper sense
-            return $ Left $ PropertySpec (Just sense') me pe
-        assertionExprMapper other = return $ other
+            return $ Concurrent $ PropertySpec (Just sense') me pe
+        assertionExprMapper other = return other
         assertionMapper (Assert e ab) = do
             e' <- assertionExprMapper e
             return $ Assert e' ab

src/Language/SystemVerilog/AST/Stmt.hs

@@ -16,8 +16,9 @@ module Language.SystemVerilog.AST.Stmt
     , SeqMatchItem (..)
     , SeqExpr      (..)
     , AssertionItem
-    , AssertionExpr
     , Assertion    (..)
+    , AssertionKind(..)
+    , Deferral     (..)
     , PropertySpec (..)
     , ViolationCheck (..)
     , BlockKW (..)
@@ -235,20 +236,34 @@ instance Show SeqExpr where
     show (SeqExprFirstMatch e a) = printf "first_match(%s, %s)" (show e) (commas $ map show a)
 
 type AssertionItem = (Identifier, Assertion)
-type AssertionExpr = Either PropertySpec Expr
+
 data Assertion
-    = Assert AssertionExpr ActionBlock
-    | Assume AssertionExpr ActionBlock
-    | Cover  AssertionExpr Stmt
+    = Assert AssertionKind ActionBlock
+    | Assume AssertionKind ActionBlock
+    | Cover  AssertionKind Stmt
     deriving Eq
 instance Show Assertion where
-    show (Assert e a) = printf "assert %s%s" (showAssertionExpr e) (show a)
-    show (Assume e a) = printf "assume %s%s" (showAssertionExpr e) (show a)
-    show (Cover  e a) = printf  "cover %s%s" (showAssertionExpr e) (show a)
+    show (Assert k a) = printf "assert %s%s" (show k) (show a)
+    show (Assume k a) = printf "assume %s%s" (show k) (show a)
+    show (Cover  k a) = printf  "cover %s%s" (show k) (show a)
 
-showAssertionExpr :: AssertionExpr -> String
-showAssertionExpr (Left e) = printf "property (%s\n)" (show e)
-showAssertionExpr (Right e) = printf "(%s)" (show e)
+data AssertionKind
+    = Concurrent PropertySpec
+    | Immediate Deferral Expr
+    deriving Eq
+instance Show AssertionKind where
+    show (Concurrent e) = printf "property (%s\n)" (show e)
+    show (Immediate d e) = printf "%s(%s)" (showPad d) (show e)
+
+data Deferral
+    = NotDeferred
+    | ObservedDeferred
+    | FinalDeferred
+    deriving Eq
+instance Show Deferral where
+    show NotDeferred = ""
+    show ObservedDeferred = "#0"
+    show FinalDeferred = "final"
 
 data PropertySpec
     = PropertySpec (Maybe Sense) Expr PropExpr

src/Language/SystemVerilog/Parser/Parse.y

@@ -733,16 +733,18 @@ ConcurrentAssertionItem :: { AssertionItem }
   : Identifier ":" ConcurrentAssertionStatement { ($1, $3) }
   |                ConcurrentAssertionStatement { ("", $1) }
 ConcurrentAssertionStatement :: { Assertion }
-  : "assert" "property" "(" PropertySpec ")" ActionBlock { Assert (Left $4) $6 }
-  | "assume" "property" "(" PropertySpec ")" ActionBlock { Assume (Left $4) $6 }
-  | "cover"  "property" "(" PropertySpec ")" Stmt        { Cover  (Left $4) $6 }
+  : "assert" "property" "(" PropertySpec ")" ActionBlock { Assert (Concurrent $4) $6 }
+  | "assume" "property" "(" PropertySpec ")" ActionBlock { Assume (Concurrent $4) $6 }
+  | "cover"  "property" "(" PropertySpec ")" Stmt        { Cover  (Concurrent $4) $6 }
 
 ImmediateAssertionStatement :: { Assertion }
-  : SimpleImmediateAssertionStatement { $1 }
-SimpleImmediateAssertionStatement :: { Assertion }
-  : "assert" "(" Expr ")" ActionBlock { Assert (Right $3) $5 }
-  | "assume" "(" Expr ")" ActionBlock { Assume (Right $3) $5 }
-  | "cover"  "(" Expr ")" Stmt        { Cover  (Right $3) $5 }
+  : "assert" Deferral "(" Expr ")" ActionBlock { Assert (Immediate $2 $4) $6 }
+  | "assume" Deferral "(" Expr ")" ActionBlock { Assume (Immediate $2 $4) $6 }
+  | "cover"  Deferral "(" Expr ")" Stmt        { Cover  (Immediate $2 $4) $6 }
+Deferral :: { Deferral }
+  : {- empty -} { NotDeferred }
+  | "#" number {% expectZeroDelay $2 ObservedDeferred }
+  | "final" { FinalDeferred }
 
 PropertySpec :: { PropertySpec }
   : opt(ClockingEvent) "disable" "iff" "(" Expr ")" PropExpr { PropertySpec $1 $5  $7 }
@@ -1682,4 +1684,12 @@ readNumber pos str = do
     hPutStrLn stderr $ show pos ++ ": Warning: " ++ msg
   return num
 
+expectZeroDelay :: Token -> a -> ParseState a
+expectZeroDelay tok a = do
+  num <- readNumber pos str
+  case num of
+    Decimal (-32) True 0 -> return a
+    _ -> parseError pos $ "expected 0 after #, but found " ++ str
+  where Token { tokenString = str, tokenPosition = pos } = tok
+
 }

test/error/assert_deferred_nonzero.sv

@@ -0,0 +1,4 @@
+// pattern: assert_deferred_nonzero.sv:3:21: Parse error: expected 0 after #, but found 1
+module top;
+    initial assert #1 (1);
+endmodule

test/nosim/assert.sv

@@ -12,7 +12,15 @@ module top;
         assert (1);
         assume (1);
         cover (1);
-        assume (1);
+        assert #0 (1);
+        assume #0 (1);
+        cover #0 (1);
+        assert #0_0 (1);
+        assume #0_0 (1);
+        cover #0_0 (1);
+        assert final (1);
+        assume final (1);
+        cover final (1);
     end
     assert property (@(posedge clk) 1)
         else $display("FOO");