Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SystemVerilog: $typename should return byte, int, shortint, etc. #978

Merged
merged 1 commit into from
Feb 9, 2025
Merged

SystemVerilog: $typename should return byte, int, shortint, etc. #978

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 12 additions & 6 deletions regression/verilog/data-types/signed2.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]");
Expand Down
2 changes: 1 addition & 1 deletion regression/verilog/packages/package_typedef1.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
34 changes: 24 additions & 10 deletions src/verilog/verilog_elaborate_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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;
}
Expand All @@ -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)
{
Expand Down
24 changes: 22 additions & 2 deletions src/verilog/verilog_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -727,19 +727,39 @@ 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)
{
s = "bit";
}
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)
{
Expand Down
47 changes: 46 additions & 1 deletion src/verilog/verilog_types.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
#define CPROVER_VERILOG_TYPES_H

#include <util/bitvector_types.h>
#include <util/ieee_float.h>

/// Used during elaboration only,
/// to signal that a symbol is yet to be elaborated.
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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;
}
};

Expand All @@ -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
Expand All @@ -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
Expand Down
Loading