		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-make-clock-inputs

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

Signature
(vl-edgesynth-make-clock-inputs edges loc delta) → (mv clk-exprs delta)
Arguments: edges — Priority-ordered edges, may be posedge/negedges.
Guard (vl-edgesynth-edgelist-p edges).; loc — Location for new module elements.
Guard (vl-location-p loc).; delta — Delta we're extending.
Guard (vl-delta-p delta).
Returns: clk-exprs — New clock expressions in priority order.
Type (vl-exprlist-p clk-exprs), given the guard.; delta — Extended delta.
Type (vl-delta-p delta), given the guard.

Our primitive n-edge-flop modules are all posedge driven. This is where we convert any negedge signals into posedge signals.

Definitions and Theorems

Function: vl-edgesynth-make-clock-inputs

(defun vl-edgesynth-make-clock-inputs (edges loc delta)
 (declare (xargs :guard (and (vl-edgesynth-edgelist-p edges)
                             (vl-location-p loc)
                             (vl-delta-p delta))))
 (let ((__function__ 'vl-edgesynth-make-clock-inputs))
  (declare (ignorable __function__))
  (b*
   (((when (atom edges)) (mv nil delta))
    ((mv rest delta)
     (vl-edgesynth-make-clock-inputs (cdr edges)
                                     loc delta))
    (expr (vl-edgesynth-edge->expr (car edges)))
    (posedgep (vl-edgesynth-edge->posedgep (car edges)))
    ((when posedgep)
     (mv (cons expr rest) delta))
    ((vl-delta delta) delta)
    (name (vl-idexpr->name expr))
    ((mv temp-name nf)
     (vl-namefactory-plain-name (cat name "_bar")
                                delta.nf))
    ((mv temp-expr temp-decl)
     (vl-occform-mkwire temp-name 1
                        :loc loc))
    (~expr (make-vl-nonatom :op :vl-unary-bitnot
                            :args (list expr)
                            :finalwidth 1
                            :finaltype (vl-expr->finaltype expr)))
    (temp-assign (make-vl-assign :lvalue temp-expr
                                 :expr ~expr
                                 :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-clock-inputs.clk-exprs

(defthm vl-exprlist-p-of-vl-edgesynth-make-clock-inputs.clk-exprs
  (implies (and (vl-edgesynth-edgelist-p edges)
                (vl-location-p loc)
                (vl-delta-p delta))
           (b* (((mv ?clk-exprs ?delta)
                 (vl-edgesynth-make-clock-inputs edges loc delta)))
             (vl-exprlist-p clk-exprs)))
  :rule-classes :rewrite)

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

(defthm vl-delta-p-of-vl-edgesynth-make-clock-inputs.delta
  (implies (and (vl-edgesynth-edgelist-p edges)
                (vl-location-p loc)
                (vl-delta-p delta))
           (b* (((mv ?clk-exprs ?delta)
                 (vl-edgesynth-make-clock-inputs edges loc delta)))
             (vl-delta-p delta)))
  :rule-classes :rewrite)

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

(defthm vl-edgesynth-make-clock-inputs-mvtypes-0
  (true-listp
       (mv-nth 0
               (vl-edgesynth-make-clock-inputs edges loc delta)))
  :rule-classes :type-prescription)