		Search-engine friendly clone of the ACL2 documentation.

Gate-elim

Vl-add-portnames-to-plainargs

Goofy operation to name the arguments as we convert gate instances.

Signature
(vl-add-portnames-to-plainargs plainargs ports) → new-args
Arguments: plainargs — Plainargs from a gate instance, which already should have their directions computed.
Guard (vl-plainarglist-p plainargs).; ports — Ports from the corresponding VL primitive. We want to give the plainargs the names from these ports.
Guard (vl-portlist-p ports).
Returns: new-args — Type (vl-plainarglist-p new-args), given the guard.

Definitions and Theorems

Function: vl-add-portnames-to-plainargs

(defun vl-add-portnames-to-plainargs (plainargs ports)
 (declare (xargs :guard (and (vl-plainarglist-p plainargs)
                             (vl-portlist-p ports))))
 (declare (xargs :guard (same-lengthp plainargs ports)))
 (let ((__function__ 'vl-add-portnames-to-plainargs))
  (declare (ignorable __function__))
  (if (atom plainargs)
      nil
    (cons (change-vl-plainarg (car plainargs)
                              :portname (vl-port->name (car ports)))
          (vl-add-portnames-to-plainargs (cdr plainargs)
                                         (cdr ports))))))

Theorem: vl-plainarglist-p-of-vl-add-portnames-to-plainargs

(defthm vl-plainarglist-p-of-vl-add-portnames-to-plainargs
 (implies
    (and (force (vl-plainarglist-p plainargs))
         (force (vl-portlist-p ports))
         (force (same-lengthp plainargs ports)))
    (b* ((new-args (vl-add-portnames-to-plainargs plainargs ports)))
      (vl-plainarglist-p new-args)))
 :rule-classes :rewrite)