3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-23 00:55:32 +00:00

verilog: fix sizing of constant args for tasks/functions

- Simplify synthetic localparams for normal calls to update their width
    - This step was inadvertently removed alongside `added_mod_children`
- Support redeclaration of constant function arguments
    - `eval_const_function` never correctly handled this, but the issue
      was not exposed in the existing tests until the recent change to
      always attempt constant function evaluation when all-const args
      are used
- Check asserts in const_arg_loop and const_func tests
- Add coverage for width mismatch error cases
This commit is contained in:
Zachary Snow 2021-02-21 14:45:21 -05:00
parent 127484e675
commit b6af90fe20
10 changed files with 124 additions and 47 deletions

View file

@ -20,11 +20,11 @@ module top;
endfunction
function automatic [31:0] operation2;
input [4:0] var;
input [4:0] inp;
input integer num;
begin
var[0] = var[0] ^ 1;
operation2 = num * var;
inp[0] = inp[0] ^ 1;
operation2 = num * inp;
end
endfunction
@ -79,15 +79,14 @@ module top;
wire [31:0] x5;
assign x5 = operation5(64);
// `define VERIFY
`ifdef VERIFY
assert property (a == 2);
assert property (A == 3);
assert property (x1 == 16);
assert property (x1b == 16);
assert property (x2 == 4);
assert property (x3 == 16);
assert property (x4 == a << 1);
assert property (x5 == 64);
`endif
always_comb begin
assert(a == 2);
assert(A == 3);
assert(x1 == 16);
assert(x1b == 16);
assert(x2 == 4);
assert(x3 == 16);
assert(x4 == a << 1);
assert(x5 == 64);
end
endmodule

View file

@ -1 +1,6 @@
read_verilog const_arg_loop.v
read_verilog -sv const_arg_loop.sv
hierarchy
proc
opt -full
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

View file

@ -62,26 +62,25 @@ module top(out);
localparam signed Y = $floor(W / X);
localparam signed Z = negate($floor(W / X));
// `define VERIFY
`ifdef VERIFY
assert property (a1 == 0);
assert property (a2 == 0);
assert property (a3 == "BAR");
assert property (a4 == 0);
assert property (b1 == "FOO");
assert property (b2 == "FOO");
assert property (b3 == 0);
assert property (b4 == "HI");
assert property (c1 == 1);
assert property (c2 == 1);
assert property (c3 == 0);
assert property (c4 == 0);
assert property (d1 == 0);
assert property (d2 == 0);
assert property (d3 == 1);
assert property (d4 == 1);
always_comb begin
assert(a1 == 0);
assert(a2 == 0);
assert(a3 == "BAR");
assert(a4 == 0);
assert(b1 == "FOO");
assert(b2 == "FOO");
assert(b3 == 0);
assert(b4 == "HI");
assert(c1 == 1);
assert(c2 == 1);
assert(c3 == 0);
assert(c4 == 0);
assert(d1 == 0);
assert(d2 == 0);
assert(d3 == 1);
assert(d4 == 1);
assert property (Y == 3);
assert property (Z == ~3);
`endif
assert(Y == 3);
assert(Z == ~3);
end
endmodule

View file

@ -1 +1,7 @@
read_verilog const_func.v
read_verilog -sv const_func.sv
hierarchy
proc
flatten
opt -full
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

View file

@ -0,0 +1,12 @@
logger -expect error "Incompatible re-declaration of wire" 1
read_verilog -sv <<EOT
module top;
function automatic integer f;
input [0:0] inp;
integer inp;
f = inp;
endfunction
integer x, y;
initial x = f(y);
endmodule
EOT

View file

@ -0,0 +1,12 @@
logger -expect error "Incompatible re-declaration of constant function wire" 1
read_verilog -sv <<EOT
module top;
function automatic integer f;
input [0:0] inp;
integer inp;
f = inp;
endfunction
integer x;
initial x = f(0);
endmodule
EOT

View file

@ -0,0 +1,12 @@
logger -expect error "Incompatible re-declaration of wire" 1
read_verilog -sv <<EOT
module top;
function automatic integer f;
input [1:0] inp;
integer inp;
f = inp;
endfunction
integer x, y;
initial x = f(y);
endmodule
EOT

View file

@ -0,0 +1,12 @@
logger -expect error "Incompatible re-declaration of constant function wire" 1
read_verilog -sv <<EOT
module top;
function automatic integer f;
input [1:0] inp;
integer inp;
f = inp;
endfunction
integer x;
initial x = f(0);
endmodule
EOT