Support SVA assert/assume

pyverilog/ast_code_generator/codegen.py

@@ -644,6 +644,43 @@ def visit_Assign(self, node):
         rslt = template.render(template_dict)
         rslt = indent_multiline_assign(rslt)
         return rslt
+
+    def visit_Assert(self, node):
+        filename = getfilename(node)
+        template = self.get_template(filename)
+        template_dict = {
+            'expr': self.visit(node.expr)
+        }
+        rslt = template.render(template_dict)
+        return rslt
+
+    def visit_Assume(self, node):
+        filename = getfilename(node)
+        template = self.get_template(filename)
+        template_dict = {
+            'expr': self.visit(node.expr)
+        }
+        rslt = template.render(template_dict)
+        return rslt
+
+
+    def visit_AssertStatement(self, node):
+        filename = getfilename(node)
+        template = self.get_template(filename)
+        template_dict = {
+            'statement': self.visit(node.statement)
+        }
+        rslt = template.render(template_dict)
+        return rslt
+
+    def visit_AssumeStatement(self, node):
+        filename = getfilename(node)
+        template = self.get_template(filename)
+        template_dict = {
+            'statement': self.visit(node.statement)
+        }
+        rslt = template.render(template_dict)
+        return rslt
 
     def visit_Always(self, node):
         filename = getfilename(node)

pyverilog/ast_code_generator/template/assert.txt

@@ -0,0 +1 @@
+assert property ( {{ expr }} );

pyverilog/ast_code_generator/template/assertstatement.txt

@@ -0,0 +1 @@
+assert ( {{ statement }} );

pyverilog/ast_code_generator/template/assume.txt

@@ -0,0 +1 @@
+assume property ( {{ expr }} );

pyverilog/ast_code_generator/template/assumestatement.txt

@@ -0,0 +1 @@
+assume ( {{ statement }} );

pyverilog/vparser/ast.py

@@ -691,6 +691,32 @@ def children(self):
             nodelist.append(self.false_value)
         return tuple(nodelist)
 
+class Assert(Node):
+    attr_names = ()
+
+    def __init__(self, expr, lineno=0):
+        self.lineno = lineno
+        self.expr = expr
+
+    def children(self):
+        nodelist = []
+        if self.expr:
+            nodelist.append(self.expr)
+        return tuple(nodelist)
+
+class Assume(Node):
+    attr_names = ()
+
+    def __init__(self, expr, lineno=0):
+        self.lineno = lineno
+        self.expr = expr
+
+    def children(self):
+        nodelist = []
+        if self.expr:
+            nodelist.append(self.expr)
+        return tuple(nodelist)
+
 
 class Assign(Node):
     attr_names = ()
@@ -1278,6 +1304,33 @@ def children(self):
         return tuple(nodelist)
 
 
+class AssumeStatement(Node):
+    attr_names = ()
+
+    def __init__(self, statement, lineno=0):
+        self.lineno = lineno
+        self.statement = statement
+
+    def children(self):
+        nodelist = []
+        if self.statement:
+            nodelist.append(self.statement)
+        return tuple(nodelist)
+
+class AssertStatement(Node):
+    attr_names = ()
+
+    def __init__(self, statement, lineno=0):
+        self.lineno = lineno
+        self.statement = statement
+
+    def children(self):
+        nodelist = []
+        if self.statement:
+            nodelist.append(self.statement)
+        return tuple(nodelist)
+
+
 class EmbeddedCode(Node):
     attr_names = ('code',)
 

pyverilog/vparser/lexer.py

@@ -57,7 +57,7 @@ def token(self):
         'PARAMETER', 'LOCALPARAM', 'SUPPLY0', 'SUPPLY1',
         'ASSIGN', 'ALWAYS', 'ALWAYS_FF', 'ALWAYS_COMB', 'ALWAYS_LATCH', 'SENS_OR', 'POSEDGE', 'NEGEDGE', 'INITIAL',
         'IF', 'ELSE', 'FOR', 'WHILE', 'CASE', 'CASEX', 'CASEZ', 'UNIQUE', 'ENDCASE', 'DEFAULT',
-        'WAIT', 'FOREVER', 'DISABLE', 'FORK', 'JOIN',
+        'WAIT', 'FOREVER', 'DISABLE', 'FORK', 'JOIN', 'ASSERT', 'ASSUME', 'PROPERTY'
     )
 
     reserved = {}

pyverilog/vparser/parser.py

@@ -510,6 +510,8 @@ def p_standard_item(self, p):
         | function
         | task
         | pragma
+        | assert
+        | assume
         """
         p[0] = p[1]
         p.set_lineno(0, p.lineno(1))
@@ -845,6 +847,16 @@ def p_assignment_delay(self, p):
         'assignment : ASSIGN delays lvalue EQUALS delays rvalue SEMICOLON'
         p[0] = Assign(p[3], p[6], p[2], p[5], lineno=p.lineno(1))
         p.set_lineno(0, p.lineno(1))
+
+    def p_assert(self, p):
+        'assert : ASSERT PROPERTY LPAREN rvalue RPAREN SEMICOLON'
+        p[0] = Assert(p[4], lineno=p.lineno(1))
+        p.set_lineno(0, p.lineno(1))
+
+    def p_assume(self, p):
+        'assume : ASSUME PROPERTY LPAREN rvalue RPAREN SEMICOLON'
+        p[0] = Assume(p[4], lineno=p.lineno(1))
+        p.set_lineno(0, p.lineno(1))
 
     # --------------------------------------------------------------------------
     def p_lpartselect_lpointer(self, p):
@@ -1435,6 +1447,8 @@ def p_basic_statement(self, p):
         | blocking_substitution
         | nonblocking_substitution
         | single_statement
+        | assert_statement
+        | assume_statement
         """
         p[0] = p[1]
         p.set_lineno(0, p.lineno(1))
@@ -2242,6 +2256,17 @@ def p_single_statement_disable(self, p):
         p[0] = SingleStatement(p[1], lineno=p.lineno(1))
         p.set_lineno(0, p.lineno(1))
 
+    def p_assert_statement_disable(self, p):
+        'assert_statement : ASSERT LPAREN expression RPAREN SEMICOLON'
+        p[0] = AssertStatement(p[3], lineno=p.lineno(1))
+        p.set_lineno(0, p.lineno(1))
+
+    def p_assume_statement_disable(self, p):
+        'assume_statement : ASSUME LPAREN expression RPAREN SEMICOLON'
+        p[0] = AssumeStatement(p[3], lineno=p.lineno(1))
+        p.set_lineno(0, p.lineno(1))
+
+
     # fix me: to support task-call-statement
     # def p_single_statement_taskcall(self, p):
     #    'single_statement : functioncall SEMICOLON'