Skip to content

Commit

Permalink
SystemVerilog: Parsing and type checking for queue types
Browse files Browse the repository at this point in the history
This adds parsing and type checking for 1800-2017 7.10 queues.
  • Loading branch information
kroening committed Feb 5, 2025
1 parent 3579ca1 commit 844da97
Show file tree
Hide file tree
Showing 8 changed files with 26 additions and 6 deletions.
2 changes: 1 addition & 1 deletion lib/cbmc
Submodule cbmc updated 457 files
6 changes: 3 additions & 3 deletions regression/verilog/data-types/queue1.desc
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
KNOWNBUG
CORE
queue1.sv

^EXIT=0$
^no properties$
^EXIT=10$
^SIGNAL=0$
--
--
Parsing fails.
2 changes: 1 addition & 1 deletion regression/verilog/data-types/queue1.sv
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module main;

byte queue_of_bytes[$];
string queue_of_strings[$:10] = { "foobar" };
string queue_of_strings[$:10];

endmodule
1 change: 1 addition & 0 deletions src/hw_cbmc_irep_ids.h
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,7 @@ IREP_ID_ONE(verilog_inside)
IREP_ID_ONE(verilog_unique)
IREP_ID_ONE(verilog_unique0)
IREP_ID_ONE(verilog_priority)
IREP_ID_ONE(verilog_queue)
IREP_ID_ONE(verilog_new)
IREP_ID_ONE(verilog_non_indexed_part_select)
IREP_ID_ONE(verilog_indexed_part_select_plus)
Expand Down
6 changes: 6 additions & 0 deletions src/verilog/expr2verilog.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2074,6 +2074,12 @@ std::string expr2verilogt::convert(const typet &type)
{
return "enum";
}
else if(type.id() == ID_verilog_queue)
{
std::string dest="queue of ";
dest += convert(to_type_with_subtype(type).subtype());
return dest;
}
else if(type.id() == ID_struct)
{
return "struct";
Expand Down
8 changes: 8 additions & 0 deletions src/verilog/parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -2114,6 +2114,7 @@ variable_dimension:
unsized_dimension
| unpacked_dimension
| associative_dimension
| queue_dimension
;

variable_dimension_brace:
Expand All @@ -2126,6 +2127,13 @@ variable_dimension_brace:
}
;

queue_dimension:
'[' '$' ']'
{ init($$, ID_verilog_queue); stack_type($$).add_subtype().make_nil(); }
| '[' '$' TOK_COLON constant_expression ']'
{ init($$, ID_verilog_queue); stack_type($$).add_subtype().make_nil(); }
;

unsized_dimension: '[' ']'
{ init($$, "unsized"); }
;
Expand Down
4 changes: 4 additions & 0 deletions src/verilog/verilog_elaborate_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -447,6 +447,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
// package::typedef
return elaborate_package_scope_typedef(to_type_with_subtypes(src));
}
else if(src.id() == ID_verilog_queue)
{
return src;
}
else
{
throw errort().with_location(source_location)
Expand Down
3 changes: 2 additions & 1 deletion src/verilog/verilog_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,8 @@ typet verilog_declaratort::merged_type(const typet &declaration_type) const
typet *p = &result;

while(p->id() == ID_verilog_unpacked_array ||
p->id() == ID_verilog_associative_array)
p->id() == ID_verilog_associative_array ||
p->id() == ID_verilog_queue)
{
p = &to_type_with_subtype(*p).subtype();
}
Expand Down

0 comments on commit 844da97

Please sign in to comment.