• 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
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
          • Vl-vardecllist-reset-atts
          • Vl-inline-rename-portdecls
          • Vl-inline-mod-in-mods-aux
          • Vl-inline-mod-in-modinst
          • Vl-inline-mod-in-modinsts
          • Vl-make-inlining-assigns
          • Vl-inline-mod-in-mod
          • Vl-inline-mods
          • Vl-ok-to-inline-list-p
          • Vl-ok-to-inline-p
          • Vl-inline-rename-portdecl
          • Vl-design-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

• Inline-mods

Vl-inline-mod-in-modinsts

Replace any instance of a module with its inlined body.

Signature

(vl-inline-mod-in-modinsts sub x nf warnings) 
  → 
(mv nf modinsts gateinsts assigns vardecls warnings)

Arguments

sub — Guard (and (vl-module-p sub) (vl-ok-to-inline-p sub)).

x — Guard (vl-modinstlist-p x).

nf — Guard (vl-namefactory-p nf).

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

Returns

nf — Type (vl-namefactory-p nf), given the guard.

modinsts — Type (vl-modinstlist-p modinsts), given the guard.

gateinsts — Type (vl-gateinstlist-p gateinsts), given the guard.

assigns — Type (vl-assignlist-p assigns), given the guard.

vardecls — Type (vl-vardecllist-p vardecls), given the guard.

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

Definitions and Theorems

Function: vl-inline-mod-in-modinsts

(defun vl-inline-mod-in-modinsts (sub x nf warnings)
  (declare (xargs :guard (and (and (vl-module-p sub)
                                   (vl-ok-to-inline-p sub))
                              (vl-modinstlist-p x)
                              (vl-namefactory-p nf)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-inline-mod-in-modinsts))
    (declare (ignorable __function__))
    (b* (((when (atom x))
          (mv nf nil nil nil nil (ok)))
         ((mv nf modinsts1
              gateinsts1 assigns1 vardecls1 warnings)
          (vl-inline-mod-in-modinst sub (car x)
                                    nf warnings))
         ((mv nf modinsts2
              gateinsts2 assigns2 vardecls2 warnings)
          (vl-inline-mod-in-modinsts sub (cdr x)
                                     nf warnings)))
      (mv nf (append modinsts1 modinsts2)
          (append gateinsts1 gateinsts2)
          (append assigns1 assigns2)
          (append vardecls1 vardecls2)
          warnings))))

Theorem: vl-namefactory-p-of-vl-inline-mod-in-modinsts.nf

(defthm vl-namefactory-p-of-vl-inline-mod-in-modinsts.nf
  (implies (and (force (if (vl-module-p sub)
                           (vl-ok-to-inline-p sub)
                         'nil))
                (force (vl-modinstlist-p x))
                (force (vl-namefactory-p nf))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?nf ?modinsts
                     ?gateinsts ?assigns ?vardecls ?warnings)
                 (vl-inline-mod-in-modinsts sub x nf warnings)))
             (vl-namefactory-p nf)))
  :rule-classes :rewrite)

Theorem: vl-modinstlist-p-of-vl-inline-mod-in-modinsts.modinsts

(defthm vl-modinstlist-p-of-vl-inline-mod-in-modinsts.modinsts
  (implies (and (force (if (vl-module-p sub)
                           (vl-ok-to-inline-p sub)
                         'nil))
                (force (vl-modinstlist-p x))
                (force (vl-namefactory-p nf))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?nf ?modinsts
                     ?gateinsts ?assigns ?vardecls ?warnings)
                 (vl-inline-mod-in-modinsts sub x nf warnings)))
             (vl-modinstlist-p modinsts)))
  :rule-classes :rewrite)

Theorem: vl-gateinstlist-p-of-vl-inline-mod-in-modinsts.gateinsts

(defthm vl-gateinstlist-p-of-vl-inline-mod-in-modinsts.gateinsts
  (implies (and (force (if (vl-module-p sub)
                           (vl-ok-to-inline-p sub)
                         'nil))
                (force (vl-modinstlist-p x))
                (force (vl-namefactory-p nf))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?nf ?modinsts
                     ?gateinsts ?assigns ?vardecls ?warnings)
                 (vl-inline-mod-in-modinsts sub x nf warnings)))
             (vl-gateinstlist-p gateinsts)))
  :rule-classes :rewrite)

Theorem: vl-assignlist-p-of-vl-inline-mod-in-modinsts.assigns

(defthm vl-assignlist-p-of-vl-inline-mod-in-modinsts.assigns
  (implies (and (force (if (vl-module-p sub)
                           (vl-ok-to-inline-p sub)
                         'nil))
                (force (vl-modinstlist-p x))
                (force (vl-namefactory-p nf))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?nf ?modinsts
                     ?gateinsts ?assigns ?vardecls ?warnings)
                 (vl-inline-mod-in-modinsts sub x nf warnings)))
             (vl-assignlist-p assigns)))
  :rule-classes :rewrite)

Theorem: vl-vardecllist-p-of-vl-inline-mod-in-modinsts.vardecls

(defthm vl-vardecllist-p-of-vl-inline-mod-in-modinsts.vardecls
  (implies (and (force (if (vl-module-p sub)
                           (vl-ok-to-inline-p sub)
                         'nil))
                (force (vl-modinstlist-p x))
                (force (vl-namefactory-p nf))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?nf ?modinsts
                     ?gateinsts ?assigns ?vardecls ?warnings)
                 (vl-inline-mod-in-modinsts sub x nf warnings)))
             (vl-vardecllist-p vardecls)))
  :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-inline-mod-in-modinsts.warnings

(defthm vl-warninglist-p-of-vl-inline-mod-in-modinsts.warnings
  (b* (((mv ?nf ?modinsts
            ?gateinsts ?assigns ?vardecls ?warnings)
        (vl-inline-mod-in-modinsts sub x nf warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-inline-mod-in-modinsts-mvtypes-1

(defthm vl-inline-mod-in-modinsts-mvtypes-1
 (true-listp (mv-nth 1
                     (vl-inline-mod-in-modinsts sub x nf warnings)))
 :rule-classes :type-prescription)

Theorem: vl-inline-mod-in-modinsts-mvtypes-2

(defthm vl-inline-mod-in-modinsts-mvtypes-2
 (true-listp (mv-nth 2
                     (vl-inline-mod-in-modinsts sub x nf warnings)))
 :rule-classes :type-prescription)

Theorem: vl-inline-mod-in-modinsts-mvtypes-3

(defthm vl-inline-mod-in-modinsts-mvtypes-3
 (true-listp (mv-nth 3
                     (vl-inline-mod-in-modinsts sub x nf warnings)))
 :rule-classes :type-prescription)

Theorem: vl-inline-mod-in-modinsts-mvtypes-4

(defthm vl-inline-mod-in-modinsts-mvtypes-4
 (true-listp (mv-nth 4
                     (vl-inline-mod-in-modinsts sub x nf warnings)))
 :rule-classes :type-prescription)