• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
        • Vl-ealist-p
        • Modinsts-to-eoccs
        • Vl-module-make-esim
        • Exploding-vectors
        • Resolving-multiple-drivers
        • Vl-modulelist-make-esims
        • Vl-module-check-e-ok
        • Vl-collect-design-wires
        • Adding-z-drivers
        • Vl-design-to-e
        • Vl-design-to-e-check-ports
        • Vl-design-to-e-main
        • Port-bit-checking
          • Vl-modulelist-check-port-bits
          • Vl-module-check-port-bits
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Port-bit-checking

Vl-modulelist-check-port-bits

(vl-modulelist-check-port-bits x) maps vl-module-check-port-bits across a list.

Signature

(vl-modulelist-check-port-bits x) → new-x

Arguments

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

Returns

new-x — Type (vl-modulelist-p new-x).

Performance note. This will look expensive because it calls vl-module-wirealist, vl-portdecls-to-i/o and vl-portlist-msb-bit-pattern on all modules. But since these are memoized, we get to reuse this work when we generate the eoccs for module instances and need to look up these patterns.

Definitions and Theorems

Function: vl-modulelist-check-port-bits-exec

(defun vl-modulelist-check-port-bits-exec
       (x acc)
       (declare (xargs :guard (vl-modulelist-p x)))
       (declare (xargs :guard t))
       (let ((__function__ 'vl-modulelist-check-port-bits-exec))
            (declare (ignorable __function__))
            (if (consp x)
                (vl-modulelist-check-port-bits-exec
                     (cdr x)
                     (cons (vl-module-check-port-bits (car x))
                           acc))
                acc)))

Function: vl-modulelist-check-port-bits-nrev

(defun
 vl-modulelist-check-port-bits-nrev
 (x nrev)
 (declare (xargs :stobjs (nrev)))
 (declare (xargs :guard (vl-modulelist-p x)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-modulelist-check-port-bits-nrev))
      (declare (ignorable __function__))
      (if (atom x)
          (nrev-fix nrev)
          (let ((nrev (nrev-push (vl-module-check-port-bits (car x))
                                 nrev)))
               (vl-modulelist-check-port-bits-nrev (cdr x)
                                                   nrev)))))

Function: vl-modulelist-check-port-bits

(defun
 vl-modulelist-check-port-bits (x)
 (declare (xargs :guard (vl-modulelist-p x)))
 (declare (xargs :guard t))
 (let
  ((__function__ 'vl-modulelist-check-port-bits))
  (declare (ignorable __function__))
  (mbe
     :logic (if (consp x)
                (cons (vl-module-check-port-bits (car x))
                      (vl-modulelist-check-port-bits (cdr x)))
                nil)
     :exec (if (atom x)
               nil
               (with-local-nrev
                    (vl-modulelist-check-port-bits-nrev x nrev))))))

Theorem: vl-modulelist-p-of-vl-modulelist-check-port-bits

(defthm vl-modulelist-p-of-vl-modulelist-check-port-bits
        (b* ((new-x (vl-modulelist-check-port-bits x)))
            (vl-modulelist-p new-x))
        :rule-classes :rewrite)

Theorem: vl-modulelist-check-port-bits-of-update-nth

(defthm
  vl-modulelist-check-port-bits-of-update-nth
  (implies
       (<= (nfix acl2::n) (len acl2::x))
       (equal (vl-modulelist-check-port-bits
                   (update-nth acl2::n acl2::v acl2::x))
              (update-nth acl2::n
                          (vl-module-check-port-bits acl2::v)
                          (vl-modulelist-check-port-bits acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: vl-modulelist-check-port-bits-of-revappend

(defthm
  vl-modulelist-check-port-bits-of-revappend
  (equal (vl-modulelist-check-port-bits (revappend acl2::x acl2::y))
         (revappend (vl-modulelist-check-port-bits acl2::x)
                    (vl-modulelist-check-port-bits acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: nthcdr-of-vl-modulelist-check-port-bits

(defthm
    nthcdr-of-vl-modulelist-check-port-bits
    (equal (nthcdr acl2::n
                   (vl-modulelist-check-port-bits acl2::x))
           (vl-modulelist-check-port-bits (nthcdr acl2::n acl2::x)))
    :rule-classes ((:rewrite)))

Theorem: nth-of-vl-modulelist-check-port-bits

(defthm
     nth-of-vl-modulelist-check-port-bits
     (equal (nth acl2::n
                 (vl-modulelist-check-port-bits acl2::x))
            (and (< (nfix acl2::n) (len acl2::x))
                 (vl-module-check-port-bits (nth acl2::n acl2::x))))
     :rule-classes ((:rewrite)))

Theorem: vl-modulelist-check-port-bits-nrev-removal

(defthm vl-modulelist-check-port-bits-nrev-removal
        (equal (vl-modulelist-check-port-bits-nrev acl2::x nrev)
               (append nrev
                       (vl-modulelist-check-port-bits acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: vl-modulelist-check-port-bits-exec-removal

(defthm
     vl-modulelist-check-port-bits-exec-removal
     (equal (vl-modulelist-check-port-bits-exec acl2::x acl2::acc)
            (revappend (vl-modulelist-check-port-bits acl2::x)
                       acl2::acc))
     :rule-classes ((:rewrite)))

Theorem: vl-modulelist-check-port-bits-of-take

(defthm
  vl-modulelist-check-port-bits-of-take
  (implies
       (<= (nfix acl2::n) (len acl2::x))
       (equal (vl-modulelist-check-port-bits (take acl2::n acl2::x))
              (take acl2::n
                    (vl-modulelist-check-port-bits acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: set-equiv-congruence-over-vl-modulelist-check-port-bits

(defthm
     set-equiv-congruence-over-vl-modulelist-check-port-bits
     (implies (set-equiv acl2::x acl2::y)
              (set-equiv (vl-modulelist-check-port-bits acl2::x)
                         (vl-modulelist-check-port-bits acl2::y)))
     :rule-classes ((:congruence)))

Theorem: subsetp-of-vl-modulelist-check-port-bits-when-subsetp

(defthm subsetp-of-vl-modulelist-check-port-bits-when-subsetp
        (implies (subsetp acl2::x acl2::y)
                 (subsetp (vl-modulelist-check-port-bits acl2::x)
                          (vl-modulelist-check-port-bits acl2::y)))
        :rule-classes ((:rewrite)))

Theorem: member-of-vl-module-check-port-bits-in-vl-modulelist-check-port-bits

(defthm
 member-of-vl-module-check-port-bits-in-vl-modulelist-check-port-bits
 (implies (member acl2::k acl2::x)
          (member (vl-module-check-port-bits acl2::k)
                  (vl-modulelist-check-port-bits acl2::x)))
 :rule-classes ((:rewrite)))

Theorem: vl-modulelist-check-port-bits-of-rev

(defthm vl-modulelist-check-port-bits-of-rev
        (equal (vl-modulelist-check-port-bits (rev acl2::x))
               (rev (vl-modulelist-check-port-bits acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: vl-modulelist-check-port-bits-of-list-fix

(defthm vl-modulelist-check-port-bits-of-list-fix
        (equal (vl-modulelist-check-port-bits (list-fix acl2::x))
               (vl-modulelist-check-port-bits acl2::x))
        :rule-classes ((:rewrite)))

Theorem: vl-modulelist-check-port-bits-of-append

(defthm
     vl-modulelist-check-port-bits-of-append
     (equal (vl-modulelist-check-port-bits (append acl2::a acl2::b))
            (append (vl-modulelist-check-port-bits acl2::a)
                    (vl-modulelist-check-port-bits acl2::b)))
     :rule-classes ((:rewrite)))

Theorem: cdr-of-vl-modulelist-check-port-bits

(defthm cdr-of-vl-modulelist-check-port-bits
        (equal (cdr (vl-modulelist-check-port-bits acl2::x))
               (vl-modulelist-check-port-bits (cdr acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: car-of-vl-modulelist-check-port-bits

(defthm car-of-vl-modulelist-check-port-bits
        (equal (car (vl-modulelist-check-port-bits acl2::x))
               (and (consp acl2::x)
                    (vl-module-check-port-bits (car acl2::x))))
        :rule-classes ((:rewrite)))

Theorem: vl-modulelist-check-port-bits-under-iff

(defthm vl-modulelist-check-port-bits-under-iff
        (iff (vl-modulelist-check-port-bits acl2::x)
             (consp acl2::x))
        :rule-classes ((:rewrite)))

Theorem: consp-of-vl-modulelist-check-port-bits

(defthm consp-of-vl-modulelist-check-port-bits
        (equal (consp (vl-modulelist-check-port-bits acl2::x))
               (consp acl2::x))
        :rule-classes ((:rewrite)))

Theorem: len-of-vl-modulelist-check-port-bits

(defthm len-of-vl-modulelist-check-port-bits
        (equal (len (vl-modulelist-check-port-bits acl2::x))
               (len acl2::x))
        :rule-classes ((:rewrite)))

Theorem: true-listp-of-vl-modulelist-check-port-bits

(defthm true-listp-of-vl-modulelist-check-port-bits
        (true-listp (vl-modulelist-check-port-bits acl2::x))
        :rule-classes :type-prescription)

Theorem: vl-modulelist-check-port-bits-when-not-consp

(defthm vl-modulelist-check-port-bits-when-not-consp
        (implies (not (consp acl2::x))
                 (equal (vl-modulelist-check-port-bits acl2::x)
                        nil))
        :rule-classes ((:rewrite)))

Theorem: vl-modulelist-check-port-bits-of-cons

(defthm
     vl-modulelist-check-port-bits-of-cons
     (equal (vl-modulelist-check-port-bits (cons acl2::a acl2::b))
            (cons (vl-module-check-port-bits acl2::a)
                  (vl-modulelist-check-port-bits acl2::b)))
     :rule-classes ((:rewrite)))

Theorem: vl-modulelist->names-of-vl-modulelist-check-port-bits

(defthm
     vl-modulelist->names-of-vl-modulelist-check-port-bits
     (equal (vl-modulelist->names (vl-modulelist-check-port-bits x))
            (vl-modulelist->names x)))