		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-3value-mask

Produces a mask identifying bits of an svex which are always non-Z

Signature
(svex-3value-mask x) → mask
Arguments: x — Guard (svex-p x).
Returns: mask — Type (4vmask-p mask).

Definitions and Theorems

Function: svex-3value-mask

(defun svex-3value-mask (x)
 (declare (xargs :guard (svex-p x)))
 (let ((__function__ 'svex-3value-mask))
  (declare (ignorable __function__))
  (svex-case
   x :var 0 :quote
   (b* (((4vec x.val)))
     (sparseint-bitorc2 (int-to-sparseint x.val.upper)
                        (int-to-sparseint x.val.lower)))
   :call
   (cond
     ((3valued-syntaxp x)
      (int-to-sparseint -1))
     ((and (eq x.fn 'concat)
           (eql (len x.args) 3)
           (svex-quoted-index-p (first x.args)))
      (sparseint-concatenate
           (2vec->val (svex-quote->val (first x.args)))
           (svex-3value-mask (second x.args))
           (svex-3value-mask (third x.args))))
     ((and (eq x.fn 'rsh)
           (eql (len x.args) 2)
           (svex-quoted-index-p (first x.args)))
      (sparseint-rightshift
           (2vec->val (svex-quote->val (first x.args)))
           (svex-3value-mask (second x.args))))
     ((and (eq x.fn 'partinst)
           (eql (len x.args) 4)
           (svex-quoted-index-p (first x.args))
           (svex-quoted-index-p (second x.args)))
      (b* ((inmask (svex-3value-mask (third x.args)))
           (valmask (svex-3value-mask (fourth x.args)))
           (lsbval (2vec->val (svex-quote->val (first x.args))))
           (widthval (2vec->val (svex-quote->val (second x.args)))))
        (sparseint-concatenate
             lsbval inmask
             (sparseint-concatenate
                  widthval valmask
                  (sparseint-rightshift (+ lsbval widthval)
                                        inmask)))))
     ((and (eq x.fn 'partsel)
           (eql (len x.args) 3)
           (svex-quoted-index-p (first x.args))
           (svex-quoted-index-p (second x.args)))
      (b* ((inmask (svex-3value-mask (third x.args)))
           (lsbval (2vec->val (svex-quote->val (first x.args))))
           (widthval (2vec->val (svex-quote->val (second x.args)))))
        (sparseint-concatenate widthval
                               (sparseint-rightshift lsbval inmask)
                               (int-to-sparseint -1))))
     (t 0)))))

Theorem: 4vmask-p-of-svex-3value-mask

(defthm 4vmask-p-of-svex-3value-mask
  (b* ((mask (svex-3value-mask x)))
    (4vmask-p mask))
  :rule-classes :rewrite)

Theorem: svex-3value-mask-correct

(defthm svex-3value-mask-correct
  (b* ((?mask (svex-3value-mask x)))
    (3vec-p (4vec-mask mask (svex-eval x env)))))