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 | 
