mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-06 01:24:10 +00:00
fb1c2be76b
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.
38 lines
884 B
Plaintext
38 lines
884 B
Plaintext
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
|