diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/verilog/void_func.ys | 37 |
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 |