		Search-engine friendly clone of the ACL2 documentation.

Exploding-vectors

Vl-wirealist-p

Associates wire names (strings) to lists of vl-emodwire-ps which represent the wire's bits in msb-first order.

Signature
(vl-wirealist-p x) → *

A wire alist provides a bit-level view of the wires in a module by associating the names of each net and register declared in the Verilog module (strings) with lists of vl-emodwire-ps that represent the individual bits of the wire, in msb-first order.

In particular,

Given a range-free Verilog wire named w, we bind the string "w" to (ACL2::w), i.e., a singleton list with just one symbol; and
Given a Verilog wire, w, with range [high:low], we bind "w" to (ACL2::w[high] ... ACL2::w[low]), i.e., a list of symbols from high to low, inclusive.
Given a Verilog wire, w, with range [low:high], we bind "w" to (ACL2::w[low] ... ACL2::w[high]).

Our vl-emodwire-p representation is robust and can reliably deal with wires no matter what their names. We can guarantee that the bits produced in a wire alist are unique as long as the net and register declarations for the module are uniquely named.

We take special care to avoid generating the names T, NIL, and F, since these have a special special meaning in Emod; see vl-plain-wire-name.

Efficiency Considerations

Profiling might "unfairly" suggest that wire-alist construction is very expensive.

In particular, the first time we build a wire alist for a module, we are generally doing "first-time" interns for the names of every bit. It is far more expensive to intern a string for the first time than to subsequently intern it again. For instance, when we run the following code in a fresh CCL session, we find that it takes 2.2 seconds to intern 100,000 fresh strings the first time, but it only takes 0.15 seconds to intern them all again.

(defpackage "FOO" (:use))

(ccl::egc nil)

(defparameter *strings*
 (loop for i fixnum from 1 to 100000
       collect
       (concatenate 'string "FOO-"
                    (format nil "~a" i))))

;; 2.21 seconds, 15 MB allocated
(time (loop for str in *strings* do (intern str "FOO")))

;; 0.15 seconds, no allocation
(time (loop for str in *strings* do (intern str "FOO")))

When we are interning millions of symbols, the package's size also has a huge impact on interning performance. Because of this, we typically build ACL2 with ACL2_SIZE=3000000 to avoid very slow interning.

Moreover, whether we intern these symbols "eagerly" by constructing a wire alist or "lazily" as they are needed, we will end up doing the same number of first-time interns. There is not really any way to avoid this interning without either fundamentally changing the design of the E language (e.g., to support vectors), or abandoning named wires in E modules (e.g., using numbers instead).

Definitions and Theorems

Function: vl-wirealist-p

(defun vl-wirealist-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-wirealist-p))
    (declare (ignorable __function__))
    (if (atom x)
        t
      (and (consp (car x))
           (stringp (caar x))
           (true-listp (cdar x))
           (vl-emodwirelist-p (cdar x))
           (vl-wirealist-p (cdr x))))))

Theorem: vl-wirealist-p-when-atom

(defthm vl-wirealist-p-when-atom
  (implies (atom x)
           (equal (vl-wirealist-p x) t)))

Theorem: vl-wirealist-p-of-cons

(defthm vl-wirealist-p-of-cons
  (equal (vl-wirealist-p (cons a x))
         (and (consp a)
              (stringp (car a))
              (true-listp (cdr a))
              (vl-emodwirelist-p (cdr a))
              (vl-wirealist-p x))))

Theorem: cons-listp-when-vl-wirealist-p

(defthm cons-listp-when-vl-wirealist-p
  (implies (vl-wirealist-p x)
           (cons-listp x)))

Theorem: vl-wirealist-p-of-hons-shrink-alist

(defthm vl-wirealist-p-of-hons-shrink-alist
  (implies (and (vl-wirealist-p x)
                (vl-wirealist-p y))
           (vl-wirealist-p (hons-shrink-alist x y))))

Theorem: vl-emodwirelist-p-of-cdr-of-hons-assoc-equal-when-vl-wirealist-p

(defthm
   vl-emodwirelist-p-of-cdr-of-hons-assoc-equal-when-vl-wirealist-p
 (implies (vl-wirealist-p walist)
          (vl-emodwirelist-p (cdr (hons-assoc-equal name walist)))))

Theorem: true-listp-of-cdr-of-hons-assoc-equal-when-vl-wirealist-p

(defthm true-listp-of-cdr-of-hons-assoc-equal-when-vl-wirealist-p
  (implies (vl-wirealist-p walist)
           (true-listp (cdr (hons-assoc-equal name walist)))))

Subtopics

Vl-msb-expr-bitlist: Produce the E-language, MSB-ordered list of bits for an expression.
Vl-plain-wire-name: (vl-plain-wire-name name) is given name, a string, and typically returns the symbol ACL2::name.
Vl-module-wirealist: Safely generate the (fast) wirealist for a module.
Vl-emodwires-from-high-to-low: (vl-emodwires-from-high-to-low name high low) returns a list of vl-emodwire-ps: (name[high] name[high-1] ... name[low])
Vl-vardecl-msb-emodwires: Compute the vl-emodwire-ps for a variable declaration, in MSB-first order.
Vl-vardecllist-to-wirealist: Generate a (fast) wirealist from a vl-vardecllist-p.
Vl-emodwires-from-msb-to-lsb: (vl-emodwires-from-msb-to-lsb name msb lsb) returns a list of vl-emodwire-ps: (name[msb] name[msb +/- 1] ... name[lsb])
Vl-verilogify-emodwirelist: Merge a list of vl-emodwire-ps into Verilog-style names.