		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-make-data-inputs

Create (if necessary) temporary wires for the data inputs.

Signature
(vl-edgesynth-make-data-inputs width target-name data-exprs loc delta) → (mv din-exprs delta)
Arguments: width — Width of the register.
Guard (posp width).; target-name — Name of the target register, for more useful name generation.
Guard (stringp target-name).; data-exprs — Right-hand side expressions for data inputs.
Guard (vl-exprlist-p data-exprs).; loc — Location for new module elements.
Guard (vl-location-p loc).; delta — A delta we're extending, for assignments, new nets, etc.
Guard (vl-delta-p delta).
Returns: din-exprs — The new expressions to use as the data inputs.
Type (vl-exprlist-p din-exprs), given the guard.; delta — Updated delta with any additional stuff.
Type (vl-delta-p delta), given the guard.

Definitions and Theorems

Function: vl-edgesynth-make-data-inputs

(defun vl-edgesynth-make-data-inputs
       (width target-name data-exprs loc delta)
 (declare (xargs :guard (and (posp width)
                             (stringp target-name)
                             (vl-exprlist-p data-exprs)
                             (vl-location-p loc)
                             (vl-delta-p delta))))
 (let ((__function__ 'vl-edgesynth-make-data-inputs))
  (declare (ignorable __function__))
  (b*
   (((when (atom data-exprs))
     (mv nil delta))
    ((mv rest delta)
     (vl-edgesynth-make-data-inputs
          width target-name (cdr data-exprs)
          loc delta))
    ((when (equal (vl-expr->finalwidth (car data-exprs))
                  width))
     (mv (cons (car data-exprs) rest) delta))
    ((vl-delta delta) delta)
    (nf delta.nf)
    ((mv temp-name nf)
     (vl-namefactory-indexed-name (cat target-name "_din")
                                  nf))
    ((mv temp-expr temp-decl)
     (vl-occform-mkwire temp-name width
                        :loc loc))
    (temp-assign (make-vl-assign :lvalue temp-expr
                                 :expr (car data-exprs)
                                 :loc loc))
    (delta
       (change-vl-delta delta
                        :nf nf
                        :vardecls (cons temp-decl delta.vardecls)
                        :assigns (cons temp-assign delta.assigns))))
   (mv (cons temp-expr rest) delta))))

Theorem: vl-exprlist-p-of-vl-edgesynth-make-data-inputs.din-exprs

(defthm vl-exprlist-p-of-vl-edgesynth-make-data-inputs.din-exprs
  (implies (and (posp width)
                (stringp target-name)
                (vl-exprlist-p data-exprs)
                (vl-location-p loc)
                (vl-delta-p delta))
           (b* (((mv ?din-exprs ?delta)
                 (vl-edgesynth-make-data-inputs
                      width
                      target-name data-exprs loc delta)))
             (vl-exprlist-p din-exprs)))
  :rule-classes :rewrite)

Theorem: vl-delta-p-of-vl-edgesynth-make-data-inputs.delta

(defthm vl-delta-p-of-vl-edgesynth-make-data-inputs.delta
  (implies (and (posp width)
                (stringp target-name)
                (vl-exprlist-p data-exprs)
                (vl-location-p loc)
                (vl-delta-p delta))
           (b* (((mv ?din-exprs ?delta)
                 (vl-edgesynth-make-data-inputs
                      width
                      target-name data-exprs loc delta)))
             (vl-delta-p delta)))
  :rule-classes :rewrite)

Theorem: vl-edgesynth-make-data-inputs-mvtypes-0

(defthm vl-edgesynth-make-data-inputs-mvtypes-0
  (true-listp (mv-nth 0
                      (vl-edgesynth-make-data-inputs
                           width
                           target-name data-exprs loc delta)))
  :rule-classes :type-prescription)