• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • 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
          • Enum-names
          • Port-resolve
            • Vl-modulelist-resolve-nonansi-interfaceports
            • Vl-interfacelist-resolve-nonansi-interfaceports
            • Vl-ansi-portdecl-resolve
            • Vl-interfacelist-resolve-ansi-portdecls
            • Vl-modulelist-resolve-ansi-portdecls
            • Vl-ansi-portdecl-to-regularport
            • Vl-ansi-portdecl-to-regularport-from-previous-regularport
            • Vl-resolve-ansi-portdecls
            • Vl-nettype-for-parsed-ansi-port
            • Vl-loaditems-remove-interfaceport-decls
            • Vl-vardecl-is-really-interfaceport
            • Vl-name-is-interface-or-type
            • Vl-interface/type-warn-about-unexpected-lookup
            • Vl-interface-resolve-nonansi-interfaceports
            • Vl-module-resolve-nonansi-interfaceports
            • Vl-interface-resolve-ansi-portdecls
            • Vl-ports-resolve-interfaces
            • Vl-module-resolve-ansi-portdecls
            • Vl-ansi-portdecl-consistency-check
            • Vl-design-resolve-nonansi-interfaceports
            • Vl-ansi-portdecl-to-interfaceport
            • Vl-ansi-portdecl-regularport-type
            • Vl-design-resolve-ansi-portdecls
          • Udp-elim
          • Vl-annotate-design
          • Vl-annotate-module
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Port-resolve

Vl-ansi-portdecl-to-regularport-from-previous-regularport

Assumes that x was just a plain variable, so it inherits all its info from the previous port.

Signature

(vl-ansi-portdecl-to-regularport-from-previous-regularport 
     x prev prev-var warnings) 
 
  → 
(mv warnings port portdecl vardecl)

Arguments

x — Guard (vl-ansi-portdecl-p x).

prev — Previous portdecl.
    Guard (vl-portdecl-p prev).

prev-var — Previous vardecl.
    Guard (vl-vardecl-p prev-var).

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

Returns

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

port — Type (vl-regularport-p port).

portdecl — Type (and (vl-portdecllist-p portdecl) (equal (len portdecl) 1)).

vardecl — Type (and (vl-vardecllist-p vardecl) (equal (len vardecl) 1)).

Definitions and Theorems

Function: vl-ansi-portdecl-to-regularport-from-previous-regularport

(defun vl-ansi-portdecl-to-regularport-from-previous-regularport
       (x prev prev-var warnings)
 (declare (xargs :guard (and (vl-ansi-portdecl-p x)
                             (vl-portdecl-p prev)
                             (vl-vardecl-p prev-var)
                             (vl-warninglist-p warnings))))
 (let
  ((__function__
        'vl-ansi-portdecl-to-regularport-from-previous-regularport))
  (declare (ignorable __function__))
  (b* (((vl-ansi-portdecl x)
        (vl-ansi-portdecl-fix x))
       ((vl-portdecl prev))
       ((vl-vardecl prev-var)))
   (mv (ok)
       (make-vl-regularport :name x.name
                            :expr (vl-idexpr x.name)
                            :loc x.loc)
       (list (change-vl-portdecl prev
                                 :name x.name
                                 :loc x.loc
                                 :atts x.atts
                                 :dir prev.dir
                                 :nettype prev.nettype
                                 :type prev.type))
       (list (change-vl-vardecl
                  prev-var :name x.name
                  :loc x.loc :type prev.type :nettype
                  prev.nettype :varp prev-var.varp :atts
                  (if x.atts (hons '("VL_ANSI_PORT_VARDECL") x.atts)
                    (hons-copy '(("VL_ANSI_PORT_VARDECL"))))
                  :initval nil
                  :constp nil
                  :lifetime nil
                  :vectoredp nil
                  :scalaredp nil
                  :delay nil
                  :cstrength nil))))))

Theorem: vl-warninglist-p-of-vl-ansi-portdecl-to-regularport-from-previous-regularport.warnings

(defthm
 vl-warninglist-p-of-vl-ansi-portdecl-to-regularport-from-previous-regularport.warnings
 (b* (((mv ?warnings ?port ?portdecl ?vardecl)
       (vl-ansi-portdecl-to-regularport-from-previous-regularport
            x prev prev-var warnings)))
   (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-regularport-p-of-vl-ansi-portdecl-to-regularport-from-previous-regularport.port

(defthm
 vl-regularport-p-of-vl-ansi-portdecl-to-regularport-from-previous-regularport.port
 (b* (((mv ?warnings ?port ?portdecl ?vardecl)
       (vl-ansi-portdecl-to-regularport-from-previous-regularport
            x prev prev-var warnings)))
   (vl-regularport-p port))
 :rule-classes :rewrite)

Theorem: return-type-of-vl-ansi-portdecl-to-regularport-from-previous-regularport.portdecl

(defthm
 return-type-of-vl-ansi-portdecl-to-regularport-from-previous-regularport.portdecl
 (b* (((mv ?warnings ?port ?portdecl ?vardecl)
       (vl-ansi-portdecl-to-regularport-from-previous-regularport
            x prev prev-var warnings)))
   (and (vl-portdecllist-p portdecl)
        (equal (len portdecl) 1)))
 :rule-classes :rewrite)

Theorem: return-type-of-vl-ansi-portdecl-to-regularport-from-previous-regularport.vardecl

(defthm
 return-type-of-vl-ansi-portdecl-to-regularport-from-previous-regularport.vardecl
 (b* (((mv ?warnings ?port ?portdecl ?vardecl)
       (vl-ansi-portdecl-to-regularport-from-previous-regularport
            x prev prev-var warnings)))
   (and (vl-vardecllist-p vardecl)
        (equal (len vardecl) 1)))
 :rule-classes :rewrite)

Theorem: vl-ansi-portdecl-to-regularport-from-previous-regularport-of-vl-ansi-portdecl-fix-x

(defthm
 vl-ansi-portdecl-to-regularport-from-previous-regularport-of-vl-ansi-portdecl-fix-x
 (equal (vl-ansi-portdecl-to-regularport-from-previous-regularport
             (vl-ansi-portdecl-fix x)
             prev prev-var warnings)
        (vl-ansi-portdecl-to-regularport-from-previous-regularport
             x prev prev-var warnings)))

Theorem: vl-ansi-portdecl-to-regularport-from-previous-regularport-vl-ansi-portdecl-equiv-congruence-on-x

(defthm
 vl-ansi-portdecl-to-regularport-from-previous-regularport-vl-ansi-portdecl-equiv-congruence-on-x
 (implies (vl-ansi-portdecl-equiv x x-equiv)
          (equal (vl-ansi-portdecl-to-regularport-from-previous-regularport
                      x prev prev-var warnings)
                 (vl-ansi-portdecl-to-regularport-from-previous-regularport
                      x-equiv prev prev-var warnings)))
 :rule-classes :congruence)

Theorem: vl-ansi-portdecl-to-regularport-from-previous-regularport-of-vl-portdecl-fix-prev

(defthm
 vl-ansi-portdecl-to-regularport-from-previous-regularport-of-vl-portdecl-fix-prev
 (equal (vl-ansi-portdecl-to-regularport-from-previous-regularport
             x (vl-portdecl-fix prev)
             prev-var warnings)
        (vl-ansi-portdecl-to-regularport-from-previous-regularport
             x prev prev-var warnings)))

Theorem: vl-ansi-portdecl-to-regularport-from-previous-regularport-vl-portdecl-equiv-congruence-on-prev

(defthm
 vl-ansi-portdecl-to-regularport-from-previous-regularport-vl-portdecl-equiv-congruence-on-prev
 (implies (vl-portdecl-equiv prev prev-equiv)
          (equal (vl-ansi-portdecl-to-regularport-from-previous-regularport
                      x prev prev-var warnings)
                 (vl-ansi-portdecl-to-regularport-from-previous-regularport
                      x prev-equiv prev-var warnings)))
 :rule-classes :congruence)

Theorem: vl-ansi-portdecl-to-regularport-from-previous-regularport-of-vl-vardecl-fix-prev-var

(defthm
 vl-ansi-portdecl-to-regularport-from-previous-regularport-of-vl-vardecl-fix-prev-var
 (equal (vl-ansi-portdecl-to-regularport-from-previous-regularport
             x prev (vl-vardecl-fix prev-var)
             warnings)
        (vl-ansi-portdecl-to-regularport-from-previous-regularport
             x prev prev-var warnings)))

Theorem: vl-ansi-portdecl-to-regularport-from-previous-regularport-vl-vardecl-equiv-congruence-on-prev-var

(defthm
 vl-ansi-portdecl-to-regularport-from-previous-regularport-vl-vardecl-equiv-congruence-on-prev-var
 (implies (vl-vardecl-equiv prev-var prev-var-equiv)
          (equal (vl-ansi-portdecl-to-regularport-from-previous-regularport
                      x prev prev-var warnings)
                 (vl-ansi-portdecl-to-regularport-from-previous-regularport
                      x prev prev-var-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-ansi-portdecl-to-regularport-from-previous-regularport-of-vl-warninglist-fix-warnings

(defthm
 vl-ansi-portdecl-to-regularport-from-previous-regularport-of-vl-warninglist-fix-warnings
 (equal (vl-ansi-portdecl-to-regularport-from-previous-regularport
             x prev
             prev-var (vl-warninglist-fix warnings))
        (vl-ansi-portdecl-to-regularport-from-previous-regularport
             x prev prev-var warnings)))

Theorem: vl-ansi-portdecl-to-regularport-from-previous-regularport-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-ansi-portdecl-to-regularport-from-previous-regularport-vl-warninglist-equiv-congruence-on-warnings
 (implies (vl-warninglist-equiv warnings warnings-equiv)
          (equal (vl-ansi-portdecl-to-regularport-from-previous-regularport
                      x prev prev-var warnings)
                 (vl-ansi-portdecl-to-regularport-from-previous-regularport
                      x prev prev-var warnings-equiv)))
 :rule-classes :congruence)