Numeric behavior

This page describes general rules followed by the CertSAFE language and primitive components. Keeping these rules in mind will make it easier to understand the behavior of your models.

Behavior of integer data types

  • The data type UIntN for N in {8, 16, 32} represents an unsigned N-bit binary integer with values in the range 0 to 2N - 1, inclusive.
  • The data type IntN for N in {8, 16, 32} represents a signed twos-complement N-bit binary integer with values in the range -2(N - 1) to 2(N - 1) - 1, inclusive.
  • Anywhere literal integer values are specified, they can be written as decimal, binary (prefixed with 0b), octal (prefixed with 0o), or hex (prefixed with 0x).
  • Comparison operations (≤, =, etc.) use the standard linear order on the integer values in the range of the data type as specified above.
  • Arithmetic operations (addition, subtraction, multiplication) overflow silently, as if the operations were performed modulo 2N.
  • Shift/rotate distances are positive when shifting to the left and negative when shifting to the right.
  • When an integer value must be padded with additional bits on the left (Copy Bits when converting to a larger data type, and Shift when shifting right), the following rule is used: if the data type of the value being padded is signed, the value is sign-extended; if the data type of the value being padded is unsigned, the value is zero-extended.

Behavior of floating-point data types

  • The data type FloatN for N in {32, 64} represents the IEEE 754-2008 binaryN format (i.e. binary32 and binary64). In particular, floating-point data types permit the values Infinity, -Infinity, NaN, +0.0, -0.0, and subnormal values in addition to the usual normal values.
  • NaN values are propagated quietly without triggering any sort of exception.
  • Arithmetic operations (addition, subtraction, multiplication, division, square root) behave as specified in IEEE 754, using the round to nearest, ties to even rounding mode.
  • For components performing floating-point arithmetic operations across a variable number of inputs, the operations are performed starting from the clockwise-most input and moving counterclockwise.
  • Rounding is performed after every floating-point operation. For example, a multiplier feeding into an adder rounds after the multiplication, and then again after the addition. A 10-input multiplier rounds 9 times, once after each multiplication performed in the counterclockwise order.
  • When a decimal literal needs to be converted to a floating point value (e.g. in the Literal or Inline Comparator components), the decimal literal is treated as an exact rational number and converted to the floating-point data type using the IEEE 754 round to nearest, ties to even rounding mode. In particular, if the magnitude of the value is too large to be represented by the floating-point type, it is rounded to ±Infinity.
  • The IEEE 754 “round to nearest, ties to even” rounding mode is also used when values need to be converted from another data type to a floating-point data type (Nearest, Frames Per Second). This does not apply to the Truncate component, which converts from a floating-point data type to an integer data type, nor the floor and ceil functions of the Special Floating Function component, which perform rounding within a single floating-point data type.
  • The transcendental functions available through the Special Floating Function component are correct to within 1 ulp of the true mathematical value, treating the input floating-point values as exact rational numbers.
  • Comparison operations (≤, =, etc.) use the IEEE 754 ordering behavior. In particular:
    • +0.0 compares equal to -0.0.
    • <, ≤, >, ≥, and = always return False if at least one of their operands is NaN. ≠ always returns True if at least one of its operands is NaN.
    • The Min/Max components are an exception to this ordering behavior. Min/Max treat -0.0 as being strictly less than +0.0, and Min/Max of anything with NaN always yields NaN.