• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Hierarchy
        • Extract-vl-types
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
          • Vl-module->modnamespace
            • Vl-module->modnamespace-nrev
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Modnamespace

Vl-module->modnamespace

Main function for gathering up the names that are declared as parameters, wires, variables, registers, and so on.

Signature

(vl-module->modnamespace x) → names

Arguments

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

Returns

names — Type (string-listp names).

Note: this function does not include the names of ports, because as noted above they are considered to be in their own namespace which is "separate but overlapping" the main namespace in the module; see modnamespace for details.

If this function returns a list that is not duplicate-free, it means the module illegally declares those duplicated names more than once.

To reduce memory usage, we optimize this function using nreverse.

Definitions and Theorems

Function: vl-module->modnamespace

(defun
 vl-module->modnamespace (x)
 (declare (xargs :guard (vl-module-p x)))
 (let
  ((__function__ 'vl-module->modnamespace))
  (declare (ignorable __function__))
  (mbe
    :logic (b* (((vl-module x) x))
               (append (vl-vardecllist->names x.vardecls)
                       (vl-paramdecllist->names x.paramdecls)
                       (vl-fundecllist->names x.fundecls)
                       (vl-taskdecllist->names x.taskdecls)
                       (vl-modinstlist->instnames x.modinsts)
                       (vl-gateinstlist->names x.gateinsts)))
    :exec (with-local-nrev (vl-module->modnamespace-nrev x nrev)))))

Theorem: string-listp-of-vl-module->modnamespace

(defthm string-listp-of-vl-module->modnamespace
        (b* ((names (vl-module->modnamespace x)))
            (string-listp names))
        :rule-classes :rewrite)

Theorem: vl-module->modnamespace-nrev-removal

(defthm vl-module->modnamespace-nrev-removal
        (equal (vl-module->modnamespace-nrev x nrev)
               (append nrev (vl-module->modnamespace x))))

Theorem: true-listp-of-vl-module->modnamespace

(defthm true-listp-of-vl-module->modnamespace
        (true-listp (vl-module->modnamespace x))
        :rule-classes :type-prescription)

Theorem: vl-module->modnamespace-of-vl-module-fix-x

(defthm vl-module->modnamespace-of-vl-module-fix-x
        (equal (vl-module->modnamespace (vl-module-fix x))
               (vl-module->modnamespace x)))

Theorem: vl-module->modnamespace-vl-module-equiv-congruence-on-x

(defthm vl-module->modnamespace-vl-module-equiv-congruence-on-x
        (implies (vl-module-equiv x x-equiv)
                 (equal (vl-module->modnamespace x)
                        (vl-module->modnamespace x-equiv)))
        :rule-classes :congruence)

Subtopics

Vl-module->modnamespace-nrev

Tail-recursive implementation of vl-module->modnamespace.