		Search-engine friendly clone of the ACL2 documentation.

Exploding-vectors

Vl-emodwire-p

(vl-emodwire-p x) recognizes symbols that VL generates as wire names for E modules.

E uses a permissive pattern system that allows almost any atom to be used as a wire name. But when VL is used to translate Verilog modules, we always produce wire names that are symbols, whose names are either simple names like "reset" or indexed names like "opcode[3]".

We always generate wire names in the ACL2 package. This is due to historic convention, but also is a good idea for efficiency: we can control the size of the ACL2 package at the time we build ACL2, but we have no method (well, ttags I suppose) to construct a new package with a larger size. See the efficiency considerations in vl-wirealist-p for more details.

Definitions and Theorems

Function: vl-emodwire-scan$inline

(defun vl-emodwire-scan$inline (name)
       (declare (type string name))
       (b* ((open (position #\[ name))
            (close (position #\] name))
            (escape (if (position #\{ name) t nil))
            (illegal (if (or (position #\. name)
                             (position #\! name)
                             (position #\/ name))
                         t nil)))
           (mv open close escape illegal)))

Function: vl-emodwire-get-index$inline

(defun
 vl-emodwire-get-index$inline
 (name open close)
 (declare (xargs :guard (and (stringp name)
                             (natp open)
                             (natp close)
                             (< open close)
                             (= close (- (length name) 1)))))
 (b*
  ((index-str (subseq name (+ open 1) close))
   ((mv index-val len)
    (str::parse-nat-from-string index-str 0 0 0 (length index-str)))
   (ok1 (= len (length index-str)))
   (ok2 (equal index-str (natstr index-val))))
  (mv (and ok1 ok2) index-val)))

Function: vl-emodwire-p

(defun
 vl-emodwire-p (x)
 (declare (xargs :guard t))
 (b*
  (((unless (and (symbolp x) x)) nil)
   (name (symbol-name x))
   ((unless (eq (intern name "ACL2") x))
    nil)
   ((mv open close escape illegal)
    (vl-emodwire-scan name))
   ((when
     (or illegal
         (and escape
              (not (vl-emodwire-encoding-valid-p (explode name))))))
    nil)
   ((when (and (not open) (not close))) t)
   ((unless (and open close (< open close)
                 (= close (- (length name) 1))))
    nil)
   ((mv okp ?idx)
    (vl-emodwire-get-index name open close)))
  okp))

Theorem: booleanp-of-vl-emodwire-p

(defthm booleanp-of-vl-emodwire-p
        (booleanp (vl-emodwire-p x))
        :rule-classes :type-prescription)

Theorem: type-of-vl-emodwire-p

(defthm type-of-vl-emodwire-p
        (implies (vl-emodwire-p x)
                 (and (symbolp x) (not (equal x nil))))
        :rule-classes :compound-recognizer)

Subtopics

Vl-emodwire: Construct an emod wire from a base name and index.
Vl-emodwire-fix
Vl-emodwirelist-highest: (vl-emodwirelist-highest basename x) returns a number n that is at least as large as the index of any wire with this basename in x.
Vl-emodwire->index: Return the index of an vl-emodwire-p as a natural, or nil if there is no index.
Vl-emodwire->basename: Returns the name of an vl-emodwire-p, excluding the index, as a string.