• 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-mods

(vl-inline-mods x all-mods) inlines all modules in x throughout all-mods.

Signature

(vl-inline-mods x all-mods) → new-mods

Arguments

x — Guard (and (vl-modulelist-p x) (vl-ok-to-inline-list-p x)).

all-mods — Guard (vl-modulelist-p all-mods).

Returns

new-mods — Type (vl-modulelist-p new-mods), given the guard.

Definitions and Theorems

Function: vl-inline-mods

(defun vl-inline-mods (x all-mods)
  (declare (xargs :guard (and (and (vl-modulelist-p x)
                                   (vl-ok-to-inline-list-p x))
                              (vl-modulelist-p all-mods))))
  (let ((__function__ 'vl-inline-mods))
    (declare (ignorable __function__))
    (if (atom x)
        all-mods
      (b* ((all-mods (vl-inline-mod-in-mods-aux (car x)
                                                all-mods)))
        (vl-inline-mods (cdr x) all-mods)))))

Theorem: vl-modulelist-p-of-vl-inline-mods

(defthm vl-modulelist-p-of-vl-inline-mods
  (implies (and (force (if (vl-modulelist-p x)
                           (vl-ok-to-inline-list-p x)
                         'nil))
                (force (vl-modulelist-p all-mods)))
           (b* ((new-mods (vl-inline-mods x all-mods)))
             (vl-modulelist-p new-mods)))
  :rule-classes :rewrite)