diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index d0180ab19f..a0a04d0e76 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst @@ -2221,7 +2221,7 @@ where :math:`f`, :math:`\sx_1`, :math:`\sx_2`, :math:`h`, and :math:`k` are inst \VEXTMUL{\K\_}\LOW{\K\_}\sx & \ivmul & \sx & \sx & 0 & M_2 \\ \VEXTMUL{\K\_}\HIGH{\K\_}\sx & \ivmul & \sx & \sx & M_2 & M_2 \\ \VDOT{\K\_}\S & \ivdot & \S & \S & 0 & M_1 \\ - \VRELAXEDDOT{\K\_}\S & \ivdotsat & \S & \relaxed(R_{\F{idot}})[ \S, \U ] & 0 & M_1 \\ + \VRELAXEDDOT{\K\_}\S & \ivrelaxeddot & \S & \relaxed(R_{\F{idot}})[ \S, \U ] & 0 & M_1 \\ \end{array} .. note:: @@ -2533,16 +2533,21 @@ where: it behaves like regular :math:`\ivswizzle`. -.. _op-irelaxed_dot: +.. _op-ivrelaxed_dot: .. _op-irelaxed_dot_add: -:math:`\VRELAXEDDOT(i_1, i_2)` -.............................. +:math:`\ivrelaxeddot_N(i_1^{2m}, i_2^{2m})` +........................................... The implementation-specific behaviour of this operation is determined by the global parameter :math:`R_{\F{idot}} \in \{0, 1\}`. -It also affects the behaviour of :math:`\VRELAXEDDOTADD`. +It also affects the behaviour of :math:`\VRELAXEDDOT` and :math:`\VRELAXEDDOTADD` specified :ref:`above `. + +* Return :math:`\relaxed(R_{\F{idot}})[ \ivdot_N(i_1^{2m}, i_2^{2m}), \ivdotsat_N(i_1^{2m}, i_2^{2m}) ]`. -Its definition is part of the definition of :math:`\vextbinop` specified :ref:`above `. +.. math:: + \begin{array}{@{}lcll} + \ivrelaxeddot_N(i_1^{2m}, i_2^{2m}) &=& \relaxed(R_{\F{idot}})[ \ivdot_N(i_1^{2m}, i_2^{2m}), \ivdotsat_N(i_1^{2m}, i_2^{2m}) ] \\ + \end{array} .. note:: Relaxed dot product is implementation-dependent when the second operand is negative in a signed intepretation. diff --git a/document/core/util/macros.def b/document/core/util/macros.def index cd9472676e..cd846e43e9 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -1700,7 +1700,7 @@ .. |frelaxedmin| mathdef:: \xref{exec/numerics}{op-frelaxed_min}{\F{frelaxed\_min}} .. |frelaxedmax| mathdef:: \xref{exec/numerics}{op-frelaxed_max}{\F{frelaxed\_max}} .. |irelaxedq15mulrs| mathdef:: \xref{exec/numerics}{op-irelaxed_q15mulr_s}{\F{irelaxed\_q15mulr\_s}} -.. |irelaxeddot| mathdef:: \xref{exec/numerics}{op-irelaxed_dot}{\F{irelaxed\_dot}} +.. |ivrelaxeddot| mathdef:: \xref{exec/numerics}{op-ivrelaxed_dot}{\F{ivrelaxed\_dot}} .. Numerics, meta functions diff --git a/specification/wasm-3.0/3.2-numerics.vector.spectec b/specification/wasm-3.0/3.2-numerics.vector.spectec index c88b9dadfb..cbdee7701e 100644 --- a/specification/wasm-3.0/3.2-numerics.vector.spectec +++ b/specification/wasm-3.0/3.2-numerics.vector.spectec @@ -368,6 +368,9 @@ def $ivdot_sat_(N, iN(N)*, iN(N)*) : iN(N)* hint(show $ivdot__sat_(%,%,%)) def $ivdot_sat_(N, i_1*, i_2*) = $iadd_sat_(N, S, j_1, j_2)* -- if $concat_(iN(N), (j_1 j_2)*) = $imul_(N, i_1, i_2)* +def $ivrelaxed_dot_(N, iN(N)*, iN(N)*) : iN(N)* hint(show $ivrelaxed__dot_(%,%,%)) +def $ivrelaxed_dot_(N, i_1*, i_2*) = $relaxed2($R_idot, iN(N)*, $ivdot_(N, i_1*, i_2*), $ivdot_sat_(N, i_1*, i_2*)) + def $vextunop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTADD_PAIRWISE sx, v_1) = $ivextunop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivadd_pairwise_, sx, v_1) @@ -376,7 +379,7 @@ def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTMUL half sx, v_1, v_2) = def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, DOT S, v_1, v_2) = $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_, S, S, 0, M_1, v_1, v_2) def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, RELAXED_DOT S, v_1, v_2) = - $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_sat_, S, $relaxed2($R_idot, sx, S, U), 0, M_1, v_1, v_2) + $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivrelaxed_dot_, S, $relaxed2($R_idot, sx, S, U), 0, M_1, v_1, v_2) (; ;; TODO(2, rossberg): this is obsolete, clean up diff --git a/specification/wasm-latest/3.2-numerics.vector.spectec b/specification/wasm-latest/3.2-numerics.vector.spectec index c88b9dadfb..cbdee7701e 100644 --- a/specification/wasm-latest/3.2-numerics.vector.spectec +++ b/specification/wasm-latest/3.2-numerics.vector.spectec @@ -368,6 +368,9 @@ def $ivdot_sat_(N, iN(N)*, iN(N)*) : iN(N)* hint(show $ivdot__sat_(%,%,%)) def $ivdot_sat_(N, i_1*, i_2*) = $iadd_sat_(N, S, j_1, j_2)* -- if $concat_(iN(N), (j_1 j_2)*) = $imul_(N, i_1, i_2)* +def $ivrelaxed_dot_(N, iN(N)*, iN(N)*) : iN(N)* hint(show $ivrelaxed__dot_(%,%,%)) +def $ivrelaxed_dot_(N, i_1*, i_2*) = $relaxed2($R_idot, iN(N)*, $ivdot_(N, i_1*, i_2*), $ivdot_sat_(N, i_1*, i_2*)) + def $vextunop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTADD_PAIRWISE sx, v_1) = $ivextunop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivadd_pairwise_, sx, v_1) @@ -376,7 +379,7 @@ def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTMUL half sx, v_1, v_2) = def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, DOT S, v_1, v_2) = $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_, S, S, 0, M_1, v_1, v_2) def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, RELAXED_DOT S, v_1, v_2) = - $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_sat_, S, $relaxed2($R_idot, sx, S, U), 0, M_1, v_1, v_2) + $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivrelaxed_dot_, S, $relaxed2($R_idot, sx, S, U), 0, M_1, v_1, v_2) (; ;; TODO(2, rossberg): this is obsolete, clean up diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index ab0c63e545..53d6f79e5a 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -5857,12 +5857,6 @@ def $ivdot_(N : N, iN(N)*, iN(N)*) : iN(N)* def $ivdot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_(N, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) -;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec -def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} - -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivextbinop__(shape_1 : shape, shape_2 : shape, def $f_(N : N, iN(N)*, iN(N)*) : iN(N)*, sx : sx, sx : sx, laneidx : laneidx, laneidx : laneidx, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -5878,6 +5872,17 @@ def $ivmul_(N : N, iN(N)*, iN(N)*) : iN(N)* ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivmul_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`} +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} + -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) + +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivrelaxed_dot_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivrelaxed_dot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $relaxed2($R_idot, syntax iN(N)*, $ivdot_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}), $ivdot_sat_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`})) + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -5885,7 +5890,7 @@ def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__ ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_, S_sx, S_sx, `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_sat_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) + def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivrelaxed_dot_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextternop__(ishape_1 : ishape, ishape_2 : ishape, vextternop__ : vextternop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index c8ffe3263f..b1fe073c22 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -8873,6 +8873,12 @@ $$ \end{array} $$ +$$ +\begin{array}[t]{@{}lcl@{}l@{}} +{{\mathrm{ivrelaxed\_dot}}}_{N}({i_1^\ast}, {i_2^\ast}) & = & {{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ {{\mathrm{ivdot}}}_{N}({i_1^\ast}, {i_2^\ast}), {{\mathrm{ivdot\_sat}}}_{N}({i_1^\ast}, {i_2^\ast}) ]} \\ +\end{array} +$$ + $$ \begin{array}[t]{@{}lcl@{}l@{}} {{\mathsf{extadd\_pairwise}}{\mathsf{\_}}{{\mathit{sx}}}}{{}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}(v_1)} & = & & \\ @@ -8901,7 +8907,7 @@ $$ {{\mathsf{relaxed\_dot}}{\mathsf{\_}}{\mathsf{s}}}{{}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}(v_1, v_2)} & = & & \\ \multicolumn{4}{@{}l@{}}{\quad \begin{array}[t]{@{}l@{}} -{{\mathrm{ivextbinop}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({\mathrm{ivdot}}_{{\mathit{sat}}}, \mathsf{s}, {{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ \mathsf{s}, \mathsf{u} ]}, 0, M_1, v_1, v_2) \\ +{{\mathrm{ivextbinop}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({\mathrm{ivrelaxed}}_{{\mathit{dot}}}, \mathsf{s}, {{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ \mathsf{s}, \mathsf{u} ]}, 0, M_1, v_1, v_2) \\ \end{array} } \\ \end{array} diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 88ff0f1960..a4bca3ba7e 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -5380,12 +5380,6 @@ def $ivdot_(N : N, iN(N)*, iN(N)*) : iN(N)* def $ivdot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_(N, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) -;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec -def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} - -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivextbinop__(shape_1 : shape, shape_2 : shape, def $f_(N : N, iN(N)*, iN(N)*) : iN(N)*, sx : sx, sx : sx, laneidx : laneidx, laneidx : laneidx, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -5401,6 +5395,17 @@ def $ivmul_(N : N, iN(N)*, iN(N)*) : iN(N)* ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivmul_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`} +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} + -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) + +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivrelaxed_dot_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivrelaxed_dot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $relaxed2($R_idot, syntax iN(N)*, $ivdot_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}), $ivdot_sat_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`})) + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -5408,7 +5413,7 @@ def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__ ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_, S_sx, S_sx, `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_sat_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) + def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivrelaxed_dot_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextternop__(ishape_1 : ishape, ishape_2 : ishape, vextternop__ : vextternop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) @@ -17289,12 +17294,6 @@ def $ivdot_(N : N, iN(N)*, iN(N)*) : iN(N)* def $ivdot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_(N, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) -;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec -def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} - -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivextbinop__(shape_1 : shape, shape_2 : shape, def $f_(N : N, iN(N)*, iN(N)*) : iN(N)*, sx : sx, sx : sx, laneidx : laneidx, laneidx : laneidx, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -17310,6 +17309,17 @@ def $ivmul_(N : N, iN(N)*, iN(N)*) : iN(N)* ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivmul_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`} +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} + -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) + +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivrelaxed_dot_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivrelaxed_dot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $relaxed2($R_idot, syntax iN(N)*, $ivdot_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}), $ivdot_sat_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`})) + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -17317,7 +17327,7 @@ def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__ ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_, S_sx, S_sx, `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_sat_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) + def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivrelaxed_dot_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextternop__(ishape_1 : ishape, ishape_2 : ishape, vextternop__ : vextternop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) @@ -29327,12 +29337,6 @@ def $ivdot_(N : N, iN(N)*, iN(N)*) : iN(N)* def $ivdot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_(N, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) -;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec -def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} - -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivextbinop__(shape_1 : shape, shape_2 : shape, def $f_(N : N, iN(N)*, iN(N)*) : iN(N)*, sx : sx, sx : sx, laneidx : laneidx, laneidx : laneidx, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -29348,6 +29352,17 @@ def $ivmul_(N : N, iN(N)*, iN(N)*) : iN(N)* ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivmul_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`} +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} + -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) + +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivrelaxed_dot_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivrelaxed_dot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $relaxed2($R_idot, syntax iN(N)*, $ivdot_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}), $ivdot_sat_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`})) + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -29355,7 +29370,7 @@ def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__ ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_, S_sx, S_sx, `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_sat_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) + def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivrelaxed_dot_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextternop__(ishape_1 : ishape, ishape_2 : ishape, vextternop__ : vextternop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index ff6159818c..c7eec9f7d8 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -26188,15 +26188,6 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #. Return :math:`{{{\mathrm{iadd}}}_{N}(j_1, j_2)^\ast}`. -:math:`{{\mathrm{ivdot\_sat}}}_{N}({i_1^\ast}, {i_2^\ast})` -........................................................... - - -1. Let :math:`{j_1~j_2^\ast}` be the result for which the :ref:`concatenation ` of :math:`{j_1~j_2^\ast}` is :math:`{{{\mathrm{imul}}}_{N}(i_1, i_2)^\ast}`. - -#. Return :math:`{{{\mathrm{iadd\_sat}}}{\mathsf{s}}{{}_{N}(j_1, j_2)}^\ast}`. - - :math:`{{\mathrm{ivextbinop}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({\mathrm{f}}, {\mathit{sx}}_1, {\mathit{sx}}_2, i, k, v_1, v_2)` ................................................................................................................................................................................ @@ -26233,6 +26224,22 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i 1. Return :math:`{{{\mathrm{imul}}}_{N}(i_1, i_2)^\ast}`. +:math:`{{\mathrm{ivdot\_sat}}}_{N}({i_1^\ast}, {i_2^\ast})` +........................................................... + + +1. Let :math:`{j_1~j_2^\ast}` be the result for which the :ref:`concatenation ` of :math:`{j_1~j_2^\ast}` is :math:`{{{\mathrm{imul}}}_{N}(i_1, i_2)^\ast}`. + +#. Return :math:`{{{\mathrm{iadd\_sat}}}{\mathsf{s}}{{}_{N}(j_1, j_2)}^\ast}`. + + +:math:`{{\mathrm{ivrelaxed\_dot}}}_{N}({i_1^\ast}, {i_2^\ast})` +............................................................... + + +1. Return :math:`{{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ {{\mathrm{ivdot}}}_{N}({i_1^\ast}, {i_2^\ast}), {{\mathrm{ivdot\_sat}}}_{N}({i_1^\ast}, {i_2^\ast}) ]}`. + + :math:`{{\mathit{vextbinop}}}{{}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}(v_1, v_2)}` ............................................................................................................................. @@ -26249,7 +26256,7 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #. Assert: Due to validation, :math:`{\mathit{vextbinop}} = `. -#. Return :math:`{{\mathrm{ivextbinop}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({\mathrm{ivdot}}_{{\mathit{sat}}}, \mathsf{s}, {{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ \mathsf{s}, \mathsf{u} ]}, 0, M_1, v_1, v_2)`. +#. Return :math:`{{\mathrm{ivextbinop}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({\mathrm{ivrelaxed}}_{{\mathit{dot}}}, \mathsf{s}, {{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ \mathsf{s}, \mathsf{u} ]}, 0, M_1, v_1, v_2)`. :math:`{}{{}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}(c_1, c_2, c_3)}` @@ -33837,10 +33844,6 @@ ivdot_ N i_1* i_2* 1. Let [j_1, j_2]* be $concat__1^-1(`iN(N), $imul_(N, i_1, i_2)*). 2. Return $iadd_(N, j_1, j_2)*. -ivdot_sat_ N i_1* i_2* -1. Let [j_1, j_2]* be $concat__1^-1(`iN(N), $imul_(N, i_1, i_2)*). -2. Return $iadd_sat_(N, S, j_1, j_2)*. - ivextbinop__ Jnn_1 X M_1 Jnn_2 X M_2 $f_ sx_1 sx_2 i k v_1 v_2 1. Let c_1* be $lanes_(Jnn_1 X M_1, v_1)[i : k]. 2. Let c_2* be $lanes_(Jnn_1 X M_1, v_2)[i : k]. @@ -33858,6 +33861,13 @@ ivextbinop__ Jnn_1 X M_1 Jnn_2 X M_2 $f_ sx_1 sx_2 i k v_1 v_2 ivmul_ N i_1* i_2* 1. Return $imul_(N, i_1, i_2)*. +ivdot_sat_ N i_1* i_2* +1. Let [j_1, j_2]* be $concat__1^-1(`iN(N), $imul_(N, i_1, i_2)*). +2. Return $iadd_sat_(N, S, j_1, j_2)*. + +ivrelaxed_dot_ N i_1* i_2* +1. Return $relaxed2($R_idot(), `iN(N)*, $ivdot_(N, i_1*, i_2*), $ivdot_sat_(N, i_1*, i_2*)). + vextbinop__ Jnn_1 X M_1 Jnn_2 X M_2 vextbinop__ v_1 v_2 1. If vextbinop__ is some EXTMUL, then: a. Let (EXTMUL half sx) be vextbinop__. @@ -33865,7 +33875,7 @@ vextbinop__ Jnn_1 X M_1 Jnn_2 X M_2 vextbinop__ v_1 v_2 2. If (vextbinop__ = DOTS), then: a. Return $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_, S, S, 0, M_1, v_1, v_2). 3. Assert: Due to validation, (vextbinop__ = RELAXED_DOTS). -4. Return $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_sat_, S, $relaxed2($R_idot(), `sx, S, U), 0, M_1, v_1, v_2). +4. Return $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivrelaxed_dot_, S, $relaxed2($R_idot(), `sx, S, U), 0, M_1, v_1, v_2). vextternop__ Jnn_1 X M_1 Jnn_2 X M_2 RELAXED_DOT_ADDS c_1 c_2 c_3 1. Let M be (2 * M_2). diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 05fbca79d2..94517f04c7 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -1796,6 +1796,7 @@ warning: definition `ivdot_sat_` was never spliced warning: definition `ivextbinop__` was never spliced warning: definition `ivextunop__` was never spliced warning: definition `ivmul_` was never spliced +warning: definition `ivrelaxed_dot_` was never spliced warning: definition `ivrelop_` was never spliced warning: definition `ivrelopsx_` was never spliced warning: definition `ivshiftop_` was never spliced @@ -2662,6 +2663,7 @@ warning: definition prose `ivdot_sat_` was never spliced warning: definition prose `ivextbinop__` was never spliced warning: definition prose `ivextunop__` was never spliced warning: definition prose `ivmul_` was never spliced +warning: definition prose `ivrelaxed_dot_` was never spliced warning: definition prose `ivrelop_` was never spliced warning: definition prose `ivrelopsx_` was never spliced warning: definition prose `ivshiftop_` was never spliced diff --git a/test/core/relaxed-simd/relaxed_dot_product.wast b/test/core/relaxed-simd/relaxed_dot_product.wast index 41dee0afcf..b04d1c4bf7 100644 --- a/test/core/relaxed-simd/relaxed_dot_product.wast +++ b/test/core/relaxed-simd/relaxed_dot_product.wast @@ -37,6 +37,26 @@ (v128.const i16x8 32512 0 0 0 0 0 0 0) (v128.const i16x8 33024 0 0 0 0 0 0 0))) +;; Repeat 4 corner cases in both 64-bit halves (i16x8 lanes 0..3 and 4..7): +;; lanes 0, 4 (a = -128, b = -128 or 128): +;; signed * signed (wrapping) : -128 * -128 * 2 = 32,768 wrapped to -32,768 +;; signed * unsigned (saturating) : -128 * 128 * 2 = -32,768 saturated to -32,768 +;; lanes 1, 5 (a = -128, b = -127 or 129): +;; signed * signed (wrapping) : -128 * -127 * 2 = 32,512 +;; signed * unsigned (saturating) : -128 * 129 * 2 = -33,024 saturated to -32,768 +;; lanes 2, 6 (a = 127, b = -128 or 128): +;; signed * signed (wrapping) : 127 * -128 * 2 = -32,512 +;; signed * unsigned (saturating) : 127 * 128 * 2 = 32,512 +;; lanes 3, 7 (a = 127, b = -1 or 255): +;; signed * signed (wrapping) : 127 * -1 * 2 = -254 +;; signed * unsigned (saturating) : 127 * 255 * 2 = 64,770 saturated to 32,767 +(assert_return (invoke "i16x8.relaxed_dot_i8x16_i7x16_s" + (v128.const i8x16 -128 -128 -128 -128 127 127 127 127 -128 -128 -128 -128 127 127 127 127) + (v128.const i8x16 -128 -128 -127 -127 -128 -128 -1 -1 -128 -128 -127 -127 -128 -128 -1 -1)) + (either + (v128.const i16x8 -32768 32512 -32512 -254 -32768 32512 -32512 -254) ;; signed * signed, wrapping add (ARM NEON smull + smull2 + addp) + (v128.const i16x8 -32768 -32768 32512 32767 -32768 -32768 32512 32767))) ;; signed * unsigned, saturating add (x86-64 vpmaddubsw) + ;; Simple values to ensure things are functional. (assert_return (invoke "i32x4.relaxed_dot_i8x16_i7x16_add_s" (v128.const i8x16 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)