diff --git a/regression/verilog/expressions/signing_cast1.desc b/regression/verilog/expressions/signing_cast1.desc new file mode 100644 index 000000000..16d684056 --- /dev/null +++ b/regression/verilog/expressions/signing_cast1.desc @@ -0,0 +1,15 @@ +KNOWNBUG +signing_cast1.sv +--module main --bound 0 +^\[main\.p0\] always signed \[0:0\]'\(1'b1\) == -1: PROVED up to bound 0$ +^\[main\.p1\] always signed \[0:0\]'\(4'b1110\) == -2: PROVED up to bound 0$ +^\[main\.p2\] always signed \[0:0\]'\(4'b0111\) == 7: PROVED up to bound 0$ +^\[main\.p3\] always signed \[0:0\]'\(!0\) == -1: PROVED up to bound 0$ +^\[main\.p4\] always \[0:0\]'\(!0\) == 1: PROVED up to bound 0$ +^\[main\.p5\] always \[0:0\]'\(-1\) == 32'hFFFFFFFF: PROVED up to bound 0$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +The width of the operand is not preserved. diff --git a/regression/verilog/expressions/signing_cast1.sv b/regression/verilog/expressions/signing_cast1.sv new file mode 100644 index 000000000..900a57162 --- /dev/null +++ b/regression/verilog/expressions/signing_cast1.sv @@ -0,0 +1,14 @@ +module main; + + // 1800-2017 6.24.1 + p0: assert final (signed'(1'b1) == -1); + p1: assert final (signed'(4'b1110) == -2); + p2: assert final (signed'(4'b0111) == 7); + p3: assert final (signed'(!0) == -1); + p4: assert final (unsigned'(!0) == 1); + p5: assert final (unsigned'(-1) == 32'hffff_ffff); + + // signing casts yield constants + parameter Q = signed'(1); + +endmodule diff --git a/regression/verilog/system-functions/signed2.desc b/regression/verilog/system-functions/signed2.desc new file mode 100644 index 000000000..9eff5979b --- /dev/null +++ b/regression/verilog/system-functions/signed2.desc @@ -0,0 +1,11 @@ +CORE +signed2.sv +--bound 0 +^\[main\.p0\] always \$signed\(1\) == 1: PROVED up to bound 0$ +^\[main\.p1\] always \$signed\(1'b1\) == -1: PROVED up to bound 0$ +^\[main\.p2\] always \$signed\(-1\) == -1: PROVED up to bound 0$ +^\[main\.p3\] always \$signed\(!0\) == -1: PROVED up to bound 0$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/system-functions/signed2.sv b/regression/verilog/system-functions/signed2.sv new file mode 100644 index 000000000..230fe5c95 --- /dev/null +++ b/regression/verilog/system-functions/signed2.sv @@ -0,0 +1,8 @@ +module main; + + p0: assert final ($signed(1) == 1); + p1: assert final ($signed(1'b1) == -1); + p2: assert final ($signed(-1) == -1); + p3: assert final ($signed(!0) == -1); + +endmodule diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 2951a0cd2..39054e148 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -784,7 +784,7 @@ exprt verilog_typecheck_exprt::convert_system_function( } else if(argument.type().id()==ID_bool) { - expr.type() = signedbv_typet{2}; + expr.type() = signedbv_typet{1}; return std::move(expr); } else