		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-shl-place-p

Generate a module that conditionally shifts an N bit number by 2**(P-1) bits to the left.

Signature
(vl-make-n-bit-shl-place-p n p) → mods
Arguments: n — Guard (posp n).; p — Guard (posp p).
Returns: mods — A non-empty module list. The first module in the list is the desired module; the other modules are any necessary supporting modules.
Type (vl-modulelist-p mods).

We generate a gate-based module that is semantically equivalent to:

module VL_N_BIT_SHL_PLACE_P (out, in, shiftp) ;
  output [n-1:0] out;
  input [n-1:0] in;
  input shiftp;

  assign out = shiftp ? (in << 2**(p-1)) : in;

endmodule

These "place shifters" can be combined to form a full shifter that operates on O(log_2 n) muxes.

Definitions and Theorems

Function: vl-make-n-bit-shl-place-p

(defun vl-make-n-bit-shl-place-p (n p)
 (declare (xargs :guard (and (posp n) (posp p))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-shl-place-p))
  (declare (ignorable __function__))
  (b*
   ((n (lposfix n))
    (p (lposfix p))
    (shift-amount (expt 2 (- p 1)))
    (name (hons-copy (cat "VL_" (natstr n)
                          "_BIT_SHL_PLACE_" (natstr p))))
    ((mv out-expr
         out-port out-portdecl out-vardecl)
     (vl-occform-mkport "out" :vl-output n))
    ((mv in-expr in-port in-portdecl in-vardecl)
     (vl-occform-mkport "in" :vl-input n))
    ((mv shiftp-expr shiftp-port
         shiftp-portdecl shiftp-vardecl)
     (vl-primitive-mkport "shiftp" :vl-input))
    (places (min n shift-amount))
    (|places'b0|
       (make-vl-atom :guts (make-vl-constint :value 0
                                             :origwidth places
                                             :origtype :vl-unsigned)
                     :finalwidth places
                     :finaltype :vl-unsigned))
    (shifted-expr
     (if (<= n shift-amount)
         |places'b0|
      (make-vl-nonatom
           :op :vl-concat
           :args
           (list (make-vl-nonatom
                      :op :vl-partselect-colon
                      :args (list in-expr
                                  (vl-make-index (- n (+ 1 places)))
                                  (vl-make-index 0))
                      :finalwidth (- n places)
                      :finaltype :vl-unsigned)
                 |places'b0|)
           :finalwidth n
           :finaltype :vl-unsigned)))
    ((cons mux-mod mux-support)
     (vl-make-n-bit-mux n t))
    (mux-inst (vl-simple-inst mux-mod "mux" out-expr
                              shiftp-expr shifted-expr in-expr)))
   (list*
        (make-vl-module
             :name name
             :origname name
             :ports (list out-port in-port shiftp-port)
             :portdecls (list out-portdecl
                              in-portdecl shiftp-portdecl)
             :vardecls (list out-vardecl in-vardecl shiftp-vardecl)
             :modinsts (list mux-inst)
             :minloc *vl-fakeloc*
             :maxloc *vl-fakeloc*)
        mux-mod mux-support))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-shl-place-p

(defthm vl-modulelist-p-of-vl-make-n-bit-shl-place-p
  (b* ((mods (vl-make-n-bit-shl-place-p n p)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-n-bit-shl-place-p

(defthm type-of-vl-make-n-bit-shl-place-p
  (and (true-listp (vl-make-n-bit-shl-place-p n p))
       (consp (vl-make-n-bit-shl-place-p n p)))
  :rule-classes :type-prescription)

Theorem: vl-make-n-bit-shl-place-p-of-pos-fix-n

(defthm vl-make-n-bit-shl-place-p-of-pos-fix-n
  (equal (vl-make-n-bit-shl-place-p (pos-fix n)
                                    p)
         (vl-make-n-bit-shl-place-p n p)))

Theorem: vl-make-n-bit-shl-place-p-pos-equiv-congruence-on-n

(defthm vl-make-n-bit-shl-place-p-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (vl-make-n-bit-shl-place-p n p)
                  (vl-make-n-bit-shl-place-p n-equiv p)))
  :rule-classes :congruence)

Theorem: vl-make-n-bit-shl-place-p-of-pos-fix-p

(defthm vl-make-n-bit-shl-place-p-of-pos-fix-p
  (equal (vl-make-n-bit-shl-place-p n (pos-fix p))
         (vl-make-n-bit-shl-place-p n p)))

Theorem: vl-make-n-bit-shl-place-p-pos-equiv-congruence-on-p

(defthm vl-make-n-bit-shl-place-p-pos-equiv-congruence-on-p
  (implies (acl2::pos-equiv p p-equiv)
           (equal (vl-make-n-bit-shl-place-p n p)
                  (vl-make-n-bit-shl-place-p n p-equiv)))
  :rule-classes :congruence)