		Search-engine friendly clone of the ACL2 documentation.

Stv-expand

Stv-hid-to-paths

Convert a Verilog-style plain or hierarchical name (optionally with a bit- or part-select) into an LSB-ordered list of non-canonical ESIM paths.

Signature
(stv-hid-to-paths x mod) → lsb-paths
Arguments: x — A string like foo, foo[3:0], foo.bar.baz, foo.bar.baz[3], etc. That is, it should either be a plain or hierarchical Verilog identifier, perhaps with a bit or part-select on the end.
Guard (stringp x).; mod — The esim module that this path should be relative to.
Returns: lsb-paths — LSB-first list of non-canonical paths for x, in the sense of mod-internal-paths.

Definitions and Theorems

Function: stv-hid-to-paths

(defun
 stv-hid-to-paths (x mod)
 (declare (xargs :guard (stringp x)))
 (let
  ((__function__ 'stv-hid-to-paths))
  (declare (ignorable __function__))
  (b*
   (((mv instnames wirename msb lsb)
     (stv-hid-parse x))
    (instnames (str::intern-list instnames))
    (submod (follow-esim-path instnames mod))
    ((unless submod)
     (raise "Error following path ~x0 in ~x1."
            x (gpl :n mod)))
    (walist (vl2014::esim-vl-wirealist submod))
    (lookup (hons-assoc-equal wirename walist))
    ((unless lookup)
     (raise
      "Can't follow ~s0: followed the instances ~x1 to an ~x2 ~
                submodule, but then there was no wire named ~s3 in the wire ~
                alist."
      x instnames (gpl :n submod)
      wirename))
    (msb-first-wires (cdr lookup))
    (lsb-first-wires (reverse msb-first-wires))
    ((unless (and msb lsb))
     (stv-turn-bits-into-non-canonical-paths
          instnames lsb-first-wires))
    (expect-bits
         (vl2014::vl-emodwires-from-msb-to-lsb wirename lsb msb))
    ((unless (ordered-subsetp expect-bits lsb-first-wires))
     (raise
      "Trying to expand ~s0, but the bits being asked for ~s1.~% ~
                 - Found wires: ~x2 through ~x3~% ~
                 - Want wires:  ~x4 through ~x5."
      x
      (if (subsetp-equal expect-bits lsb-first-wires)
          "are not in the right order"
          "are not found")
      (car lsb-first-wires)
      (car (last lsb-first-wires))
      (car expect-bits)
      (car (last expect-bits)))))
   (stv-turn-bits-into-non-canonical-paths instnames expect-bits))))

Subtopics

Stv-turn-bits-into-non-canonical-paths