diff --git a/regression/verilog/data-types/signed1.desc b/regression/verilog/data-types/signed1.desc new file mode 100644 index 000000000..893d20965 --- /dev/null +++ b/regression/verilog/data-types/signed1.desc @@ -0,0 +1,6 @@ +CORE +signed1.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/data-types/signed1.sv b/regression/verilog/data-types/signed1.sv new file mode 100644 index 000000000..08ab50c23 --- /dev/null +++ b/regression/verilog/data-types/signed1.sv @@ -0,0 +1,13 @@ +module main; + + wire signed one_bit_signed = -1; + + assert final (one_bit_signed == -1); + assert final ($bits(one_bit_signed) == 1); + + wire unsigned one_bit_unsigned = 1; + + assert final (one_bit_unsigned == 1); + assert final ($bits(one_bit_unsigned) == 1); + +endmodule diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp index c9402f428..d1503dad3 100644 --- a/src/verilog/verilog_elaborate_type.cpp +++ b/src/verilog/verilog_elaborate_type.cpp @@ -166,6 +166,16 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) // it's just a bit return bool_typet().with_source_location(source_location); } + else if(src.id() == ID_signed) + { + // one bit, signed + return signedbv_typet{1}.with_source_location(source_location); + } + else if(src.id() == ID_unsigned) + { + // one bit, unsigned + return unsignedbv_typet{1}.with_source_location(source_location); + } else if(src.id() == ID_verilog_byte) { return signedbv_typet{8}.with_source_location(source_location);