• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
          • Vl-wirealist-p
            • Vl-msb-expr-bitlist
            • Vl-plain-wire-name
            • Vl-module-wirealist
            • Vl-emodwires-from-high-to-low
            • Vl-vardecl-msb-emodwires
            • Vl-vardecllist-to-wirealist
            • Vl-emodwires-from-msb-to-lsb
            • Vl-verilogify-emodwirelist
          • Emodwire-encoding
          • Vl-emodwire-p
          • Vl-emodwirelistlist
          • Vl-emodwirelist
        • 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
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-wirealist-p

Vl-emodwires-from-high-to-low

(vl-emodwires-from-high-to-low name high low) returns a list of vl-emodwire-ps: (name[high] name[high-1] ... name[low])

The range is inclusive on both sides, so if low and high are the same you still get one wire.

Definitions and Theorems

Function: vl-emodwires-from-high-to-low-aux

(defun vl-emodwires-from-high-to-low-aux (name high low acc)
  (declare (type string name)
           (xargs :guard (and (natp high)
                              (natp low)
                              (>= high low))))
  (b* ((name[low] (vl-emodwire-encoded name low))
       (acc (cons name[low] acc))
       ((when (mbe :logic (<= (nfix high) (nfix low))
                   :exec (= high low)))
        acc))
    (vl-emodwires-from-high-to-low-aux name (lnfix high)
                                       (+ 1 (lnfix low))
                                       acc)))

Function: vl-emodwires-from-high-to-low-aux-fixnum$inline

(defun vl-emodwires-from-high-to-low-aux-fixnum$inline
       (name high low acc)
 (declare (type string name)
          (type (unsigned-byte 32) high)
          (type (unsigned-byte 32) low)
          (xargs :guard (>= high low)))
 (b*
  ((name[low]
     (mbe :logic (vl-emodwire-encoded name low)
          :exec
          (if (< (the (unsigned-byte 32) low) 256)
              (intern (cat name
                           (aref1 '*vl-indexed-wire-name-array*
                                  *vl-indexed-wire-name-array* low))
                      "ACL2")
            (intern (cat name "[" (natstr low) "]")
                    "ACL2"))))
   (acc (cons name[low] acc))
   ((when (mbe :logic (<= (nfix high) (nfix low))
               :exec (= (the (unsigned-byte 32) high)
                        (the (unsigned-byte 32) low))))
    acc))
  (vl-emodwires-from-high-to-low-aux-fixnum
       name (lnfix high)
       (mbe :logic (+ 1 (nfix low))
            :exec (the (unsigned-byte 32) (+ low 1)))
       acc)))

Function: vl-emodwires-from-high-to-low

(defun vl-emodwires-from-high-to-low (name high low)
 (declare (type string name)
          (xargs :guard (and (natp high)
                             (natp low)
                             (>= high low))))
 (mbe
  :logic
  (vl-emodwires-from-high-to-low-aux
       (vl-emodwire-encode (string-fix name))
       (nfix high)
       (nfix low)
       nil)
  :exec
  (let ((name (vl-emodwire-encode name)))
    (if (< high (expt 2 30))
        (vl-emodwires-from-high-to-low-aux-fixnum name high low nil)
      (vl-emodwires-from-high-to-low-aux name high low nil)))))

Theorem: true-listp-of-vl-emodwires-from-high-to-low

(defthm true-listp-of-vl-emodwires-from-high-to-low
  (true-listp (vl-emodwires-from-high-to-low name high low))
  :rule-classes :type-prescription)

Theorem: vl-emodwirelist-p-of-vl-emodwires-from-high-to-low

(defthm vl-emodwirelist-p-of-vl-emodwires-from-high-to-low
  (vl-emodwirelist-p (vl-emodwires-from-high-to-low name high low)))

Theorem: basenames-of-vl-emodwires-from-high-to-low

(defthm basenames-of-vl-emodwires-from-high-to-low
 (equal
      (vl-emodwirelist->basenames
           (vl-emodwires-from-high-to-low name high low))
      (replicate (len (vl-emodwires-from-high-to-low name high low))
                 (string-fix name))))

Theorem: member-equal-of-indicies-of-vl-emodwires-from-high-to-low

(defthm member-equal-of-indicies-of-vl-emodwires-from-high-to-low
 (implies
      (>= (nfix high) (nfix low))
      (iff (member-equal
                idx
                (vl-emodwirelist->indices
                     (vl-emodwires-from-high-to-low name high low)))
           (and (natp idx)
                (<= (nfix low) idx)
                (<= idx (nfix high))))))

Theorem: unique-indicies-of-vl-emodwires-from-high-to-low

(defthm unique-indicies-of-vl-emodwires-from-high-to-low
  (no-duplicatesp-equal
       (vl-emodwirelist->indices
            (vl-emodwires-from-high-to-low name high low))))

Theorem: no-duplicatesp-equal-of-vl-emodwires-from-high-to-low

(defthm no-duplicatesp-equal-of-vl-emodwires-from-high-to-low
  (no-duplicatesp-equal
       (vl-emodwires-from-high-to-low name high low)))

Theorem: len-of-vl-emodwires-from-high-to-low

(defthm len-of-vl-emodwires-from-high-to-low
  (equal (len (vl-emodwires-from-high-to-low name high low))
         (+ 1 (nfix (- (nfix high) (nfix low))))))