		Search-engine friendly clone of the ACL2 documentation.

Stv-expand

Stv-hid-parse

Match a Verilog-style plain or hierarchical name, perhaps with a bit- or part-select on the end of it.

Signature
(stv-hid-parse str) → (mv instnames wirename msb-idx lsb-idx)
Arguments: str — The string to parse and split up.
Guard (stringp str).
Returns: instnames — Type (true-listp instnames).; wirename — Type (stringp wirename).; msb-idx — Type (or (not msb-idx) (natp msb-idx)).; lsb-idx — Type (or (not lsb-idx) (natp lsb-idx)).

This is sort of misnamed; it works for normal identifiers as well as hierarchical identifiers.

Examples:

                      instnames    wirename   msb    lsb
foo[3]           -->  nil          foo        3      3
foo.bar.baz      -->  (foo bar)    baz        nil    nil
foo.bar.baz[3]   -->  (foo bar)    baz        3      3
foo.bar.baz[3:0] -->  (foo bar)    baz        3      0

If the input string name isn't of an acceptable form, we cause an error.

Definitions and Theorems

Function: stv-hid-parse

(defun stv-hid-parse (str)
  (declare (xargs :guard (stringp str)))
  (let ((__function__ 'stv-hid-parse))
    (declare (ignorable __function__))
    (b* ((expr (vl2014::vl-parse-expr-from-str str))
         ((unless expr)
          (raise "Failed to parse: ~s0" str)
          (mv nil "" nil nil))
         ((mv err from msb lsb)
          (stv-maybe-match-select expr))
         ((when err)
          (raise "~s0" err)
          (mv nil "" nil nil))
         ((when (vl2014::vl-idexpr-p from))
          (mv nil (vl2014::vl-idexpr->name from)
              msb lsb))
         ((unless (vl2014::vl-hidexpr-p from))
          (raise "Invalid STV wire name: ~s0" str)
          (mv nil "" nil nil))
         ((mv instnames wirename)
          (stv-hid-split from)))
      (mv instnames wirename msb lsb))))

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

(defthm true-listp-of-stv-hid-parse.instnames
  (b* (((mv ?instnames ?wirename ?msb-idx ?lsb-idx)
        (stv-hid-parse str)))
    (true-listp instnames))
  :rule-classes :type-prescription)

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

(defthm stringp-of-stv-hid-parse.wirename
  (b* (((mv ?instnames ?wirename ?msb-idx ?lsb-idx)
        (stv-hid-parse str)))
    (stringp wirename))
  :rule-classes :type-prescription)

Theorem: return-type-of-stv-hid-parse.msb-idx

(defthm return-type-of-stv-hid-parse.msb-idx
  (b* (((mv ?instnames ?wirename ?msb-idx ?lsb-idx)
        (stv-hid-parse str)))
    (or (not msb-idx) (natp msb-idx)))
  :rule-classes :type-prescription)

Theorem: return-type-of-stv-hid-parse.lsb-idx

(defthm return-type-of-stv-hid-parse.lsb-idx
  (b* (((mv ?instnames ?wirename ?msb-idx ?lsb-idx)
        (stv-hid-parse str)))
    (or (not lsb-idx) (natp lsb-idx)))
  :rule-classes :type-prescription)

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

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

Subtopics

Vl2014::vl-explode-hidindex: Explode a (resolved) vl2014::vl-hidindex-p into a flat list of its components.
Vl2014::vl-explode-hid: Explode a (resolved) vl2014::vl-hidexpr-p into a flat list of its components.