From 413d94f01db2b89c3b2b5cff80a75a183fdbc23d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 8 Feb 2025 17:36:35 +0000 Subject: [PATCH] SystemVerilog: $typename should return byte, int, shortint, etc. When given byte, int, shortint, int, longint, $typename needs to return that instead of the expansion. --- regression/verilog/data-types/signed2.sv | 18 ++++--- .../verilog/packages/package_typedef1.sv | 2 +- src/verilog/verilog_elaborate_type.cpp | 34 ++++++++++---- src/verilog/verilog_typecheck_expr.cpp | 24 +++++++++- src/verilog/verilog_types.h | 47 ++++++++++++++++++- 5 files changed, 105 insertions(+), 20 deletions(-) diff --git a/regression/verilog/data-types/signed2.sv b/regression/verilog/data-types/signed2.sv index 6a654590..a191b89e 100644 --- a/regression/verilog/data-types/signed2.sv +++ b/regression/verilog/data-types/signed2.sv @@ -5,12 +5,18 @@ module main; assert final ($typename(bit unsigned[1:0]) == "bit[1:0]"); assert final ($typename(bit signed) == "bit signed[0:0]"); assert final ($typename(bit signed[1:0]) == "bit signed[1:0]"); - assert final ($typename(byte) == "bit signed[7:0]"); - assert final ($typename(byte unsigned) == "bit[7:0]"); - assert final ($typename(byte signed) == "bit signed[7:0]"); - assert final ($typename(int) == "bit signed[31:0]"); - assert final ($typename(int unsigned) == "bit[31:0]"); - assert final ($typename(int signed) == "bit signed[31:0]"); + assert final ($typename(byte) == "byte"); + assert final ($typename(byte unsigned) == "byte unsigned"); + assert final ($typename(byte signed) == "byte"); + assert final ($typename(int) == "int"); + assert final ($typename(int unsigned) == "int unsigned"); + assert final ($typename(int signed) == "int"); + assert final ($typename(shortint) == "shortint"); + assert final ($typename(shortint unsigned) == "shortint unsigned"); + assert final ($typename(shortint signed) == "shortint"); + assert final ($typename(longint) == "longint"); + assert final ($typename(longint unsigned) == "longint unsigned"); + assert final ($typename(longint signed) == "longint"); assert final ($typename(integer) == "bit signed[31:0]"); assert final ($typename(integer unsigned) == "bit[31:0]"); assert final ($typename(integer signed) == "bit signed[31:0]"); diff --git a/regression/verilog/packages/package_typedef1.sv b/regression/verilog/packages/package_typedef1.sv index 4484e35d..2eb2fd70 100644 --- a/regression/verilog/packages/package_typedef1.sv +++ b/regression/verilog/packages/package_typedef1.sv @@ -8,6 +8,6 @@ module main; moo::my_type some_var; - assert final ($typename(some_var) == "bit signed[7:0]"); + assert final ($typename(some_var) == "byte"); endmodule diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp index b291782e..f297f7b6 100644 --- a/src/verilog/verilog_elaborate_type.cpp +++ b/src/verilog/verilog_elaborate_type.cpp @@ -219,7 +219,15 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) auto rec = elaborate_type(subtype); if(rec.id() == ID_unsignedbv) - return signedbv_typet{to_unsignedbv_type(rec).width()}; + { + typet dest = signedbv_typet{to_unsignedbv_type(rec).width()}; + + auto verilog_type = rec.get(ID_C_verilog_type); + if(verilog_type != irep_idt{}) + dest.set(ID_C_verilog_type, verilog_type); + + return dest; + } else if(rec.id() == ID_bool) return signedbv_typet{1}; else @@ -241,7 +249,15 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) auto rec = elaborate_type(subtype); if(rec.id() == ID_signedbv) - return unsignedbv_typet{to_signedbv_type(rec).width()}; + { + typet dest = unsignedbv_typet{to_signedbv_type(rec).width()}; + + auto verilog_type = rec.get(ID_C_verilog_type); + if(verilog_type != irep_idt{}) + dest.set(ID_C_verilog_type, verilog_type); + + return dest; + } else return rec; } @@ -255,23 +271,21 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) } else if(src.id() == ID_verilog_byte) { - // two-valued type, signed - return signedbv_typet{8}.with_source_location(source_location); + return verilog_byte_typet{}.lower().with_source_location(source_location); } else if(src.id() == ID_verilog_shortint) { - // two-valued type, signed - return signedbv_typet{16}.with_source_location(source_location); + return verilog_shortint_typet{}.lower().with_source_location( + source_location); } else if(src.id() == ID_verilog_int) { - // two-valued type, signed - return signedbv_typet{32}.with_source_location(source_location); + return verilog_int_typet{}.lower().with_source_location(source_location); } else if(src.id() == ID_verilog_longint) { - // two-valued type, signed - return signedbv_typet{64}.with_source_location(source_location); + return verilog_longint_typet{}.lower().with_source_location( + source_location); } else if(src.id() == ID_verilog_integer) { diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index d85f3c8d..920648c6 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -727,11 +727,22 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr) auto left = this->left(expr); auto right = this->right(expr); + const auto verilog_type = type.get(ID_C_verilog_type); + std::string s; if(type.id() == ID_unsignedbv || type.id() == ID_verilog_unsignedbv) { - s = "bit[" + to_string(left) + ":" + to_string(right) + "]"; + if(verilog_type == ID_verilog_byte) + s = "byte unsigned"; + else if(verilog_type == ID_verilog_int) + s = "int unsigned"; + else if(verilog_type == ID_verilog_longint) + s = "longint unsigned"; + else if(verilog_type == ID_verilog_shortint) + s = "shortint unsigned"; + else + s = "bit[" + to_string(left) + ":" + to_string(right) + "]"; } else if(type.id() == ID_bool) { @@ -739,7 +750,16 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr) } else if(type.id() == ID_signedbv || type.id() == ID_verilog_signedbv) { - s = "bit signed[" + to_string(left) + ":" + to_string(right) + "]"; + if(verilog_type == ID_verilog_byte) + s = "byte"; + else if(verilog_type == ID_verilog_int) + s = "int"; + else if(verilog_type == ID_verilog_longint) + s = "longint"; + else if(verilog_type == ID_verilog_shortint) + s = "shortint"; + else + s = "bit signed[" + to_string(left) + ":" + to_string(right) + "]"; } else if(type.id() == ID_verilog_realtime) { diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h index 81a95cf3..64eddfd7 100644 --- a/src/verilog/verilog_types.h +++ b/src/verilog/verilog_types.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_VERILOG_TYPES_H #include +#include /// Used during elaboration only, /// to signal that a symbol is yet to be elaborated. @@ -162,6 +163,13 @@ class verilog_real_typet:public typet { return 64; } + + typet lower() const + { + typet type = ieee_float_spect::double_precision().to_type(); + type.set(ID_C_verilog_type, ID_verilog_real); + return type; + } }; /// 32-bit floating point @@ -176,6 +184,13 @@ class verilog_shortreal_typet:public typet { return 32; } + + typet lower() const + { + typet type = ieee_float_spect::single_precision().to_type(); + type.set(ID_C_verilog_type, ID_verilog_shortreal); + return type; + } }; /// 64-bit floating point @@ -190,6 +205,13 @@ class verilog_realtime_typet:public typet { return 64; } + + typet lower() const + { + typet type = ieee_float_spect::double_precision().to_type(); + type.set(ID_C_verilog_type, ID_verilog_realtime); + return type; + } }; /// 2-state data type, 16-bit signed integer @@ -204,6 +226,13 @@ class verilog_shortint_typet : public typet { return 16; } + + typet lower() const + { + typet type = signedbv_typet{width()}; + type.set(ID_C_verilog_type, ID_verilog_shortint); + return type; + } }; /// 2-state data type, 32-bit signed integer @@ -221,7 +250,9 @@ class verilog_int_typet : public typet typet lower() const { - return signedbv_typet{width()}; + typet type = signedbv_typet{width()}; + type.set(ID_C_verilog_type, ID_verilog_int); + return type; } }; @@ -237,6 +268,13 @@ class verilog_longint_typet : public typet { return 64; } + + typet lower() const + { + typet type = signedbv_typet{width()}; + type.set(ID_C_verilog_type, ID_verilog_longint); + return type; + } }; /// 2-state data type, 8-bit signed integer @@ -251,6 +289,13 @@ class verilog_byte_typet : public typet { return 8; } + + typet lower() const + { + typet type = signedbv_typet{width()}; + type.set(ID_C_verilog_type, ID_verilog_byte); + return type; + } }; /// 2-state data type, for vectors, unsigned