		Search-engine friendly clone of the ACL2 documentation.

Esim-vl

Esim-vl-designwires

Produce a flat vl-emodwirelist-p that contains the E names of every bit that is visible in the original Verilog module.

(esim-vl-designwires mod) is given an E module and returns an vl-emodwirelist-p.

This list should include the E names for every bit that is declared in the original Verilog module; see VL's designwires transform. It should not include the new, intermediate wire names that VL generates during transformations like split and occform. Note that some of the names in this list might be unused, and hence might not occur in the occs of the module.

Run-time checks ensure that the :design-wires attribute of the module contains a valid vl-emodwirelist-p. This should work for any E module produced by VL, but 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-designwires

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

Theorem: vl-emodwirelist-p-of-esim-vl-designwires

(defthm vl-emodwirelist-p-of-esim-vl-designwires
  (vl-emodwirelist-p (esim-vl-designwires mod)))