Merge pull request #1569 from YosysHQ/eddie/fix_1531

verilog: preserve size of $genval$-s in for loops
This commit is contained in:
Eddie Hung 2019-12-19 12:21:33 -05:00 committed by GitHub
commit d406f2ffd7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 50 additions and 0 deletions

View File

@ -1198,6 +1198,14 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
varbuf = new AstNode(AST_LOCALPARAM, varbuf);
varbuf->str = init_ast->children[0]->str;
auto resolved = current_scope.at(init_ast->children[0]->str);
if (resolved->range_valid) {
varbuf->range_left = resolved->range_left;
varbuf->range_right = resolved->range_right;
varbuf->range_swapped = resolved->range_swapped;
varbuf->range_valid = resolved->range_valid;
}
AstNode *backup_scope_varbuf = current_scope[varbuf->str];
current_scope[varbuf->str] = varbuf;
@ -2998,6 +3006,14 @@ void AstNode::expand_genblock(std::string index_var, std::string prefix, std::ma
current_ast_mod->children.push_back(p);
str = p->str;
id2ast = p;
auto resolved = current_scope.at(index_var);
if (resolved->range_valid) {
p->range_left = resolved->range_left;
p->range_right = resolved->range_right;
p->range_swapped = resolved->range_swapped;
p->range_valid = resolved->range_valid;
}
}
}

34
tests/various/bug1531.ys Normal file
View File

@ -0,0 +1,34 @@
read_verilog <<EOT
module top (y, clk, w);
output reg y = 1'b0;
input clk, w;
reg [1:0] i = 2'b00;
always @(posedge clk)
// If the constant below is set to 2'b00, the correct output is generated.
// vvvv
for (i = 1'b0; i < 2'b01; i = i + 2'b01)
y <= w || i[1:1];
endmodule
EOT
synth
design -stash gate
read_verilog <<EOT
module gold (y, clk, w);
input clk;
wire [1:0] i;
input w;
output y;
reg y = 1'h0;
always @(posedge clk)
y <= w;
assign i = 2'h0;
endmodule
EOT
proc gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -seq 10 -verify -prove-asserts -show-ports miter