From f4f153bbfbe15782a21f4278c8b35ae924fc1fd0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 14 Jan 2025 11:45:14 -0800 Subject: [PATCH] SystemVerilog checkers This adds 1800-2017 Sec. 17 checkers. --- CHANGELOG | 1 + regression/verilog/checker/checker2.desc | 7 +++ regression/verilog/checker/checker2.sv | 9 +++ regression/verilog/checker/checker3.desc | 9 +++ regression/verilog/checker/checker3.sv | 14 +++++ src/hw_cbmc_irep_ids.h | 1 + src/verilog/parser.y | 76 +++++++++++++++++++++--- src/verilog/verilog_expr.cpp | 7 +++ src/verilog/verilog_expr.h | 12 ++++ src/verilog/verilog_parse_tree.cpp | 4 +- 10 files changed, 130 insertions(+), 10 deletions(-) create mode 100644 regression/verilog/checker/checker2.desc create mode 100644 regression/verilog/checker/checker2.sv create mode 100644 regression/verilog/checker/checker3.desc create mode 100644 regression/verilog/checker/checker3.sv diff --git a/CHANGELOG b/CHANGELOG index 8537c373..39080a61 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -10,6 +10,7 @@ * SystemVerilog: $itor, $rtoi * SystemVerilog: chandle, event, string * SystemVerilog: package scope operator +* SystemVerilog: checkers # EBMC 5.4 diff --git a/regression/verilog/checker/checker2.desc b/regression/verilog/checker/checker2.desc new file mode 100644 index 00000000..9a77a715 --- /dev/null +++ b/regression/verilog/checker/checker2.desc @@ -0,0 +1,7 @@ +CORE +checker2.sv +--bound 20 +^\[main\.c\.assert\.1\] always myChecker\.data != 10: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/checker/checker2.sv b/regression/verilog/checker/checker2.sv new file mode 100644 index 00000000..e1a8e276 --- /dev/null +++ b/regression/verilog/checker/checker2.sv @@ -0,0 +1,9 @@ +checker myChecker(input logic [31:0] data); + assert property (data != 10); +endchecker + +module main(input clk); + reg [31:0] counter = 0; + always_ff @(posedge clk) counter++; + myChecker c(counter); +endmodule diff --git a/regression/verilog/checker/checker3.desc b/regression/verilog/checker/checker3.desc new file mode 100644 index 00000000..7f9bbb4d --- /dev/null +++ b/regression/verilog/checker/checker3.desc @@ -0,0 +1,9 @@ +KNOWNBUG +checker3.sv +--bound 20 +^\[main\.c\.assert\.1\] always myChecker\.data != 10: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Support for property parameters is missing. diff --git a/regression/verilog/checker/checker3.sv b/regression/verilog/checker/checker3.sv new file mode 100644 index 00000000..f6900a40 --- /dev/null +++ b/regression/verilog/checker/checker3.sv @@ -0,0 +1,14 @@ +checker myChecker(property p); + assert property (p); +endchecker + +module main(input clk); + reg [31:0] counter = 0; + always_ff @(posedge clk) counter++; + + property my_prop; + counter != 10 + endproperty; + + myChecker c(my_prop); +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 628ac28f..6de2e27f 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -100,6 +100,7 @@ IREP_ID_ONE(verilog_indexed_part_select_minus) IREP_ID_ONE(verilog_past) IREP_ID_ONE(verilog_property_declaration) IREP_ID_ONE(verilog_sequence_declaration) +IREP_ID_ONE(verilog_sequence) IREP_ID_ONE(verilog_value_range) IREP_ID_ONE(verilog_void) IREP_ID_ONE(verilog_streaming_concatenation_left_to_right) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 6ef9a7d4..476dd85f 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -750,19 +750,68 @@ program_declaration: ; checker_declaration: - TOK_CHECKER checker_identifier - { - init($$, ID_verilog_checker); - stack_expr($$).set(ID_base_name, stack_expr($2).id()); - } - ';' + TOK_CHECKER { init($$); } checker_identifier + checker_port_list_paren_opt ';' checker_or_generate_item_brace TOK_ENDCHECKER { - $$ = $3; + init($$); + irept attributes; + exprt parameter_port_list; + stack_expr($$) = verilog_parse_treet::create_module( + attributes, // attributes, + stack_expr($2), // module_keyword + stack_expr($3), // name + parameter_port_list, // parameter_port_list + stack_expr($4), // ports + stack_expr($6) // module_items + ); + stack_expr($$).id(ID_verilog_checker); } ; +checker_port_list_paren_opt: + /* Optional */ + { init($$); } + | '(' checker_port_list_opt ')' + { $$ = $2; } + ; + +checker_port_list_opt: + /* Optional */ + { init($$); } + | checker_port_list + ; + +checker_port_list: + checker_port_item + { init($$); mts($$, $1); } + | checker_port_list checker_port_item + { $$ = $1; mts($$, $2); } + ; + +checker_port_item: + attribute_instance_brace + checker_port_direction_opt + property_formal_type + formal_port_identifier + variable_dimension_brace + { init($$, ID_decl); + stack_expr($$).set(ID_class, stack_expr($2).id()); + addswap($$, ID_type, $3); + mto($$, $4); /* declarator */ + } + ; + +checker_port_direction_opt: + /* Optional */ + { init($$); } + | TOK_INPUT + { init($$, ID_input); } + | TOK_OUTPUT + { init($$, ID_output); } + ; + class_declaration: TOK_CLASS class_identifier ';' @@ -1030,7 +1079,9 @@ non_port_interface_item: checker_or_generate_item_brace: /* Optional */ + { init($$); } | checker_or_generate_item_brace attribute_instance_brace checker_or_generate_item + { $$ = $1; mts($$, $3); } ; checker_or_generate_item: @@ -2323,7 +2374,8 @@ property_port_item: ; property_formal_type: - TOK_PROPERTY + sequence_formal_type + | TOK_PROPERTY ; property_spec: @@ -2334,6 +2386,14 @@ property_spec: | property_expr ; +sequence_formal_type: + data_type + | TOK_SEQUENCE + { init($$, ID_verilog_sequence); } + | TOK_UNTYPED + { init($$, ID_verilog_untyped); } + ; + // The 1800-2017 grammar has an ambiguity where // '(' expression ')' can either be an expression or a property_expr, // which yields a reduce/reduce conflict. Hence, we split the rules diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp index 56edaa5d..faf88735 100644 --- a/src/verilog/verilog_expr.cpp +++ b/src/verilog/verilog_expr.cpp @@ -124,6 +124,13 @@ void verilog_checkert::show(std::ostream &out) const { out << "Checker: " << base_name() << '\n'; + out << " Ports:\n"; + + for(auto &port : ports()) + out << " " << port.pretty() << '\n'; + + out << '\n'; + out << " Items:\n"; for(auto &item : items()) diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 16fa339e..4ee3d256 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -2354,6 +2354,18 @@ class verilog_checkert : public verilog_item_containert { } + using portst = std::vector; + + portst &ports() + { + return (portst &)(add(ID_ports).get_sub()); + } + + const portst &ports() const + { + return (const portst &)(find(ID_ports).get_sub()); + } + void show(std::ostream &) const; }; diff --git a/src/verilog/verilog_parse_tree.cpp b/src/verilog/verilog_parse_tree.cpp index 93df40db..f796bd51 100644 --- a/src/verilog/verilog_parse_tree.cpp +++ b/src/verilog/verilog_parse_tree.cpp @@ -61,7 +61,7 @@ void verilog_parse_treet::modules_provided( { for(auto &item : items) { - if(item.id() == ID_verilog_module) + if(item.id() == ID_verilog_module || item.id() == ID_verilog_checker) { module_set.insert(id2string( verilog_module_symbol(to_verilog_module_source(item).base_name()))); @@ -92,7 +92,7 @@ void verilog_parse_treet::build_item_map() for(const auto &item : items) { - if(item.id() == ID_verilog_module) + if(item.id() == ID_verilog_module || item.id() == ID_verilog_checker) { auto &verilog_module = to_verilog_module_source(item); item_map[verilog_module.base_name()] = &verilog_module;