SystemVerilog: conversion functions

This adds the conversion functions from 1800-2017 20.5.

Author: kroening

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
 

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.

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

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));
 

regression/verilog/system-functions/bitstoreal1.desc

@@ -0,0 +1,7 @@
+CORE
+bitstoreal1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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

regression/verilog/system-functions/bitstoshortreal1.desc

@@ -0,0 +1,7 @@
+CORE
+bitstoshortreal1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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

regression/verilog/system-functions/itor1.desc

@@ -0,0 +1,7 @@
+CORE
+itor1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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

regression/verilog/system-functions/realtobits1.desc

@@ -0,0 +1,7 @@
+CORE
+realtobits1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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

regression/verilog/system-functions/rtoi1.desc

@@ -0,0 +1,7 @@
+CORE
+rtoi1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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

regression/verilog/system-functions/shortrealtobits1.desc

@@ -0,0 +1,7 @@
+CORE
+shortrealtobits1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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