From fb1c2be76ba065a3da04f279b11e1ed2e59c75c5 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Mon, 20 Mar 2023 12:50:14 +0100
Subject: [PATCH] verilog: Support void functions

The difference between void functions and tasks is that always_comb's
implicit sensitivity list behaves as if functions were inlined, but
ignores signals read only in tasks. This only matters for event based
simulation, and for synthesis we can treat a void function like a task.
---
 frontends/verilog/verilog_lexer.l  |  1 +
 frontends/verilog/verilog_parser.y | 19 ++++++++++++++-
 tests/verilog/void_func.ys         | 37 ++++++++++++++++++++++++++++++
 3 files changed, 56 insertions(+), 1 deletion(-)
 create mode 100644 tests/verilog/void_func.ys

diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 958809319..249986668 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -276,6 +276,7 @@ TIME_SCALE_SUFFIX [munpf]?s
 "byte"       { SV_KEYWORD(TOK_BYTE); }
 "shortint"   { SV_KEYWORD(TOK_SHORTINT); }
 "longint"    { SV_KEYWORD(TOK_LONGINT); }
+"void"       { SV_KEYWORD(TOK_VOID); }
 
 "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 87b50438a..96413afb0 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -372,7 +372,7 @@ static void rewriteGenForDeclInit(AstNode *loop)
 %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_LONGINT TOK_UNION
+%token TOK_STRUCT TOK_PACKED TOK_UNSIGNED TOK_INT TOK_BYTE TOK_SHORTINT TOK_LONGINT TOK_VOID TOK_UNION
 %token TOK_BIT_OR_ASSIGN TOK_BIT_AND_ASSIGN TOK_BIT_XOR_ASSIGN TOK_ADD_ASSIGN
 %token TOK_SUB_ASSIGN TOK_DIV_ASSIGN TOK_MOD_ASSIGN TOK_MUL_ASSIGN
 %token TOK_SHL_ASSIGN TOK_SHR_ASSIGN TOK_SSHL_ASSIGN TOK_SSHR_ASSIGN
@@ -1020,6 +1020,23 @@ task_func_decl:
 		current_function_or_task = NULL;
 		ast_stack.pop_back();
 	} |
+	attr TOK_FUNCTION opt_automatic TOK_VOID TOK_ID {
+		// The difference between void functions and tasks is that
+		// always_comb's implicit sensitivity list behaves as if functions were
+		// inlined, but ignores signals read only in tasks. This only matters
+		// for event based simulation, and for synthesis we can treat a void
+		// function like a task.
+		current_function_or_task = new AstNode(AST_TASK);
+		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);
+		current_function_or_task_port_id = 1;
+		delete $5;
+	} task_func_args_opt ';' task_func_body TOK_ENDFUNCTION {
+		current_function_or_task = NULL;
+		ast_stack.pop_back();
+	} |
 	attr TOK_FUNCTION opt_automatic func_return_type TOK_ID {
 		current_function_or_task = new AstNode(AST_FUNCTION);
 		current_function_or_task->str = *$5;
diff --git a/tests/verilog/void_func.ys b/tests/verilog/void_func.ys
new file mode 100644
index 000000000..6fb7b4b56
--- /dev/null
+++ b/tests/verilog/void_func.ys
@@ -0,0 +1,37 @@
+read_verilog -sv <<EOF
+module top_func(input [7:0] a, output [7:0] b);
+    function automatic void clear_b; b = 0; endfunction
+    function automatic void increment_b; b += a; endfunction
+    always_comb begin
+        clear_b;
+        increment_b;
+        increment_b;
+    end
+endmodule
+
+module top_task(input [7:0] a, output [7:0] b);
+    task automatic clear_b; b = 0; endtask
+    task automatic increment_b; b += a; endtask
+    always_comb begin
+        clear_b;
+        increment_b;
+        increment_b;
+    end
+endmodule
+
+module top_inline(input [7:0] a, output [7:0] b);
+    always_comb begin
+        b = 0;
+        b += a;
+        b += a;
+    end
+endmodule
+EOF
+
+prep
+
+miter -equiv -flatten -make_assert top_inline top_task miter_task
+sat -verify -prove-asserts miter_task
+
+miter -equiv -flatten -make_assert top_inline top_func miter_func
+sat -verify -prove-asserts miter_func