Transform a merged index list into Verilog-style wire names.
(vl-verilogify-merged-indices name x) takes
(vl-verilogify-merged-indices "foo" '(1 (3 . 6) 8)) --> ("foo[1]" "foo[6:3]" "foo[8]")
Function:
(defun vl-verilogify-merged-indices (name x) (declare (xargs :guard (and (stringp name) (vl-merged-index-list-p x)))) (if (atom x) nil (cons (cond ((not (car x)) name) ((natp (car x)) (cat name "[" (natstr (car x)) "]")) ((consp (car x)) (let ((low (caar x)) (high (cdar x))) (cat name "[" (natstr high) ":" (natstr low) "]")))) (vl-verilogify-merged-indices name (cdr x)))))
Theorem:
(defthm string-listp-of-vl-verilogify-merged-indices (implies (and (force (stringp name)) (force (vl-merged-index-list-p x))) (string-listp (vl-verilogify-merged-indices name x))))