		Search-engine friendly clone of the ACL2 documentation.

Stv-expand

Stv-expand-name

Expand a name from a symbolic test vector's line into explicit lists of E bits.

Signature
(stv-expand-name x type mod) → lsb-bits
Arguments: x — The name that the user put at the start of some STV line.; type — Either :i or :o and says whether this should be the name of an input or output.
Guard (or (eq type :i) (eq type :o)).; mod — The esim module we are working in, so we can look up names.
Returns: lsb-bits — An LSB-first list of E bits for a non-hierarchical valid STV signal name, e.g., (|foo[0]| |foo[1]| ...).

Recall from symbolic-test-vector-format that signal names for :input and :output lines can be either:

A string that names a particular input bus,
A string that is a Veriog-style bit- or part-select from a particular input bus, or
An explicit list of E bits (in LSB-first order).

Here, our goal is to convert any such name, x, into the explicit bit list form. If x is already a list of bits then this is trivial. Otherwise, we have to look it up in the module. We do basic error checking to make sure that the name refers to valid input or output bits.

Definitions and Theorems

Function: stv-expand-name

(defun stv-expand-name (x type mod)
 (declare (xargs :guard (or (eq type :i) (eq type :o))))
 (let ((__function__ 'stv-expand-name))
  (declare (ignorable __function__))
  (b*
   ((pat (gpl type mod))
    (modname (gpl :n mod))
    ((when (stringp x))
     (b*
      (((mv ?err basename msb lsb)
        (stv-wirename-parse x))
       ((when err) (raise "~s0" err))
       (basename-bits (vl2014::esim-vl-find-io basename pat))
       ((unless basename-bits)
        (raise
         "Trying to expand ~s0, but there is no ~s1 named ~s2 in ~
                      ~x3."
         x (if (eq type :i) "input" "output")
         basename modname))
       ((unless (and msb lsb)) basename-bits)
       (expect-bits
            (vl2014::vl-emodwires-from-msb-to-lsb basename lsb msb))
       ((unless (ordered-subsetp expect-bits basename-bits))
        (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 basename-bits)
             "are not in the right order"
           "are not found")
         (car basename-bits)
         (car (last basename-bits))
         (car expect-bits)
         (car (last expect-bits)))))
      expect-bits))
    ((unless (symbol-listp x))
     (raise
      "Invalid input name (expected string or a list of e bits), but ~
                found ~x0."
      x))
    (flat-pat (pat-flatten1 pat))
    ((unless (subsetp-equal x flat-pat))
     (raise
         "Trying to provide bindings for ~s0 that don't exist: ~x1."
         (if (eq type :i) "inputs" "outputs")
         (set-difference-equal flat-pat x))))
   x)))