		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-===*

Approximation of Verilog-style ``case equality'' of 4vecs that is X-monotonic when one argument is constant

Signature
(4vec-===* left right) → equal
Arguments: left — Guard (4vec-p left).; right — Guard (4vec-p right).
Returns: equal — Type (4vec-p equal).

This is a substitute for 4vec-=== that is X-monotonic, but is hoped to be good enough for most purposes.

One of the common ways of using the === operator in SystemVerilog is to check some value is exactly X, and if so, return an X result. In such cases it suffices to produce X instead of 1 for the result of the ===, and this can make the result monotonic.

We return, following the boolean-convention,

True (all 1s) when the inputs are both all non-X and identical, or
False (all 0s) when some corresponding non-X bits of the inputs are not identical, or or when some bit of the left input is non-X and the corresponding bit of the right input is X
Otherwise, X.

Definitions and Theorems

Function: 4vec-===*

(defun 4vec-===* (left right)
 (declare (xargs :guard (and (4vec-p left) (4vec-p right))))
 (let ((__function__ '4vec-===*))
   (declare (ignorable __function__))
   (b* (((4vec left))
        ((4vec right))
        (uppers-diff (logxor left.upper right.upper))
        (lowers-diff (logxor left.lower right.lower))
        (diff (logior uppers-diff lowers-diff))
        (left-non-x (logorc1 left.upper left.lower))
        (true (equal -1 (logandc1 diff left-non-x)))
        ((when true) -1)
        (right-non-x (logorc1 right.upper right.lower))
        (not-false
             (equal 0
                    (logand left-non-x (logorc2 diff right-non-x))))
        ((when not-false) (4vec-x)))
     0)))

Theorem: 4vec-p-of-4vec-===*

(defthm 4vec-p-of-4vec-===*
  (b* ((equal (4vec-===* left right)))
    (4vec-p equal))
  :rule-classes :rewrite)

Theorem: 4vec-===*-of-4vec-fix-left

(defthm 4vec-===*-of-4vec-fix-left
  (equal (4vec-===* (4vec-fix left) right)
         (4vec-===* left right)))

Theorem: 4vec-===*-4vec-equiv-congruence-on-left

(defthm 4vec-===*-4vec-equiv-congruence-on-left
  (implies (4vec-equiv left left-equiv)
           (equal (4vec-===* left right)
                  (4vec-===* left-equiv right)))
  :rule-classes :congruence)

Theorem: 4vec-===*-of-4vec-fix-right

(defthm 4vec-===*-of-4vec-fix-right
  (equal (4vec-===* left (4vec-fix right))
         (4vec-===* left right)))

Theorem: 4vec-===*-4vec-equiv-congruence-on-right

(defthm 4vec-===*-4vec-equiv-congruence-on-right
  (implies (4vec-equiv right right-equiv)
           (equal (4vec-===* left right)
                  (4vec-===* left right-equiv)))
  :rule-classes :congruence)