		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-nedgeflop-ifstmt

Build the Verilog if-statement for a primitive n-edge flop.

Signature
(vl-nedgeflop-ifstmt q-expr clk-exprs data-exprs) → guts
Arguments: q-expr — e.g., q.
Guard (vl-expr-p q-expr).; clk-exprs — e.g., (clk0 clk1 clk2).
Guard (vl-exprlist-p clk-exprs).; data-exprs — e.g., (d0 d1 d2).
Guard (vl-exprlist-p data-exprs).
Returns: guts — e.g., if (clk0) q <= d0; else if (clk1) q <= d1; else q <= d2;.
Type (vl-stmt-p guts), given the guard.

Definitions and Theorems

Function: vl-nedgeflop-ifstmt

(defun vl-nedgeflop-ifstmt (q-expr clk-exprs data-exprs)
  (declare (xargs :guard (and (vl-expr-p q-expr)
                              (vl-exprlist-p clk-exprs)
                              (vl-exprlist-p data-exprs))))
  (declare (xargs :guard (and (consp clk-exprs)
                              (same-lengthp clk-exprs data-exprs))))
  (let ((__function__ 'vl-nedgeflop-ifstmt))
    (declare (ignorable __function__))
    (b* (((when (atom clk-exprs))
          (impossible)
          (make-vl-nullstmt))
         (assign1 (make-vl-assignstmt :type :vl-nonblocking
                                      :lvalue q-expr
                                      :expr (car data-exprs)
                                      :loc *vl-fakeloc*))
         ((when (atom (cdr clk-exprs))) assign1))
      (make-vl-ifstmt
           :condition (car clk-exprs)
           :truebranch assign1
           :falsebranch (vl-nedgeflop-ifstmt q-expr (cdr clk-exprs)
                                             (cdr data-exprs))))))

Theorem: vl-stmt-p-of-vl-nedgeflop-ifstmt

(defthm vl-stmt-p-of-vl-nedgeflop-ifstmt
 (implies
      (and (force (vl-expr-p q-expr))
           (force (vl-exprlist-p clk-exprs))
           (force (vl-exprlist-p data-exprs))
           (force (consp clk-exprs))
           (force (same-lengthp clk-exprs data-exprs)))
      (b* ((guts (vl-nedgeflop-ifstmt q-expr clk-exprs data-exprs)))
        (vl-stmt-p guts)))
 :rule-classes :rewrite)