		Search-engine friendly clone of the ACL2 documentation.

Vl-wirealist-p

Vl-verilogify-emodwirelist

Merge a list of vl-emodwire-ps into Verilog-style names.

Definitions and Theorems

Function: vl-verilogify-emodwirelist

(defun vl-verilogify-emodwirelist (x)
  (declare (xargs :guard (vl-emodwirelist-p x)))
  (vl-verilogify-emodwirelist-0 (vl-emodwire-sort (list-fix x))))

Theorem: string-listp-of-vl-verilogify-emodwirelist

(defthm string-listp-of-vl-verilogify-emodwirelist
  (implies (force (vl-emodwirelist-p x))
           (string-listp (vl-verilogify-emodwirelist x))))

Subtopics

Vl-match-contiguous-indices: Identify one strictly increasing segment of a vl-maybe-nat-listp.
Vl-verilogify-merged-indices: Transform a merged index list into Verilog-style wire names.
Vl-merge-contiguous-indices: Transform a vl-maybe-nat-listp by combining contiguous sequences of indices into (low . high) pairs.