From 88715b0f9dd7ce9623096873edfa0313382fd260 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 16 Apr 2024 16:31:08 -0700 Subject: [PATCH] Verilog: parse covergroup declarations This adds grammar rules for SystemVerilog covergroup declarations. --- .../verilog/covergroup/covergroup1.desc | 7 ++ regression/verilog/covergroup/covergroup1.sv | 9 +++ src/hw_cbmc_irep_ids.h | 1 + src/verilog/parser.y | 71 ++++++++++++++++++- src/verilog/verilog_elaborate.cpp | 3 + src/verilog/verilog_interfaces.cpp | 3 + src/verilog/verilog_synthesis.cpp | 3 + src/verilog/verilog_typecheck.cpp | 3 + 8 files changed, 99 insertions(+), 1 deletion(-) create mode 100644 regression/verilog/covergroup/covergroup1.desc create mode 100644 regression/verilog/covergroup/covergroup1.sv diff --git a/regression/verilog/covergroup/covergroup1.desc b/regression/verilog/covergroup/covergroup1.desc new file mode 100644 index 000000000..3eff5392a --- /dev/null +++ b/regression/verilog/covergroup/covergroup1.desc @@ -0,0 +1,7 @@ +CORE +covergroup1.sv + +^no properties$ +^EXIT=10$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/covergroup/covergroup1.sv b/regression/verilog/covergroup/covergroup1.sv new file mode 100644 index 000000000..7821d097f --- /dev/null +++ b/regression/verilog/covergroup/covergroup1.sv @@ -0,0 +1,9 @@ +module main; + + wire clk, some_signal; + + covergroup cg @(posedge clk); + coverpoint some_signal; + endgroup + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index b50452141..3ce9d96c3 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -77,6 +77,7 @@ IREP_ID_ONE(verilog_smv_using) 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) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 16f0a16e9..8cab2aebf 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -891,7 +891,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 ';' | ';' @@ -1027,6 +1027,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); } ; @@ -1285,6 +1286,9 @@ enum_name_declaration_list: { $$=$1; mts($$, $3); } ; +class_scope: class_type TOK_COLONCOLON + ; + integer_type: integer_vector_type | integer_atom_type @@ -1864,6 +1868,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($$); } @@ -2067,6 +2078,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 @@ -2910,6 +2970,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); } @@ -3396,6 +3461,8 @@ ps_covergroup_identifier: memory_identifier: identifier; +method_identifier: identifier; + type_identifier: TOK_TYPE_IDENTIFIER { init($$, ID_typedef_type); @@ -3429,6 +3496,8 @@ function_identifier: hierarchical_identifier hierarchical_event_identifier: event_identifier; +hierarchical_block_identifier: hierarchical_identifier; + hierarchical_identifier: identifier | hierarchical_identifier '.' identifier diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 0822b2c99..73a0259f8 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -773,6 +773,9 @@ void verilog_typecheckt::collect_symbols( else if(module_item.id() == ID_verilog_package_import) { } + else if(module_item.id() == ID_verilog_covergroup) + { + } else DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string()); } diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index c7afac3e0..57698a6f6 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -296,6 +296,9 @@ void verilog_typecheckt::interface_module_item( else if(module_item.id() == ID_verilog_package_import) { } + else if(module_item.id() == ID_verilog_covergroup) + { + } else { DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string()); diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 4e23b5e89..d125fc3b2 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -2744,6 +2744,9 @@ void verilog_synthesist::synth_module_item( { // done already } + else if(module_item.id() == ID_verilog_covergroup) + { + } else { throw errort().with_location(module_item.source_location()) diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index b987503e0..bd0d920fe 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1587,6 +1587,9 @@ void verilog_typecheckt::convert_module_item( else if(module_item.id() == ID_verilog_package_import) { } + else if(module_item.id() == ID_verilog_covergroup) + { + } else { throw errort().with_location(module_item.source_location())