• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
        • Elaborate
        • Addnames
        • Annotate
          • Increment-elim
          • Make-implicit-wires
          • Basic-bind-elim
          • Argresolve
            • Vl-convert-namedargs
            • Vl-unhierarchicalize-interfaceport
            • Vl-interfacelist-argresolve
            • Vl-modulelist-argresolve
            • Vl-gateinst-dirassign
            • Vl-arguments-argresolve
            • Vl-unhierarchicalize-interfaceports
            • Vl-check-blankargs
            • Vl-annotate-plainargs
            • Vl-modinst-maybe-argresolve
            • Vl-modinst-argresolve
            • Vl-modinstlist-argresolve
            • Vl-gateinstlist-dirassign
            • Vl-interface-argresolve
            • Vl-module-argresolve
            • Vl-namedarglist-alist
            • Vl-make-namedarg-alist
            • Vl-design-argresolve
            • Vl-fast-find-namedarg
            • Vl-namedarg-alist
            • Vl-scopeitem-modport-p
            • Vl-scopeitem-modinst-p
            • Vl-scopeitem-interfaceport-p
            • Vl-port-interface-p
          • Basicsanity
          • Portdecl-sign
          • Enum-names
          • Port-resolve
          • Udp-elim
          • Vl-annotate-design
          • Vl-annotate-module
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Argresolve

Vl-annotate-plainargs

Annotates a plain argument list with port names and directions.

Signature

(vl-annotate-plainargs args ports scope) → annotated-args

Arguments

args — plainargs that typically have no :dir or :portname information; we want to annotate them.
    Guard (vl-plainarglist-p args).

ports — corresponding ports for the submodule.
    Guard (vl-portlist-p ports).

scope — Guard (vl-scope-p scope).

Returns

annotated-args — annotated version of args, semantically equivalent but typically has :dir and :portname information.
    Type (and (vl-plainarglist-p annotated-args) (equal (len annotated-args) (len args))) .

This is a "best-effort" process which may fail to add annotations to any or all arguments. Such failures are expected, so we do not generate any warnings or errors in response to them.

What causes these failures?

• Not all ports necessarily have a name, so we cannot add a :portname for every port.
• The direction of a port may also not be apparent in some cases; see vl-port-direction for details.

Definitions and Theorems

Function: vl-annotate-plainargs

(defun vl-annotate-plainargs (args ports scope)
  (declare (xargs :guard (and (vl-plainarglist-p args)
                              (vl-portlist-p ports)
                              (vl-scope-p scope))))
  (declare (xargs :guard (same-lengthp args ports)))
  (let ((__function__ 'vl-annotate-plainargs))
    (declare (ignorable __function__))
    (b* (((when (atom args)) nil)
         (name (vl-port->name (car ports)))
         ((mv & dir)
          (vl-port-direction (car ports)
                             scope nil))
         (arg-prime (change-vl-plainarg (car args)
                                        :dir dir
                                        :portname name)))
      (cons arg-prime
            (vl-annotate-plainargs (cdr args)
                                   (cdr ports)
                                   scope)))))

Theorem: return-type-of-vl-annotate-plainargs

(defthm return-type-of-vl-annotate-plainargs
  (b* ((annotated-args (vl-annotate-plainargs args ports scope)))
    (and (vl-plainarglist-p annotated-args)
         (equal (len annotated-args)
                (len args))))
  :rule-classes :rewrite)

Theorem: vl-annotate-plainargs-of-vl-plainarglist-fix-args

(defthm vl-annotate-plainargs-of-vl-plainarglist-fix-args
  (equal (vl-annotate-plainargs (vl-plainarglist-fix args)
                                ports scope)
         (vl-annotate-plainargs args ports scope)))

Theorem: vl-annotate-plainargs-vl-plainarglist-equiv-congruence-on-args

(defthm
     vl-annotate-plainargs-vl-plainarglist-equiv-congruence-on-args
  (implies (vl-plainarglist-equiv args args-equiv)
           (equal (vl-annotate-plainargs args ports scope)
                  (vl-annotate-plainargs args-equiv ports scope)))
  :rule-classes :congruence)

Theorem: vl-annotate-plainargs-of-vl-portlist-fix-ports

(defthm vl-annotate-plainargs-of-vl-portlist-fix-ports
  (equal (vl-annotate-plainargs args (vl-portlist-fix ports)
                                scope)
         (vl-annotate-plainargs args ports scope)))

Theorem: vl-annotate-plainargs-vl-portlist-equiv-congruence-on-ports

(defthm vl-annotate-plainargs-vl-portlist-equiv-congruence-on-ports
  (implies (vl-portlist-equiv ports ports-equiv)
           (equal (vl-annotate-plainargs args ports scope)
                  (vl-annotate-plainargs args ports-equiv scope)))
  :rule-classes :congruence)

Theorem: vl-annotate-plainargs-of-vl-scope-fix-scope

(defthm vl-annotate-plainargs-of-vl-scope-fix-scope
  (equal (vl-annotate-plainargs args ports (vl-scope-fix scope))
         (vl-annotate-plainargs args ports scope)))

Theorem: vl-annotate-plainargs-vl-scope-equiv-congruence-on-scope

(defthm vl-annotate-plainargs-vl-scope-equiv-congruence-on-scope
  (implies (vl-scope-equiv scope scope-equiv)
           (equal (vl-annotate-plainargs args ports scope)
                  (vl-annotate-plainargs args ports scope-equiv)))
  :rule-classes :congruence)