From ed026f5592e0baf1dc9f115a6c89ecb914ac0fd2 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 22 Jan 2025 11:57:49 -0800 Subject: [PATCH] SystemVerilog: clocking declarations This adds parsing for 1800-2017 14.3 clocking block declarations. --- CHANGELOG | 1 + regression/verilog/clocking/clocking1.desc | 9 +++ regression/verilog/clocking/clocking1.sv | 10 +++ src/hw_cbmc_irep_ids.h | 1 + src/verilog/parser.y | 76 ++++++++++++++++++++++ src/verilog/verilog_elaborate.cpp | 3 + src/verilog/verilog_interfaces.cpp | 3 + src/verilog/verilog_synthesis.cpp | 3 + src/verilog/verilog_typecheck.cpp | 3 + 9 files changed, 109 insertions(+) create mode 100644 regression/verilog/clocking/clocking1.desc create mode 100644 regression/verilog/clocking/clocking1.sv diff --git a/CHANGELOG b/CHANGELOG index 39080a61..550e0233 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -11,6 +11,7 @@ * SystemVerilog: chandle, event, string * SystemVerilog: package scope operator * SystemVerilog: checkers +* SystemVerilog: clocking block declarations # EBMC 5.4 diff --git a/regression/verilog/clocking/clocking1.desc b/regression/verilog/clocking/clocking1.desc new file mode 100644 index 00000000..3af165b6 --- /dev/null +++ b/regression/verilog/clocking/clocking1.desc @@ -0,0 +1,9 @@ +CORE +clocking1.sv + +^no properties$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/clocking/clocking1.sv b/regression/verilog/clocking/clocking1.sv new file mode 100644 index 00000000..52cb869d --- /dev/null +++ b/regression/verilog/clocking/clocking1.sv @@ -0,0 +1,10 @@ +module main(input clk); + + clocking my_clocking @(posedge clk); + endclocking + + // The identifier is optional. + default clocking @(posedge clk); + endclocking + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 97910226..8de1e135 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -132,6 +132,7 @@ IREP_ID_ONE(posedge) IREP_ID_ONE(event_guard) IREP_ID_ONE(verilog_star_event) IREP_ID_ONE(verilog_checker) +IREP_ID_ONE(verilog_clocking) IREP_ID_ONE(verilog_cycle_delay) IREP_ID_ONE(delay) IREP_ID_ONE(verilog_non_blocking_assign) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index c0f7ad3a..a041d68f 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1024,6 +1024,9 @@ module_or_generate_item: module_or_generate_item_declaration: package_or_generate_item_declaration | genvar_declaration + | clocking_declaration + | TOK_DEFAULT TOK_CLOCKING clocking_identifier ';' + | TOK_DEFAULT TOK_DISABLE TOK_IFF expression_or_dist ';' ; non_port_module_item: @@ -1106,6 +1109,7 @@ checker_or_generate_item_declaration: | assertion_item_declaration | covergroup_declaration | genvar_declaration + | clocking_declaration | TOK_DEFAULT TOK_CLOCKING clocking_identifier ';' | TOK_DEFAULT TOK_DISABLE TOK_IFF expression_or_dist ';' | ';' @@ -3483,6 +3487,12 @@ delay_or_event_control: { init($$, ID_repeat); } ; + +delay_control_opt: + /* Optional */ + | delay_control + ; + delay_control: '#' delay_value { init($$, ID_delay); mto($$, $2); } @@ -3754,11 +3764,73 @@ procedural_timing_control: // System Verilog standard 1800-2017 // A.6.11 Clocking block +clocking_declaration: + TOK_DEFAULT TOK_CLOCKING clocking_identifier_opt clocking_event ';' + clocking_item_brace + TOK_ENDCLOCKING + { init($$, ID_verilog_clocking); } + | TOK_CLOCKING clocking_identifier_opt clocking_event ';' + clocking_item_brace + TOK_ENDCLOCKING + { init($$, ID_verilog_clocking); } + | TOK_GLOBAL TOK_CLOCKING clocking_identifier_opt clocking_event ';' + TOK_ENDCLOCKING + { init($$, ID_verilog_clocking); } + ; + +clocking_identifier_opt: + /* Optional */ + | clocking_identifier + ; + clocking_event: '@' identifier | '@' '(' event_expression ')' ; +clocking_item_brace: + /* Optional */ + | clocking_item_brace clocking_item + ; + +clocking_item: + TOK_DEFAULT default_skew ';' + | attribute_instance_brace assertion_item_declaration + ; + +default_skew: + TOK_INPUT clocking_skew + | TOK_OUTPUT clocking_skew + | TOK_INPUT clocking_skew TOK_OUTPUT clocking_skew + ; + +clocking_direction: + TOK_INPUT clocking_skew_opt + | TOK_OUTPUT clocking_skew_opt + | TOK_INPUT clocking_skew_opt TOK_OUTPUT clocking_skew_opt + | TOK_INOUT + ; + +list_of_clocking_decl_assign: + clocking_decl_assign + | list_of_clocking_decl_assign ',' clocking_decl_assign + ; + +clocking_decl_assign: + signal_identifier + | signal_identifier '=' expression + ; + +clocking_skew_opt: + /* Optional */ + | clocking_skew + ; + +clocking_skew: + edge_identifier delay_control_opt + | delay_control + ; + cycle_delay: "##" number { init($$, ID_verilog_cycle_delay); mto($$, $2); } @@ -4297,6 +4369,8 @@ class_identifier: TOK_NON_TYPE_IDENTIFIER; constraint_identifier: TOK_NON_TYPE_IDENTIFIER; +edge_identifier: identifier; + formal_port_identifier: identifier; genvar_identifier: identifier; @@ -4335,6 +4409,8 @@ memory_identifier: identifier; method_identifier: identifier; +signal_identifier: identifier; + type_identifier: TOK_TYPE_IDENTIFIER { init($$, ID_typedef_type); diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index e39b0d6d..ccd7cce1 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -844,6 +844,9 @@ void verilog_typecheckt::collect_symbols( else if(module_item.id() == ID_verilog_package_import) { } + else if(module_item.id() == ID_verilog_clocking) + { + } else if(module_item.id() == ID_verilog_covergroup) { } diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index d542d071..d3d4721f 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -300,6 +300,9 @@ void verilog_typecheckt::interface_module_item( else if(module_item.id() == ID_verilog_package_import) { } + else if(module_item.id() == ID_verilog_clocking) + { + } else if(module_item.id() == ID_verilog_covergroup) { } diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index b2e0606c..e516dcc3 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -3276,6 +3276,9 @@ void verilog_synthesist::synth_module_item( { // done already } + else if(module_item.id() == ID_verilog_clocking) + { + } else if(module_item.id() == ID_verilog_covergroup) { } diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index b2134c08..03400d46 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1734,6 +1734,9 @@ void verilog_typecheckt::convert_module_item( else if(module_item.id() == ID_verilog_package_import) { } + else if(module_item.id() == ID_verilog_clocking) + { + } else if(module_item.id() == ID_verilog_covergroup) { }