A Formal Specification of Tensor Cores via Satisfiability Modulo Theories

Supporting Data generated by SMT

Precision of Accumulation

$\bo a↖{→}$ $-1.9990234375·2^{-1}$ $-1.9990234375·2^{-1}$
$\bo b↖{→}$ $-1.9990234375·2^{-1}$ $1.4990234375·2^{-1}$
Exact Result $1.9990234375·2^{-3}$
Result (half) $1.0·2^{-2}$
Hardware Result $1.9990234375·2^{-3}$

Precision of Multiplication

$\bo a_ \bo 1$ $1.2587890625·2^{-15}$
$\bo b_ \bo 1$ $1.3681640625·2^{-1}$
Exact Result $1.4162635803222656·2^{-17}$
Result (half) $1.1767578125·2^{-15}$
Hardware Result $1.4162635803222656·2^{-17}$

Rounding of Final Result to Half-Precision

$\bo a_\bo1$ $\bo b_\bo1$ rm Result for rm Hardware Matches
$1.3330078125·2^{-13}$ $-1.5·2^{-1}$ RNE $-1· 2^{-13}$ ✔
RTP $-1.9990234375·2^{-14}$ ✘
$1.3330078125·2^{-9}$ $1.5·2^{-1}$ RNE $1·2^{-9}$ ✔
RTZ $1.9990234375·2^{-10}$ ✘
$1.9619140625·2^{-15}$ $-1.7744140625·2^{-9}$ RNE $-1.0029296875·2^{-15}$ ✔
RTN $-1.00390625·2^{-15}$ ✘

Rounding of Intermediate Sums

$\bo a_\bo1$ $\bo b_\bo1$ $\bo c$ rm Result for rm Hardware Matches
$1.5· 2^{15}$ $1.5 · 2^{-4}$ $-1.0029296875 · 2^{15}$ RNE $1.1249693632125854· 2^{30}$ ✔
RTP $1.124969482421875·2^{30}$ ✘
$1.0302734375·2^{15}$ $1.748046875·2^{15}$ $1.5009765625·2^{8}$ RNE $1.8009666204452515·2^{30}$ ✔
RTP $1.800966739654541·2^{30}$ ✘
$1.767578125·2^{15}$ $-1.1142578125 · 2^{15}$ $1.643554687·2^2$ RNE $-1.9695377349853516·2^{30}$ ✔
RTZ $-1.969537615776062·2^{30}$ ✘
$1.7822265625·2^{-3}$ $1.0048828125·2^{-15}$ $1.9951171875·2^{-8}$ RNE $1.9951342344284058·2^{-8}$ ✘
RTZ $1.9951341152191162·2^{-8}$ ✔
$1.7060546875·2^{15}$ $-1.7646484375·2^{13}$ $1.9970703125·2^{8}$ RNE $-1.5052924156188965·2^{29}$ ✔
RTN $-1.505292534828186·2^{29}$ ✘
$2^1$ $1.9990234375·2^{-9}$ $-2^{13}$ RTZ $-1.9999980926513672·2^{12}$ ✔
RTN $-1.9999982118606567· 2^{12}$ ✘

Accumulation Order

$\bo a↖{→}$ $1.9990234375·2^{-9}$ $1.999023475·2^{-1}$
$\bo b↖{→}$ $1.9990234375·2^{-1}$ $1.9990234375· 2^{-1}$
$\bo c$ $1.0021368265151978·2^{15}$
Test 1: $\bo (\bo a_\bo 1\bo b_\bo 1 \bo + \bo a_\bo 2 \bo b_ \bo 2 \bo ) \bo + \bo c$ $1.0021673440933228·2^{15}$
Test 2: $\bo a_\bo 1\bo b_\bo 1 \bo + \bo ( \bo a_\bo 2 \bo b_ \bo 2 \bo \bo + \bo c \bo )$ $1.0021672248840332·2^{15}$
Hardware Result (Test 1) $1.0021672248840332·2^{15}$
Hardware Result (Test 2) $1.0021672248840332·2^{15}$

Normalization during Accumulation

$\bo a↖{→}$ $1.5302734375·2^{-15}$ $1.0·2^{-14}$
$\bo b↖{→}$ $1.8857421875·2^{-11}$ $1.00097656255· 2^{-15}$
$\bo c$ $1.8124666213989258·2^{-2}$
With Normalization $1.8124667406082153·2^{-2}$
No Normalization $1.8124666213989258·2^{-2}$
Hardware Result $1.8124666213989258·2^{-2}$

Number of Carry-Out Bits Required due to Lack of Normalization

$\bo a↖{→}$ $1.6484375·2^{-5}$ $1.765625·2^{-3}$ $1.5·2^{15}$ $1.0·2^{10}$
$\bo b↖{→}$ $1.0615234375·2^{9}$ $1.9833984375· 2^{6}$ $1.3330078125·2^{-11}$ $1.0·2^{-7}$
$\bo c$ $1.999664306640625·2^{4}$
With 2 bits $0.0$, since largest exponent is $2^{-4}$ before accumulation
With 3 bits $2^7$
Result $2^7$

Ootomo and Yokota versus Markidis et al.

$\bo a↖{→}$ $1.0009765625·2^{-8}$ $1.326171875·2^{-14}$ $2^{-12}$ $2^{-12}$
$\bo b↖{→}$ $1.998046875·2^{-7}$ $1.4443359375· 2^{-7}$ $2^{-12}$ $2^{-12}$
$\bo c$ $2^{-24}$
Actual $1.0 + 2^{-23}$
Markidis et al. $1.0 + 2^{-23}$
Ootomo and Yokota $1.0$