aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--frontends/ast/simplify.cc178
-rw-r--r--frontends/verific/verific.cc6
-rw-r--r--passes/sat/formalff.cc3
-rw-r--r--tests/svtypes/struct_array.sv60
-rw-r--r--tests/various/cellarray_array_connections.ys45
6 files changed, 195 insertions, 99 deletions
diff --git a/Makefile b/Makefile
index 2816c1946..a51bfa1ce 100644
--- a/Makefile
+++ b/Makefile
@@ -142,7 +142,7 @@ LDLIBS += -lrt
endif
endif
-YOSYS_VER := 0.24+1
+YOSYS_VER := 0.24+10
# Note: We arrange for .gitcommit to contain the (short) commit hash in
# tarballs generated with git-archive(1) using .gitattributes. The git repo
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 57237f4b3..da7933d2f 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -273,9 +273,9 @@ static int range_width(AstNode *node, AstNode *rnode)
return rnode->range_left - rnode->range_right + 1;
}
-[[noreturn]] static void struct_array_dimension_error(AstNode *node)
+[[noreturn]] static void struct_array_packing_error(AstNode *node)
{
- log_file_error(node->filename, node->location.first_line, "Currently limited to two dimensions in packed struct/union member %s\n", node->str.c_str());
+ log_file_error(node->filename, node->location.first_line, "Unpacked array in packed struct/union member %s\n", node->str.c_str());
}
static void save_struct_array_width(AstNode *node, int width)
@@ -291,15 +291,6 @@ static void save_struct_range_swapped(AstNode *node, bool range_swapped)
}
-static int get_struct_array_width(AstNode *node)
-{
- // This function is only useful for up to two array dimensions.
- log_assert(node->multirange_dimensions.size() <= 2);
- // the stride for the array, 1 if not an array
- return (node->multirange_dimensions.size() != 2 ? 1 : node->multirange_dimensions[1]);
-
-}
-
static int size_packed_struct(AstNode *snode, int base_offset)
{
// Struct members will be laid out in the structure contiguously from left to right.
@@ -341,11 +332,12 @@ static int size_packed_struct(AstNode *snode, int base_offset)
width *= array_count;
}
else {
- // Currently limited to at most two dimensions.
- struct_array_dimension_error(node);
+ // The Yosys extension for unpacked arrays in packed structs / unions
+ // only supports memories, i.e. e.g. logic [7:0] a [256] - see above.
+ struct_array_packing_error(node);
}
} else {
- // Vector.
+ // Vector
save_struct_array_width(node, width);
save_struct_range_swapped(node, node->children[0]->range_swapped);
}
@@ -355,19 +347,19 @@ static int size_packed_struct(AstNode *snode, int base_offset)
node->children.clear();
}
else if (node->children.size() > 0 && node->children[0]->type == AST_MULTIRANGE) {
- // packed 2D array, e.g. bit [3:0][63:0] a
- auto rnode = node->children[0];
- if (node->children.size() != 1 || rnode->children.size() != 2) {
- // Currently limited to at most two dimensions.
- struct_array_dimension_error(node);
+ // Packed array, e.g. bit [3:0][63:0] a
+ if (node->children.size() != 1) {
+ // The Yosys extension for unpacked arrays in packed structs / unions
+ // only supports memories, i.e. e.g. logic [7:0] a [256] - see above.
+ struct_array_packing_error(node);
+ }
+ width = 1;
+ for (auto rnode : node->children[0]->children) {
+ int rwidth = range_width(node, rnode);
+ save_struct_array_width(node, rwidth);
+ save_struct_range_swapped(node, rnode->range_swapped);
+ width *= rwidth;
}
- int array_count = range_width(node, rnode->children[0]);
- save_struct_array_width(node, array_count);
- save_struct_range_swapped(node, rnode->children[0]->range_swapped);
- width = range_width(node, rnode->children[1]);
- save_struct_array_width(node, width);
- save_struct_range_swapped(node, rnode->children[1]->range_swapped);
- width *= array_count;
// range nodes are now redundant
for (AstNode *child : node->children)
delete child;
@@ -426,75 +418,51 @@ static AstNode *multiply_by_const(AstNode *expr_node, int stride)
return new AstNode(AST_MUL, expr_node, node_int(stride));
}
-static AstNode *offset_indexed_range(int offset, int stride, AstNode *left_expr, AstNode *right_expr)
+static AstNode *normalize_struct_index(AstNode *expr, AstNode *member_node, int dimension)
{
- // adjust the range expressions to add an offset into the struct
- // and maybe index using an array stride
- auto left = left_expr->clone();
- auto right = right_expr->clone();
- if (stride > 1) {
- // newleft = (left + 1) * stride - 1
- left = new AstNode(AST_SUB, multiply_by_const(new AstNode(AST_ADD, left, node_int(1)), stride), node_int(1));
- // newright = right * stride
- right = multiply_by_const(right, stride);
- }
- // add the offset
- if (offset) {
- left = new AstNode(AST_ADD, node_int(offset), left);
- right = new AstNode(AST_ADD, node_int(offset), right);
+ expr = expr->clone();
+
+ if (member_node->multirange_swapped[dimension]) {
+ // The dimension has swapped range; swap index into the struct accordingly.
+ int msb = member_node->multirange_dimensions[dimension] - 1;
+ expr = new AstNode(AST_SUB, node_int(msb), expr);
}
- return new AstNode(AST_RANGE, left, right);
+
+ return expr;
}
-static AstNode *make_struct_index_range(AstNode *node, AstNode *rnode, int stride, int offset, AstNode *member_node)
+static AstNode *struct_index_lsb_offset(AstNode *lsb_offset, AstNode *rnode, AstNode *member_node, int dimension, int &stride)
{
- // This function should be rewritten to support more than two array dimensions.
- log_assert(member_node->multirange_dimensions.size() <= 2 && member_node->multirange_swapped.size() <= 2);
- if (member_node->multirange_swapped[0]) {
- // The struct item has swapped range; swap index into the struct accordingly.
- int msb = member_node->multirange_dimensions[0] - 1;
- for (auto &expr : rnode->children) {
- expr = new AstNode(AST_SUB, node_int(msb), expr);
- }
- }
+ stride /= member_node->multirange_dimensions[dimension];
+ auto right = normalize_struct_index(rnode->children.back(), member_node, dimension);
+ auto offset = stride > 1 ? multiply_by_const(right, stride) : right;
+ return new AstNode(AST_ADD, lsb_offset, offset);
+}
- // generate a range node to perform either bit or array indexing
+static AstNode *struct_index_msb_offset(AstNode *lsb_offset, AstNode *rnode, AstNode *member_node, int dimension, int stride)
+{
+ log_assert(rnode->children.size() <= 2);
+
+ // Offset to add to LSB
+ AstNode *offset;
if (rnode->children.size() == 1) {
- // index e.g. s.a[i]
- return offset_indexed_range(offset, stride, rnode->children[0], rnode->children[0]);
- }
- else if (rnode->children.size() == 2) {
- // slice e.g. s.a[i:j]
- return offset_indexed_range(offset, stride, rnode->children[0], rnode->children[1]);
+ // Index, e.g. s.a[i]
+ offset = node_int(stride - 1);
}
else {
- struct_op_error(node);
- }
-}
-
-static AstNode *slice_range(AstNode *rnode, AstNode *snode, AstNode *member_node)
-{
- // This function should be rewritten to support more than two array dimensions.
- log_assert(member_node->multirange_dimensions.size() <= 2 && member_node->multirange_swapped.size() <= 2);
- if (member_node->multirange_swapped[1]) {
- // The second dimension has swapped range; swap index into the struct accordingly.
- int msb = member_node->multirange_dimensions[1] - 1;
- for (auto &expr : snode->children) {
- expr = new AstNode(AST_SUB, node_int(msb), expr);
+ // rnode->children.size() == 2
+ // Slice, e.g. s.a[i:j]
+ auto left = normalize_struct_index(rnode->children[0], member_node, dimension);
+ auto right = normalize_struct_index(rnode->children[1], member_node, dimension);
+ offset = new AstNode(AST_SUB, left, right);
+ if (stride > 1) {
+ // offset = (msb - lsb + 1)*stride - 1
+ auto slice_width = new AstNode(AST_ADD, offset, node_int(1));
+ offset = new AstNode(AST_SUB, multiply_by_const(slice_width, stride), node_int(1));
}
}
- // apply the bit slice indicated by snode to the range rnode
- log_assert(rnode->type==AST_RANGE);
- auto left = rnode->children[0];
- auto right = rnode->children[1];
- log_assert(snode->type==AST_RANGE);
- auto slice_left = snode->children[0];
- auto slice_right = snode->children[1];
- auto width = new AstNode(AST_SUB, slice_left->clone(), slice_right->clone());
- right = new AstNode(AST_ADD, right->clone(), slice_right->clone());
- left = new AstNode(AST_ADD, right->clone(), width);
- return new AstNode(AST_RANGE, left, right);
+ return new AstNode(AST_ADD, lsb_offset, offset);
}
@@ -509,26 +477,38 @@ AstNode *AST::make_struct_member_range(AstNode *node, AstNode *member_node)
// no range operations apply, return the whole width
return make_range(range_left, range_right);
}
- // This function should be rewritten to support more than two array dimensions.
- log_assert(member_node->multirange_dimensions.size() <= 2 && member_node->multirange_swapped.size() <= 2);
- int stride = get_struct_array_width(member_node);
- if (node->children.size() == 1 && node->children[0]->type == AST_RANGE) {
- // bit or array indexing e.g. s.a[2] or s.a[1:0]
- return make_struct_index_range(node, node->children[0], stride, range_right, member_node);
+
+ if (node->children.size() != 1) {
+ struct_op_error(node);
}
- else if (node->children.size() == 1 && node->children[0]->type == AST_MULTIRANGE) {
- // multirange, i.e. bit slice after array index, e.g. s.a[i][p:q]
- log_assert(stride > 1);
- auto mrnode = node->children[0];
- auto element_range = make_struct_index_range(node, mrnode->children[0], stride, range_right, member_node);
- // then apply bit slice range
- auto range = slice_range(element_range, mrnode->children[1], member_node);
- delete element_range;
- return range;
+
+ // Range operations
+ auto rnode = node->children[0];
+ auto lsb_offset = node_int(member_node->range_right);
+ int stride = range_left - range_right + 1;
+ size_t i = 0;
+
+ // Calculate LSB offset for the final index / slice
+ if (rnode->type == AST_RANGE) {
+ lsb_offset = struct_index_lsb_offset(lsb_offset, rnode, member_node, i, stride);
+ }
+ else if (rnode->type == AST_MULTIRANGE) {
+ // Add offset for each dimension
+ auto mrnode = rnode;
+ for (i = 0; i < mrnode->children.size(); i++) {
+ rnode = mrnode->children[i];
+ lsb_offset = struct_index_lsb_offset(lsb_offset, rnode, member_node, i, stride);
+ }
+ i--; // Step back to the final index / slice
}
else {
struct_op_error(node);
}
+
+ // Calculate MSB offset for the final index / slice
+ auto msb_offset = struct_index_msb_offset(lsb_offset->clone(), rnode, member_node, i, stride);
+
+ return new AstNode(AST_RANGE, msb_offset, lsb_offset);
}
static void add_members_to_scope(AstNode *snode, std::string name)
@@ -1627,6 +1607,8 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
break;
if (type == AST_GENBLOCK)
break;
+ if (type == AST_CELLARRAY && children[i]->type == AST_CELL)
+ continue;
if (type == AST_BLOCK && !str.empty())
break;
if (type == AST_PREFIX && i >= 1)
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 40f96e82c..a93d79c80 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1125,6 +1125,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
NetBus *netbus;
Instance *inst;
PortRef *pr;
+ Att *attr;
+
+ FOREACH_ATTRIBUTE(nl, mi, attr) {
+ if (!strcmp(attr->Key(), "noblackbox"))
+ module->set_bool_attribute(ID::blackbox, false);
+ }
FOREACH_PORT_OF_NETLIST(nl, mi, port)
{
diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
index 209486a37..962e350a1 100644
--- a/passes/sat/formalff.cc
+++ b/passes/sat/formalff.cc
@@ -479,6 +479,9 @@ struct FormalFfPass : public Pass {
if (ff.sig_clk.is_fully_const())
log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n",
log_id(cell), log_id(cell->type), log_id(module));
+ if (ff.has_aload || ff.has_arst || ff.has_sr)
+ log_error("Async inputs on %s (%s) from module %s, run async2sync first.\n",
+ log_id(cell), log_id(cell->type), log_id(module));
auto clk_wire = ff.sig_clk.is_wire() ? ff.sig_clk.as_wire() : nullptr;
diff --git a/tests/svtypes/struct_array.sv b/tests/svtypes/struct_array.sv
index f69c4c577..739f202ab 100644
--- a/tests/svtypes/struct_array.sv
+++ b/tests/svtypes/struct_array.sv
@@ -81,6 +81,66 @@ module top;
always_comb assert(s3_b==80'hFC00_4200_0012_3400_FFFC);
+ struct packed {
+ bit [0:7] [0:1] [0:3] a;
+ bit [0:15] b; // filler for non-zero offset
+ } s3_lll;
+
+ initial begin
+ s3_lll = '0;
+
+ s3_lll.a[5:6] = 16'h1234;
+ s3_lll.a[2] = 8'h42;
+
+ s3_lll.a[0] = '1;
+ s3_lll.a[0][1][2:3] = '0;
+
+ s3_lll.b = '1;
+ s3_lll.b[14:15] = '0;
+ end
+
+ always_comb assert(s3_lll==80'hFC00_4200_0012_3400_FFFC);
+
+ struct packed {
+ bit [0:7] [1:0] [0:3] a;
+ bit [0:15] b; // filler for non-zero offset
+ } s3_lbl;
+
+ initial begin
+ s3_lbl = '0;
+
+ s3_lbl.a[5:6] = 16'h1234;
+ s3_lbl.a[2] = 8'h42;
+
+ s3_lbl.a[0] = '1;
+ s3_lbl.a[0][0][2:3] = '0;
+
+ s3_lbl.b = '1;
+ s3_lbl.b[14:15] = '0;
+ end
+
+ always_comb assert(s3_lbl==80'hFC00_4200_0012_3400_FFFC);
+
+ struct packed {
+ bit [0:7] [0:1] [3:0] a;
+ bit [0:15] b; // filler for non-zero offset
+ } s3_llb;
+
+ initial begin
+ s3_llb = '0;
+
+ s3_llb.a[5:6] = 16'h1234;
+ s3_llb.a[2] = 8'h42;
+
+ s3_llb.a[0] = '1;
+ s3_llb.a[0][1][1:0] = '0;
+
+ s3_llb.b = '1;
+ s3_llb.b[14:15] = '0;
+ end
+
+ always_comb assert(s3_llb==80'hFC00_4200_0012_3400_FFFC);
+
`ifndef VERIFIC
// Note that the tests below for unpacked arrays in structs rely on the
// fact that they are actually packed in Yosys.
diff --git a/tests/various/cellarray_array_connections.ys b/tests/various/cellarray_array_connections.ys
new file mode 100644
index 000000000..ef36a9a45
--- /dev/null
+++ b/tests/various/cellarray_array_connections.ys
@@ -0,0 +1,45 @@
+# Regression test for #3467
+read_verilog <<EOT
+
+module bit_buf (
+ input wire bit_in,
+ output wire bit_out
+);
+ assign bit_out = bit_in;
+endmodule
+
+module top (
+ input wire [3:0] data_in,
+ output wire [3:0] data_out
+);
+
+ wire [3:0] data [0:4];
+
+ assign data[0] = data_in;
+ assign data_out = data[4];
+
+ genvar i;
+ generate
+ for (i=0; i<=3; i=i+1) begin
+ bit_buf bit_buf_instance[3:0] (
+ .bit_in(data[i]),
+ .bit_out(data[i + 1])
+ );
+ end
+ endgenerate
+endmodule
+
+module top2 (
+ input wire [3:0] data_in,
+ output wire [3:0] data_out
+);
+ assign data_out = data_in;
+endmodule
+
+EOT
+
+hierarchy
+proc
+
+miter -equiv -make_assert -flatten top top2 miter
+sat -prove-asserts -verify miter
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-30 16:07:06 +0000