• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
        • Vl-ealist-p
        • Modinsts-to-eoccs
        • Vl-module-make-esim
        • Exploding-vectors
          • Vl-wirealist-p
            • Vl-msb-expr-bitlist
            • Vl-plain-wire-name
            • Vl-module-wirealist
            • Vl-emodwires-from-high-to-low
            • Vl-vardecl-msb-emodwires
            • Vl-vardecllist-to-wirealist
            • Vl-emodwires-from-msb-to-lsb
            • Vl-verilogify-emodwirelist
          • Emodwire-encoding
          • Vl-emodwire-p
          • Vl-emodwirelistlist
          • Vl-emodwirelist
        • Resolving-multiple-drivers
        • Vl-modulelist-make-esims
        • Vl-module-check-e-ok
        • Vl-collect-design-wires
        • Adding-z-drivers
        • Vl-design-to-e
        • Vl-design-to-e-check-ports
        • Vl-design-to-e-main
        • Port-bit-checking
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-wirealist-p

Vl-module-wirealist

Safely generate the (fast) wirealist for a module.

Signature

(vl-module-wirealist x warnings) 
  → 
(mv successp warnings wire-alist)

Arguments

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

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

Returns

successp — Type (booleanp successp).

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

wire-alist — Type (vl-wirealist-p wire-alist).

Note: this function is memoized and generates fast alists. You should be sure to clear its memo table so that these fast alists can be garbage collected.

This function can fail, setting successp to nil and adding fatal warnings, when:

• there's a problem with the module's namespace, i.e., the net/reg names are not unique,
• the range of some net/reg has not been resolved, or
• some net/reg has arrdims (i.e., it's a "2 dimensional array" or higher)

But unless the failure is due to a namespace problem, the resulting wire alist will be at least a partial wire alist for this module that has entries for all of the wires that don't have problems.

A key property of this function is that the wire alist it generates binds completely unique bits to all of the wires. This is proven as the following theorem:

Theorem: no-duplicatesp-equal-of-append-alist-vals-of-vl-module-wirealist

(defthm
   no-duplicatesp-equal-of-append-alist-vals-of-vl-module-wirealist
  (let ((walist (mv-nth 2 (vl-module-wirealist x warnings))))
    (no-duplicatesp-equal (append-alist-vals walist))))

Definitions and Theorems

Function: vl-module-wirealist

(defun vl-module-wirealist (x warnings)
 (declare (xargs :guard (and (vl-module-p x)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-module-wirealist))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) x)
    ((unless
      (mbe
       :logic (uniquep (vl-vardecllist->names x.vardecls))
       :exec (uniquep (vl-vardecllist->names-exec x.vardecls nil))))
     (mv
      nil
      (fatal
       :type :vl-namespace-error
       :msg "~m0 illegally redefines ~&1."
       :args
       (list
           x.name
           (duplicated-members (vl-vardecllist->names x.vardecls))))
      nil)))
   (vl-vardecllist-to-wirealist x.vardecls warnings))))

Theorem: booleanp-of-vl-module-wirealist.successp

(defthm booleanp-of-vl-module-wirealist.successp
  (b* (((mv ?successp ?warnings ?wire-alist)
        (vl-module-wirealist x warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-module-wirealist.warnings

(defthm vl-warninglist-p-of-vl-module-wirealist.warnings
  (b* (((mv ?successp ?warnings ?wire-alist)
        (vl-module-wirealist x warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-wirealist-p-of-vl-module-wirealist.wire-alist

(defthm vl-wirealist-p-of-vl-module-wirealist.wire-alist
  (b* (((mv ?successp ?warnings ?wire-alist)
        (vl-module-wirealist x warnings)))
    (vl-wirealist-p wire-alist))
  :rule-classes :rewrite)

Theorem: no-duplicatesp-equal-of-append-alist-vals-of-vl-module-wirealist

(defthm
   no-duplicatesp-equal-of-append-alist-vals-of-vl-module-wirealist
  (let ((walist (mv-nth 2 (vl-module-wirealist x warnings))))
    (no-duplicatesp-equal (append-alist-vals walist))))