4vec-<<=
Lattice relation (information order) on 4vec values.
- Signature
(4vec-<<= a b) → approxp
- Arguments
- a — Guard (4vec-p a).
- b — Guard (4vec-p b).
(4vec-<<= a b) is true when a is a ``conservative
approximation'' of b. That is, when every pair of corresponding bits,
a_i from a and b_i from b, are the same unless a_i is
X.
Almost all svex functions satisfy a monotonicity property with
respect to this relation, i.e., if f is a one-argument function, it will
satisfy:
(implies (4vec-<<= a b)
(4vec-<<= (f a) (f b)))
Intuitively, this property essentially means that each operator properly
treats X bits as unknown.
A notable exception is the === operator, i.e., 4vec-===, which
is a ``bad'' operator that can non-conservatively treat X bits as being equal
to other X bits. This operator is included in sv for better
compatibility with hardware description languages like Verilog, but should
generally be avoided when possible.
4vec-<<= is essentially a bitwise/vector analogue of the similar 4v function called ACL2::4v-<=; see also ACL2::4v-monotonicity.
Definitions and Theorems
Function: 4vec-<<=
(defun 4vec-<<= (a b)
(declare (xargs :guard (and (4vec-p a) (4vec-p b))))
(let ((__function__ '4vec-<<=))
(declare (ignorable __function__))
(b* (((4vec a) a) ((4vec b) b))
(eql -1
(logior (logand (logeqv a.upper b.upper)
(logeqv a.lower b.lower))
(logand a.upper (lognot a.lower)))))))
Theorem: 4vec-<<=-of-4vec-fix-a
(defthm 4vec-<<=-of-4vec-fix-a
(equal (4vec-<<= (4vec-fix a) b)
(4vec-<<= a b)))
Theorem: 4vec-<<=-4vec-equiv-congruence-on-a
(defthm 4vec-<<=-4vec-equiv-congruence-on-a
(implies (4vec-equiv a a-equiv)
(equal (4vec-<<= a b)
(4vec-<<= a-equiv b)))
:rule-classes :congruence)
Theorem: 4vec-<<=-of-4vec-fix-b
(defthm 4vec-<<=-of-4vec-fix-b
(equal (4vec-<<= a (4vec-fix b))
(4vec-<<= a b)))
Theorem: 4vec-<<=-4vec-equiv-congruence-on-b
(defthm 4vec-<<=-4vec-equiv-congruence-on-b
(implies (4vec-equiv b b-equiv)
(equal (4vec-<<= a b)
(4vec-<<= a b-equiv)))
:rule-classes :congruence)
Theorem: 4vec-<<=-self
(defthm 4vec-<<=-self (4vec-<<= x x))
Theorem: 4vec-<<=-x
(defthm 4vec-<<=-x
(4vec-<<= (4vec-x) y))
Theorem: 4vec-<<=-transitive-1
(defthm 4vec-<<=-transitive-1
(implies (and (4vec-<<= a b) (4vec-<<= b c))
(4vec-<<= a c)))
Theorem: 4vec-<<=-transitive-2
(defthm 4vec-<<=-transitive-2
(implies (and (4vec-<<= b c) (4vec-<<= a b))
(4vec-<<= a c)))
Theorem: 4vec-<<=-2vec
(defthm 4vec-<<=-2vec
(implies (2vec-p n)
(equal (4vec-<<= n n1)
(4vec-equiv n n1))))
Theorem: 4vec-<<=-asymm
(defthm 4vec-<<=-asymm
(implies (4vec-<<= x y)
(iff (4vec-<<= y x) (4vec-equiv y x))))
Subtopics
- 4vec-monotonicity
- Monotonicity properties for the basic svex functions.
- Svex-monotonify
- Svex-alist-partial-monotonic
- Svex-alist-monotonic-on-vars
- 4veclist-<<=
- Nth-wise lattice ordering for 4veclists.
- Svexlist-partial-monotonic
- Svex-partial-monotonic
- Svex-alist-<<=
- Svex-alist-ovmonotonic
- Svexlist-<<=
- Svex-env-<<=
- (svex-env-<<= x y) checks whether an entire svex-env
conservatively approximates another: i.e., is every variable's value in x
an approximation of its value in y?
- Svex-alist-ovcongruent
- Svex-alist-monotonic-p
- Svexlist-monotonic-on-vars
- Svex-monotonic-on-vars
- Svex-<<=
- Svexlist-monotonic-p
- 4vec-xfree-p
- Recognizer for 4vecs with no X bits. These have a special
relationship with svex-xeval.
- Svex-apply-monotonocity
- svex-apply is almost always monotonic :-(
- Svexlist-ovmonotonic
- Svexlist-ovcongruent
- Svex-ovmonotonic
- Svex-monotonic-p
