Build a 4v-sexpr that captures when any clock has just had a posedge.
(vl-nedgeflop-some-edge-sexpr clks clk-prevs) → 4v-sexpr
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.
Function:
(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)))))