		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-nedgeflop-posedge-clks

Build the Verilog sensitivity list for a primitive n-edge flop.

Signature
(vl-nedgeflop-posedge-clks clk-exprs) → evatoms
Arguments: clk-exprs — e.g., (clk0 clk1 clk2).
Guard (vl-exprlist-p clk-exprs).
Returns: evatoms — e.g., posedge clk0 or posedge clk1 or posedge clk2.
Type (vl-evatomlist-p evatoms), given the guard.

Definitions and Theorems

Function: vl-nedgeflop-posedge-clks

(defun vl-nedgeflop-posedge-clks (clk-exprs)
  (declare (xargs :guard (vl-exprlist-p clk-exprs)))
  (let ((__function__ 'vl-nedgeflop-posedge-clks))
    (declare (ignorable __function__))
    (if (atom clk-exprs)
        nil
      (cons (make-vl-evatom :type :vl-posedge
                            :expr (car clk-exprs))
            (vl-nedgeflop-posedge-clks (cdr clk-exprs))))))

Theorem: vl-evatomlist-p-of-vl-nedgeflop-posedge-clks

(defthm vl-evatomlist-p-of-vl-nedgeflop-posedge-clks
  (implies (and (force (vl-exprlist-p clk-exprs)))
           (b* ((evatoms (vl-nedgeflop-posedge-clks clk-exprs)))
             (vl-evatomlist-p evatoms)))
  :rule-classes :rewrite)