		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-make-nedgeflop-insts

Signature
(vl-make-nedgeflop-insts primitive q-expr d-exprs clk-exprs n) → insts
Arguments: primitive — Guard (vl-module-p primitive).; q-expr — Guard (vl-expr-p q-expr).; d-exprs — Guard (vl-exprlist-p d-exprs).; clk-exprs — Guard (vl-exprlist-p clk-exprs).; n — Initially width.
Guard (natp n).
Returns: insts — Type (vl-modinstlist-p insts), given the guard.

Definitions and Theorems

Function: vl-make-nedgeflop-insts

(defun vl-make-nedgeflop-insts
       (primitive q-expr d-exprs clk-exprs n)
 (declare (xargs :guard (and (vl-module-p primitive)
                             (vl-expr-p q-expr)
                             (vl-exprlist-p d-exprs)
                             (vl-exprlist-p clk-exprs)
                             (natp n))))
 (declare (xargs :guard (same-lengthp d-exprs clk-exprs)))
 (let ((__function__ 'vl-make-nedgeflop-insts))
   (declare (ignorable __function__))
   (b* (((when (zp n)) nil)
        (n (- n 1))
        (q-bit (vl-make-bitselect q-expr n))
        (d-bits (vl-make-same-bitselect-from-each d-exprs n))
        (args (cons q-bit (append d-bits clk-exprs))))
     (cons (vl-simple-instantiate primitive
                                  (hons-copy (cat "bit" (natstr n)))
                                  args)
           (vl-make-nedgeflop-insts primitive
                                    q-expr d-exprs clk-exprs n)))))

Theorem: vl-modinstlist-p-of-vl-make-nedgeflop-insts

(defthm vl-modinstlist-p-of-vl-make-nedgeflop-insts
  (implies (and (force (vl-module-p primitive))
                (force (vl-expr-p q-expr))
                (force (vl-exprlist-p d-exprs))
                (force (vl-exprlist-p clk-exprs))
                (force (natp n))
                (force (same-lengthp d-exprs clk-exprs)))
           (b* ((insts (vl-make-nedgeflop-insts
                            primitive q-expr d-exprs clk-exprs n)))
             (vl-modinstlist-p insts)))
  :rule-classes :rewrite)