diff --git a/regression/verilog/checker/checker1.desc b/regression/verilog/checker/checker1.desc new file mode 100644 index 00000000..9bfecb60 --- /dev/null +++ b/regression/verilog/checker/checker1.desc @@ -0,0 +1,7 @@ +CORE +checker1.sv +--show-parse +^Checker: myChecker$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/checker/checker1.sv b/regression/verilog/checker/checker1.sv new file mode 100644 index 00000000..cec625ca --- /dev/null +++ b/regression/verilog/checker/checker1.sv @@ -0,0 +1,5 @@ +checker myChecker; +endchecker + +module main; +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index b9da5497..5bacb381 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -119,6 +119,7 @@ IREP_ID_ONE(negedge) IREP_ID_ONE(posedge) IREP_ID_ONE(event_guard) IREP_ID_ONE(verilog_star_event) +IREP_ID_ONE(verilog_checker) 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 d09a3d94..5fbc846f 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -746,6 +746,20 @@ program_declaration: TOK_PROGRAM TOK_ENDPROGRAM ; +checker_declaration: + TOK_CHECKER checker_identifier + { + init($$, ID_verilog_checker); + stack_expr($$).set(ID_base_name, stack_expr($2).id()); + } + ';' + checker_or_generate_item_brace + TOK_ENDCHECKER + { + $$ = $3; + } + ; + class_declaration: TOK_CLASS class_identifier ';' @@ -1007,6 +1021,42 @@ non_port_interface_item: | interface_declaration /* | timeunits_declaration */ ; + +// System Verilog standard 1800-2017 +// A.1.9 Checker items + +checker_or_generate_item_brace: + /* Optional */ + | checker_or_generate_item_brace attribute_instance_brace checker_or_generate_item + ; + +checker_or_generate_item: + checker_or_generate_item_declaration + | initial_construct + | always_construct + | final_construct + | assertion_item + | continuous_assign + | checker_generate_item + ; + +checker_or_generate_item_declaration: + data_declaration + | function_declaration + | checker_declaration + | assertion_item_declaration + | covergroup_declaration + | genvar_declaration + | TOK_DEFAULT TOK_CLOCKING clocking_identifier ';' + | TOK_DEFAULT TOK_DISABLE TOK_IFF expression_or_dist ';' + | ';' + ; + +checker_generate_item: + loop_generate_construct + | conditional_generate_construct + | generate_region + ; // System Verilog standard 1800-2017 // A.1.9 Class items @@ -1170,6 +1220,7 @@ package_or_generate_item_declaration: | data_declaration | task_declaration | function_declaration + | checker_declaration | class_declaration | local_parameter_declaration ';' | parameter_declaration ';' @@ -4076,6 +4127,10 @@ endmodule_identifier_opt: | TOK_COLON module_identifier ; +clocking_identifier: TOK_NON_TYPE_IDENTIFIER; + +checker_identifier: TOK_NON_TYPE_IDENTIFIER; + net_identifier: identifier; package_identifier: TOK_NON_TYPE_IDENTIFIER; diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp index 6ff6b0aa..de05478d 100644 --- a/src/verilog/verilog_expr.cpp +++ b/src/verilog/verilog_expr.cpp @@ -112,6 +112,18 @@ std::vector verilog_item_containert::dependencies() const return result; } +void verilog_checkert::show(std::ostream &out) const +{ + out << "Checker: " << base_name() << '\n'; + + out << " Items:\n"; + + for(auto &item : items()) + out << " " << item.pretty() << '\n'; + + out << '\n'; +} + void verilog_packaget::show(std::ostream &out) const { out << "Pacakge: " << base_name() << '\n'; diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 83e6cb4a..8feff587 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -2143,6 +2143,29 @@ inline verilog_module_sourcet &to_verilog_module_source(irept &irep) return static_cast(irep); } +class verilog_checkert : public verilog_item_containert +{ +public: + explicit verilog_checkert(irep_idt _base_name) + : verilog_item_containert(ID_verilog_module, _base_name) + { + } + + void show(std::ostream &) const; +}; + +inline const verilog_checkert &to_verilog_checker(const irept &irep) +{ + PRECONDITION(irep.id() == ID_verilog_checker); + return static_cast(irep); +} + +inline verilog_checkert &to_verilog_checker(irept &irep) +{ + PRECONDITION(irep.id() == ID_verilog_checker); + return static_cast(irep); +} + class verilog_packaget : public verilog_item_containert { public: diff --git a/src/verilog/verilog_parse_tree.cpp b/src/verilog/verilog_parse_tree.cpp index 5356f86f..d4bcb6d4 100644 --- a/src/verilog/verilog_parse_tree.cpp +++ b/src/verilog/verilog_parse_tree.cpp @@ -131,7 +131,9 @@ Function: verilog_parse_treet::show void verilog_parse_treet::show(const itemt &item, std::ostream &out) const { - if(item.id() == ID_verilog_class) + if(item.id() == ID_verilog_checker) + to_verilog_checker(item).show(out); + else if(item.id() == ID_verilog_class) to_verilog_class(item).show(out); else if(item.id() == ID_verilog_interface) to_verilog_interface(item).show(out);