		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.