From d31183fa37f99c7cac138c9f908ecad9d1c13edd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 21 Nov 2024 06:15:07 -0800 Subject: [PATCH] SystemVerilog: event data type This adds 1800-2017 6.17 event. --- CHANGELOG | 2 +- regression/verilog/data-types/event1.desc | 6 ++++ regression/verilog/data-types/event1.sv | 18 +++++++++++ src/hw_cbmc_irep_ids.h | 3 +- src/verilog/expr2verilog.cpp | 4 ++- src/verilog/parser.y | 5 +-- src/verilog/verilog_elaborate.cpp | 3 ++ src/verilog/verilog_elaborate_type.cpp | 4 +++ src/verilog/verilog_lowering.cpp | 14 +++++++++ src/verilog/verilog_synthesis.cpp | 4 +++ src/verilog/verilog_typecheck.cpp | 4 +++ src/verilog/verilog_typecheck_expr.cpp | 16 ++++++++-- src/verilog/verilog_types.cpp | 5 +++ src/verilog/verilog_types.h | 37 +++++++++++++++++++++++ src/verilog/vtype.cpp | 13 ++++++-- src/verilog/vtype.h | 11 +++++-- 16 files changed, 136 insertions(+), 13 deletions(-) create mode 100644 regression/verilog/data-types/event1.desc create mode 100644 regression/verilog/data-types/event1.sv diff --git a/CHANGELOG b/CHANGELOG index 77f8ec1a..6cabeda5 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -6,7 +6,7 @@ * Verilog: fix for nor/nand/xnor primitive gates * SystemVerilog: $bitstoreal/$bitstoshortreal, $realtobits/$shortrealtobits * SystemVerilog: $itor, $rtoi -* SystemVerilog: chandle +* SystemVerilog: chandle, event # EBMC 5.4 diff --git a/regression/verilog/data-types/event1.desc b/regression/verilog/data-types/event1.desc new file mode 100644 index 00000000..3f34a56c --- /dev/null +++ b/regression/verilog/data-types/event1.desc @@ -0,0 +1,6 @@ +CORE +event1.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/data-types/event1.sv b/regression/verilog/data-types/event1.sv new file mode 100644 index 00000000..2dbbf2ea --- /dev/null +++ b/regression/verilog/data-types/event1.sv @@ -0,0 +1,18 @@ +module main; + + // IEEE 1800-2017 6.17 + event done; + event empty = null; + + task trigger_done; + -> done; + endtask + + task wait_until_done; + @ done; + endtask + + p0: assert final (empty == null); + p1: assert final ($typename(event) == "event"); + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index e51f9a65..5ece86e0 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -106,7 +106,8 @@ IREP_ID_ONE(verilog_streaming_concatenation_left_to_right) IREP_ID_ONE(verilog_streaming_concatenation_right_to_left) IREP_ID_ONE(verilog_chandle) IREP_ID_ONE(verilog_null) -IREP_ID_ONE(event) +IREP_ID_ONE(verilog_event) +IREP_ID_ONE(verilog_event_trigger) IREP_ID_ONE(reg) IREP_ID_ONE(macromodule) IREP_ID_ONE(output_register) diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 971c4165..ba204c42 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1260,7 +1260,7 @@ expr2verilogt::resultt expr2verilogt::convert_constant( dest += '"'; } - else if(type.id() == ID_verilog_chandle) + else if(type.id() == ID_verilog_chandle || type.id() == ID_verilog_event) { if(src.get_value() == ID_NULL) { @@ -2041,6 +2041,8 @@ std::string expr2verilogt::convert(const typet &type) } else if(type.id() == ID_verilog_chandle) return "chandle"; + else if(type.id() == ID_verilog_event) + return "event"; else if(type.id() == ID_verilog_genvar) return "genvar"; else if(type.id()==ID_integer) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 1d20e592..7466356b 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1486,7 +1486,7 @@ data_type: $$ = $2; } // | class_type | TOK_EVENT - { init($$, ID_event); } + { init($$, ID_verilog_event); } /* | ps_covergroup_identifier */ @@ -3403,7 +3403,7 @@ event_control: ored_event_expression: event_expression - { init($$, ID_event); mto($$, $1); } + { init($$, ID_verilog_event); mto($$, $1); } | ored_event_expression TOK_OR event_expression { $$=$1; mto($$, $3); } | ored_event_expression ',' event_expression @@ -3878,6 +3878,7 @@ function_subroutine_call: subroutine_call ; event_trigger: TOK_MINUSGREATER hierarchical_event_identifier ';' + { init($$, ID_verilog_event_trigger); mto($$, $2); } ; // System Verilog standard 1800-2017 diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 5feb041d..e39b0d6d 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -751,6 +751,9 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement) else if(statement.id() == ID_wait) { } + else if(statement.id() == ID_verilog_event_trigger) + { + } else DATA_INVARIANT(false, "unexpected statement: " + statement.id_string()); } diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp index 413ad7fa..e2afb8ce 100644 --- a/src/verilog/verilog_elaborate_type.cpp +++ b/src/verilog/verilog_elaborate_type.cpp @@ -302,6 +302,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) result.set(ID_C_identifier, enum_type.identifier()); return result.with_source_location(source_location); } + else if(src.id() == ID_verilog_event) + { + return src; + } else if(src.id() == ID_verilog_packed_array) { return convert_packed_array_type(to_type_with_subtype(src)); diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp index 533d5e52..a94c6522 100644 --- a/src/verilog/verilog_lowering.cpp +++ b/src/verilog/verilog_lowering.cpp @@ -47,6 +47,10 @@ typet verilog_lowering(typet type) { return to_verilog_chandle_type(type).encoding(); } + else if(type.id() == ID_verilog_event) + { + return to_verilog_event_type(type).encoding(); + } else return type; } @@ -357,6 +361,11 @@ exprt verilog_lowering(exprt expr) // this is 'null' return to_verilog_chandle_type(expr.type()).null_expr(); } + else if(expr.type().id() == ID_verilog_event) + { + // this is 'null' + return to_verilog_event_type(expr.type()).null_expr(); + } return expr; } @@ -369,6 +378,11 @@ exprt verilog_lowering(exprt expr) return symbol_exprt{ symbol_expr.get_identifier(), chandle_type.encoding()}; } + else if(expr.type().id() == ID_verilog_event) + { + auto &event_type = to_verilog_event_type(expr.type()); + return symbol_exprt{symbol_expr.get_identifier(), event_type.encoding()}; + } else return expr; } diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index eace9eb3..f125b773 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -3185,6 +3185,10 @@ void verilog_synthesist::synth_statement( } else if(statement.id() == ID_verilog_label_statement) synth_statement(to_verilog_label_statement(statement).statement()); + else if(statement.id() == ID_verilog_event_trigger) + { + // not synthesized + } else { throw errort().with_location(statement.source_location()) diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 4ad34382..e61b46a4 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1613,6 +1613,10 @@ void verilog_typecheckt::convert_statement( else if(statement.id() == ID_wait) { } + else if(statement.id() == ID_verilog_event_trigger) + { + convert_expr(to_unary_expr(statement).op()); + } else { throw errort().with_location(statement.source_location()) diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 7574023d..c06631f1 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -345,7 +345,7 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr) { // variable number of operands - if(expr.id() == ID_event) + if(expr.id() == ID_verilog_event) { expr.type() = bool_typet(); @@ -757,6 +757,10 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr) { s = "chandle"; } + else if(type.id() == ID_verilog_event) + { + s = "event"; + } else s = "?"; @@ -2052,7 +2056,9 @@ void verilog_typecheck_exprt::implicit_typecast( } else if(src_type.id() == ID_verilog_null) { - if(dest_type.id() == ID_verilog_chandle) + if( + dest_type.id() == ID_verilog_chandle || + dest_type.id() == ID_verilog_event) { if(expr.id() == ID_constant) { @@ -2319,6 +2325,12 @@ typet verilog_typecheck_exprt::max_type( if(vt0.is_chandle() || vt1.is_null()) return t0; + if(vt0.is_null() || vt1.is_event()) + return t1; + + if(vt0.is_event() || vt1.is_null()) + return t0; + if(vt0.is_other() || vt1.is_other()) return static_cast(get_nil_irep()); diff --git a/src/verilog/verilog_types.cpp b/src/verilog/verilog_types.cpp index 75ecf9ed..9395b3a8 100644 --- a/src/verilog/verilog_types.cpp +++ b/src/verilog/verilog_types.cpp @@ -14,3 +14,8 @@ constant_exprt verilog_chandle_typet::null_expr() const { return encoding().all_zeros_expr(); } + +constant_exprt verilog_event_typet::null_expr() const +{ + return encoding().all_zeros_expr(); +} diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h index 40f4ec41..d723839b 100644 --- a/src/verilog/verilog_types.h +++ b/src/verilog/verilog_types.h @@ -581,4 +581,41 @@ inline verilog_chandle_typet &to_verilog_chandle_type(typet &type) return static_cast(type); } +/// The SystemVerilog event type +class verilog_event_typet : public typet +{ +public: + verilog_event_typet() : typet(ID_verilog_event) + { + } + + constant_exprt null_expr() const; + + bv_typet encoding() const + { + return bv_typet{32}; + } +}; + +/// \brief Cast a typet to a \ref verilog_event_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// verilog_event_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref verilog_event_typet +inline const verilog_event_typet &to_verilog_event_type(const typet &type) +{ + PRECONDITION(type.id() == ID_verilog_event); + return static_cast(type); +} + +/// \copydoc to_event_type(const typet &) +inline verilog_event_typet &to_verilog_event_type(typet &type) +{ + PRECONDITION(type.id() == ID_verilog_event); + return static_cast(type); +} + #endif diff --git a/src/verilog/vtype.cpp b/src/verilog/vtype.cpp index 788cc79a..c562ace7 100644 --- a/src/verilog/vtype.cpp +++ b/src/verilog/vtype.cpp @@ -78,6 +78,11 @@ vtypet::vtypet(const typet &type) vtype = CHANDLE; width = 32; } + else if(type.id() == ID_verilog_event) + { + vtype = EVENT; + width = 32; + } else { width=0; @@ -122,11 +127,14 @@ std::ostream &operator << (std::ostream &out, const vtypet &vtype) case vtypet::VERILOG_REAL: return out << "real"; + case vtypet::NULL_TYPE: + return out << "null"; + case vtypet::CHANDLE: return out << "chandle"; - case vtypet::NULL_TYPE: - return out << "null"; + case vtypet::EVENT: + return out << "event"; case vtypet::UNKNOWN: case vtypet::OTHER: @@ -134,4 +142,3 @@ std::ostream &operator << (std::ostream &out, const vtypet &vtype) return out << "?"; } } - diff --git a/src/verilog/vtype.h b/src/verilog/vtype.h index 1d9e6346..3b490bba 100644 --- a/src/verilog/vtype.h +++ b/src/verilog/vtype.h @@ -31,13 +31,17 @@ class vtypet { return vtype == VERILOG_REAL; } + bool is_null() const + { + return vtype == NULL_TYPE; + } bool is_chandle() const { return vtype == CHANDLE; } - bool is_null() const + inline bool is_event() const { - return vtype == NULL_TYPE; + return vtype == EVENT; } inline bool is_other() const { return vtype==OTHER; } @@ -52,8 +56,9 @@ class vtypet VERILOG_SIGNED, VERILOG_UNSIGNED, VERILOG_REAL, - CHANDLE, NULL_TYPE, + CHANDLE, + EVENT, OTHER } _vtypet; _vtypet vtype;