• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
          • Vl-expr-lvaluep
            • Vl-exprlist-lvaluesp
          • Lvaluecheck
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Lvalues
• Vl-expr-p

Vl-expr-lvaluep

Determine if an expression looks like a good lvalue.

Signature

(vl-expr-lvaluep x) → *

Arguments

x — Guard (vl-expr-p x).

We say the lvalue expressions are the subset of expressions formed by recursively closing

• the identifiers (whether simple or hierarchical), and
• bit- and part-selects, including indexed part-selects like [i +: 3]

under concatenation. This definition is permissive enough to include the structural net expressions (see section 12.3.9.2) used in port connections and also the lvalues which are permitted in continuous and procedural assignment statements.

Theorem: vl-exprlist-lvaluesp-of-cons

(defthm vl-exprlist-lvaluesp-of-cons
  (equal (vl-exprlist-lvaluesp (cons acl2::a acl2::x))
         (and (vl-expr-lvaluep acl2::a)
              (vl-exprlist-lvaluesp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-cdr-when-vl-exprlist-lvaluesp

(defthm vl-exprlist-lvaluesp-of-cdr-when-vl-exprlist-lvaluesp
  (implies (vl-exprlist-lvaluesp (double-rewrite acl2::x))
           (vl-exprlist-lvaluesp (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-when-not-consp

(defthm vl-exprlist-lvaluesp-when-not-consp
  (implies (not (consp acl2::x))
           (vl-exprlist-lvaluesp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: vl-expr-lvaluep-of-car-when-vl-exprlist-lvaluesp

(defthm vl-expr-lvaluep-of-car-when-vl-exprlist-lvaluesp
  (implies (vl-exprlist-lvaluesp acl2::x)
           (iff (vl-expr-lvaluep (car acl2::x))
                (consp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-append

(defthm vl-exprlist-lvaluesp-of-append
  (equal (vl-exprlist-lvaluesp (append acl2::a acl2::b))
         (and (vl-exprlist-lvaluesp acl2::a)
              (vl-exprlist-lvaluesp acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-list-fix

(defthm vl-exprlist-lvaluesp-of-list-fix
  (equal (vl-exprlist-lvaluesp (list-fix acl2::x))
         (vl-exprlist-lvaluesp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-sfix

(defthm vl-exprlist-lvaluesp-of-sfix
  (iff (vl-exprlist-lvaluesp (sfix acl2::x))
       (or (vl-exprlist-lvaluesp acl2::x)
           (not (setp acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-insert

(defthm vl-exprlist-lvaluesp-of-insert
  (iff (vl-exprlist-lvaluesp (insert acl2::a acl2::x))
       (and (vl-exprlist-lvaluesp (sfix acl2::x))
            (vl-expr-lvaluep acl2::a)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-delete

(defthm vl-exprlist-lvaluesp-of-delete
  (implies (vl-exprlist-lvaluesp acl2::x)
           (vl-exprlist-lvaluesp (delete acl2::k acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-mergesort

(defthm vl-exprlist-lvaluesp-of-mergesort
  (iff (vl-exprlist-lvaluesp (mergesort acl2::x))
       (vl-exprlist-lvaluesp (list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-union

(defthm vl-exprlist-lvaluesp-of-union
  (iff (vl-exprlist-lvaluesp (union acl2::x acl2::y))
       (and (vl-exprlist-lvaluesp (sfix acl2::x))
            (vl-exprlist-lvaluesp (sfix acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-intersect-1

(defthm vl-exprlist-lvaluesp-of-intersect-1
  (implies (vl-exprlist-lvaluesp acl2::x)
           (vl-exprlist-lvaluesp (intersect acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-intersect-2

(defthm vl-exprlist-lvaluesp-of-intersect-2
  (implies (vl-exprlist-lvaluesp acl2::y)
           (vl-exprlist-lvaluesp (intersect acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-difference

(defthm vl-exprlist-lvaluesp-of-difference
  (implies (vl-exprlist-lvaluesp acl2::x)
           (vl-exprlist-lvaluesp (difference acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-duplicated-members

(defthm vl-exprlist-lvaluesp-of-duplicated-members
  (implies (vl-exprlist-lvaluesp acl2::x)
           (vl-exprlist-lvaluesp (duplicated-members acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-rev

(defthm vl-exprlist-lvaluesp-of-rev
  (equal (vl-exprlist-lvaluesp (rev acl2::x))
         (vl-exprlist-lvaluesp (list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-rcons

(defthm vl-exprlist-lvaluesp-of-rcons
  (iff (vl-exprlist-lvaluesp (acl2::rcons acl2::a acl2::x))
       (and (vl-expr-lvaluep acl2::a)
            (vl-exprlist-lvaluesp (list-fix acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: vl-expr-lvaluep-when-member-equal-of-vl-exprlist-lvaluesp

(defthm vl-expr-lvaluep-when-member-equal-of-vl-exprlist-lvaluesp
  (and (implies (and (member-equal acl2::a acl2::x)
                     (vl-exprlist-lvaluesp acl2::x))
                (vl-expr-lvaluep acl2::a))
       (implies (and (vl-exprlist-lvaluesp acl2::x)
                     (member-equal acl2::a acl2::x))
                (vl-expr-lvaluep acl2::a)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-when-subsetp-equal

(defthm vl-exprlist-lvaluesp-when-subsetp-equal
  (and (implies (and (subsetp-equal acl2::x acl2::y)
                     (vl-exprlist-lvaluesp acl2::y))
                (vl-exprlist-lvaluesp acl2::x))
       (implies (and (vl-exprlist-lvaluesp acl2::y)
                     (subsetp-equal acl2::x acl2::y))
                (vl-exprlist-lvaluesp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-set-equiv-congruence

(defthm vl-exprlist-lvaluesp-set-equiv-congruence
  (implies (set-equiv acl2::x acl2::y)
           (equal (vl-exprlist-lvaluesp acl2::x)
                  (vl-exprlist-lvaluesp acl2::y)))
  :rule-classes :congruence)

Theorem: vl-exprlist-lvaluesp-of-set-difference-equal

(defthm vl-exprlist-lvaluesp-of-set-difference-equal
 (implies
      (vl-exprlist-lvaluesp acl2::x)
      (vl-exprlist-lvaluesp (set-difference-equal acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-intersection-equal-1

(defthm vl-exprlist-lvaluesp-of-intersection-equal-1
  (implies
       (vl-exprlist-lvaluesp (double-rewrite acl2::x))
       (vl-exprlist-lvaluesp (intersection-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-intersection-equal-2

(defthm vl-exprlist-lvaluesp-of-intersection-equal-2
  (implies
       (vl-exprlist-lvaluesp (double-rewrite acl2::y))
       (vl-exprlist-lvaluesp (intersection-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-union-equal

(defthm vl-exprlist-lvaluesp-of-union-equal
  (equal (vl-exprlist-lvaluesp (union-equal acl2::x acl2::y))
         (and (vl-exprlist-lvaluesp (list-fix acl2::x))
              (vl-exprlist-lvaluesp (double-rewrite acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-take

(defthm vl-exprlist-lvaluesp-of-take
  (implies (vl-exprlist-lvaluesp (double-rewrite acl2::x))
           (iff (vl-exprlist-lvaluesp (take acl2::n acl2::x))
                (or (vl-expr-lvaluep nil)
                    (<= (nfix acl2::n) (len acl2::x)))))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-repeat

(defthm vl-exprlist-lvaluesp-of-repeat
  (iff (vl-exprlist-lvaluesp (repeat acl2::n acl2::x))
       (or (vl-expr-lvaluep acl2::x)
           (zp acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: vl-expr-lvaluep-of-nth-when-vl-exprlist-lvaluesp

(defthm vl-expr-lvaluep-of-nth-when-vl-exprlist-lvaluesp
  (implies (vl-exprlist-lvaluesp acl2::x)
           (iff (vl-expr-lvaluep (nth acl2::n acl2::x))
                (< (nfix acl2::n) (len acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-update-nth

(defthm vl-exprlist-lvaluesp-of-update-nth
 (implies
    (vl-exprlist-lvaluesp (double-rewrite acl2::x))
    (iff (vl-exprlist-lvaluesp (update-nth acl2::n acl2::y acl2::x))
         (and (vl-expr-lvaluep acl2::y)
              (or (<= (nfix acl2::n) (len acl2::x))
                  (vl-expr-lvaluep nil)))))
 :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-butlast

(defthm vl-exprlist-lvaluesp-of-butlast
  (implies (vl-exprlist-lvaluesp (double-rewrite acl2::x))
           (vl-exprlist-lvaluesp (butlast acl2::x acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-nthcdr

(defthm vl-exprlist-lvaluesp-of-nthcdr
  (implies (vl-exprlist-lvaluesp (double-rewrite acl2::x))
           (vl-exprlist-lvaluesp (nthcdr acl2::n acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-last

(defthm vl-exprlist-lvaluesp-of-last
  (implies (vl-exprlist-lvaluesp (double-rewrite acl2::x))
           (vl-exprlist-lvaluesp (last acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-remove

(defthm vl-exprlist-lvaluesp-of-remove
  (implies (vl-exprlist-lvaluesp acl2::x)
           (vl-exprlist-lvaluesp (remove acl2::a acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-lvaluesp-of-revappend

(defthm vl-exprlist-lvaluesp-of-revappend
  (equal (vl-exprlist-lvaluesp (revappend acl2::x acl2::y))
         (and (vl-exprlist-lvaluesp (list-fix acl2::x))
              (vl-exprlist-lvaluesp acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-expr-lvaluep-of-vl-expr-fix-x

(defthm vl-expr-lvaluep-of-vl-expr-fix-x
  (equal (vl-expr-lvaluep (vl-expr-fix x))
         (vl-expr-lvaluep x)))

Theorem: vl-exprlist-lvaluesp-of-vl-exprlist-fix-x

(defthm vl-exprlist-lvaluesp-of-vl-exprlist-fix-x
  (equal (vl-exprlist-lvaluesp (vl-exprlist-fix x))
         (vl-exprlist-lvaluesp x)))

Theorem: vl-expr-lvaluep-vl-expr-equiv-congruence-on-x

(defthm vl-expr-lvaluep-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-expr-lvaluep x)
                  (vl-expr-lvaluep x-equiv)))
  :rule-classes :congruence)

Theorem: vl-exprlist-lvaluesp-vl-exprlist-equiv-congruence-on-x

(defthm vl-exprlist-lvaluesp-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-exprlist-lvaluesp x)
                  (vl-exprlist-lvaluesp x-equiv)))
  :rule-classes :congruence)

Theorem: vl-exprlist-lvaluesp-of-vl-nonatom->args-when-concat

(defthm vl-exprlist-lvaluesp-of-vl-nonatom->args-when-concat
  (implies (and (equal (vl-nonatom->op x) :vl-concat)
                (force (not (vl-atom-p x)))
                (force (vl-expr-lvaluep x)))
           (vl-exprlist-lvaluesp (vl-nonatom->args x))))

Subtopics

Vl-exprlist-lvaluesp