		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-create

Signature
(vl-edgesynth-create target priority-edges data-exprs delay loc delta &key vecp) → new-delta
Arguments: target — Guard (vl-expr-p target).; priority-edges — Guard (vl-edgesynth-edgelist-p priority-edges).; data-exprs — Guard (vl-exprlist-p data-exprs).; delay — Guard (maybe-natp delay).; loc — Guard (vl-location-p loc).; delta — Guard (vl-delta-p delta).
Returns: new-delta — Type (vl-delta-p new-delta), given the guard.

Definitions and Theorems

Function: vl-edgesynth-create-fn

(defun vl-edgesynth-create-fn
       (target priority-edges
               data-exprs delay loc delta vecp)
 (declare
      (xargs :guard (and (vl-expr-p target)
                         (vl-edgesynth-edgelist-p priority-edges)
                         (vl-exprlist-p data-exprs)
                         (maybe-natp delay)
                         (vl-location-p loc)
                         (vl-delta-p delta))))
 (declare
      (xargs :guard (and (vl-idexpr-p target)
                         (posp (vl-expr->finalwidth target))
                         (same-lengthp priority-edges data-exprs)
                         (consp priority-edges))))
 (let ((__function__ 'vl-edgesynth-create))
  (declare (ignorable __function__))
  (b*
   ((width (vl-expr->finalwidth target))
    (name (vl-idexpr->name target))
    (nedges (len priority-edges))
    ((mv data-inputs delta)
     (vl-edgesynth-make-data-inputs
          width name data-exprs loc delta))
    ((mv clock-inputs delta)
     (vl-edgesynth-make-clock-inputs priority-edges loc delta))
    ((vl-delta delta) delta)
    (nf delta.nf)
    ((mv instname nf)
     (vl-namefactory-plain-name (cat name "_inst")
                                nf))
    ((when vecp)
     (b*
       ((addmods (vl-make-nedgeflop-vec width nedges (or delay 0)))
        (submod (car addmods))
        (inst (vl-simple-instantiate
                   submod instname
                   (cons target
                         (append data-inputs clock-inputs)))))
       (change-vl-delta delta
                        :nf nf
                        :modinsts (cons inst delta.modinsts)
                        :addmods (append addmods delta.addmods))))
    ((mv delfree-name nf)
     (vl-namefactory-plain-name (cat name "_delfree")
                                nf))
    ((mv delfree-expr delfree-decl)
     (vl-occform-mkwire delfree-name width
                        :loc loc))
    (addmods (vl-make-nedgeflop width nedges))
    (submod (car addmods))
    (inst
     (vl-simple-instantiate submod instname
                            (cons delfree-expr
                                  (append data-inputs clock-inputs))
                            :loc loc))
    (main-ass
         (make-vl-assign
              :lvalue target
              :expr delfree-expr
              :loc loc
              :delay (and delay
                          (let ((amt-expr (vl-make-index delay)))
                            (make-vl-gatedelay :rise amt-expr
                                               :fall amt-expr
                                               :high amt-expr))))))
   (change-vl-delta delta
                    :nf nf
                    :assigns (cons main-ass delta.assigns)
                    :vardecls (cons delfree-decl delta.vardecls)
                    :modinsts (cons inst delta.modinsts)
                    :addmods (append addmods delta.addmods)))))

Theorem: vl-delta-p-of-vl-edgesynth-create

(defthm vl-delta-p-of-vl-edgesynth-create
 (implies
   (and (force (vl-expr-p target))
        (force (vl-edgesynth-edgelist-p priority-edges))
        (force (vl-exprlist-p data-exprs))
        (force (acl2::maybe-natp$inline delay))
        (force (vl-location-p loc))
        (force (vl-delta-p delta))
        (force (vl-idexpr-p$inline target))
        (force (posp (vl-expr->finalwidth$inline target)))
        (force (same-lengthp priority-edges data-exprs))
        (force (consp priority-edges)))
   (b*
    ((new-delta
          (vl-edgesynth-create-fn target priority-edges
                                  data-exprs delay loc delta vecp)))
    (vl-delta-p new-delta)))
 :rule-classes :rewrite)