Skip to content

Commit

Permalink
Verilog: parse covergroup declarations
Browse files Browse the repository at this point in the history
This adds grammar rules for SystemVerilog covergroup declarations.
  • Loading branch information
kroening committed Apr 16, 2024
1 parent 132151e commit 622f08b
Show file tree
Hide file tree
Showing 8 changed files with 99 additions and 1 deletion.
7 changes: 7 additions & 0 deletions regression/verilog/covergroup/covergroup1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
covergroup1.sv

^no properties$
^EXIT=10$
^SIGNAL=0$
--
9 changes: 9 additions & 0 deletions regression/verilog/covergroup/covergroup1.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module main;

wire clk, some_signal;

covergroup cg @(posedge clk);
coverpoint some_signal;
endgroup

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 @@ -73,6 +73,7 @@ IREP_ID_ONE(wait)
IREP_ID_ONE(verilog_assert_property)
IREP_ID_ONE(verilog_assume_property)
IREP_ID_ONE(verilog_cover_property)
IREP_ID_ONE(verilog_covergroup)
IREP_ID_ONE(verilog_smv_assert)
IREP_ID_ONE(verilog_smv_assume)
IREP_ID_ONE(verilog_always)
Expand Down
71 changes: 70 additions & 1 deletion src/verilog/parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -882,7 +882,7 @@ class_item:
// | attribute_instance_brace class_method
// | attribute_instance_brace class_constraint
attribute_instance_brace class_declaration
// | attribute_instance_brace covergroup_declaration
| attribute_instance_brace covergroup_declaration
| local_parameter_declaration ';'
| parameter_declaration ';'
| ';'
Expand Down Expand Up @@ -1018,6 +1018,7 @@ package_or_generate_item_declaration:
that let constructs may be declared in a
module/interface/program/checker etc. */
| let_declaration
| covergroup_declaration
| ';'
{ init($$, ID_verilog_empty_item); }
;
Expand Down Expand Up @@ -1249,6 +1250,9 @@ enum_name_declaration_list:
{ $$=$1; mts($$, $3); }
;

class_scope: class_type TOK_COLONCOLON
;

integer_type:
integer_vector_type
| integer_atom_type
Expand Down Expand Up @@ -1828,6 +1832,13 @@ task_declaration:
task_prototype: TOK_TASK task_identifier
;

tf_port_list_paren_opt:
/* Optional */
{ init($$); }
| '(' tf_port_list_opt ')'
{ $$ = $2; }
;

tf_port_list_opt:
/* Optional */
{ init($$); }
Expand Down Expand Up @@ -2002,6 +2013,55 @@ expression_or_dist:
expression
;

// System Verilog standard 1800-2017
// A.2.11 Covergroup declarations

covergroup_declaration:
TOK_COVERGROUP new_identifier tf_port_list_paren_opt coverage_event_opt ';'
coverage_spec_or_option_brace TOK_ENDGROUP
{ init($$, ID_verilog_covergroup); }
;

coverage_spec_or_option_brace:
/* Optional */
| coverage_spec_or_option_brace coverage_spec_or_option
;

coverage_spec_or_option:
attribute_instance_brace coverage_spec
;

coverage_spec:
cover_point
;

coverage_event_opt:
/* Optional */
| coverage_event
;

coverage_event:
clocking_event
;

block_event_expression:
block_event_expression TOK_OR block_event_expression
| TOK_BEGIN hierarchical_btf_identifier
| TOK_END hierarchical_btf_identifier
;

hierarchical_btf_identifier:
hierarchical_tf_identifier
| hierarchical_block_identifier
| method_identifier
| hierarchical_identifier '.' method_identifier
| class_scope method_identifier
;

cover_point:
TOK_COVERPOINT expression ';'
;

// System Verilog standard 1800-2017
// A.2.12 Let declarations

Expand Down Expand Up @@ -2845,6 +2905,11 @@ procedural_timing_control:
// System Verilog standard 1800-2017
// A.6.11 Clocking block

clocking_event:
'@' identifier
| '@' '(' event_expression ')'
;

cycle_delay:
"##" number
{ init($$, ID_verilog_cycle_delay); mto($$, $2); }
Expand Down Expand Up @@ -3329,6 +3394,8 @@ ps_covergroup_identifier:
memory_identifier: identifier;
method_identifier: identifier;
type_identifier: TOK_TYPE_IDENTIFIER
{
init($$, ID_typedef_type);
Expand Down Expand Up @@ -3362,6 +3429,8 @@ function_identifier: hierarchical_identifier
hierarchical_event_identifier: event_identifier;
hierarchical_block_identifier: hierarchical_identifier;
hierarchical_identifier:
identifier
| hierarchical_identifier '.' identifier
Expand Down
3 changes: 3 additions & 0 deletions src/verilog/verilog_elaborate.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -760,6 +760,9 @@ void verilog_typecheckt::collect_symbols(
else if(module_item.id() == ID_verilog_empty_item)
{
}
else if(module_item.id() == ID_verilog_covergroup)
{
}
else
DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());
}
Expand Down
3 changes: 3 additions & 0 deletions src/verilog/verilog_interfaces.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -287,6 +287,9 @@ void verilog_typecheckt::interface_module_item(
else if(module_item.id() == ID_verilog_empty_item)
{
}
else if(module_item.id() == ID_verilog_covergroup)
{
}
else
{
DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());
Expand Down
3 changes: 3 additions & 0 deletions src/verilog/verilog_synthesis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2740,6 +2740,9 @@ void verilog_synthesist::synth_module_item(
else if(module_item.id() == ID_verilog_empty_item)
{
}
else if(module_item.id() == ID_verilog_covergroup)
{
}
else
{
throw errort().with_location(module_item.source_location())
Expand Down
3 changes: 3 additions & 0 deletions src/verilog/verilog_typecheck.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1575,6 +1575,9 @@ void verilog_typecheckt::convert_module_item(
else if(module_item.id() == ID_verilog_empty_item)
{
}
else if(module_item.id() == ID_verilog_covergroup)
{
}
else
{
throw errort().with_location(module_item.source_location())
Expand Down

0 comments on commit 622f08b

Please sign in to comment.