		Search-engine friendly clone of the ACL2 documentation.

Argument-partitioning

Vl-partition-plainarg

Partition a plain argument into slices.

Signature
(vl-partition-plainarg arg port-width insts ss elem warnings) → (mv okp warnings plainargs)
Arguments: arg — An argument we need to replicate.
Guard (vl-plainarg-p arg).; port-width — Width of the port this argument is connected to.
Guard (posp port-width).; insts — Number of instances in this instance array.
Guard (posp insts).; ss — Guard (vl-scopestack-p ss).; elem — Context for warnings.
Guard (vl-modelement-p elem).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: okp — Type (booleanp okp).; warnings — Type (vl-warninglist-p warnings).; plainargs — Type (vl-plainarglist-p plainargs).

Our goal is to create a list of the insts-many plainargs which this port is to be partitioned into. On success, plainargs will be a list of insts arguments, each of which has width port-width. The arguments are in "msb-first" order, i.e., the "msb-most slice" of arg comes first.

We might fail with a fatal warning if there is some problem with the actual; we expect the actual to be already sized, well-typed, and sliceable), and its width must be compatible with the width of the port, as described in argument-partitioning.

Definitions and Theorems

Function: vl-partition-plainarg

(defun vl-partition-plainarg (arg port-width insts ss elem warnings)
 (declare (xargs :guard (and (vl-plainarg-p arg)
                             (posp port-width)
                             (posp insts)
                             (vl-scopestack-p ss)
                             (vl-modelement-p elem)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-partition-plainarg))
  (declare (ignorable __function__))
  (b*
   ((arg (vl-plainarg-fix arg))
    (port-width (lposfix port-width))
    (insts (lposfix insts))
    (ss (vl-scopestack-fix ss))
    (elem (vl-modelement-fix elem))
    (warnings (vl-warninglist-fix warnings))
    ((vl-plainarg arg) arg)
    ((unless arg.expr)
     (mv t (ok) (replicate insts arg)))
    (expr-width (vl-expr->finalwidth arg.expr))
    ((unless (posp expr-width))
     (mv
      nil
      (fatal
       :type :vl-bad-argument
       :msg
       "~a0: expected argument widths to be computed, but ~
                         found argument ~a1 without any width assigned."
       :args (list elem arg.expr))
      nil))
    ((when (eql expr-width port-width))
     (mv t (ok) (replicate insts arg)))
    ((unless (eql expr-width (* port-width insts)))
     (mv
      nil
      (fatal
       :type :vl-bad-argument
       :msg
       "~a0: argument ~a1 has width ~x2, which is not ~
                         compatible with this array instance.  (Since the ~
                         port has width ~x3, the only acceptable widths are ~
                         ~x3 and ~x4.)"
       :args (list elem arg.expr expr-width
                   port-width (* port-width insts)))
      nil))
    ((unless (vl-expr-sliceable-p arg.expr))
     (mv
      nil
      (fatal
           :type :vl-bad-argument
           :msg "~a0: trying to slice an unsliceable argument, ~a1."
           :args (list elem arg.expr))
      nil))
    ((unless (vl-expr-welltyped-p arg.expr))
     (mv
       nil
       (fatal :type :vl-bad-argument
              :msg "~a0: trying to slice up ill-typed argument ~a1."
              :args (list elem arg.expr))
       nil))
    ((mv successp warnings bits)
     (vl-msb-bitslice-expr arg.expr ss warnings))
    ((unless successp)
     (mv nil warnings nil))
    (partitions (vl-partition-msb-bitslices port-width bits))
    (plainargs (vl-exprlist-to-plainarglist partitions
                                            :dir arg.dir
                                            :atts arg.atts)))
   (mv t warnings plainargs))))

Theorem: booleanp-of-vl-partition-plainarg.okp

(defthm booleanp-of-vl-partition-plainarg.okp
  (b*
   (((mv ?okp ?warnings ?plainargs)
     (vl-partition-plainarg arg port-width insts ss elem warnings)))
   (booleanp okp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-partition-plainarg.warnings

(defthm vl-warninglist-p-of-vl-partition-plainarg.warnings
  (b*
   (((mv ?okp ?warnings ?plainargs)
     (vl-partition-plainarg arg port-width insts ss elem warnings)))
   (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-plainarglist-p-of-vl-partition-plainarg.plainargs

(defthm vl-plainarglist-p-of-vl-partition-plainarg.plainargs
  (b*
   (((mv ?okp ?warnings ?plainargs)
     (vl-partition-plainarg arg port-width insts ss elem warnings)))
   (vl-plainarglist-p plainargs))
  :rule-classes :rewrite)

Theorem: len-of-vl-partition-plainarg

(defthm len-of-vl-partition-plainarg
 (let
  ((ret
     (vl-partition-plainarg arg port-width insts ss elem warnings)))
  (implies (mv-nth 0 ret)
           (equal (len (mv-nth 2 ret))
                  (pos-fix insts)))))

Theorem: vl-partition-plainarg-of-vl-plainarg-fix-arg

(defthm vl-partition-plainarg-of-vl-plainarg-fix-arg
 (equal
     (vl-partition-plainarg (vl-plainarg-fix arg)
                            port-width insts ss elem warnings)
     (vl-partition-plainarg arg port-width insts ss elem warnings)))

Theorem: vl-partition-plainarg-vl-plainarg-equiv-congruence-on-arg

(defthm vl-partition-plainarg-vl-plainarg-equiv-congruence-on-arg
 (implies
  (vl-plainarg-equiv arg arg-equiv)
  (equal
       (vl-partition-plainarg arg port-width insts ss elem warnings)
       (vl-partition-plainarg arg-equiv
                              port-width insts ss elem warnings)))
 :rule-classes :congruence)

Theorem: vl-partition-plainarg-of-pos-fix-port-width

(defthm vl-partition-plainarg-of-pos-fix-port-width
 (equal
     (vl-partition-plainarg arg (pos-fix port-width)
                            insts ss elem warnings)
     (vl-partition-plainarg arg port-width insts ss elem warnings)))

Theorem: vl-partition-plainarg-pos-equiv-congruence-on-port-width

(defthm vl-partition-plainarg-pos-equiv-congruence-on-port-width
 (implies
  (acl2::pos-equiv port-width port-width-equiv)
  (equal
       (vl-partition-plainarg arg port-width insts ss elem warnings)
       (vl-partition-plainarg arg port-width-equiv
                              insts ss elem warnings)))
 :rule-classes :congruence)

Theorem: vl-partition-plainarg-of-pos-fix-insts

(defthm vl-partition-plainarg-of-pos-fix-insts
 (equal
     (vl-partition-plainarg arg port-width (pos-fix insts)
                            ss elem warnings)
     (vl-partition-plainarg arg port-width insts ss elem warnings)))

Theorem: vl-partition-plainarg-pos-equiv-congruence-on-insts

(defthm vl-partition-plainarg-pos-equiv-congruence-on-insts
 (implies
  (acl2::pos-equiv insts insts-equiv)
  (equal
       (vl-partition-plainarg arg port-width insts ss elem warnings)
       (vl-partition-plainarg arg port-width
                              insts-equiv ss elem warnings)))
 :rule-classes :congruence)

Theorem: vl-partition-plainarg-of-vl-scopestack-fix-ss

(defthm vl-partition-plainarg-of-vl-scopestack-fix-ss
 (equal
     (vl-partition-plainarg arg
                            port-width insts (vl-scopestack-fix ss)
                            elem warnings)
     (vl-partition-plainarg arg port-width insts ss elem warnings)))

Theorem: vl-partition-plainarg-vl-scopestack-equiv-congruence-on-ss

(defthm vl-partition-plainarg-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
       (vl-partition-plainarg arg port-width insts ss elem warnings)
       (vl-partition-plainarg arg port-width
                              insts ss-equiv elem warnings)))
 :rule-classes :congruence)

Theorem: vl-partition-plainarg-of-vl-modelement-fix-elem

(defthm vl-partition-plainarg-of-vl-modelement-fix-elem
 (equal
     (vl-partition-plainarg arg port-width
                            insts ss (vl-modelement-fix elem)
                            warnings)
     (vl-partition-plainarg arg port-width insts ss elem warnings)))

Theorem: vl-partition-plainarg-vl-modelement-equiv-congruence-on-elem

(defthm vl-partition-plainarg-vl-modelement-equiv-congruence-on-elem
 (implies
  (vl-modelement-equiv elem elem-equiv)
  (equal
       (vl-partition-plainarg arg port-width insts ss elem warnings)
       (vl-partition-plainarg arg port-width
                              insts ss elem-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-partition-plainarg-of-vl-warninglist-fix-warnings

(defthm vl-partition-plainarg-of-vl-warninglist-fix-warnings
 (equal
     (vl-partition-plainarg arg port-width insts
                            ss elem (vl-warninglist-fix warnings))
     (vl-partition-plainarg arg port-width insts ss elem warnings)))

Theorem: vl-partition-plainarg-vl-warninglist-equiv-congruence-on-warnings

(defthm
  vl-partition-plainarg-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
       (vl-partition-plainarg arg port-width insts ss elem warnings)
       (vl-partition-plainarg arg port-width
                              insts ss elem warnings-equiv)))
 :rule-classes :congruence)