		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-nedgeflop-update-sexpr

Build a 4v-sexpr with the update function upon a posedge.

Signature
(vl-nedgeflop-update-sexpr clks dat-prevs) → 4v-sexpr
Arguments: clks — E wire names for the current clock values.; dat-prevs — E wires names for the previous data values.

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 q when a posedge has occurred. The goal, then, is to build an expression that is, e.g., in this example:

(if clk0
    data-prev0
  (if clk1
      data-prev1
    data-prev2))

Definitions and Theorems

Function: vl-nedgeflop-update-sexpr

(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)))))