		Search-engine friendly clone of the ACL2 documentation.

Occform

vl-2-bit-dynamic-bitselect

Primitive dynamic bit-selection module.

VL_2_BIT_DYNAMIC_BITSELECT(out, in, idx) conservatively approximates out = in[idx] and is used to implement bit-selects where the index is not fixed. Its Verilog definition is as follows:

module VL_2_BIT_DYNAMIC_BITSELECT (out, in, idx) ;

   output out;
   input [1:0] in;
   input idx;

   wire idx_bar;
   wire idx_x;
   wire a;
   wire b;
   wire main;

   // Choose in[0] or in[1] based on idx

   not (idx_bar, idx);
   and (a, idx, in[1]) ;
   and (b, idx_bar, in[0]) ;
   or  (main, a, b) ;

   // Make sure we emit X if idx is X/Z

   xor (idx_x, idx, idx);
   xor (out, idx_x, main);

endmodule

The only place we this inexactly approximates the real Verilog semantics is when in contains Z's. In Verilog, such a Z can be selected and returned, but in our module X is returned instead. Actually this seems good -- our behavior probably more closely corresponds to what real hardware would do for a dynamic bit-select, anyway.

The XOR gates at the end are needed to obtain this X behavior. Without them, in cases where in[1] === in[0], we might return 0 or 1 even when idx is X. This wouldn't be okay: the Verilog specification mandates that if any bit of idx is X, then X is returned from the bit select.

Definition: *vl-2-bit-dynamic-bitselect*

(defconst *vl-2-bit-dynamic-bitselect*
 (b* ((name (hons-copy "VL_2_BIT_DYNAMIC_BITSELECT"))
      ((mv out-expr
           out-port out-portdecl out-vardecl)
       (vl-primitive-mkport "out" :vl-output))
      ((mv in-expr in-port in-portdecl in-vardecl)
       (vl-occform-mkport "in" :vl-input 2))
      ((mv idx-expr
           idx-port idx-portdecl idx-vardecl)
       (vl-primitive-mkport "idx" :vl-input))
      ((mv ~idx-expr ~idx-vardecl)
       (vl-primitive-mkwire "idx_bar"))
      ((mv idx_x-expr idx_x-vardecl)
       (vl-primitive-mkwire "idx_x"))
      ((mv a-expr a-vardecl)
       (vl-primitive-mkwire "a"))
      ((mv b-expr b-vardecl)
       (vl-primitive-mkwire "b"))
      ((mv main-expr main-vardecl)
       (vl-primitive-mkwire "main"))
      (in[0]-expr (vl-make-bitselect in-expr 0))
      (in[1]-expr (vl-make-bitselect in-expr 1))
      (~idx-inst (vl-simple-inst *vl-1-bit-not*
                                 "mk_idx_bar" ~idx-expr idx-expr))
      (a-inst (vl-simple-inst *vl-1-bit-and*
                              "mk_a" a-expr idx-expr in[1]-expr))
      (b-inst (vl-simple-inst *vl-1-bit-and*
                              "mk_b" b-expr ~idx-expr in[0]-expr))
      (main-inst (vl-simple-inst *vl-1-bit-or*
                                 "mk_main" main-expr a-expr b-expr))
      (idx_x-inst (vl-simple-inst *vl-1-bit-xor* "mk_idx_x"
                                  idx_x-expr idx-expr idx-expr))
      (out-inst (vl-simple-inst *vl-1-bit-xor* "mk_out"
                                out-expr idx_x-expr main-expr)))
   (hons-copy
        (make-vl-module
             :name name
             :origname name
             :ports (list out-port in-port idx-port)
             :portdecls (list out-portdecl in-portdecl idx-portdecl)
             :vardecls (list out-vardecl in-vardecl
                             idx-vardecl ~idx-vardecl a-vardecl
                             b-vardecl main-vardecl idx_x-vardecl)
             :modinsts (list ~idx-inst a-inst
                             b-inst main-inst idx_x-inst out-inst)
             :minloc *vl-fakeloc*
             :maxloc *vl-fakeloc*))))