From 25636cffd471857c5f7824b78afcf817a1eba169 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 2 Dec 2024 16:37:29 +0000 Subject: [PATCH] SystemVerilog: named sequences This adds SystemVerilog named sequences. --- CHANGELOG | 1 + regression/verilog/SVA/named_sequence1.desc | 9 ++++ regression/verilog/SVA/named_sequence1.sv | 16 +++++++ src/hw_cbmc_irep_ids.h | 1 + src/verilog/parser.y | 46 ++++++++++++++++++++- src/verilog/verilog_elaborate.cpp | 9 ++++ src/verilog/verilog_expr.h | 38 +++++++++++++++++ src/verilog/verilog_interfaces.cpp | 3 ++ src/verilog/verilog_synthesis.cpp | 3 ++ src/verilog/verilog_typecheck.cpp | 38 +++++++++++++++++ src/verilog/verilog_typecheck.h | 2 + 11 files changed, 165 insertions(+), 1 deletion(-) create mode 100644 regression/verilog/SVA/named_sequence1.desc create mode 100644 regression/verilog/SVA/named_sequence1.sv diff --git a/CHANGELOG b/CHANGELOG index 70565eb2c..051cc3482 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -6,6 +6,7 @@ * BMC: support SVA sequence intersect * SystemVerilog: streaming concatenation {<<{...}} and {>>{...}} * SystemVerilog: set membership operator +* SystemVerilog: named sequences # EBMC 5.3 diff --git a/regression/verilog/SVA/named_sequence1.desc b/regression/verilog/SVA/named_sequence1.desc new file mode 100644 index 000000000..97b51302f --- /dev/null +++ b/regression/verilog/SVA/named_sequence1.desc @@ -0,0 +1,9 @@ +CORE +named_sequence1.sv +--bound 0 +^\[main\.assert\.1\] always main\.x_is_ten: PROVED up to bound 0$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/named_sequence1.sv b/regression/verilog/SVA/named_sequence1.sv new file mode 100644 index 000000000..b568a82a4 --- /dev/null +++ b/regression/verilog/SVA/named_sequence1.sv @@ -0,0 +1,16 @@ +module main(input clk); + + wire [31:0] x = 10; + + sequence x_is_ten; + x == 10 ##1 x >= 0 + endsequence : x_is_ten + + assert property (x_is_ten); + + sequence x_is_twenty; + // the ; is optional + x == 20; + endsequence : x_is_twenty + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 1eaa9bd49..2f3efca0a 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -96,6 +96,7 @@ IREP_ID_ONE(verilog_indexed_part_select_plus) 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_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 37b07a200..04f01ae5e 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2245,11 +2245,12 @@ expect_property_statement: TOK_EXPECT '(' property_spec ')' action_block assertion_item_declaration: property_declaration + | sequence_declaration ; property_declaration: TOK_PROPERTY property_identifier property_port_list_paren_opt ';' - property_spec + property_spec semicolon_opt TOK_ENDPROPERTY property_identifier_opt { init($$, ID_verilog_property_declaration); stack_expr($$).set(ID_base_name, stack_expr($2).id()); @@ -2386,6 +2387,47 @@ property_case_item: { init($$, ID_case_item); mto($$, $3); } ; +sequence_declaration: + "sequence" { init($$, ID_verilog_sequence_declaration); } + sequence_identifier sequence_port_list_opt ';' + sequence_expr semicolon_opt + "endsequence" sequence_identifier_opt + { $$=$2; + stack_expr($$).set(ID_base_name, stack_expr($3).id()); + mto($$, $6); + } + ; + +sequence_port_list_opt: + /* Optional */ + { init($$); } + | '(' ')' + { init($$); } + | '(' sequence_port_list ')' + { $$=$2; } + ; + +sequence_port_list: + sequence_port_item + { init($$); mto($$, $1); } + | sequence_port_list sequence_port_item + { $$=$1; mto($$, $2); } + ; + +sequence_port_item: + formal_port_identifier + ; + +sequence_identifier_opt: + /* Optional */ + | TOK_COLON sequence_identifier + ; + +semicolon_opt: + /* Optional */ + | ';' + ; + expression_or_dist_brace: expression_or_dist { init($$, "patterns"); mto($$, $1); } @@ -4190,6 +4232,8 @@ identifier: non_type_identifier; property_identifier: TOK_NON_TYPE_IDENTIFIER; +sequence_identifier: TOK_NON_TYPE_IDENTIFIER; + variable_identifier: identifier; %% diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 38b1f313c..f2724eae7 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -118,6 +118,11 @@ void verilog_typecheckt::collect_symbols( { } +void verilog_typecheckt::collect_symbols( + const verilog_sequence_declarationt &declaration) +{ +} + void verilog_typecheckt::collect_symbols(const typet &type) { // These types are not yet converted. @@ -834,6 +839,10 @@ void verilog_typecheckt::collect_symbols( { collect_symbols(to_verilog_property_declaration(module_item)); } + else if(module_item.id() == ID_verilog_sequence_declaration) + { + collect_symbols(to_verilog_sequence_declaration(module_item)); + } else DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string()); } diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 9b2898e44..49e08aa60 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -2620,6 +2620,44 @@ to_verilog_property_declaration(exprt &expr) return static_cast(expr); } +class verilog_sequence_declarationt : public verilog_module_itemt +{ +public: + explicit verilog_sequence_declarationt(exprt sequence) + { + add_to_operands(std::move(sequence)); + } + + const irep_idt &base_name() const + { + return get(ID_base_name); + } + + const exprt &sequence() const + { + return op0(); + } + + exprt &sequence() + { + return op0(); + } +}; + +inline const verilog_sequence_declarationt & +to_verilog_sequence_declaration(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_verilog_sequence_declaration); + return static_cast(expr); +} + +inline verilog_sequence_declarationt & +to_verilog_sequence_declaration(exprt &expr) +{ + PRECONDITION(expr.id() == ID_verilog_sequence_declaration); + return static_cast(expr); +} + class verilog_streaming_concatenation_exprt : public exprt { public: diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index 741b5177d..d542d071a 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -306,6 +306,9 @@ void verilog_typecheckt::interface_module_item( else if(module_item.id() == ID_verilog_property_declaration) { } + else if(module_item.id() == ID_verilog_sequence_declaration) + { + } 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 2698d4796..47527286b 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -3290,6 +3290,9 @@ void verilog_synthesist::synth_module_item( else if(module_item.id() == ID_verilog_property_declaration) { } + else if(module_item.id() == ID_verilog_sequence_declaration) + { + } else { throw errort().with_location(module_item.source_location()) diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index c57016338..1f4bb7dcf 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1699,6 +1699,10 @@ void verilog_typecheckt::convert_module_item( { convert_property_declaration(to_verilog_property_declaration(module_item)); } + else if(module_item.id() == ID_verilog_sequence_declaration) + { + convert_sequence_declaration(to_verilog_sequence_declaration(module_item)); + } else { throw errort().with_location(module_item.source_location()) @@ -1743,6 +1747,40 @@ void verilog_typecheckt::convert_property_declaration( /*******************************************************************\ +Function: verilog_typecheckt::convert_sequence_declaration + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void verilog_typecheckt::convert_sequence_declaration( + verilog_sequence_declarationt &declaration) +{ + auto base_name = declaration.base_name(); + auto full_identifier = hierarchical_identifier(base_name); + + convert_sva(declaration.sequence()); + + auto type = bool_typet{}; + type.set(ID_C_verilog_type, ID_verilog_sequence_declaration); + symbolt symbol{full_identifier, type, mode}; + + symbol.module = module_identifier; + symbol.base_name = base_name; + symbol.pretty_name = strip_verilog_prefix(symbol.name); + symbol.is_macro = true; + symbol.value = declaration.sequence(); + symbol.location = declaration.source_location(); + + add_symbol(std::move(symbol)); +} + +/*******************************************************************\ + Function: verilog_typecheckt::convert_statements Inputs: diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index 3a29a9212..94f01d936 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -106,6 +106,7 @@ class verilog_typecheckt: void collect_symbols(const verilog_lett &); void collect_symbols(const verilog_statementt &); void collect_symbols(const verilog_property_declarationt &); + void collect_symbols(const verilog_sequence_declarationt &); void collect_symbols(const typet &, const verilog_parameter_declt::declaratort &); void collect_port_symbols(const verilog_declt &); @@ -187,6 +188,7 @@ class verilog_typecheckt: void convert_module_item(class verilog_module_itemt &); void convert_parameter_override(const class verilog_parameter_overridet &); void convert_property_declaration(class verilog_property_declarationt &); + void convert_sequence_declaration(class verilog_sequence_declarationt &); void integer_expr(exprt &expr);