• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
          • 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
    • Svl
    • X86isa
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Port-resolve

Vl-ansi-portdecl-to-regularport

Assumes x was NOT just a plain identifier (or we are in the erroneous case where it was a plain identifier, but there was no previous port to base it on.) Type and nettype info comes from x itself; only the direction may come from the previous port.

Signature

(vl-ansi-portdecl-to-regularport x ports-acc portdecls-acc warnings) 
  → 
(mv warnings port portdecl? vardecl?)

Arguments

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

ports-acc — Previous ports. Empty implies this is the first.
    Guard (vl-portlist-p ports-acc).

portdecls-acc — Previous portdecls -- may be shorter than ports-acc.
    Guard (vl-portdecllist-p portdecls-acc).

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?) (vl-port-case port :vl-interfaceport 0 :vl-regularport 1))) .

vardecl? — Type (and (vl-vardecllist-p vardecl?) (equal (len vardecl?) (vl-port-case port :vl-interfaceport 0 :vl-regularport 1))) .

Definitions and Theorems

Function: vl-ansi-portdecl-to-regularport

(defun vl-ansi-portdecl-to-regularport
       (x ports-acc portdecls-acc warnings)
 (declare (xargs :guard (and (vl-ansi-portdecl-p x)
                             (vl-portlist-p ports-acc)
                             (vl-portdecllist-p portdecls-acc)
                             (vl-warninglist-p warnings))))
 (declare
  (xargs :guard (equal (len portdecls-acc)
                       (len (vl-collect-regular-ports ports-acc)))))
 (let ((__function__ 'vl-ansi-portdecl-to-regularport))
  (declare (ignorable __function__))
  (b*
   (((vl-ansi-portdecl x)
     (vl-ansi-portdecl-fix x))
    ((mv dir warnings)
     (cond
      (x.dir (mv x.dir (ok)))
      ((atom ports-acc) (mv :vl-inout nil))
      (t
       (b* ((port1 (car ports-acc)))
        (vl-port-case
         port1
         :vl-regularport (mv (vl-portdecl->dir (car portdecls-acc))
                             (ok))
         :vl-interfaceport
         (mv
          :vl-inout
          (fatal
           :type :vl-bad-ports
           :msg
           "~a0: can't infer direction for port ~a1 ~
                                      since it follows an interface port.  ~
                                      Please explicitly specify a direction ~
                                      (input, output, ...)"
           :args (list x.loc x.name))))))))
    (nettype (vl-nettype-for-parsed-ansi-port dir x))
    (type (vl-ansi-portdecl-regularport-type x)))
   (mv (ok)
       (make-vl-regularport :name x.name
                            :expr (vl-idexpr x.name)
                            :loc x.loc)
       (list (make-vl-portdecl :name x.name
                               :dir dir
                               :nettype nettype
                               :type type
                               :atts x.atts
                               :loc x.loc))
       (list (make-vl-vardecl
                  :name x.name :nettype
                  nettype :type type :varp x.varp :atts
                  (if x.atts (hons '("VL_ANSI_PORT_VARDECL") x.atts)
                    (hons-copy '(("VL_ANSI_PORT_VARDECL"))))
                  :loc x.loc))))))

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

(defthm vl-warninglist-p-of-vl-ansi-portdecl-to-regularport.warnings
  (b* (((mv ?warnings ?port ?portdecl? ?vardecl?)
        (vl-ansi-portdecl-to-regularport
             x ports-acc portdecls-acc warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

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

(defthm vl-regularport-p-of-vl-ansi-portdecl-to-regularport.port
  (b* (((mv ?warnings ?port ?portdecl? ?vardecl?)
        (vl-ansi-portdecl-to-regularport
             x ports-acc portdecls-acc warnings)))
    (vl-regularport-p port))
  :rule-classes :rewrite)

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

(defthm return-type-of-vl-ansi-portdecl-to-regularport.portdecl?
  (b* (((mv ?warnings ?port ?portdecl? ?vardecl?)
        (vl-ansi-portdecl-to-regularport
             x ports-acc portdecls-acc warnings)))
    (and (vl-portdecllist-p portdecl?)
         (equal (len portdecl?)
                (vl-port-case port
                              :vl-interfaceport 0
                              :vl-regularport 1))))
  :rule-classes :rewrite)

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

(defthm return-type-of-vl-ansi-portdecl-to-regularport.vardecl?
  (b* (((mv ?warnings ?port ?portdecl? ?vardecl?)
        (vl-ansi-portdecl-to-regularport
             x ports-acc portdecls-acc warnings)))
    (and (vl-vardecllist-p vardecl?)
         (equal (len vardecl?)
                (vl-port-case port
                              :vl-interfaceport 0
                              :vl-regularport 1))))
  :rule-classes :rewrite)

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

(defthm vl-ansi-portdecl-to-regularport-of-vl-ansi-portdecl-fix-x
 (equal
  (vl-ansi-portdecl-to-regularport (vl-ansi-portdecl-fix x)
                                   ports-acc portdecls-acc warnings)
  (vl-ansi-portdecl-to-regularport
       x ports-acc portdecls-acc warnings)))

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

(defthm
 vl-ansi-portdecl-to-regularport-vl-ansi-portdecl-equiv-congruence-on-x
 (implies (vl-ansi-portdecl-equiv x x-equiv)
          (equal (vl-ansi-portdecl-to-regularport
                      x ports-acc portdecls-acc warnings)
                 (vl-ansi-portdecl-to-regularport
                      x-equiv
                      ports-acc portdecls-acc warnings)))
 :rule-classes :congruence)

Theorem: vl-ansi-portdecl-to-regularport-of-vl-portlist-fix-ports-acc

(defthm vl-ansi-portdecl-to-regularport-of-vl-portlist-fix-ports-acc
 (equal
      (vl-ansi-portdecl-to-regularport x (vl-portlist-fix ports-acc)
                                       portdecls-acc warnings)
      (vl-ansi-portdecl-to-regularport
           x ports-acc portdecls-acc warnings)))

Theorem: vl-ansi-portdecl-to-regularport-vl-portlist-equiv-congruence-on-ports-acc

(defthm
 vl-ansi-portdecl-to-regularport-vl-portlist-equiv-congruence-on-ports-acc
 (implies
   (vl-portlist-equiv ports-acc ports-acc-equiv)
   (equal (vl-ansi-portdecl-to-regularport
               x ports-acc portdecls-acc warnings)
          (vl-ansi-portdecl-to-regularport x ports-acc-equiv
                                           portdecls-acc warnings)))
 :rule-classes :congruence)

Theorem: vl-ansi-portdecl-to-regularport-of-vl-portdecllist-fix-portdecls-acc

(defthm
 vl-ansi-portdecl-to-regularport-of-vl-portdecllist-fix-portdecls-acc
 (equal (vl-ansi-portdecl-to-regularport
             x ports-acc
             (vl-portdecllist-fix portdecls-acc)
             warnings)
        (vl-ansi-portdecl-to-regularport
             x ports-acc portdecls-acc warnings)))

Theorem: vl-ansi-portdecl-to-regularport-vl-portdecllist-equiv-congruence-on-portdecls-acc

(defthm
 vl-ansi-portdecl-to-regularport-vl-portdecllist-equiv-congruence-on-portdecls-acc
 (implies
  (vl-portdecllist-equiv portdecls-acc portdecls-acc-equiv)
  (equal
    (vl-ansi-portdecl-to-regularport
         x ports-acc portdecls-acc warnings)
    (vl-ansi-portdecl-to-regularport x ports-acc
                                     portdecls-acc-equiv warnings)))
 :rule-classes :congruence)

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

(defthm
     vl-ansi-portdecl-to-regularport-of-vl-warninglist-fix-warnings
 (equal
     (vl-ansi-portdecl-to-regularport x ports-acc portdecls-acc
                                      (vl-warninglist-fix warnings))
     (vl-ansi-portdecl-to-regularport
          x ports-acc portdecls-acc warnings)))

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

(defthm
 vl-ansi-portdecl-to-regularport-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
    (vl-ansi-portdecl-to-regularport
         x ports-acc portdecls-acc warnings)
    (vl-ansi-portdecl-to-regularport x ports-acc
                                     portdecls-acc warnings-equiv)))
 :rule-classes :congruence)