		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-dynamic-bitselect-m

Generate a dynamic bit-selection module for an N bit wire and an M bit select.

Signature
(vl-make-n-bit-dynamic-bitselect-m 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 produce VL_N_BIT_DYNAMIC_BITSELECT_M(out, in, idx), a conservative approximation of out = in[idx] where in has width N and idx has width M.

Prerequisite: see vl-make-n-bit-dynamic-bitselect, which can be used to introduce a module VL_N_BIT_DYNAMIC_BITSELECT(out, in, idx), where in has width N and idx has width W where W is the the smallest number W such that N <= 2^W.

The problem with just using VL_N_BIT_DYNAMIC_BITSELECT directly to synthesize expressions of the form in[idx] is that, in practice, the width of idx may be smaller or larger than W. When smaller, we need to pad it with zeros. When larger, we need to do additional out-of-bounds checking.

Definitions and Theorems

Function: vl-make-n-bit-dynamic-bitselect-m

(defun vl-make-n-bit-dynamic-bitselect-m (n m)
 (declare (xargs :guard (and (posp n) (posp m))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-dynamic-bitselect-m))
  (declare (ignorable __function__))
  (b*
   ((n (lposfix n))
    (m (lposfix m))
    (coremods (vl-make-n-bit-dynamic-bitselect n))
    (coremod (car coremods))
    (k
      (b*
        ((portdecls (vl-module->portdecls coremod))
         (idx (vl-find-portdecl "idx" portdecls))
         ((unless idx)
          (raise "coremod has no index port?")
          m)
         (type (vl-portdecl->type idx))
         ((unless (eq (vl-datatype-kind type)
                      :vl-coretype))
          (raise "coremod port isn't a coretype?")
          m)
         ((vl-coretype type))
         ((unless (and (atom type.udims)
                       (or (atom type.pdims)
                           (and (atom (cdr type.pdims))
                                (not (eq (car type.pdims)
                                         :vl-unsized-dimension))))))
          (raise "coremod index unexpected array dims")
          m)
         (range (and (consp type.pdims)
                     (car type.pdims)))
         ((unless (vl-maybe-range-resolved-p range))
          (raise "coremod index range not resolved?")
          m))
        (vl-maybe-range-size range)))
    ((when (eql k m)) coremods)
    (name (cat "VL_" (natstr n)
               "_BIT_DYNAMIC_BITSELECT_" (natstr m)))
    ((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 n))
    ((mv idx-expr
         idx-port idx-portdecl idx-vardecl)
     (vl-occform-mkport "idx" :vl-input m))
    ((when (< k m))
     (b*
      ((lowbits (vl-make-partselect idx-expr (- k 1) 0))
       (highbits (vl-make-partselect idx-expr (- m 1) k))
       ((mv main-expr main-vardecl)
        (vl-primitive-mkwire "main"))
       (core-inst (vl-simple-inst (car coremods)
                                  "core" main-expr in-expr lowbits))
       ((cons extra-mod extra-support)
        (vl-make-n-bit-reduction-op :vl-unary-bitor (- m k)))
       ((mv extra-expr extra-vardecl)
        (vl-primitive-mkwire "any_extra"))
       (extra-inst
            (vl-simple-inst extra-mod
                            "mk_any_extra" extra-expr highbits))
       ((mv noextra-expr noextra-vardecl)
        (vl-primitive-mkwire "no_extra"))
       ((mv a-expr a-vardecl)
        (vl-primitive-mkwire "a"))
       ((mv b-expr b-vardecl)
        (vl-primitive-mkwire "b"))
       (noextra-inst
            (vl-simple-inst *vl-1-bit-not*
                            "mk_no_extra" noextra-expr extra-expr))
       (a-inst
            (vl-simple-inst *vl-1-bit-and*
                            "mk_a" a-expr noextra-expr main-expr))
       (b-inst (vl-simple-inst *vl-1-bit-and* "mk_b"
                               b-expr extra-expr |*sized-1'bx*|))
       (out-inst (vl-simple-inst *vl-1-bit-or*
                                 "mk_out" out-expr a-expr b-expr))
       (mod
        (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 main-vardecl extra-vardecl
                             noextra-vardecl a-vardecl b-vardecl)
             :modinsts (list core-inst extra-inst
                             noextra-inst a-inst b-inst out-inst)
             :minloc *vl-fakeloc*
             :maxloc *vl-fakeloc*)))
      (list* mod extra-mod
             (append coremods extra-support))))
    (padsize (- k m))
    (pad-expr
       (make-vl-atom :guts (make-vl-constint :value 0
                                             :origwidth padsize
                                             :origtype :vl-unsigned)
                     :finalwidth padsize
                     :finaltype :vl-unsigned))
    (padded-idx (make-vl-nonatom :op :vl-concat
                                 :args (list pad-expr idx-expr)
                                 :finalwidth k
                                 :finaltype :vl-unsigned))
    (core-inst (vl-simple-inst (car coremods)
                               "core" out-expr in-expr padded-idx)))
   (list*
        (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)
             :modinsts (list core-inst)
             :minloc *vl-fakeloc*
             :maxloc *vl-fakeloc*)
        *vl-1-bit-not* *vl-1-bit-and*
        *vl-1-bit-or* coremods))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-dynamic-bitselect-m

(defthm vl-modulelist-p-of-vl-make-n-bit-dynamic-bitselect-m
  (b* ((mods (vl-make-n-bit-dynamic-bitselect-m n m)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-n-bit-dynamic-bitselect-m

(defthm type-of-vl-make-n-bit-dynamic-bitselect-m
  (and (true-listp (vl-make-n-bit-dynamic-bitselect-m n m))
       (consp (vl-make-n-bit-dynamic-bitselect-m n m)))
  :rule-classes :type-prescription)

Theorem: vl-make-n-bit-dynamic-bitselect-m-of-pos-fix-n

(defthm vl-make-n-bit-dynamic-bitselect-m-of-pos-fix-n
  (equal (vl-make-n-bit-dynamic-bitselect-m (pos-fix n)
                                            m)
         (vl-make-n-bit-dynamic-bitselect-m n m)))

Theorem: vl-make-n-bit-dynamic-bitselect-m-pos-equiv-congruence-on-n

(defthm vl-make-n-bit-dynamic-bitselect-m-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (vl-make-n-bit-dynamic-bitselect-m n m)
                  (vl-make-n-bit-dynamic-bitselect-m n-equiv m)))
  :rule-classes :congruence)

Theorem: vl-make-n-bit-dynamic-bitselect-m-of-pos-fix-m

(defthm vl-make-n-bit-dynamic-bitselect-m-of-pos-fix-m
  (equal (vl-make-n-bit-dynamic-bitselect-m n (pos-fix m))
         (vl-make-n-bit-dynamic-bitselect-m n m)))

Theorem: vl-make-n-bit-dynamic-bitselect-m-pos-equiv-congruence-on-m

(defthm vl-make-n-bit-dynamic-bitselect-m-pos-equiv-congruence-on-m
  (implies (acl2::pos-equiv m m-equiv)
           (equal (vl-make-n-bit-dynamic-bitselect-m n m)
                  (vl-make-n-bit-dynamic-bitselect-m n m-equiv)))
  :rule-classes :congruence)