		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-nedgeflop-some-edge-sexpr

Build a 4v-sexpr that captures when any clock has just had a posedge.

Signature
(vl-nedgeflop-some-edge-sexpr clks clk-prevs) → 4v-sexpr
Arguments: clks — E wire names for current clock values.; clk-prevs — E wire names for previous clock values.

The idea here is to build an expression like:

(or (and clk1 (not clk1-prev))  ;; first clk had a posedge
    (and clk2 (not clk2-prev))  ;; second clk had a posedge
    ...)

This is the expression that will trigger an update of the flop.

Definitions and Theorems

Function: vl-nedgeflop-some-edge-sexpr

(defun vl-nedgeflop-some-edge-sexpr (clks clk-prevs)
 (declare (xargs :guard (and (consp clks)
                             (same-lengthp clks clk-prevs))))
 (let ((__function__ 'vl-nedgeflop-some-edge-sexpr))
  (declare (ignorable __function__))
  (b* (((cons clk1 rest-clks) clks)
       ((cons clk1-prev rest-clk-prevs)
        clk-prevs)
       (edge1 (acl2::4vs-and clk1 (acl2::4vs-not clk1-prev)))
       ((when (atom rest-clks)) edge1))
    (acl2::4vs-or
         edge1
         (vl-nedgeflop-some-edge-sexpr rest-clks rest-clk-prevs)))))