• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
        • Vl-lintconfig-p
        • Lucid
        • Skip-detection
        • Vl-lintresult-p
        • Lint-warning-suppression
        • Condcheck
        • Selfassigns
          • Vl-modulelist-check-selfassigns
          • Vl-expr-approx-bits
          • Vl-assignlist-check-selfassigns
          • Vl-assign-check-selfassigns
          • Vl-module-check-selfassigns
          • Vl-selfassign-bits
          • Vl-design-check-selfassigns
          • Vl-selfassign-bit
        • Leftright-check
        • Dupeinst-check
        • Oddexpr-check
        • Remove-toohard
        • Qmarksize-check
        • Portcheck
        • Duplicate-detect
        • Vl-print-certain-warnings
        • Duperhs-check
        • *vl-lint-help*
        • Lint-stmt-rewrite
        • Drop-missing-submodules
        • Check-case
        • Drop-user-submodules
        • Check-namespace
        • Vl-lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Selfassigns

Vl-assignlist-check-selfassigns

(vl-assignlist-check-selfassigns x mod ialist) applies vl-assign-check-selfassigns to every member of the list x, and appends together all the resulting lists.

This is an ordinary defmapappend.

Function: vl-assignlist-check-selfassigns

(defun vl-assignlist-check-selfassigns (x mod ialist)
 (declare
    (xargs :guard (and (vl-assignlist-p x)
                       (vl-module-p mod)
                       (equal ialist (vl-make-moditem-alist mod)))))
 (mbe
     :logic
     (if (consp x)
         (append (vl-assign-check-selfassigns (car x)
                                              mod ialist)
                 (vl-assignlist-check-selfassigns (cdr x)
                                                  mod ialist))
       nil)
     :exec
     (reverse
          (vl-assignlist-check-selfassigns-exec x mod ialist nil))))

Definitions and Theorems

Function: vl-assignlist-check-selfassigns-exec

(defun vl-assignlist-check-selfassigns-exec (x mod ialist acc)
 (declare
    (xargs :guard (and (vl-assignlist-p x)
                       (vl-module-p mod)
                       (equal ialist (vl-make-moditem-alist mod)))))
 (if (consp x)
     (vl-assignlist-check-selfassigns-exec
          (cdr x)
          mod ialist
          (revappend (vl-assign-check-selfassigns (car x)
                                                  mod ialist)
                     acc))
   acc))

Function: vl-assignlist-check-selfassigns

(defun vl-assignlist-check-selfassigns (x mod ialist)
 (declare
    (xargs :guard (and (vl-assignlist-p x)
                       (vl-module-p mod)
                       (equal ialist (vl-make-moditem-alist mod)))))
 (mbe
     :logic
     (if (consp x)
         (append (vl-assign-check-selfassigns (car x)
                                              mod ialist)
                 (vl-assignlist-check-selfassigns (cdr x)
                                                  mod ialist))
       nil)
     :exec
     (reverse
          (vl-assignlist-check-selfassigns-exec x mod ialist nil))))

Theorem: vl-assignlist-check-selfassigns-exec-removal

(defthm vl-assignlist-check-selfassigns-exec-removal
 (equal
     (vl-assignlist-check-selfassigns-exec
          acl2::x mod ialist acl2::acc)
     (revappend (vl-assignlist-check-selfassigns acl2::x mod ialist)
                acl2::acc))
 :rule-classes ((:rewrite)))

Theorem: set-equiv-congruence-over-vl-assignlist-check-selfassigns

(defthm set-equiv-congruence-over-vl-assignlist-check-selfassigns
 (implies
   (set-equiv acl2::x acl2::y)
   (set-equiv (vl-assignlist-check-selfassigns acl2::x mod ialist)
              (vl-assignlist-check-selfassigns acl2::y mod ialist)))
 :rule-classes ((:congruence)))

Theorem: subsetp-of-vl-assignlist-check-selfassigns-when-subsetp

(defthm subsetp-of-vl-assignlist-check-selfassigns-when-subsetp
 (implies
     (subsetp acl2::x acl2::y)
     (subsetp (vl-assignlist-check-selfassigns acl2::x mod ialist)
              (vl-assignlist-check-selfassigns acl2::y mod ialist)))
 :rule-classes ((:rewrite)))

Theorem: member-in-vl-assignlist-check-selfassigns

(defthm member-in-vl-assignlist-check-selfassigns
 (implies
      (and (member acl2::k
                   (vl-assign-check-selfassigns acl2::j mod ialist))
           (member acl2::j acl2::x))
      (member acl2::k
              (vl-assignlist-check-selfassigns acl2::x mod ialist)))
 :rule-classes ((:rewrite)))

Theorem: vl-assignlist-check-selfassigns-of-list-fix

(defthm vl-assignlist-check-selfassigns-of-list-fix
  (equal (vl-assignlist-check-selfassigns (list-fix acl2::x)
                                          mod ialist)
         (vl-assignlist-check-selfassigns acl2::x mod ialist))
  :rule-classes ((:rewrite)))

Theorem: vl-assignlist-check-selfassigns-of-append

(defthm vl-assignlist-check-selfassigns-of-append
 (equal
      (vl-assignlist-check-selfassigns (append acl2::a acl2::b)
                                       mod ialist)
      (append (vl-assignlist-check-selfassigns acl2::a mod ialist)
              (vl-assignlist-check-selfassigns acl2::b mod ialist)))
 :rule-classes ((:rewrite)))

Theorem: vl-assignlist-check-selfassigns-when-not-consp

(defthm vl-assignlist-check-selfassigns-when-not-consp
  (implies
       (not (consp acl2::x))
       (equal (vl-assignlist-check-selfassigns acl2::x mod ialist)
              nil))
  :rule-classes ((:rewrite)))

Theorem: vl-assignlist-check-selfassigns-of-cons

(defthm vl-assignlist-check-selfassigns-of-cons
 (equal
      (vl-assignlist-check-selfassigns (cons acl2::a acl2::b)
                                       mod ialist)
      (append (vl-assign-check-selfassigns acl2::a mod ialist)
              (vl-assignlist-check-selfassigns acl2::b mod ialist)))
 :rule-classes ((:rewrite)))