diff --git a/regression/verilog/data-types/type_operator.desc b/regression/verilog/data-types/type_operator.desc new file mode 100644 index 000000000..45cf876ca --- /dev/null +++ b/regression/verilog/data-types/type_operator.desc @@ -0,0 +1,8 @@ +CORE +type_operator.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/data-types/type_operator.sv b/regression/verilog/data-types/type_operator.sv new file mode 100644 index 000000000..0aff35ede --- /dev/null +++ b/regression/verilog/data-types/type_operator.sv @@ -0,0 +1,12 @@ +module main; + + wire [31:0] some_wire; + wire type(some_wire) other_wire; + + typedef bit [31:0] some_type; + wire some_type next_wire; + + p0: assert property ($bits(other_wire) == 32); + p1: assert property ($bits(next_wire) == 32); + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 9b84e7729..8ec5930c1 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -106,6 +106,7 @@ IREP_ID_ONE(uwire) IREP_ID_ONE(wand) IREP_ID_ONE(automatic) IREP_ID_ONE(verilog_enum) +IREP_ID_ONE(verilog_type_reference) IREP_ID_ONE(enum_names) IREP_ID_ONE(var) IREP_ID_ONE(trireg) diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index b4e19e66a..238df294c 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1180,6 +1180,14 @@ std::string expr2verilogt::convert(const typet &type) { return "enum"; } + else if(type.id() == ID_verilog_type_reference) + { + auto &type_reference = to_verilog_type_reference(type); + if(type_reference.expression_op().is_not_nil()) + return "type(" + convert(type_reference.expression_op()) + ")"; + else + return "type(" + convert(type_reference.type_op()) + ")"; + } return "IREP("+type.pretty()+")"; } diff --git a/src/verilog/parser.y b/src/verilog/parser.y index c00a04e68..3dc412111 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1255,6 +1255,7 @@ data_type: /* | ps_covergroup_identifier */ + | type_reference ; enum_name_value_opt: @@ -1388,6 +1389,13 @@ simple_type: data_type_or_void: data_type | TOK_VOID ; +type_reference: + TOK_TYPE '(' expression ')' + { init($$, ID_verilog_type_reference); mto($$, $3); } + | TOK_TYPE '(' data_type ')' + { init($$, ID_verilog_type_reference); addswap($$, ID_type_arg, $3); } + ; + // System Verilog standard 1800-2017 // A.2.2.2 Strengths diff --git a/src/verilog/verilog_typecheck_type.cpp b/src/verilog/verilog_typecheck_type.cpp index 924335f3e..5ddcaf652 100644 --- a/src/verilog/verilog_typecheck_type.cpp +++ b/src/verilog/verilog_typecheck_type.cpp @@ -164,6 +164,19 @@ typet verilog_typecheck_exprt::convert_type(const typet &src) return std::move(result); } } + else if(src.id() == ID_verilog_type_reference) + { + auto &type_reference = to_verilog_type_reference(src); + if(type_reference.expression_op().is_not_nil()) + { + // the expression is not evaluated + auto expr = type_reference.expression_op(); + convert_expr(expr); + return expr.type(); + } + else + return convert_type(type_reference.type_op()); + } else { error().source_location = source_location; diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h index 854253242..5f25065be 100644 --- a/src/verilog/verilog_types.h +++ b/src/verilog/verilog_types.h @@ -407,4 +407,49 @@ inline verilog_enum_typet &to_verilog_enum_type(typet &type) return static_cast(type); } +class verilog_type_referencet : public typet +{ +public: + // This comes in two flavors: a reference to the type + // of a given type, or of a given expression. + const exprt &expression_op() const + { + if(get_sub().size() == 1) + return static_cast(get_sub().front()); + else + return static_cast(get_nil_irep()); + } + + const typet &type_op() const + { + return static_cast(find(ID_type_arg)); + } +}; + +/*! \brief Cast a generic typet to a \ref verilog_type_referencet + * + * This is an unchecked conversion. \a type must be known to be \ref + * verilog_type_referencet. + * + * \param type Source type + * \return Object of type \ref verilog_type_referencet + * + * \ingroup gr_std_types +*/ +inline const verilog_type_referencet & +to_verilog_type_reference(const typet &type) +{ + PRECONDITION(type.id() == ID_verilog_type_reference); + return static_cast(type); +} + +/*! \copydoc to_verilog_type_reference(const typet &) + * \ingroup gr_std_types +*/ +inline verilog_type_referencet &to_verilog_type_reference(typet &type) +{ + PRECONDITION(type.id() == ID_verilog_type_reference); + return static_cast(type); +} + #endif