From d935c4ecd5a6e888ce36da732b7954948c9e5ba5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 20 Dec 2024 17:28:25 +0000 Subject: [PATCH] SystemVerilog: conversion functions This adds the conversion functions from 1800-2017 20.5. --- CHANGELOG | 2 + .../verilog/expressions/cast_from_real1.desc | 9 + .../verilog/expressions/cast_from_real1.sv | 9 + .../verilog/expressions/cast_to_real1.sv | 2 +- .../verilog/system-functions/bitstoreal1.desc | 7 + .../verilog/system-functions/bitstoreal1.sv | 11 + .../system-functions/bitstoshortreal1.desc | 7 + .../system-functions/bitstoshortreal1.sv | 11 + .../verilog/system-functions/itor1.desc | 7 + regression/verilog/system-functions/itor1.sv | 9 + .../verilog/system-functions/realtobits1.desc | 7 + .../verilog/system-functions/realtobits1.sv | 11 + .../verilog/system-functions/rtoi1.desc | 7 + regression/verilog/system-functions/rtoi1.sv | 10 + .../system-functions/shortrealtobits1.desc | 7 + .../system-functions/shortrealtobits1.sv | 11 + src/verilog/verilog_lowering.cpp | 240 ++++++++++++------ src/verilog/verilog_synthesis.cpp | 2 +- src/verilog/verilog_typecheck_expr.cpp | 85 ++++++- 19 files changed, 371 insertions(+), 83 deletions(-) create mode 100644 regression/verilog/expressions/cast_from_real1.desc create mode 100644 regression/verilog/expressions/cast_from_real1.sv create mode 100644 regression/verilog/system-functions/bitstoreal1.desc create mode 100644 regression/verilog/system-functions/bitstoreal1.sv create mode 100644 regression/verilog/system-functions/bitstoshortreal1.desc create mode 100644 regression/verilog/system-functions/bitstoshortreal1.sv create mode 100644 regression/verilog/system-functions/itor1.desc create mode 100644 regression/verilog/system-functions/itor1.sv create mode 100644 regression/verilog/system-functions/realtobits1.desc create mode 100644 regression/verilog/system-functions/realtobits1.sv create mode 100644 regression/verilog/system-functions/rtoi1.desc create mode 100644 regression/verilog/system-functions/rtoi1.sv create mode 100644 regression/verilog/system-functions/shortrealtobits1.desc create mode 100644 regression/verilog/system-functions/shortrealtobits1.sv diff --git a/CHANGELOG b/CHANGELOG index 05f28e60..25f42790 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -4,6 +4,8 @@ * Verilog: fix for primitive gates with more than two inputs * Verilog: Support $past when using AIG-based engines * Verilog: fix for nor/nand/xnor primitive gates +* SystemVerilog: $bitstoreal/$bitstoshortreal, $realtobits/$shortrealtobits +* SystemVerilog: $itor, $rtoi # EBMC 5.4 diff --git a/regression/verilog/expressions/cast_from_real1.desc b/regression/verilog/expressions/cast_from_real1.desc new file mode 100644 index 00000000..685e4a11 --- /dev/null +++ b/regression/verilog/expressions/cast_from_real1.desc @@ -0,0 +1,9 @@ +KNOWNBUG +cast_from_real1.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Verilog casts from real to integer round, and do not truncate. diff --git a/regression/verilog/expressions/cast_from_real1.sv b/regression/verilog/expressions/cast_from_real1.sv new file mode 100644 index 00000000..c1f704d1 --- /dev/null +++ b/regression/verilog/expressions/cast_from_real1.sv @@ -0,0 +1,9 @@ +module main; + + always assert (integer'(1.0) == 1); + always assert (integer'(-1.0) == -1); + + // Casting rounds away from zero (1800-2017 6.12.2) + always assert (integer'(1.9) == 2); + +endmodule diff --git a/regression/verilog/expressions/cast_to_real1.sv b/regression/verilog/expressions/cast_to_real1.sv index 9f354b54..5810cc64 100644 --- a/regression/verilog/expressions/cast_to_real1.sv +++ b/regression/verilog/expressions/cast_to_real1.sv @@ -4,7 +4,7 @@ module main; p0: assert final (real'(0) == 0.0); p1: assert final (real'(1) == 1.0); - // rounding + // rounding, away from zero p2: assert final (real'('hffff_ffff_ffff_ffff) == real'('h1_0000_0000_0000_0000)); p3: assert final (real'(-'sh0_ffff_ffff_ffff_ffff) == real'(-'sh1_0000_0000_0000_0000)); diff --git a/regression/verilog/system-functions/bitstoreal1.desc b/regression/verilog/system-functions/bitstoreal1.desc new file mode 100644 index 00000000..e8ce6ead --- /dev/null +++ b/regression/verilog/system-functions/bitstoreal1.desc @@ -0,0 +1,7 @@ +CORE +bitstoreal1.sv +--module main --bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/system-functions/bitstoreal1.sv b/regression/verilog/system-functions/bitstoreal1.sv new file mode 100644 index 00000000..5e5d5466 --- /dev/null +++ b/regression/verilog/system-functions/bitstoreal1.sv @@ -0,0 +1,11 @@ +module main; + + // Not a conversion, just reinterpretation + always assert ($bitstoreal(0)==0.0); + always assert ($bitstoreal('h3ff00000_00000000)==1); + always assert ($bitstoreal('hc0000000_00000000)==-2.0); + + // good as constant + parameter p = $bitstoreal(0); + +endmodule diff --git a/regression/verilog/system-functions/bitstoshortreal1.desc b/regression/verilog/system-functions/bitstoshortreal1.desc new file mode 100644 index 00000000..4ca90c29 --- /dev/null +++ b/regression/verilog/system-functions/bitstoshortreal1.desc @@ -0,0 +1,7 @@ +CORE +bitstoshortreal1.sv +--module main --bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/system-functions/bitstoshortreal1.sv b/regression/verilog/system-functions/bitstoshortreal1.sv new file mode 100644 index 00000000..5c6d71e5 --- /dev/null +++ b/regression/verilog/system-functions/bitstoshortreal1.sv @@ -0,0 +1,11 @@ +module main; + + // Not a conversion, just reinterpretation + always assert ($bitstoshortreal(0)==0.0); + always assert ($bitstoshortreal('h3f80_0000)==1.0); + always assert ($bitstoshortreal('hc000_0000)==-2.0); + + // good as constant + parameter p = $bitstoshortreal(0); + +endmodule diff --git a/regression/verilog/system-functions/itor1.desc b/regression/verilog/system-functions/itor1.desc new file mode 100644 index 00000000..c920f6c3 --- /dev/null +++ b/regression/verilog/system-functions/itor1.desc @@ -0,0 +1,7 @@ +CORE +itor1.sv +--module main --bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/system-functions/itor1.sv b/regression/verilog/system-functions/itor1.sv new file mode 100644 index 00000000..b0252e52 --- /dev/null +++ b/regression/verilog/system-functions/itor1.sv @@ -0,0 +1,9 @@ +module main; + + always assert ($itor(1)==1.0); + always assert ($itor(-1)==-1.0); + + // good as constant + parameter p = $itor(1); + +endmodule diff --git a/regression/verilog/system-functions/realtobits1.desc b/regression/verilog/system-functions/realtobits1.desc new file mode 100644 index 00000000..a9bcf247 --- /dev/null +++ b/regression/verilog/system-functions/realtobits1.desc @@ -0,0 +1,7 @@ +CORE +realtobits1.sv +--module main --bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/system-functions/realtobits1.sv b/regression/verilog/system-functions/realtobits1.sv new file mode 100644 index 00000000..909a3d08 --- /dev/null +++ b/regression/verilog/system-functions/realtobits1.sv @@ -0,0 +1,11 @@ +module main; + + // Not a conversion, just reinterpretation + always assert ($realtobits(0.0)==0); + always assert ($realtobits(1.0)=='h3ff00000_00000000); + always assert ($realtobits(-2.0)=='hc0000000_00000000); + + // good as constant + parameter p = $realtobits(0.0); + +endmodule diff --git a/regression/verilog/system-functions/rtoi1.desc b/regression/verilog/system-functions/rtoi1.desc new file mode 100644 index 00000000..af39174a --- /dev/null +++ b/regression/verilog/system-functions/rtoi1.desc @@ -0,0 +1,7 @@ +CORE +rtoi1.sv +--module main --bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/system-functions/rtoi1.sv b/regression/verilog/system-functions/rtoi1.sv new file mode 100644 index 00000000..9d7b38cc --- /dev/null +++ b/regression/verilog/system-functions/rtoi1.sv @@ -0,0 +1,10 @@ +module main; + + // These truncate + always assert ($rtoi(1.9)==1); + always assert ($rtoi(-1.9)==-1); + + // good as constant + parameter p = $rtoi(1.9); + +endmodule diff --git a/regression/verilog/system-functions/shortrealtobits1.desc b/regression/verilog/system-functions/shortrealtobits1.desc new file mode 100644 index 00000000..785671a8 --- /dev/null +++ b/regression/verilog/system-functions/shortrealtobits1.desc @@ -0,0 +1,7 @@ +CORE +shortrealtobits1.sv +--module main --bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/system-functions/shortrealtobits1.sv b/regression/verilog/system-functions/shortrealtobits1.sv new file mode 100644 index 00000000..8ea9a207 --- /dev/null +++ b/regression/verilog/system-functions/shortrealtobits1.sv @@ -0,0 +1,11 @@ +module main; + + // Not a conversion, just reinterpretation + always assert ($shortrealtobits(0.0)==0); + always assert ($shortrealtobits(1.0)=='h3f80_0000); + always assert ($shortrealtobits(-2.0)=='hc000_0000); + + // good as constant + parameter p = $shortrealtobits(0.0); + +endmodule diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp index 3a3cf26b..72b15efc 100644 --- a/src/verilog/verilog_lowering.cpp +++ b/src/verilog/verilog_lowering.cpp @@ -13,13 +13,16 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "aval_bval_encoding.h" #include "verilog_bits.h" #include "verilog_expr.h" -/// If applicable, lower the three Verilog real types to floatbv. -typet lower_verilog_real_types(typet type) +/// Lowers +/// * the three Verilog real types to floatbv; +/// * Verilog integer to signedbv[32] +typet verilog_lowering(typet type) { if(type.id() == ID_verilog_real || type.id() == ID_verilog_realtime) { @@ -29,8 +32,17 @@ typet lower_verilog_real_types(typet type) { return ieee_float_spect::single_precision().to_type(); } + else if(type.id() == ID_verilog_integer) + { + return signedbv_typet{32}; + } + else if( + type.id() == ID_verilog_signedbv || type.id() == ID_verilog_unsignedbv) + { + return lower_to_aval_bval(type); + } else - PRECONDITION(false); + return type; } exprt extract( @@ -152,8 +164,136 @@ exprt to_bitvector(const exprt &src) } } +exprt verilog_lowering_system_function(const function_call_exprt &call) +{ + auto identifier = to_symbol_expr(call.function()).get_identifier(); + auto &arguments = call.arguments(); + + if(identifier == "$signed" || identifier == "$unsigned") + { + // lower to typecast + DATA_INVARIANT( + arguments.size() == 1, id2string(identifier) + " takes one argument"); + return typecast_exprt{arguments[0], call.type()}; + } + else if(identifier == "$rtoi") + { + DATA_INVARIANT( + arguments.size(), id2string(identifier) + " takes one argument"); + // These truncate, and do not round. + return floatbv_typecast_exprt{ + arguments[0], + ieee_floatt::rounding_mode_expr( + ieee_floatt::rounding_modet::ROUND_TO_ZERO), + verilog_lowering(call.type())}; + } + else if(identifier == "$itor") + { + DATA_INVARIANT( + arguments.size(), id2string(identifier) + " takes one argument"); + // No rounding required, any 32-bit integer will fit into double. + return floatbv_typecast_exprt{ + arguments[0], + ieee_floatt::rounding_mode_expr( + ieee_floatt::rounding_modet::ROUND_TO_ZERO), + verilog_lowering(call.type())}; + } + else if(identifier == "$bitstoreal") + { + DATA_INVARIANT( + arguments.size(), id2string(identifier) + " takes one argument"); + // not a conversion -- this returns the given bit-pattern as a real + return typecast_exprt{ + zero_extend_exprt{arguments[0], bv_typet{64}}, + verilog_lowering(call.type())}; + } + else if(identifier == "$bitstoshortreal") + { + DATA_INVARIANT( + arguments.size(), id2string(identifier) + " takes one argument"); + // not a conversion -- this returns the given bit-pattern as a real + return typecast_exprt{ + zero_extend_exprt{arguments[0], bv_typet{32}}, + verilog_lowering(call.type())}; + } + else if(identifier == "$realtobits") + { + DATA_INVARIANT( + arguments.size(), id2string(identifier) + " takes one argument"); + // not a conversion -- this returns the given floating-point bit-pattern as [63:0] + return zero_extend_exprt{ + typecast_exprt{arguments[0], bv_typet{64}}, call.type()}; + } + else if(identifier == "$shortrealtobits") + { + DATA_INVARIANT( + arguments.size(), id2string(identifier) + " takes one argument"); + // not a conversion -- this returns the given floating-point bit-pattern as [31:0] + return zero_extend_exprt{ + typecast_exprt{arguments[0], bv_typet{32}}, call.type()}; + } + else + return call; +} + +exprt verilog_lowering_cast(typecast_exprt expr) +{ + auto &src_type = expr.op().type(); + auto &dest_type = expr.type(); + + if( + dest_type.id() == ID_verilog_real || + dest_type.id() == ID_verilog_shortreal || + dest_type.id() == ID_verilog_realtime || src_type.id() == ID_floatbv) + { + // This may require rounding, hence add rounding mode. + // 1800-2017 6.12.2 requires rounding away from zero, + // which we don't have. + expr.type() = verilog_lowering(dest_type); + auto new_cast = floatbv_typecast_exprt{ + expr.op(), + ieee_floatt::rounding_mode_expr( + ieee_floatt::rounding_modet::ROUND_TO_EVEN), + verilog_lowering(dest_type)}; + return std::move(new_cast); + } + + if(is_aval_bval(src_type) && dest_type.id() == ID_bool) + { + // When casting a four-valued scalar to bool, + // 'true' is defined as a "nonzero known value" (1800-2017 12.4). + return aval_bval(expr); + } + else + { + if( + dest_type.id() == ID_verilog_unsignedbv || + dest_type.id() == ID_verilog_signedbv) + { + auto aval_bval_type = lower_to_aval_bval(dest_type); + return aval_bval_conversion(expr.op(), aval_bval_type); + } + else if(dest_type.id() == ID_struct || dest_type.id() == ID_union) + { + return from_bitvector(expr.op(), 0, dest_type); + } + else + { + if(src_type.id() == ID_struct || src_type.id() == ID_union) + { + return extract(to_bitvector(expr.op()), 0, dest_type); + } + } + } + + return std::move(expr); +} + exprt verilog_lowering(exprt expr) { + // lowered already + PRECONDITION(expr.id() != ID_floatbv_typecast); + if(expr.id() == ID_verilog_inside) { // The lowering uses wildcard equality, which needs to be further lowered @@ -196,7 +336,7 @@ exprt verilog_lowering(exprt expr) { // turn into floatbv -- same encoding, // no need to change value - expr.type() = lower_verilog_real_types(expr.type()); + expr.type() = verilog_lowering(expr.type()); } return expr; @@ -247,63 +387,12 @@ exprt verilog_lowering(exprt expr) } else if(expr.id() == ID_typecast) { - auto &typecast_expr = to_typecast_expr(expr); - - if( - typecast_expr.type().id() == ID_verilog_real || - typecast_expr.type().id() == ID_verilog_shortreal || - typecast_expr.type().id() == ID_verilog_realtime) - { - typecast_expr.type() = lower_verilog_real_types(typecast_expr.type()); - } - - if(is_aval_bval(typecast_expr.op()) && typecast_expr.type().id() == ID_bool) - { - // When casting a four-valued scalar to bool, - // 'true' is defined as a "nonzero known value" (1800-2017 12.4). - return aval_bval(typecast_expr); - } - else - { - const auto &src_type = typecast_expr.op().type(); - const auto &dest_type = typecast_expr.type(); - - if( - dest_type.id() == ID_verilog_unsignedbv || - dest_type.id() == ID_verilog_signedbv) - { - auto aval_bval_type = lower_to_aval_bval(dest_type); - return aval_bval_conversion(typecast_expr.op(), aval_bval_type); - } - else if(dest_type.id() == ID_struct || dest_type.id() == ID_union) - { - return from_bitvector(typecast_expr.op(), 0, dest_type); - } - else - { - if(src_type.id() == ID_struct || src_type.id() == ID_union) - { - return extract(to_bitvector(typecast_expr.op()), 0, dest_type); - } - } - } - - // Cast to float? Turn into floatbv_typecast, - // with rounding mode. - if(typecast_expr.type().id() == ID_floatbv) - { - auto rm = ieee_floatt::rounding_mode_expr( - ieee_floatt::rounding_modet::ROUND_TO_EVEN); - auto floatbv_typecast = - floatbv_typecast_exprt{typecast_expr.op(), rm, typecast_expr.type()}; - return std::move(floatbv_typecast); - } - else - return expr; + return verilog_lowering_cast(to_typecast_expr(expr)); } else if(expr.id() == ID_verilog_explicit_type_cast) { - return to_verilog_explicit_type_cast_expr(expr).lower(); + return verilog_lowering_cast( + to_typecast_expr(to_verilog_explicit_type_cast_expr(expr).lower())); } else if(expr.id() == ID_verilog_explicit_signing_cast) { @@ -410,32 +499,25 @@ exprt verilog_lowering(exprt expr) // Is it a 'system function call'? auto &call = to_function_call_expr(expr); if(call.is_system_function_call()) - { - auto identifier = to_symbol_expr(call.function()).get_identifier(); - if(identifier == "$signed" || identifier == "$unsigned") - { - // lower to typecast - DATA_INVARIANT( - call.arguments().size() == 1, - id2string(identifier) + " must have one argument"); - return typecast_exprt{call.arguments()[0], call.type()}; - } - else - return expr; - } + return verilog_lowering_system_function(call); else return expr; } + else if(expr.id() == ID_unary_minus) + { + if( + expr.type().id() == ID_verilog_real || + expr.type().id() == ID_verilog_realtime || + expr.type().id() == ID_verilog_shortreal) + { + // turn into floatbv + expr.type() = verilog_lowering(expr.type()); + } + + return expr; + } else return expr; // leave as is UNREACHABLE; } - -typet verilog_lowering(typet type) -{ - if(type.id() == ID_verilog_signedbv || type.id() == ID_verilog_unsignedbv) - return lower_to_aval_bval(type); - else - return type; -} diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index a3f76ec8..bfe6d3cd 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -79,7 +79,7 @@ exprt verilog_synthesist::synth_expr_rec(exprt expr, symbol_statet symbol_state) // Do the operands recursively for(auto &op : expr.operands()) - op = synth_expr(op, symbol_state); + op = synth_expr_rec(op, symbol_state); if(expr.id()==ID_symbol) { diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 5881b699..41ab5ada 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -960,6 +960,84 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(expr); } + else if(identifier == "$rtoi") + { + if(arguments.size() != 1) + { + throw errort().with_location(expr.source_location()) + << identifier << " takes one argument"; + } + + expr.type() = verilog_integer_typet(); + + return std::move(expr); + } + else if(identifier == "$itor") + { + if(arguments.size() != 1) + { + throw errort().with_location(expr.source_location()) + << identifier << " takes one argument"; + } + + expr.type() = verilog_real_typet(); + + return std::move(expr); + } + else if(identifier == "$bitstoreal") + { + if(arguments.size() != 1) + { + throw errort().with_location(expr.source_location()) + << identifier << " takes one argument"; + } + + expr.type() = verilog_real_typet(); + + return std::move(expr); + } + else if(identifier == "$bitstoshortreal") + { + if(arguments.size() != 1) + { + throw errort().with_location(expr.source_location()) + << identifier << " takes one argument"; + } + + expr.type() = verilog_shortreal_typet(); + + return std::move(expr); + } + else if(identifier == "$realtobits") + { + if(arguments.size() != 1) + { + throw errort().with_location(expr.source_location()) + << identifier << " takes one argument"; + } + + arguments[0] = + typecast_exprt::conditional_cast(arguments[0], verilog_real_typet{}); + + expr.type() = unsignedbv_typet{64}; + + return std::move(expr); + } + else if(identifier == "$shortrealtobits") + { + if(arguments.size() != 1) + { + throw errort().with_location(expr.source_location()) + << identifier << " takes one argument"; + } + + arguments[0] = + typecast_exprt::conditional_cast(arguments[0], verilog_shortreal_typet{}); + + expr.type() = unsignedbv_typet{32}; + + return std::move(expr); + } else if(identifier == "$typename") { if(arguments.size() != 1) @@ -1815,7 +1893,7 @@ void verilog_typecheck_exprt::implicit_typecast( else if( src_type.id() == ID_bool || src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv || src_type.id() == ID_verilog_unsignedbv || - src_type.id() == ID_verilog_signedbv) + src_type.id() == ID_verilog_signedbv || src_type.id() == ID_verilog_integer) { // from bits to s.th. else if(dest_type.id()==ID_bool) @@ -1951,8 +2029,11 @@ void verilog_typecheck_exprt::implicit_typecast( } else if(src_type.id() == ID_verilog_real) { - if(dest_type.id() == ID_verilog_realtime) + if( + dest_type.id() == ID_verilog_realtime || + dest_type.id() == ID_verilog_shortreal) { + // The rounding mode, if needed, is added during lowering. expr = typecast_exprt{expr, dest_type}; return; }