Solve-lane-by-lane-masked
Equality check that works around hard SAT/fraiging problems caused by writemasking.
- Signature
(solve-lane-by-lane-masked x y mask width) → *
This addresses a problem that sometimes comes up in proving
correctness of SIMD operations with writemasking. Suppose an instruction
applies function F to each 32-bit lane of a vector, with writemasking; that is,
the spec for lane i is mask[i] ? F(src.lanes32[i]) : dst.lanes32[i]. Now,
perhaps the implementation applies the same function F, but instead operates on
mask[i] ? src.lanes32[i] : 0. Of course this is OK because when
mask[i] is 0 we don't care what the function computes. But unfortunately
when we pack the lanes together and try to equivalence check spec versus
implementation, one of our best tools, fraiging (aka SAT sweeping) doesn't
work. This is because there are no equivalent formulas within the computation
of the function F: each subformula G within F shows up in the spec as
G(src.lanes32[i]) but in the implementation as G(mask[i] ?
src.lanes32[i] : 0), which is obviously not equivalent.
A workaround for this problem is to split the check for each lane into cases
according to mask[i] and propagate that assumption into their formulas.
That is, when mask[i] is assumed true, replace mask[i] ?
src.lanes32[i] : 0 with just src.lanes32[i]. FGL has a special function
called fgl-pathcond-fix that can do this: logically it is the
identity function, but under FGL it rewrites the input symbolic object to
assume the current path condition. That is, for each Boolean formula in the
symbolic object, that formula is simplified by replacing any AIG literals known
to be true (false) under the path condition with 1 (0). In many cases simply
splitting into cases for each lane's corresponding mask bit, specializing each
equivalence under both cases, produces a formula that is much easier to solve
than the original, especially using fraiging.
Sometimes this may not work; for a somewhat more aggressive strategy, see
solve-lane-by-lane-masked+.
Definitions and Theorems
Function: solve-lane-by-lane-masked
(defun solve-lane-by-lane-masked
(x y mask width)
(declare (xargs :guard t))
(let ((__function__ 'solve-lane-by-lane-masked))
(declare (ignorable __function__))
(equal x y)))
Theorem: solve-lane-by-lane-masked-impl
(defthm
solve-lane-by-lane-masked-impl
(implies
(and (syntaxp (posp width))
(check-integerp xintp x)
(check-integerp yintp y))
(equal (solve-lane-by-lane-masked x y mask width)
(if (and (check-int-endp x-endp x)
(check-int-endp y-endp y))
(equal x y)
(and* (b* ((lane-equiv (equal (loghead width x)
(loghead width y))))
(if (logbitp 0 mask)
(fgl-pathcond-fix lane-equiv)
(fgl-pathcond-fix lane-equiv)))
(solve-lane-by-lane-masked (logtail width x)
(logtail width y)
(logcdr mask)
width))))))
