Associates wire names (strings) to lists of vl-emodwire-ps which represent the wire's bits in msb-first order.
(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.
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
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"
(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
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).
(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))))))
(defthm vl-wirealist-p-when-atom (implies (atom x) (equal (vl-wirealist-p x) t)))
(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))))
(defthm cons-listp-when-vl-wirealist-p (implies (vl-wirealist-p x) (cons-listp x)))
(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))))
(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)))))
(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)))))