		Search-engine friendly clone of the ACL2 documentation.

Vl-wirealist-p

Vl-emodwires-from-msb-to-lsb

(vl-emodwires-from-msb-to-lsb name msb lsb) returns a list of vl-emodwire-ps: (name[msb] name[msb +/- 1] ... name[lsb])

Signature
(vl-emodwires-from-msb-to-lsb name msb lsb) → *
Arguments: name — Guard (stringp name).; msb — Guard (natp msb).; lsb — Guard (natp lsb).

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

Definitions and Theorems

Function: vl-emodwires-from-msb-to-lsb

(defun vl-emodwires-from-msb-to-lsb (name msb lsb)
 (declare (xargs :guard (and (stringp name)
                             (natp msb)
                             (natp lsb))))
 (let ((__function__ 'vl-emodwires-from-msb-to-lsb))
  (declare (ignorable __function__))
  (b* ((high (max msb lsb))
       (low (min msb lsb))
       (|w[high:low]| (vl-emodwires-from-high-to-low name high low))
       (|w[msb:lsb]| (if (>= msb lsb)
                         |w[high:low]|
                       (reverse |w[high:low]|))))
    |w[msb:lsb]|)))