• 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
          • Basicsanity
          • Portdecl-sign
            • Vl-modulelist-portdecl-sign
            • Vl-portdecl-sign-list
            • Vl-portdecl-sign-1
            • Vl-portdecl-sign-main
            • Vl-portdecl-type-set-signed
            • Vl-module-portdecl-sign
            • Vl-design-portdecl-sign
            • Vl-datatype->signedp
          • 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

• Portdecl-sign

Vl-portdecl-sign-list

Signature

(vl-portdecl-sign-list portdecls vardecls warnings) 
  → 
(mv successp warnings new-ports new-vars)

Arguments

portdecls — Port declarations to process, which we recur through.
    Guard (vl-portdecllist-p portdecls).

vardecls — Exactly the corresponding variable declarations.
    Guard (vl-vardecllist-p vardecls).

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

Returns

successp — Type (booleanp successp).

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

new-ports — Type (vl-portdecllist-p new-ports).

new-vars — Type (vl-vardecllist-p new-vars).

Definitions and Theorems

Function: vl-portdecl-sign-list

(defun vl-portdecl-sign-list (portdecls vardecls warnings)
  (declare (xargs :guard (and (vl-portdecllist-p portdecls)
                              (vl-vardecllist-p vardecls)
                              (vl-warninglist-p warnings))))
  (declare (xargs :guard (equal (vl-portdecllist->names portdecls)
                                (vl-vardecllist->names vardecls))))
  (let ((__function__ 'vl-portdecl-sign-list))
    (declare (ignorable __function__))
    (b* (((when (atom portdecls))
          (mv t (ok) nil nil))
         ((mv okp1 warnings port1 var1)
          (vl-portdecl-sign-1 (car portdecls)
                              (car vardecls)
                              warnings))
         ((mv okp2 warnings ports2 vars2)
          (vl-portdecl-sign-list (cdr portdecls)
                                 (cdr vardecls)
                                 warnings)))
      (mv (and okp1 okp2)
          warnings (cons port1 ports2)
          (cons var1 vars2)))))

Theorem: booleanp-of-vl-portdecl-sign-list.successp

(defthm booleanp-of-vl-portdecl-sign-list.successp
  (b* (((mv ?successp
            ?warnings ?new-ports ?new-vars)
        (vl-portdecl-sign-list portdecls vardecls warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-portdecl-sign-list.warnings

(defthm vl-warninglist-p-of-vl-portdecl-sign-list.warnings
  (b* (((mv ?successp
            ?warnings ?new-ports ?new-vars)
        (vl-portdecl-sign-list portdecls vardecls warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-portdecllist-p-of-vl-portdecl-sign-list.new-ports

(defthm vl-portdecllist-p-of-vl-portdecl-sign-list.new-ports
  (b* (((mv ?successp
            ?warnings ?new-ports ?new-vars)
        (vl-portdecl-sign-list portdecls vardecls warnings)))
    (vl-portdecllist-p new-ports))
  :rule-classes :rewrite)

Theorem: vl-vardecllist-p-of-vl-portdecl-sign-list.new-vars

(defthm vl-vardecllist-p-of-vl-portdecl-sign-list.new-vars
  (b* (((mv ?successp
            ?warnings ?new-ports ?new-vars)
        (vl-portdecl-sign-list portdecls vardecls warnings)))
    (vl-vardecllist-p new-vars))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-portdecl-sign-list.new-ports

(defthm true-listp-of-vl-portdecl-sign-list.new-ports
  (b* (((mv ?successp
            ?warnings ?new-ports ?new-vars)
        (vl-portdecl-sign-list portdecls vardecls warnings)))
    (true-listp new-ports))
  :rule-classes :type-prescription)

Theorem: true-listp-of-vl-portdecl-sign-list.new-vars

(defthm true-listp-of-vl-portdecl-sign-list.new-vars
  (b* (((mv ?successp
            ?warnings ?new-ports ?new-vars)
        (vl-portdecl-sign-list portdecls vardecls warnings)))
    (true-listp new-vars))
  :rule-classes :type-prescription)

Theorem: vl-portdecl-sign-list-of-vl-portdecllist-fix-portdecls

(defthm vl-portdecl-sign-list-of-vl-portdecllist-fix-portdecls
  (equal (vl-portdecl-sign-list (vl-portdecllist-fix portdecls)
                                vardecls warnings)
         (vl-portdecl-sign-list portdecls vardecls warnings)))

Theorem: vl-portdecl-sign-list-vl-portdecllist-equiv-congruence-on-portdecls

(defthm
 vl-portdecl-sign-list-vl-portdecllist-equiv-congruence-on-portdecls
 (implies
  (vl-portdecllist-equiv portdecls portdecls-equiv)
  (equal (vl-portdecl-sign-list portdecls vardecls warnings)
         (vl-portdecl-sign-list portdecls-equiv vardecls warnings)))
 :rule-classes :congruence)

Theorem: vl-portdecl-sign-list-of-vl-vardecllist-fix-vardecls

(defthm vl-portdecl-sign-list-of-vl-vardecllist-fix-vardecls
 (equal
      (vl-portdecl-sign-list portdecls (vl-vardecllist-fix vardecls)
                             warnings)
      (vl-portdecl-sign-list portdecls vardecls warnings)))

Theorem: vl-portdecl-sign-list-vl-vardecllist-equiv-congruence-on-vardecls

(defthm
  vl-portdecl-sign-list-vl-vardecllist-equiv-congruence-on-vardecls
 (implies
  (vl-vardecllist-equiv vardecls vardecls-equiv)
  (equal (vl-portdecl-sign-list portdecls vardecls warnings)
         (vl-portdecl-sign-list portdecls vardecls-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-portdecl-sign-list-of-vl-warninglist-fix-warnings

(defthm vl-portdecl-sign-list-of-vl-warninglist-fix-warnings
 (equal
      (vl-portdecl-sign-list portdecls
                             vardecls (vl-warninglist-fix warnings))
      (vl-portdecl-sign-list portdecls vardecls warnings)))

Theorem: vl-portdecl-sign-list-vl-warninglist-equiv-congruence-on-warnings

(defthm
  vl-portdecl-sign-list-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal (vl-portdecl-sign-list portdecls vardecls warnings)
         (vl-portdecl-sign-list portdecls vardecls warnings-equiv)))
 :rule-classes :congruence)