fix codegen for assertion property and sequence expressions

- updated representation and added codegen for sequence match items
- fix incorrect codegen for `iff` property expression

src/Convert/Traverse.hs

@@ -309,14 +309,14 @@ traverseAssertionExprsM mapper = assertionMapper
             s' <- seqExprMapper s
             items' <- mapM seqMatchItemMapper items
             return $ SeqExprFirstMatch s' items'
-        seqMatchItemMapper (Left (a, b, c)) = do
+        seqMatchItemMapper (SeqMatchAsgn (a, b, c)) = do
             c' <- mapper c
-            return $ Left (a, b, c')
+            return $ SeqMatchAsgn (a, b, c')
-        seqMatchItemMapper (Right (x, (Args l p))) = do
+        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 $ Right (x, Args l' p')
+            return $ SeqMatchCall x (Args l' p')
         ppMapper constructor p1 p2 = do
             p1' <- propExprMapper p1
             p2' <- propExprMapper p2

src/Language/SystemVerilog/AST/Stmt.hs

@@ -13,7 +13,7 @@ module Language.SystemVerilog.AST.Stmt
     , Case
     , ActionBlock  (..)
     , PropExpr     (..)
-    , SeqMatchItem
+    , SeqMatchItem (..)
     , SeqExpr      (..)
     , AssertionItem
     , AssertionExpr
@@ -28,7 +28,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(Nil), Args(..))
+import Language.SystemVerilog.AST.Expr (Expr(Call, Ident, Nil), Args(..))
 import Language.SystemVerilog.AST.LHS (LHS)
 import Language.SystemVerilog.AST.Op (AsgnOp(AsgnOpEq))
 import Language.SystemVerilog.AST.Type (Identifier)
@@ -80,8 +80,6 @@ instance Show Stmt where
             showInits :: [(LHS, Expr)] -> String
             showInits = commas . map showInit
                 where showInit (l, e) = showAssign (l, AsgnOpEq, e)
-            showAssign :: (LHS, AsgnOp, Expr) -> String
-            showAssign (l, op, e) = (showPad l) ++ (showPad op) ++ (show e)
     show (Subroutine e a) = printf "%s%s;" (show e) aStr
         where aStr = if a == Args [] [] then "" else show a
     show (Asgn  o t v e) = printf "%s %s %s%s;" (show v) (show o) tStr (show e)
@@ -105,6 +103,9 @@ instance Show Stmt where
             then "// " ++ show c
             else "// " ++ c
 
+showAssign :: (LHS, AsgnOp, Expr) -> String
+showAssign (l, op, e) = (showPad l) ++ (showPad op) ++ (show e)
+
 showBranch :: Stmt -> String
 showBranch (Block Seq "" [] (stmts @ [CommentStmt{}, _])) =
     '\n' : (indent $ show stmts)
@@ -208,8 +209,14 @@ instance Show PropExpr where
     show (PropExprImpliesNO a b) = printf "(%s |=> %s)" (show a) (show b)
     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 and %s)" (show a) (show b)
+    show (PropExprIff a b) = printf "(%s iff %s)" (show a) (show b)
-type SeqMatchItem = Either (LHS, AsgnOp, Expr) (Identifier, Args)
+data SeqMatchItem
+    = SeqMatchAsgn (LHS, AsgnOp, Expr)
+    | SeqMatchCall Identifier Args
+    deriving Eq
+instance Show SeqMatchItem where
+    show (SeqMatchAsgn asgn) = showAssign asgn
+    show (SeqMatchCall ident args) = show $ Call (Ident ident) args
 data SeqExpr
     = SeqExpr Expr
     | SeqExprAnd        SeqExpr SeqExpr
@@ -228,7 +235,7 @@ instance Show SeqExpr where
     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 (SeqExprFirstMatch e a) = printf "first_match(%s, %s)" (show e) (show a)
+    show (SeqExprFirstMatch e a) = printf "first_match(%s, %s)" (show e) (commas $ map show a)
 
 type AssertionItem = (Identifier, Assertion)
 type AssertionExpr = Either PropertySpec Expr

src/Language/SystemVerilog/Parser/Parse.y

@@ -774,8 +774,8 @@ SeqMatchItems :: { [SeqMatchItem] }
   : "," SeqMatchItem               { [$2] }
   | SeqMatchItems "," SeqMatchItem { $1 ++ [$3] }
 SeqMatchItem :: { SeqMatchItem }
-  : ForStepAssignment   { Left $1 }
+  : ForStepAssignment   { SeqMatchAsgn $1 }
-  | Identifier CallArgs { Right ($1, $2) }
+  | Identifier CallArgs { SeqMatchCall $1 $2 }
 
 ActionBlock :: { ActionBlock }
   : Stmt %prec NoElse { ActionBlock $1 Null }

test/nosim/assert.sv

@@ -0,0 +1,31 @@
+module top;
+    reg clk;
+    initial begin
+        clk = 0;
+        repeat (100) #1 clk = ~clk;
+        $finish;
+    end
+    assert property (@(posedge clk) 1);
+    assume property (@(posedge clk) 1);
+    cover property (@(posedge clk) 1);
+    initial begin
+        assert (1);
+        assume (1);
+        cover (1);
+        assume (1);
+    end
+    assert property (@(posedge clk) 1)
+        else $display("FOO");
+    assume property (@(posedge clk) 1)
+            $display("FOO");
+        else
+            $display("BAR");
+    assert property (@(posedge clk)
+        (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) 1 ##1 1);
+    assert property (@(posedge clk) ##1 1);
+    integer x;
+    assert property (@(posedge clk) first_match(1, x++, $display("a", clk), $display("b", clk)));
+endmodule