		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-shl-by-m-bits

Generate a module that shifts an N bit number left by an M bit number.

Signature
(vl-make-n-bit-shl-by-m-bits n m) → mods
Arguments: n — Guard (posp n).; m — Guard (posp m).
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_BY_M_BITS (out, a, b) ;
  output [n-1:0] out;
  input [n-1:0] a;
  input [m-1:0] b;
  assign out = a << b;
endmodule

Definitions and Theorems

Function: vl-make-n-bit-shl-by-m-bits

(defun vl-make-n-bit-shl-by-m-bits (n m)
 (declare (xargs :guard (and (posp n) (posp m))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-shl-by-m-bits))
  (declare (ignorable __function__))
  (b*
   ((n (lposfix n))
    (m (lposfix m))
    (name (hons-copy (cat "VL_" (natstr n)
                          "_BIT_SHL_BY_" (natstr m)
                          "_BITS")))
    ((mv out-expr
         out-port out-portdecl out-vardecl)
     (vl-occform-mkport "out" :vl-output n))
    ((mv a-expr a-port a-portdecl a-vardecl)
     (vl-occform-mkport "a" :vl-input n))
    ((mv b-expr b-port b-portdecl b-vardecl)
     (vl-occform-mkport "b" :vl-input m))
    (k (min (+ (integer-length n) 1) m))
    ((mv pshift-mods pshift-support)
     (vl-make-n-bit-shl-place-ps n k))
    (pshift-mods (reverse pshift-mods))
    (temp-vardecls
     (reverse
       (vl-make-list-of-netdecls k "temp" (vl-make-n-bit-range n))))
    (temp-exprs
         (vl-make-idexpr-list (vl-vardecllist->names temp-vardecls)
                              n :vl-unsigned))
    (last-temp (car (last temp-exprs)))
    ((cons xdet-mod xdet-support)
     (vl-make-n-bit-xdetect m))
    ((cons xeach-mod xeach-support)
     (vl-make-n-bit-xor-each n))
    (supporting-mods (list* xdet-mod xeach-mod
                            (append xdet-support xeach-support
                                    pshift-mods pshift-support)))
    ((mv bx-expr bx-vardecl)
     (vl-occform-mkwire "bx" 1))
    (bx-modinst (vl-simple-inst xdet-mod "mk_bx" bx-expr b-expr))
    (out-modinst
         (vl-simple-inst xeach-mod
                         "mk_out" out-expr bx-expr last-temp))
    (lhs-exprs (cons a-expr (butlast temp-exprs 1)))
    (b-wires (vl-make-list-of-bitselects b-expr 0 (- m 1)))
    ((when (eql m k))
     (b*
      ((pshift-insts
           (vl-make-modinsts-for-shl 1 pshift-mods
                                     temp-exprs lhs-exprs b-wires)))
      (cons
           (make-vl-module
                :name name
                :origname name
                :ports (list out-port a-port b-port)
                :portdecls (list out-portdecl a-portdecl b-portdecl)
                :vardecls (list* out-vardecl a-vardecl
                                 b-vardecl bx-vardecl temp-vardecls)
                :modinsts (append pshift-insts
                                  (list bx-modinst out-modinst))
                :minloc *vl-fakeloc*
                :maxloc *vl-fakeloc*)
           supporting-mods)))
    (diff (+ 1 (- m k)))
    ((cons merged-mod merged-support)
     (vl-make-n-bit-reduction-op :vl-unary-bitor diff))
    ((mv merged-expr merged-vardecl)
     (vl-primitive-mkwire "merged_high"))
    (high-bits
         (make-vl-nonatom :op :vl-partselect-colon
                          :args (list b-expr (vl-make-index (- m 1))
                                      (vl-make-index (- k 1)))
                          :finalwidth diff
                          :finaltype :vl-unsigned))
    (merged-inst
         (vl-simple-inst merged-mod
                         "merge_high" merged-expr high-bits))
    (lower-wires (take (- k 1) b-wires))
    (rhs-exprs (append lower-wires (list merged-expr)))
    (pshift-insts
         (vl-make-modinsts-for-shl 1 pshift-mods
                                   temp-exprs lhs-exprs rhs-exprs)))
   (list*
      (make-vl-module
           :name name
           :origname name
           :ports (list out-port a-port b-port)
           :portdecls (list out-portdecl a-portdecl b-portdecl)
           :vardecls (list* out-vardecl a-vardecl b-vardecl
                            bx-vardecl merged-vardecl temp-vardecls)
           :modinsts (cons merged-inst
                           (append pshift-insts
                                   (list bx-modinst out-modinst)))
           :minloc *vl-fakeloc*
           :maxloc *vl-fakeloc*)
      merged-mod
      (append merged-support supporting-mods)))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-shl-by-m-bits

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

Theorem: type-of-vl-make-n-bit-shl-by-m-bits

(defthm type-of-vl-make-n-bit-shl-by-m-bits
  (and (true-listp (vl-make-n-bit-shl-by-m-bits n m))
       (consp (vl-make-n-bit-shl-by-m-bits n m)))
  :rule-classes :type-prescription)

Theorem: vl-make-n-bit-shl-by-m-bits-of-pos-fix-n

(defthm vl-make-n-bit-shl-by-m-bits-of-pos-fix-n
  (equal (vl-make-n-bit-shl-by-m-bits (pos-fix n)
                                      m)
         (vl-make-n-bit-shl-by-m-bits n m)))

Theorem: vl-make-n-bit-shl-by-m-bits-pos-equiv-congruence-on-n

(defthm vl-make-n-bit-shl-by-m-bits-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (vl-make-n-bit-shl-by-m-bits n m)
                  (vl-make-n-bit-shl-by-m-bits n-equiv m)))
  :rule-classes :congruence)

Theorem: vl-make-n-bit-shl-by-m-bits-of-pos-fix-m

(defthm vl-make-n-bit-shl-by-m-bits-of-pos-fix-m
  (equal (vl-make-n-bit-shl-by-m-bits n (pos-fix m))
         (vl-make-n-bit-shl-by-m-bits n m)))

Theorem: vl-make-n-bit-shl-by-m-bits-pos-equiv-congruence-on-m

(defthm vl-make-n-bit-shl-by-m-bits-pos-equiv-congruence-on-m
  (implies (acl2::pos-equiv m m-equiv)
           (equal (vl-make-n-bit-shl-by-m-bits n m)
                  (vl-make-n-bit-shl-by-m-bits n m-equiv)))
  :rule-classes :congruence)