• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
        • Expression-sizing
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
        • Caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
        • Replicate-insts
          • Vl-replicated-instnames
          • Vl-modulelist-replicate
          • Argument-partitioning
            • Vl-partition-plainarg
            • Vl-partition-msb-bitslices
            • Vl-partition-plainarglist
            • Vl-reorient-partitioned-args
            • Vl-assemble-gateinsts
            • Vl-plainarglists-to-arguments
          • Vl-replicate-gateinst
          • Vl-replicate-gateinstlist
          • Vl-module-port-widths
          • Vl-replicate-modinst
          • Vl-replicate-arguments
          • Vl-replicate-orig-instnames
          • Vl-assemble-modinsts
          • Vl-module-replicate
          • Vl-replicate-modinstlist
          • Vl-modinst-origname/idx
          • Vl-modinst-origname
          • Vl-gateinst-origname/idx
          • Vl-gateinst-origname
          • Vl-gateinst-origidx
          • Vl-modinst-origidx
          • Vl-design-replicate
          • Vl-some-modinst-array-p
          • Vl-some-gateinst-array-p
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Argument-partitioning

Vl-partition-plainarglist

Extend vl-partition-plainarg across a list of arguments.

Signature

(vl-partition-plainarglist args port-widths insts ss elem warnings) 
  → 
(mv successp warnings plainarglists)

Arguments

args — Arguments to some submodule.
    Guard (vl-plainarglist-p args).

port-widths — Corresponding widths of the submodule's ports.
    Guard (pos-listp port-widths).

insts — How many instances there are.
    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

successp — Type (booleanp successp).

warnings — Type (vl-warninglist-p warnings).

plainarglists — Type (vl-plainarglistlist-p plainarglists).

Supposing that args has length N, the result we return on success is a list of N plainarglists (one for each argument), and each of these lists has insts-many plainargs. That is, each element of the result is the partitioning of the corresponding argument.

Definitions and Theorems

Function: vl-partition-plainarglist

(defun vl-partition-plainarglist
       (args port-widths insts ss elem warnings)
  (declare (xargs :guard (and (vl-plainarglist-p args)
                              (pos-listp port-widths)
                              (posp insts)
                              (vl-scopestack-p ss)
                              (vl-modelement-p elem)
                              (vl-warninglist-p warnings))))
  (declare (xargs :guard (same-lengthp args port-widths)))
  (let ((__function__ 'vl-partition-plainarglist))
    (declare (ignorable __function__))
    (b* (((when (atom args)) (mv t (ok) nil))
         ((mv successp warnings car-result)
          (vl-partition-plainarg (car args)
                                 (car port-widths)
                                 insts ss elem warnings))
         ((unless successp)
          (mv nil warnings nil))
         ((mv successp warnings cdr-result)
          (vl-partition-plainarglist (cdr args)
                                     (cdr port-widths)
                                     insts ss elem warnings))
         ((unless successp)
          (mv nil warnings nil)))
      (mv t warnings
          (cons car-result cdr-result)))))

Theorem: booleanp-of-vl-partition-plainarglist.successp

(defthm booleanp-of-vl-partition-plainarglist.successp
 (b*
  (((mv ?successp ?warnings ?plainarglists)
    (vl-partition-plainarglist args
                               port-widths insts ss elem warnings)))
  (booleanp successp))
 :rule-classes :type-prescription)

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

(defthm vl-warninglist-p-of-vl-partition-plainarglist.warnings
 (b*
  (((mv ?successp ?warnings ?plainarglists)
    (vl-partition-plainarglist args
                               port-widths insts ss elem warnings)))
  (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-plainarglistlist-p-of-vl-partition-plainarglist.plainarglists

(defthm
   vl-plainarglistlist-p-of-vl-partition-plainarglist.plainarglists
 (b*
  (((mv ?successp ?warnings ?plainarglists)
    (vl-partition-plainarglist args
                               port-widths insts ss elem warnings)))
  (vl-plainarglistlist-p plainarglists))
 :rule-classes :rewrite)

Theorem: vl-partition-plainarglist-mvtypes-0

(defthm vl-partition-plainarglist-mvtypes-0
 (booleanp
  (mv-nth
    0
    (vl-partition-plainarglist args
                               port-widths insts ss elem warnings)))
 :rule-classes :type-prescription)

Theorem: vl-partition-plainarglist-mvtypes-2

(defthm vl-partition-plainarglist-mvtypes-2
 (true-listp
  (mv-nth
    2
    (vl-partition-plainarglist args
                               port-widths insts ss elem warnings)))
 :rule-classes :type-prescription)

Theorem: all-have-len-of-vl-partition-plainarglist

(defthm all-have-len-of-vl-partition-plainarglist
 (let
  ((ret
    (vl-partition-plainarglist args
                               port-widths insts ss elem warnings)))
  (implies (and (mv-nth 0 ret)
                (equal len (pos-fix insts)))
           (all-have-len (mv-nth 2 ret) len))))

Theorem: vl-partition-plainarglist-of-vl-plainarglist-fix-args

(defthm vl-partition-plainarglist-of-vl-plainarglist-fix-args
 (equal
    (vl-partition-plainarglist (vl-plainarglist-fix args)
                               port-widths insts ss elem warnings)
    (vl-partition-plainarglist args
                               port-widths insts ss elem warnings)))

Theorem: vl-partition-plainarglist-vl-plainarglist-equiv-congruence-on-args

(defthm
 vl-partition-plainarglist-vl-plainarglist-equiv-congruence-on-args
 (implies
  (vl-plainarglist-equiv args args-equiv)
  (equal
    (vl-partition-plainarglist
         args port-widths insts ss elem warnings)
    (vl-partition-plainarglist args-equiv
                               port-widths insts ss elem warnings)))
 :rule-classes :congruence)

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

(defthm vl-partition-plainarglist-of-pos-fix-insts
 (equal
    (vl-partition-plainarglist args port-widths (pos-fix insts)
                               ss elem warnings)
    (vl-partition-plainarglist args
                               port-widths insts ss elem warnings)))

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

(defthm vl-partition-plainarglist-pos-equiv-congruence-on-insts
 (implies
   (acl2::pos-equiv insts insts-equiv)
   (equal (vl-partition-plainarglist
               args port-widths insts ss elem warnings)
          (vl-partition-plainarglist args port-widths
                                     insts-equiv ss elem warnings)))
 :rule-classes :congruence)

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

(defthm vl-partition-plainarglist-of-vl-scopestack-fix-ss
 (equal
    (vl-partition-plainarglist
         args
         port-widths insts (vl-scopestack-fix ss)
         elem warnings)
    (vl-partition-plainarglist args
                               port-widths insts ss elem warnings)))

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

(defthm
     vl-partition-plainarglist-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal (vl-partition-plainarglist
               args port-widths insts ss elem warnings)
          (vl-partition-plainarglist args port-widths
                                     insts ss-equiv elem warnings)))
 :rule-classes :congruence)

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

(defthm vl-partition-plainarglist-of-vl-modelement-fix-elem
 (equal
    (vl-partition-plainarglist args port-widths
                               insts ss (vl-modelement-fix elem)
                               warnings)
    (vl-partition-plainarglist args
                               port-widths insts ss elem warnings)))

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

(defthm
   vl-partition-plainarglist-vl-modelement-equiv-congruence-on-elem
 (implies
   (vl-modelement-equiv elem elem-equiv)
   (equal (vl-partition-plainarglist
               args port-widths insts ss elem warnings)
          (vl-partition-plainarglist args port-widths
                                     insts ss elem-equiv warnings)))
 :rule-classes :congruence)

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

(defthm vl-partition-plainarglist-of-vl-warninglist-fix-warnings
 (equal
   (vl-partition-plainarglist args port-widths insts
                              ss elem (vl-warninglist-fix warnings))
   (vl-partition-plainarglist args
                              port-widths insts ss elem warnings)))

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

(defthm
 vl-partition-plainarglist-vl-warninglist-equiv-congruence-on-warnings
 (implies
   (vl-warninglist-equiv warnings warnings-equiv)
   (equal (vl-partition-plainarglist
               args port-widths insts ss elem warnings)
          (vl-partition-plainarglist args port-widths
                                     insts ss elem warnings-equiv)))
 :rule-classes :congruence)