aboutsummaryrefslogtreecommitdiffstats
path: root/tests/verilog/void_func.ys
diff options
context:
space:
mode:
Diffstat (limited to 'tests/verilog/void_func.ys')
-rw-r--r--tests/verilog/void_func.ys37
1 files changed, 37 insertions, 0 deletions
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