		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-nedgeflop-always

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

Signature
(vl-nedgeflop-always q-expr clk-exprs data-exprs) → always
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: always — Type (vl-always-p always), given the guard.

Definitions and Theorems

Function: vl-nedgeflop-always

(defun vl-nedgeflop-always (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-always))
    (declare (ignorable __function__))
    (b* ((evatoms (vl-nedgeflop-posedge-clks clk-exprs))
         (evctrl (make-vl-eventcontrol :starp nil
                                       :atoms evatoms))
         (body (vl-nedgeflop-ifstmt q-expr clk-exprs data-exprs))
         (stmt (make-vl-timingstmt :ctrl evctrl
                                   :body body)))
      (make-vl-always :type :vl-always
                      :stmt stmt
                      :loc *vl-fakeloc*))))

Theorem: vl-always-p-of-vl-nedgeflop-always

(defthm vl-always-p-of-vl-nedgeflop-always
 (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* ((always (vl-nedgeflop-always q-expr clk-exprs data-exprs)))
      (vl-always-p always)))
 :rule-classes :rewrite)