significantly stronger support, and proper handling of assertions

src/Convert.hs

@@ -11,6 +11,7 @@ import qualified Job (Exclude(..))
 
 import qualified Convert.AlwaysKW
 import qualified Convert.AsgnOp
+import qualified Convert.Assertion
 import qualified Convert.Bits
 import qualified Convert.Enum
 import qualified Convert.FuncRet
@@ -31,6 +32,7 @@ type Phase = AST -> AST
 phases :: [Job.Exclude] -> [Phase]
 phases excludes =
     [ Convert.AsgnOp.convert
+    , Convert.Assertion.convert
     , Convert.Bits.convert
     , selectExclude (Job.Logic    , Convert.Logic.convert)
     , Convert.FuncRet.convert

src/Convert/Assertion.hs

@@ -0,0 +1,22 @@
+{- sv2v
+ - Author: Zachary Snow <zach@zachjs.com>
+ -
+ - Conversion which simply removes assertions
+ -}
+
+module Convert.Assertion (convert) where
+
+import Convert.Traverse
+import Language.SystemVerilog.AST
+
+convert :: AST -> AST
+convert = traverseDescriptions $ traverseModuleItems convertModuleItem
+
+convertModuleItem :: ModuleItem -> ModuleItem
+convertModuleItem (AssertionItem _) =
+    MIPackageItem $ Comment "removed an assertion item"
+convertModuleItem other = traverseStmts convertStmt other
+
+convertStmt :: Stmt -> Stmt
+convertStmt (Assertion _) = Null
+convertStmt other = other

src/Convert/Traverse.hs

@@ -195,8 +195,113 @@ traverseNestedStmtsM mapper = fullMapper
         cs (Return expr) = return $ Return expr
         cs (Subroutine f exprs) = return $ Subroutine f exprs
         cs (Trigger x) = return $ Trigger x
+        cs (Assertion a) =
+            traverseAssertionStmtsM fullMapper a >>= return . Assertion
         cs (Null) = return Null
 
+traverseAssertionStmtsM :: Monad m => MapperM m Stmt -> MapperM m Assertion
+traverseAssertionStmtsM mapper = assertionMapper
+    where
+        actionBlockMapper (ActionBlockIf stmt) =
+            mapper stmt >>= return . ActionBlockIf
+        actionBlockMapper (ActionBlockElse Nothing stmt) =
+            mapper stmt >>= return . ActionBlockElse Nothing
+        actionBlockMapper (ActionBlockElse (Just s1) s2) = do
+            s1' <- mapper s1
+            s2' <- mapper s2
+            return $ ActionBlockElse (Just s1') s2'
+        assertionMapper (Assert e ab) =
+            actionBlockMapper ab >>= return . Assert e
+        assertionMapper (Assume e ab) =
+            actionBlockMapper ab >>= return . Assume e
+        assertionMapper (Cover e stmt) =
+            mapper stmt >>= return . Cover e
+
+-- 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 e s) = do
+            ms' <- case ms of
+                Nothing -> return Nothing
+                Just x -> seqExprMapper x >>= return . Just
+            e' <- mapper e
+            s' <- seqExprMapper s
+            return $ SeqExprDelay ms' e' s'
+        seqExprMapper (SeqExprFirstMatch s items) = do
+            s' <- seqExprMapper s
+            items' <- mapM seqMatchItemMapper items
+            return $ SeqExprFirstMatch s' items'
+        seqMatchItemMapper (Left (a, b, c)) = do
+            c' <- mapper c
+            return $ Left (a, b, c')
+        seqMatchItemMapper (Right (x, (Args l p))) = do
+            l' <- mapM maybeExprMapper l
+            pes <- mapM maybeExprMapper $ map snd p
+            let p' = zip (map fst p) pes
+            return $ Right (x, Args l' p')
+        maybeExprMapper Nothing = return Nothing
+        maybeExprMapper (Just e) =
+            mapper e >>= return . Just
+        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 ms me pe) = do
+            me' <- case me of
+                Nothing -> return Nothing
+                Just e -> mapper e >>= return . Just
+            pe' <- propExprMapper pe
+            return $ PropertySpec ms me' pe'
+        assertionExprMapper (Left e) =
+            propSpecMapper e >>= return . Left
+        assertionExprMapper (Right e) =
+            mapper e >>= return . Right
+        assertionMapper (Assert e ab) = do
+            e' <- assertionExprMapper e
+            return $ Assert e' ab
+        assertionMapper (Assume e ab) = do
+            e' <- assertionExprMapper e
+            return $ Assume e' ab
+        assertionMapper (Cover e stmt) = do
+            e' <- assertionExprMapper e
+            return $ Cover e' stmt
+
 traverseStmtLHSsM :: Monad m => MapperM m LHS -> MapperM m Stmt
 traverseStmtLHSsM mapper = traverseNestedStmtsM stmtMapper
     where
@@ -210,6 +315,8 @@ traverseStmtLHSsM mapper = traverseNestedStmtsM stmtMapper
             return $ Asgn (Just $ Event sense') lhs' expr
         stmtMapper (AsgnBlk op lhs expr) = fullMapper lhs >>= \lhs' -> return $ AsgnBlk op lhs' expr
         stmtMapper (Asgn    mt lhs expr) = fullMapper lhs >>= \lhs' -> return $ Asgn    mt lhs' expr
+        stmtMapper (Assertion a) =
+            assertionMapper a >>= return . Assertion
         stmtMapper other = return other
         senseMapper (Sense        lhs) = fullMapper lhs >>= return . Sense
         senseMapper (SensePosedge lhs) = fullMapper lhs >>= return . SensePosedge
@@ -219,6 +326,19 @@ traverseStmtLHSsM mapper = traverseNestedStmtsM stmtMapper
             s2' <- senseMapper s2
             return $ SenseOr s1' s2'
         senseMapper (SenseStar       ) = return SenseStar
+        assertionExprMapper (Left (PropertySpec (Just sense) me pe)) = do
+            sense' <- senseMapper sense
+            return $ Left $ PropertySpec (Just sense') me pe
+        assertionExprMapper other = return $ other
+        assertionMapper (Assert e ab) = do
+            e' <- assertionExprMapper e
+            return $ Assert e' ab
+        assertionMapper (Assume e ab) = do
+            e' <- assertionExprMapper e
+            return $ Assume e' ab
+        assertionMapper (Cover e stmt) = do
+            e' <- assertionExprMapper e
+            return $ Cover e' stmt
 
 traverseStmtLHSs :: Mapper LHS -> Mapper Stmt
 traverseStmtLHSs = unmonad traverseStmtLHSsM
@@ -348,6 +468,10 @@ traverseExprsM' strat mapper = moduleItemMapper
     flatStmtMapper (Return expr) =
         exprMapper expr >>= return . Return
     flatStmtMapper (Trigger x) = return $ Trigger x
+    flatStmtMapper (Assertion a) = do
+        a' <- traverseAssertionStmtsM stmtMapper a
+        a'' <- traverseAssertionExprsM exprMapper a'
+        return $ Assertion a''
     flatStmtMapper (Null) = return Null
 
     initMapper (Left decl) = declMapper decl >>= return . Left
@@ -413,6 +537,10 @@ traverseExprsM' strat mapper = moduleItemMapper
         return $ MIPackageItem $ Typedef t x
     moduleItemMapper (MIPackageItem (Comment c)) =
         return $ MIPackageItem $ Comment c
+    moduleItemMapper (AssertionItem (mx, a)) = do
+        a' <- traverseAssertionStmtsM stmtMapper a
+        a'' <- traverseAssertionExprsM exprMapper a'
+        return $ AssertionItem (mx, a'')
 
     genItemMapper (GenFor (x1, e1) cc (x2, op2, e2) mn subItems) = do
         e1' <- exprMapper e1
@@ -462,6 +590,9 @@ traverseLHSsM' strat mapper item =
         traverseModuleItemLHSsM (NInputGate  kw x lhs exprs) = do
             lhs' <- mapper lhs
             return $ NInputGate kw x lhs' exprs
+        traverseModuleItemLHSsM (AssertionItem (mx, a)) = do
+            Assertion a' <- traverseStmtLHSsM mapper (Assertion a)
+            return $ AssertionItem (mx, a')
         traverseModuleItemLHSsM other = return other
 
 traverseLHSs' :: TFStrategy -> Mapper LHS -> Mapper ModuleItem

src/Language/SystemVerilog/AST.hs

@@ -128,8 +128,7 @@ data ModuleItem
   | MIPackageItem PackageItem
   | NInputGate  NInputGateKW  (Maybe Identifier)  LHS [Expr]
   | NOutputGate NOutputGateKW (Maybe Identifier) [LHS] Expr
-  -- TODO: Should we support coversion of assertions?
+  | AssertionItem AssertionItem
-  -- | AssertionItem AssertionItem
   deriving Eq
 
 data AlwaysKW
@@ -167,7 +166,8 @@ instance Show ModuleItem where
     MIPackageItem i  -> show i
     NInputGate  kw x lhs  exprs -> printf "%s%s (%s, %s);" (show kw) (maybe "" (" " ++) x) (show lhs) (commas $ map show exprs)
     NOutputGate kw x lhss expr  -> printf "%s%s (%s, %s);" (show kw) (maybe "" (" " ++) x) (commas $ map show lhss) (show expr)
-    --AssertionItem a -> show a
+    AssertionItem (Nothing, a) -> show a
+    AssertionItem (Just x, a) -> printf "%s : %s" x (show a)
     where
     showPorts :: [PortBinding] -> String
     showPorts ports = indentedParenList $ map showPort ports

src/Language/SystemVerilog/AST/Stmt.hs

@@ -16,6 +16,7 @@ module Language.SystemVerilog.AST.Stmt
     , SeqMatchItem
     , SeqExpr      (..)
     , AssertionItem
+    , AssertionExpr
     , Assertion    (..)
     , PropertySpec (..)
     , UniquePriority (..)
@@ -47,8 +48,7 @@ data Stmt
     | Return  Expr
     | Subroutine Identifier Args
     | Trigger Identifier
-    -- TODO: Should we support coversion of assertions?
+    | Assertion Assertion
-    -- | Assertion Assertion
     | Null
     deriving Eq
 
@@ -91,7 +91,7 @@ instance Show Stmt where
     show (Return e   ) = printf "return %s;" (show e)
     show (Timing t s ) = printf "%s %s" (show t) (show s)
     show (Trigger x  ) = printf "-> %s;" x
-    --show (Assertion a) = show a
+    show (Assertion a) = show a
     show (Null       ) = ";"
 
 data CaseKW
@@ -180,23 +180,31 @@ instance Show SeqExpr where
     show (SeqExprFirstMatch e a) = printf "first_match(%s, %s)" (show e) (show a)
 
 type AssertionItem = (Maybe Identifier, Assertion)
+type AssertionExpr = Either PropertySpec Expr
 data Assertion
-    = Assert         Expr         ActionBlock
+    = Assert AssertionExpr ActionBlock
-    | AssertProperty PropertySpec ActionBlock
+    | Assume AssertionExpr ActionBlock
+    | Cover  AssertionExpr Stmt
     deriving Eq
 instance Show Assertion where
-    show (Assert e a) =
+    show (Assert e a) = printf "assert %s%s" (showAssertionExpr e) (show a)
-        printf "assert (%s)%s" (show e) (show a)
+    show (Assume e a) = printf "assume %s%s" (showAssertionExpr e) (show a)
-    show (AssertProperty p a) =
+    show (Cover  e a) = printf  "cover %s%s" (showAssertionExpr e) (show a)
-        printf "assert property (%s)%s" (show p) (show a)
+
+showAssertionExpr :: AssertionExpr -> String
+showAssertionExpr (Left e) = printf "property (%s)" (show e)
+showAssertionExpr (Right e) = printf "(%s)" (show e)
 
 data PropertySpec
     = PropertySpec (Maybe Sense) (Maybe Expr) PropExpr
     deriving Eq
 instance Show PropertySpec where
     show (PropertySpec ms me pe) =
-        printf "%s%s%s" (maybe "" showPad ms) meStr (show pe)
+        printf "%s%s%s" msStr meStr (show pe)
         where
+            msStr = case ms of
+                Nothing -> ""
+                Just s -> printf "@(%s) " (show s)
             meStr = case me of
                 Nothing -> ""
                 Just e -> printf "disable iff (%s) " (show e)

src/Language/SystemVerilog/Parser/Lex.x

@@ -113,6 +113,7 @@ tokens :-
     "and"              { tok KW_and          }
     "assert"           { tok KW_assert       }
     "assign"           { tok KW_assign       }
+    "assume"           { tok KW_assume       }
     "automatic"        { tok KW_automatic    }
     "begin"            { tok KW_begin        }
     "bit"              { tok KW_bit          }
@@ -121,6 +122,7 @@ tokens :-
     "case"             { tok KW_case         }
     "casex"            { tok KW_casex        }
     "casez"            { tok KW_casez        }
+    "cover"            { tok KW_cover        }
     "default"          { tok KW_default      }
     "defparam"         { tok KW_defparam     }
     "disable"          { tok KW_disable      }

src/Language/SystemVerilog/Parser/Parse.y

@@ -33,6 +33,7 @@ import Language.SystemVerilog.Parser.Tokens
 "and"              { Token KW_and          _ _ }
 "assert"           { Token KW_assert       _ _ }
 "assign"           { Token KW_assign       _ _ }
+"assume"           { Token KW_assume       _ _ }
 "automatic"        { Token KW_automatic    _ _ }
 "begin"            { Token KW_begin        _ _ }
 "bit"              { Token KW_bit          _ _ }
@@ -41,6 +42,7 @@ import Language.SystemVerilog.Parser.Tokens
 "case"             { Token KW_case         _ _ }
 "casex"            { Token KW_casex        _ _ }
 "casez"            { Token KW_casez        _ _ }
+"cover"            { Token KW_cover        _ _ }
 "default"          { Token KW_default      _ _ }
 "defparam"         { Token KW_defparam     _ _ }
 "disable"          { Token KW_disable      _ _ }
@@ -440,7 +442,7 @@ ModuleItem :: { [ModuleItem] }
   | NInputGateKW  NInputGates  ";"       { map (\(a, b, c) -> NInputGate  $1 a b c) $2 }
   | NOutputGateKW NOutputGates ";"       { map (\(a, b, c) -> NOutputGate $1 a b c) $2 }
   | AttributeInstance ModuleItem         { map (MIAttr $1) $2 }
-  | AssertionItem                        { [] } -- AssertionItem $1] }
+  | AssertionItem                        { [AssertionItem $1] }
 
 -- for ModuleItem, for now
 AssertionItem :: { AssertionItem }
@@ -455,14 +457,16 @@ ConcurrentAssertionItem :: { AssertionItem }
   : Identifier ":" ConcurrentAssertionStatement { (Just $1, $3) }
   |                ConcurrentAssertionStatement { (Nothing, $1) }
 ConcurrentAssertionStatement :: { Assertion }
-  : "assert" "property" "(" PropertySpec ")" ActionBlock { AssertProperty $4 $6 }
+  : "assert" "property" "(" PropertySpec ")" ActionBlock { Assert (Left $4) $6 }
-  -- TODO: Add support for assume, cover, and restrict
+  | "assume" "property" "(" PropertySpec ")" ActionBlock { Assume (Left $4) $6 }
+  | "cover"  "property" "(" PropertySpec ")" Stmt        { Cover  (Left $4) $6 }
 
 ImmediateAssertionStatement :: { Assertion }
   : SimpleImmediateAssertionStatement { $1 }
 SimpleImmediateAssertionStatement :: { Assertion }
-  : "assert" "(" Expr ")" ActionBlock { Assert $3 $5 }
+  : "assert" "(" Expr ")" ActionBlock { Assert (Right $3) $5 }
-  -- TODO: Add support for assume and cover
+  | "assume" "(" Expr ")" ActionBlock { Assume (Right $3) $5 }
+  | "cover"  "(" Expr ")" Stmt        { Cover  (Right $3) $5 }
 
 PropertySpec :: { PropertySpec }
   : opt(ClockingEvent) "disable" "iff" "(" Expr ")" PropExpr { PropertySpec $1 (Just $5) $7 }
@@ -470,15 +474,19 @@ PropertySpec :: { PropertySpec }
 
 PropExpr :: { PropExpr }
   : SeqExpr { PropExpr $1 }
+  | PropExprParens { $1 }
+PropExprParens :: { PropExpr }
+  : "(" PropExprParens ")" { $2 }
   | SeqExpr "|->" PropExpr { PropExprImpliesO  $1 $3 }
   | SeqExpr "|=>" PropExpr { PropExprImpliesNO $1 $3 }
   | SeqExpr "#-#" PropExpr { PropExprFollowsO  $1 $3 }
   | SeqExpr "#=#" PropExpr { PropExprFollowsNO $1 $3 }
   | PropExpr "iff" PropExpr { PropExprIff $1 $3 }
-  -- | "(" PropExpr ")"  { $2 }
-
 SeqExpr :: { SeqExpr }
   : Expr { SeqExpr $1 }
+  | SeqExprParens { $1 }
+SeqExprParens :: { SeqExpr }
+  : "(" SeqExprParens ")" { $2 }
   | SeqExpr "and"        SeqExpr { SeqExprAnd        $1 $3 }
   | SeqExpr "or"         SeqExpr { SeqExprOr         $1 $3 }
   | SeqExpr "intersect"  SeqExpr { SeqExprIntersect  $1 $3 }
@@ -649,7 +657,7 @@ StmtNonAsgn :: { Stmt }
   | "forever" Stmt                             { Forever $2 }
   | "->" Identifier ";"                        { Trigger $2 }
   | AttributeInstance Stmt                     { StmtAttr $1 $2 }
-  | ProceduralAssertionStatement               { Null } --Assertion $1 }
+  | ProceduralAssertionStatement               { Assertion $1 }
 
 Unique :: { Maybe UniquePriority }
   : {- empty -} { Nothing }

sv2v.cabal

@@ -51,6 +51,7 @@ executable sv2v
     Convert
     Convert.AlwaysKW
     Convert.AsgnOp
+    Convert.Assertion
     Convert.Bits
     Convert.Enum
     Convert.FuncRet