• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
        • Defstv
        • Stv-compile
        • Symbolic-test-vector-format
        • Stv-implementation-details
        • Compiled-stv-p
        • Stv-run-for-all-dontcares
        • Stv-run
        • Stv-process
        • Stv-run-check-dontcares
        • Symbolic-test-vector-composition
        • Stv-expand
          • Stv-expand-name
          • Stv-hid-parse
          • Stv-wirename-parse
          • Stv-hid-to-paths
          • Stv-maybe-match-select
          • Stv-hid-split
          • Stv-expand-hids-in-lines
          • Stv-expand-names-in-lines
          • Stv-expand-hid
          • Stv-check-noncanonical-paths
        • Stv-easy-bindings
        • Stv-debug
        • Stv-run-squash-dontcares
        • Stvdata-p
        • Stv-doc
        • Stv2c
        • Stv-widen
        • Stv-out->width
        • Stv-in->width
        • Stv-number-of-phases
        • Stv->outs
        • Stv->ins
        • Stv-suffix-signals
        • Stv->vars
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Stv-expand

Stv-wirename-parse

Match a Verilog-style wire name, bit-select, or part-select.

Signature

(stv-wirename-parse str) → (mv err? basename msb? lsb?)

Arguments

str — Guard (stringp str).

Returns

err? — Type (maybe-stringp err?).

basename — Type (stringp basename).

msb? — Type (maybe-natp msb?).

lsb? — Type (maybe-natp lsb?).

Examples:

• "foo" becomes (mv nil "foo" nil nil)
• "foo[3]" becomes (mv nil "foo" 3 3)
• "foo[5:3]" becomes (mv nil "foo" 5 3)
• "foo[3:5]" becomes (mv nil "foo" 3 5)

If the wire name isn't of an acceptable form, an error message is returned as the first return value.

Definitions and Theorems

Function: stv-wirename-parse

(defun stv-wirename-parse (str)
  (declare (xargs :guard (stringp str)))
  (let ((__function__ 'stv-wirename-parse))
    (declare (ignorable __function__))
    (b* ((expr (vl2014::vl-parse-expr-from-str str))
         ((unless expr)
          (mv (str::cat (symbol-name __function__)
                        ": failed to parse: " str)
              "" nil nil))
         ((mv err from msb lsb)
          (stv-maybe-match-select expr))
         ((when err) (mv err "" nil nil))
         ((unless (vl2014::vl-idexpr-p from))
          (mv (str::cat (symbol-name __function__)
                        ": invalid wire name: " str)
              "" nil nil)))
      (mv nil (vl2014::vl-idexpr->name from)
          msb lsb))))

Theorem: maybe-stringp-of-stv-wirename-parse.err?

(defthm maybe-stringp-of-stv-wirename-parse.err?
  (b* (((mv ?err? ?basename ?msb? ?lsb?)
        (stv-wirename-parse str)))
    (maybe-stringp err?))
  :rule-classes :type-prescription)

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

(defthm stringp-of-stv-wirename-parse.basename
  (b* (((mv ?err? ?basename ?msb? ?lsb?)
        (stv-wirename-parse str)))
    (stringp basename))
  :rule-classes :rewrite)

Theorem: maybe-natp-of-stv-wirename-parse.msb?

(defthm maybe-natp-of-stv-wirename-parse.msb?
  (b* (((mv ?err? ?basename ?msb? ?lsb?)
        (stv-wirename-parse str)))
    (maybe-natp msb?))
  :rule-classes :type-prescription)

Theorem: maybe-natp-of-stv-wirename-parse.lsb?

(defthm maybe-natp-of-stv-wirename-parse.lsb?
  (b* (((mv ?err? ?basename ?msb? ?lsb?)
        (stv-wirename-parse str)))
    (maybe-natp lsb?))
  :rule-classes :type-prescription)