sv: extended support for integer types

- Standard data declarations can now use any integer type
- Parameters and localparams can now use any integer type
- Function returns types can now use any integer type
- Fix `parameter logic`, `localparam reg`, etc. to be 1 bit (previously 32 bits)
- Added longint type (64 bits)
- Unified parser source for integer type widths

diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index eeb7440f81f963962fc8db91f597943f458543e2..66772a097580b1d4e496797f79186e2799b7cc8b 100644 (file)
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -267,6 +267,7 @@ static bool isUserType(std::string &s)
 "int"        { SV_KEYWORD(TOK_INT); }
 "byte"       { SV_KEYWORD(TOK_BYTE); }
 "shortint"   { SV_KEYWORD(TOK_SHORTINT); }
+"longint"    { SV_KEYWORD(TOK_LONGINT); }
 
 "eventually"   { if (formal_mode) return TOK_EVENTUALLY; SV_KEYWORD(TOK_EVENTUALLY); }
 "s_eventually" { if (formal_mode) return TOK_EVENTUALLY; SV_KEYWORD(TOK_EVENTUALLY); }

diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index dc7ec8348735c75f81c1b8d5baff673e423fd901..476ee68ad1e155b62330f094f442e804444804d7 100644 (file)
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -253,6 +253,7 @@ static void rewriteAsMemoryNode(AstNode *node, AstNode *rangeNode)
        struct specify_rise_fall *specify_rise_fall_ptr;
        bool boolean;
        char ch;
+       int integer;
 }
 
 %token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE
@@ -278,15 +279,17 @@ static void rewriteAsMemoryNode(AstNode *node, AstNode *rangeNode)
 %token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
 %token TOK_RAND TOK_CONST TOK_CHECKER TOK_ENDCHECKER TOK_EVENTUALLY
 %token TOK_INCREMENT TOK_DECREMENT TOK_UNIQUE TOK_UNIQUE0 TOK_PRIORITY
-%token TOK_STRUCT TOK_PACKED TOK_UNSIGNED TOK_INT TOK_BYTE TOK_SHORTINT TOK_UNION
+%token TOK_STRUCT TOK_PACKED TOK_UNSIGNED TOK_INT TOK_BYTE TOK_SHORTINT TOK_LONGINT TOK_UNION
 %token TOK_OR_ASSIGN TOK_XOR_ASSIGN TOK_AND_ASSIGN TOK_SUB_ASSIGN
 
-%type <ast> range range_or_multirange  non_opt_range non_opt_multirange range_or_signed_int
+%type <ast> range range_or_multirange non_opt_range non_opt_multirange
 %type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list non_io_wire_type io_wire_type
 %type <string> opt_label opt_sva_label tok_prim_wrapper hierarchical_id hierarchical_type_id integral_number
 %type <string> type_name
-%type <ast> opt_enum_init enum_type struct_type non_wire_data_type
-%type <boolean> opt_signed opt_property always_comb_or_latch always_or_always_ff
+%type <ast> opt_enum_init enum_type struct_type non_wire_data_type func_return_type
+%type <boolean> opt_property always_comb_or_latch always_or_always_ff
+%type <boolean> opt_signedness_default_signed opt_signedness_default_unsigned
+%type <integer> integer_atom_type
 %type <al> attr case_attr
 %type <ast> struct_union
 
@@ -716,12 +719,19 @@ wire_type_token:
 logic_type:
        TOK_LOGIC {
        } |
-       TOK_INTEGER {
-               astbuf3->range_left = 31;
+       integer_atom_type {
+               astbuf3->range_left = $1 - 1;
                astbuf3->range_right = 0;
                astbuf3->is_signed = true;
        };
 
+integer_atom_type:
+       TOK_INTEGER     { $$ = 32; } |
+       TOK_INT         { $$ = 32; } |
+       TOK_SHORTINT    { $$ = 16; } |
+       TOK_LONGINT     { $$ = 64; } |
+       TOK_BYTE        { $$ =  8; } ;
+
 non_opt_range:
        '[' expr ':' expr ']' {
                $$ = new AstNode(AST_RANGE);
@@ -766,11 +776,6 @@ range_or_multirange:
        range { $$ = $1; } |
        non_opt_multirange { $$ = $1; };
 
-range_or_signed_int:
-         range                 { $$ = $1; }
-       | TOK_INTEGER           { $$ = makeRange(); }
-       ;
-
 module_body:
        module_body module_body_stmt |
        /* the following line makes the generate..endgenrate keywords optional */
@@ -841,29 +846,58 @@ task_func_decl:
                current_function_or_task = NULL;
                ast_stack.pop_back();
        } |
-       attr TOK_FUNCTION opt_automatic opt_signed range_or_signed_int TOK_ID {
+       attr TOK_FUNCTION opt_automatic func_return_type TOK_ID {
                current_function_or_task = new AstNode(AST_FUNCTION);
-               current_function_or_task->str = *$6;
+               current_function_or_task->str = *$5;
                append_attr(current_function_or_task, $1);
                ast_stack.back()->children.push_back(current_function_or_task);
                ast_stack.push_back(current_function_or_task);
                AstNode *outreg = new AstNode(AST_WIRE);
-               outreg->str = *$6;
-               outreg->is_signed = $4;
+               outreg->str = *$5;
+               outreg->is_signed = false;
                outreg->is_reg = true;
-               if ($5 != NULL) {
-                       outreg->children.push_back($5);
-                       outreg->is_signed = $4 || $5->is_signed;
-                       $5->is_signed = false;
+               if ($4 != NULL) {
+                       outreg->children.push_back($4);
+                       outreg->is_signed = $4->is_signed;
+                       $4->is_signed = false;
                }
                current_function_or_task->children.push_back(outreg);
                current_function_or_task_port_id = 1;
-               delete $6;
+               delete $5;
        } task_func_args_opt ';' task_func_body TOK_ENDFUNCTION {
                current_function_or_task = NULL;
                ast_stack.pop_back();
        };
 
+func_return_type:
+       opt_type_vec opt_signedness_default_unsigned {
+               $$ = makeRange(0, 0, $2);
+       } |
+       opt_type_vec opt_signedness_default_unsigned non_opt_range {
+               $$ = $3;
+               $$->is_signed = $2;
+       } |
+       integer_atom_type opt_signedness_default_signed {
+               $$ = makeRange($1 - 1, 0, $2);
+       };
+
+opt_type_vec:
+         %empty
+       | TOK_REG
+       | TOK_LOGIC
+       ;
+
+opt_signedness_default_signed:
+         %empty        { $$ = true; }
+       | TOK_SIGNED    { $$ = true; }
+       | TOK_UNSIGNED  { $$ = false; }
+       ;
+opt_signedness_default_unsigned:
+         %empty        { $$ = false; }
+       | TOK_SIGNED    { $$ = true; }
+       | TOK_UNSIGNED  { $$ = false; }
+       ;
+
 dpi_function_arg:
        TOK_ID TOK_ID {
                current_function_or_task->children.push_back(AstNode::mkconst_str(*$1));
@@ -889,14 +923,6 @@ opt_automatic:
        TOK_AUTOMATIC |
        %empty;
 
-opt_signed:
-       TOK_SIGNED {
-               $$ = true;
-       } |
-       %empty {
-               $$ = false;
-       };
-
 task_func_args_opt:
        '(' ')' | %empty | '(' {
                albuf = nullptr;
@@ -1379,11 +1405,8 @@ param_signed:
        } | %empty;
 
 param_integer:
-       TOK_INTEGER {
-               astbuf1->children.push_back(new AstNode(AST_RANGE));
-               astbuf1->children.back()->children.push_back(AstNode::mkconst_int(31, true));
-               astbuf1->children.back()->children.push_back(AstNode::mkconst_int(0, true));
-               astbuf1->is_signed = true;
+       type_atom {
+               astbuf1->is_reg = false;
        };
 
 param_real:
@@ -1399,7 +1422,13 @@ param_range:
        };
 
 param_integer_type: param_integer param_signed;
-param_range_type: type_vec param_signed param_range;
+param_range_type:
+       type_vec param_signed {
+               addRange(astbuf1, 0, 0);
+       } |
+       type_vec param_signed non_opt_range {
+               astbuf1->children.push_back($3);
+       };
 param_implicit_type: param_signed param_range;
 
 param_type:
@@ -1496,11 +1525,12 @@ enum_base_type: type_atom type_signing
        | %empty                        { astbuf1->is_reg = true; addRange(astbuf1); }
        ;
 
-type_atom: TOK_INTEGER         { astbuf1->is_reg = true; astbuf1->is_signed = true; addRange(astbuf1); }               // 4-state signed
-       |  TOK_INT              { astbuf1->is_reg = true; astbuf1->is_signed = true; addRange(astbuf1); }               // 2-state signed
-       |  TOK_SHORTINT         { astbuf1->is_reg = true; astbuf1->is_signed = true; addRange(astbuf1, 15, 0); }        // 2-state signed
-       |  TOK_BYTE             { astbuf1->is_reg = true; astbuf1->is_signed = true; addRange(astbuf1,  7, 0); }        // 2-state signed
-       ;
+type_atom:
+       integer_atom_type {
+               astbuf1->is_reg = true;
+               astbuf1->is_signed = true;
+               addRange(astbuf1, $1 - 1, 0);
+       };
 
 type_vec: TOK_REG              { astbuf1->is_reg   = true; }           // unsigned
        | TOK_LOGIC             { astbuf1->is_logic = true; }           // unsigned

diff --git a/tests/verilog/int_types.sv b/tests/verilog/int_types.sv
new file mode 100644 (file)
index 0000000..8133f82
--- /dev/null
+++ b/tests/verilog/int_types.sv
@@ -0,0 +1,47 @@
+`define TEST(typ, width, is_signed) \
+    if (1) begin \
+        typ x = -1; \
+        localparam typ y = -1; \
+        logic [127:0] a = x; \
+        logic [127:0] b = y; \
+        if ($bits(x) != width) \
+            $error(`"typ doesn't have expected size width`"); \
+        if ($bits(x) != $bits(y)) \
+            $error(`"localparam typ doesn't match size of typ`"); \
+        function automatic typ f; \
+            input integer x; \
+            f = x; \
+        endfunction \
+        logic [127:0] c = f(-1); \
+        always @* begin \
+            assert (x == y); \
+            assert (a == b); \
+            assert (a == c); \
+            assert ((a == -1) == is_signed); \
+        end \
+    end
+
+`define TEST_INTEGER_ATOM(typ, width) \
+    `TEST(typ, width, 1) \
+    `TEST(typ signed, width, 1) \
+    `TEST(typ unsigned, width, 0)
+
+`define TEST_INTEGER_VECTOR(typ) \
+    `TEST(typ, 1, 0) \
+    `TEST(typ signed, 1, 1) \
+    `TEST(typ unsigned, 1, 0) \
+    `TEST(typ [1:0], 2, 0) \
+    `TEST(typ signed [1:0], 2, 1) \
+    `TEST(typ unsigned [1:0], 2, 0)
+
+module top;
+    `TEST_INTEGER_ATOM(integer, 32)
+    `TEST_INTEGER_ATOM(int, 32)
+    `TEST_INTEGER_ATOM(shortint, 16)
+    `TEST_INTEGER_ATOM(longint, 64)
+    `TEST_INTEGER_ATOM(byte, 8)
+
+    `TEST_INTEGER_VECTOR(reg)
+    `TEST_INTEGER_VECTOR(logic)
+    `TEST_INTEGER_VECTOR(bit)
+endmodule

diff --git a/tests/verilog/int_types.ys b/tests/verilog/int_types.ys
new file mode 100644 (file)
index 0000000..c17c44b
--- /dev/null
+++ b/tests/verilog/int_types.ys
@@ -0,0 +1,7 @@
+read_verilog -sv int_types.sv
+hierarchy
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all

diff --git a/tests/verilog/param_int_types.sv b/tests/verilog/param_int_types.sv
new file mode 100644 (file)
index 0000000..3228369
--- /dev/null
+++ b/tests/verilog/param_int_types.sv
@@ -0,0 +1,19 @@
+module gate(out);
+    parameter integer a = -1;
+    parameter int b = -2;
+    parameter shortint c = -3;
+    parameter longint d = -4;
+    parameter byte e = -5;
+    output wire [1023:0] out;
+    assign out = {a, b, c, d, e};
+endmodule
+
+module gold(out);
+    integer a = -1;
+    int b = -2;
+    shortint c = -3;
+    longint d = -4;
+    byte e = -5;
+    output wire [1023:0] out;
+    assign out = {a, b, c, d, e};
+endmodule

diff --git a/tests/verilog/param_int_types.ys b/tests/verilog/param_int_types.ys
new file mode 100644 (file)
index 0000000..7727801
--- /dev/null
+++ b/tests/verilog/param_int_types.ys
@@ -0,0 +1,5 @@
+read_verilog -sv param_int_types.sv
+proc
+equiv_make gold gate equiv
+equiv_simple
+equiv_status -assert