		Search-engine friendly clone of the ACL2 documentation.

Stv-expand

Stv-hid-split

Splits up a HID into a list of instance names and a wire name.

Signature
(stv-hid-split hid) → (mv instnames wirename)
Arguments: hid — Guard (and (vl2014::vl-expr-p hid) (vl2014::vl-hidexpr-p hid)).
Returns: instnames — Type (true-listp instnames).; wirename — Type (stringp wirename).

Definitions and Theorems

Function: stv-hid-split

(defun stv-hid-split (hid)
 (declare (xargs :guard (and (vl2014::vl-expr-p hid)
                             (vl2014::vl-hidexpr-p hid))))
 (let ((__function__ 'stv-hid-split))
  (declare (ignorable __function__))
  (b*
   (((unless (vl2014::vl-hidexpr-resolved-p hid))
     (raise "HID has unresolved indices: ~s0~%"
            (vl2014::vl-pps-expr hid))
     (mv nil ""))
    (parts (vl2014::vl-explode-hid hid))
    ((unless (string-listp parts))
     (raise
      "We don't currently support hierarchical identifiers that go ~
                through array instances, like foo.bar[3].baz.  The HID that ~
                triggered this error was: ~s0~%"
      (vl2014::vl-pps-expr hid))
     (mv nil ""))
    ((when (< (len parts) 2))
     (raise "Somehow the HID has only one piece?  ~s0~%"
            (vl2014::vl-pps-expr hid))
     (mv nil ""))
    (instnames (butlast parts 1))
    (wirename (car (last parts))))
   (mv instnames wirename))))

Theorem: true-listp-of-stv-hid-split.instnames

(defthm true-listp-of-stv-hid-split.instnames
  (b* (((mv ?instnames ?wirename)
        (stv-hid-split hid)))
    (true-listp instnames))
  :rule-classes :type-prescription)

Theorem: stringp-of-stv-hid-split.wirename

(defthm stringp-of-stv-hid-split.wirename
  (b* (((mv ?instnames ?wirename)
        (stv-hid-split hid)))
    (stringp wirename))
  :rule-classes :type-prescription)

Theorem: string-listp-of-stv-hid-split

(defthm string-listp-of-stv-hid-split
  (string-listp (mv-nth 0 (stv-hid-split hid))))