Build a 4v-sexpr with the update function upon a posedge.
(vl-nedgeflop-update-sexpr clks dat-prevs) → 4v-sexpr
We're dealing here with an always block such as:
always @(posedge clk0 or posedge clk1 or posedge clk2) if (clk0) q <= d0; else if (clk1) q <= d1; else q <= d2;
We're going to build the sexpr to assign to
(if clk0 data-prev0 (if clk1 data-prev1 data-prev2))
Function:
(defun vl-nedgeflop-update-sexpr (clks dat-prevs) (declare (xargs :guard (and (consp clks) (same-lengthp clks dat-prevs)))) (let ((__function__ 'vl-nedgeflop-update-sexpr)) (declare (ignorable __function__)) (b* (((cons clk1 rest-clks) clks) ((cons dat-prev1 rest-dat-prevs) dat-prevs) ((when (atom rest-clks)) dat-prev1)) (acl2::4vs-ite*-dumb clk1 dat-prev1 (vl-nedgeflop-update-sexpr rest-clks rest-dat-prevs)))))