From 3fb4d16541439478b36e58b558dd6dce75b5f665 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 21 Nov 2024 06:02:23 -0800 Subject: [PATCH] SystemVerilog: string data type This adds 1800-2017 6.16 string. --- CHANGELOG | 2 +- regression/verilog/data-types/string1.desc | 7 +++++++ regression/verilog/data-types/string1.sv | 7 +++++++ src/hw_cbmc_irep_ids.h | 1 + src/verilog/expr2verilog.cpp | 2 ++ src/verilog/parser.y | 2 +- src/verilog/verilog_elaborate_type.cpp | 4 ++++ src/verilog/verilog_typecheck_expr.cpp | 19 +++++++++++++++++++ src/verilog/vtype.cpp | 8 ++++++++ src/verilog/vtype.h | 5 +++++ 10 files changed, 55 insertions(+), 2 deletions(-) create mode 100644 regression/verilog/data-types/string1.desc create mode 100644 regression/verilog/data-types/string1.sv diff --git a/CHANGELOG b/CHANGELOG index 0f4f3e15..652c7e4a 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -8,7 +8,7 @@ * Verilog: fix for nor/nand/xnor primitive gates * SystemVerilog: $bitstoreal/$bitstoshortreal, $realtobits/$shortrealtobits * SystemVerilog: $itor, $rtoi -* SystemVerilog: chandle, event +* SystemVerilog: chandle, event, string # EBMC 5.4 diff --git a/regression/verilog/data-types/string1.desc b/regression/verilog/data-types/string1.desc new file mode 100644 index 00000000..d1b6fc37 --- /dev/null +++ b/regression/verilog/data-types/string1.desc @@ -0,0 +1,7 @@ +CORE +string1.sv +--bound 0 +^no properties$ +^EXIT=10$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/data-types/string1.sv b/regression/verilog/data-types/string1.sv new file mode 100644 index 00000000..a96106a2 --- /dev/null +++ b/regression/verilog/data-types/string1.sv @@ -0,0 +1,7 @@ +module main; + + // IEEE 1800-2017 6.16 + string xyz; + string my_string = xyz; + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 5ece86e0..443cba59 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -108,6 +108,7 @@ IREP_ID_ONE(verilog_chandle) IREP_ID_ONE(verilog_null) IREP_ID_ONE(verilog_event) IREP_ID_ONE(verilog_event_trigger) +IREP_ID_ONE(verilog_string) 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 ba204c42..dfa72fe2 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1988,6 +1988,8 @@ std::string expr2verilogt::convert(const typet &type) return "logic"; else if(type.id() == ID_verilog_integer) return "integer"; + else if(type.id() == ID_verilog_string) + return "string"; else if(type.id() == ID_verilog_reg) return "reg"; else if(type.id() == ID_verilog_time) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 7466356b..d7e9814a 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1475,7 +1475,7 @@ data_type: stack_expr($$).set(ID_identifier, id); } | TOK_STRING - { init($$, ID_string); } + { init($$, ID_verilog_string); } | TOK_CHANDLE { init($$, ID_verilog_chandle); } | TOK_VIRTUAL interface_opt interface_identifier diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp index e2afb8ce..6c48c8f0 100644 --- a/src/verilog/verilog_elaborate_type.cpp +++ b/src/verilog/verilog_elaborate_type.cpp @@ -379,6 +379,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) return struct_union_typet{src.id(), std::move(components)} .with_source_location(src.source_location()); } + else if(src.id() == ID_verilog_string) + { + return src; + } else if(src.id() == ID_type) { return src; diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index c06631f1..359a6db6 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -761,6 +761,10 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr) { s = "event"; } + else if(type.id() == ID_verilog_string) + { + s = "string"; + } else s = "?"; @@ -2331,6 +2335,21 @@ typet verilog_typecheck_exprt::max_type( if(vt0.is_event() || vt1.is_null()) return t0; + if( + vt0.is_string() && (vt1.is_signed() || vt1.is_unsigned() || + vt1.is_verilog_signed() || vt1.is_verilog_unsigned())) + { + return t0; + } + + if( + (vt0.is_signed() || vt0.is_unsigned() || vt0.is_verilog_signed() || + vt0.is_verilog_unsigned()) && + vt0.is_string()) + { + return t1; + } + if(vt0.is_other() || vt1.is_other()) return static_cast(get_nil_irep()); diff --git a/src/verilog/vtype.cpp b/src/verilog/vtype.cpp index c562ace7..2d3c3931 100644 --- a/src/verilog/vtype.cpp +++ b/src/verilog/vtype.cpp @@ -83,6 +83,11 @@ vtypet::vtypet(const typet &type) vtype = EVENT; width = 32; } + else if(type.id() == ID_verilog_string) + { + vtype = STRING; + width = 0; + } else { width=0; @@ -136,6 +141,9 @@ std::ostream &operator << (std::ostream &out, const vtypet &vtype) case vtypet::EVENT: return out << "event"; + case vtypet::STRING: + return out << "string"; + case vtypet::UNKNOWN: case vtypet::OTHER: default: diff --git a/src/verilog/vtype.h b/src/verilog/vtype.h index 3b490bba..b87f2fd2 100644 --- a/src/verilog/vtype.h +++ b/src/verilog/vtype.h @@ -43,6 +43,10 @@ class vtypet { return vtype == EVENT; } + bool is_string() const + { + return vtype == STRING; + } inline bool is_other() const { return vtype==OTHER; } protected: @@ -59,6 +63,7 @@ class vtypet NULL_TYPE, CHANDLE, EVENT, + STRING, OTHER } _vtypet; _vtypet vtype;