		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-nedgeflop-data-mux

Signature
(vl-nedgeflop-data-mux clks ds width) → x
Arguments: clks — Guard (vl-exprlist-p clks).; ds — Guard (vl-exprlist-p ds).; width — Guard (posp width).
Returns: x — Type (vl-expr-p x), given the guard.

Definitions and Theorems

Function: vl-nedgeflop-data-mux

(defun vl-nedgeflop-data-mux (clks ds width)
  (declare (xargs :guard (and (vl-exprlist-p clks)
                              (vl-exprlist-p ds)
                              (posp width))))
  (declare (xargs :guard (and (consp clks)
                              (eql (len clks) (len ds)))))
  (let ((__function__ 'vl-nedgeflop-data-mux))
    (declare (ignorable __function__))
    (if (atom (cdr clks))
        (car ds)
      (make-vl-nonatom :op :vl-qmark
                       :args (list (car clks)
                                   (car ds)
                                   (vl-nedgeflop-data-mux (cdr clks)
                                                          (cdr ds)
                                                          width))
                       :finalwidth width
                       :finaltype :vl-unsigned))))

Theorem: vl-expr-p-of-vl-nedgeflop-data-mux

(defthm vl-expr-p-of-vl-nedgeflop-data-mux
  (implies (and (vl-exprlist-p clks)
                (vl-exprlist-p ds)
                (posp width)
                (consp clks)
                (eql (len clks) (len ds)))
           (b* ((x (vl-nedgeflop-data-mux clks ds width)))
             (vl-expr-p x)))
  :rule-classes :rewrite)