mirror of https://github.com/YosysHQ/yosys.git
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
|