		Search-engine friendly clone of the ACL2 documentation.

Esim-vl

Esim-vl-wirealist

Obtain the vl-wirealist-p for an E module produced by VL.

(esim-vl-wirealist mod) returns a vl-wirealist-p.

This is the "final" wirealist for the module, and typically will include temporary wires introduced by VL. The wirealist will be nil for certain primitive modules.

Run-time checks ensure the :wire-alist annotation of the module is a valid wirealist. This should work for any E module produced by VL, but it may cause an error if used on other modules. We memoize the function to minimize the expense of these checks.

Definitions and Theorems

Function: esim-vl-wirealist

(defun
 esim-vl-wirealist (mod)
 (declare (xargs :guard t))
 (b* ((name (gpl :n mod))
      (annotations (esim-vl-annotations mod))
      (lookup (assoc :wire-alist annotations))
      ((unless lookup)
       (if (gpl :x mod)
           nil
           (cw "Note: E module ~s0 has no :wire-alist annotation!~%"
               name)))
      (walist (cdr lookup))
      ((unless (vl-wirealist-p walist))
       (er hard? 'esim-vl-wirealist
           "In E module ~s0, :wire-alist fails vl-wirealist-p check"
           name)))
     walist))

Theorem: vl-wirealist-p-of-esim-vl-wirealist

(defthm vl-wirealist-p-of-esim-vl-wirealist
        (vl-wirealist-p (esim-vl-wirealist mod)))