• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
          • Make-implicit-wires
          • Resolve-indexing
          • Origexprs
          • Argresolve
          • 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
          • Designwires
          • Udp-elim
          • Vl-annotate-design
        • Latchcode
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Portdecl-sign

Vl-portdecl-sign-main

Signature

(vl-portdecl-sign-main portdecls vardecls warnings) 
  → 
(mv warnings new-portdecls new-vardecls)

Arguments

portdecls — Guard (vl-portdecllist-p portdecls).

vardecls — Guard (vl-vardecllist-p vardecls).

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

Returns

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

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

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

Definitions and Theorems

Function: vl-portdecl-sign-main

(defun vl-portdecl-sign-main (portdecls vardecls warnings)
 (declare (xargs :guard (and (vl-portdecllist-p portdecls)
                             (vl-vardecllist-p vardecls)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-portdecl-sign-main))
  (declare (ignorable __function__))
  (b*
   ((portdecls (vl-portdecllist-fix portdecls))
    (vardecls (vl-vardecllist-fix vardecls))
    (pnames (vl-portdecllist->names portdecls))
    (vnames (vl-vardecllist->names vardecls))
    (dupe-ports (duplicated-members pnames))
    ((when dupe-ports)
     (mv (fatal :type :vl-bad-ports
                :msg "Ports are declared multiple times: ~&0."
                :args (list dupe-ports))
         portdecls vardecls))
    (dupe-vars (duplicated-members vnames))
    ((when dupe-vars)
     (mv (fatal :type :vl-bad-variables
                :msg "Variables are declared multiple times: ~&0."
                :args (list dupe-vars))
         portdecls vardecls))
    (missing (difference (mergesort pnames)
                         (mergesort vnames)))
    ((when missing)
     (mv
      (fatal
       :type :vl-bad-ports
       :msg
       "Ports have no corresponding variable ~
                         declarations: ~&0."
       :args (list missing))
      portdecls vardecls))
    (port-vars (vl-reorder-vardecls pnames vardecls))
    (non-port-vars (vl-delete-vardecls pnames vardecls))
    ((mv ?okp
         warnings new-portdecls new-port-vars)
     (vl-portdecl-sign-list portdecls port-vars warnings))
    (new-vardecls (append new-port-vars non-port-vars)))
   (mv (ok) new-portdecls new-vardecls))))

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

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

Theorem: vl-portdecllist-p-of-vl-portdecl-sign-main.new-portdecls

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

Theorem: vl-vardecllist-p-of-vl-portdecl-sign-main.new-vardecls

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

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

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

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

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

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

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

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

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

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

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

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

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