• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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-resolve

Turns an ANSI portdecl into a real port, (possible) portdecl, and (possible) vardecl.

Signature

(vl-ansi-portdecl-resolve x ports-acc portdecls-acc vardecls-acc ss) 
  → 
(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).

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

ss — Guard (vl-scopestack-p ss).

Returns

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

port — Type (vl-port-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))) .

This takes care of ambiguous interface ports in ANSI modules, and also creates implicit variable declarations. We assume these do not already exist; if they do, we'll be creating new ones, but this should be checked by make-implicit-wires.

This warns if there is an ambiguity in whether it's an interface or regular port, but does not warn about all possible bad cases. E.g., if it's known to be a regular port, we don't look up the datatype to make sure it exists.

Definitions and Theorems

Function: vl-ansi-portdecl-resolve

(defun vl-ansi-portdecl-resolve
       (x ports-acc portdecls-acc vardecls-acc ss)
 (declare (xargs :guard (and (vl-ansi-portdecl-p x)
                             (vl-portlist-p ports-acc)
                             (vl-portdecllist-p portdecls-acc)
                             (vl-vardecllist-p vardecls-acc)
                             (vl-scopestack-p ss))))
 (declare
  (xargs
   :guard (and (equal (len portdecls-acc)
                      (len (vl-collect-regular-ports ports-acc)))
               (equal (len vardecls-acc)
                      (len (vl-collect-regular-ports ports-acc))))))
 (let ((__function__ 'vl-ansi-portdecl-resolve))
  (declare (ignorable __function__))
  (b*
   (((vl-ansi-portdecl x)
     (vl-ansi-portdecl-fix x))
    (warnings nil)
    ((when (and (not x.dir)
                (not x.nettype)
                (not x.varp)
                (not x.type)
                (not x.typename)
                (not x.pdims)
                (not x.signedness)))
     (b*
      (((when (atom ports-acc))
        (b*
         ((warnings
           (warn
            :type :vl-ansi-port-programming-error
            :msg
            "~a0: When the first port in the list has no ~
                            direction, nettype, var keyword, datatype, or ~
                            dimensions, or signedness, then it should have ~
                            been parsed as a non-ANSI portlist."
            :args (list x))))
         (vl-ansi-portdecl-to-regularport
              x ports-acc portdecls-acc warnings)))
       (prev (vl-port-fix (car ports-acc))))
      (vl-port-case
           prev :vl-interfaceport
           (b* (((vl-interfaceport prev)))
             (mv warnings
                 (make-vl-interfaceport :name x.name
                                        :ifname prev.ifname
                                        :modport prev.modport
                                        :udims x.udims
                                        :loc x.loc)
                 nil nil))
           :vl-regularport (vl-ansi-portdecl-to-regularport-from-previous-regularport
                                x (car portdecls-acc)
                                (car vardecls-acc)
                                warnings))))
    ((unless (and x.typename (not x.dir)
                  (not x.nettype)
                  (not x.varp)))
     (vl-ansi-portdecl-to-regularport
          x ports-acc portdecls-acc warnings))
    ((when x.modport)
     (mv warnings
         (vl-ansi-portdecl-to-interfaceport x)
         nil nil))
    ((wmv warnings is-interface is-type
          :ctx x)
     (vl-name-is-interface-or-type x.typename ss))
    (warnings
     (if
      (iff is-type is-interface)
      (fatal
       :type :vl-ambiguous-port :msg
       "~a0: Ambiguous whether this is an interface ~
                                  port because ~x1 is ~s2 an interface ~s3 a ~
                                  type name.  Making it ~s4 port."
       :args
       (if is-type (list x x.typename "both" "and" "a regular")
         (list x x.typename
               "neither" "nor" "an interface")))
      warnings))
    ((when is-type)
     (vl-ansi-portdecl-to-regularport
          x ports-acc portdecls-acc warnings)))
   (mv warnings
       (vl-ansi-portdecl-to-interfaceport x)
       nil nil))))

Theorem: vl-warninglist-p-of-vl-ansi-portdecl-resolve.warnings

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

Theorem: vl-port-p-of-vl-ansi-portdecl-resolve.port

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

Theorem: return-type-of-vl-ansi-portdecl-resolve.portdecl?

(defthm return-type-of-vl-ansi-portdecl-resolve.portdecl?
  (b* (((mv ?warnings ?port ?portdecl? ?vardecl?)
        (vl-ansi-portdecl-resolve x ports-acc
                                  portdecls-acc vardecls-acc ss)))
    (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-resolve.vardecl?

(defthm return-type-of-vl-ansi-portdecl-resolve.vardecl?
  (b* (((mv ?warnings ?port ?portdecl? ?vardecl?)
        (vl-ansi-portdecl-resolve x ports-acc
                                  portdecls-acc vardecls-acc ss)))
    (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-resolve-of-vl-ansi-portdecl-fix-x

(defthm vl-ansi-portdecl-resolve-of-vl-ansi-portdecl-fix-x
 (equal
  (vl-ansi-portdecl-resolve (vl-ansi-portdecl-fix x)
                            ports-acc portdecls-acc vardecls-acc ss)
  (vl-ansi-portdecl-resolve x ports-acc
                            portdecls-acc vardecls-acc ss)))

Theorem: vl-ansi-portdecl-resolve-vl-ansi-portdecl-equiv-congruence-on-x

(defthm
    vl-ansi-portdecl-resolve-vl-ansi-portdecl-equiv-congruence-on-x
 (implies
   (vl-ansi-portdecl-equiv x x-equiv)
   (equal (vl-ansi-portdecl-resolve
               x
               ports-acc portdecls-acc vardecls-acc ss)
          (vl-ansi-portdecl-resolve x-equiv ports-acc
                                    portdecls-acc vardecls-acc ss)))
 :rule-classes :congruence)

Theorem: vl-ansi-portdecl-resolve-of-vl-portlist-fix-ports-acc

(defthm vl-ansi-portdecl-resolve-of-vl-portlist-fix-ports-acc
  (equal (vl-ansi-portdecl-resolve x (vl-portlist-fix ports-acc)
                                   portdecls-acc vardecls-acc ss)
         (vl-ansi-portdecl-resolve x ports-acc
                                   portdecls-acc vardecls-acc ss)))

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

(defthm
 vl-ansi-portdecl-resolve-vl-portlist-equiv-congruence-on-ports-acc
 (implies
   (vl-portlist-equiv ports-acc ports-acc-equiv)
   (equal (vl-ansi-portdecl-resolve
               x
               ports-acc portdecls-acc vardecls-acc ss)
          (vl-ansi-portdecl-resolve x ports-acc-equiv
                                    portdecls-acc vardecls-acc ss)))
 :rule-classes :congruence)

Theorem: vl-ansi-portdecl-resolve-of-vl-portdecllist-fix-portdecls-acc

(defthm
      vl-ansi-portdecl-resolve-of-vl-portdecllist-fix-portdecls-acc
  (equal
       (vl-ansi-portdecl-resolve x ports-acc
                                 (vl-portdecllist-fix portdecls-acc)
                                 vardecls-acc ss)
       (vl-ansi-portdecl-resolve x ports-acc
                                 portdecls-acc vardecls-acc ss)))

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

(defthm
 vl-ansi-portdecl-resolve-vl-portdecllist-equiv-congruence-on-portdecls-acc
 (implies
  (vl-portdecllist-equiv portdecls-acc portdecls-acc-equiv)
  (equal
    (vl-ansi-portdecl-resolve
         x
         ports-acc portdecls-acc vardecls-acc ss)
    (vl-ansi-portdecl-resolve x ports-acc
                              portdecls-acc-equiv vardecls-acc ss)))
 :rule-classes :congruence)

Theorem: vl-ansi-portdecl-resolve-of-vl-vardecllist-fix-vardecls-acc

(defthm vl-ansi-portdecl-resolve-of-vl-vardecllist-fix-vardecls-acc
  (equal (vl-ansi-portdecl-resolve x ports-acc portdecls-acc
                                   (vl-vardecllist-fix vardecls-acc)
                                   ss)
         (vl-ansi-portdecl-resolve x ports-acc
                                   portdecls-acc vardecls-acc ss)))

Theorem: vl-ansi-portdecl-resolve-vl-vardecllist-equiv-congruence-on-vardecls-acc

(defthm
 vl-ansi-portdecl-resolve-vl-vardecllist-equiv-congruence-on-vardecls-acc
 (implies
  (vl-vardecllist-equiv vardecls-acc vardecls-acc-equiv)
  (equal
    (vl-ansi-portdecl-resolve
         x
         ports-acc portdecls-acc vardecls-acc ss)
    (vl-ansi-portdecl-resolve x ports-acc
                              portdecls-acc vardecls-acc-equiv ss)))
 :rule-classes :congruence)

Theorem: vl-ansi-portdecl-resolve-of-vl-scopestack-fix-ss

(defthm vl-ansi-portdecl-resolve-of-vl-scopestack-fix-ss
 (equal
      (vl-ansi-portdecl-resolve x ports-acc portdecls-acc
                                vardecls-acc (vl-scopestack-fix ss))
      (vl-ansi-portdecl-resolve x ports-acc
                                portdecls-acc vardecls-acc ss)))

Theorem: vl-ansi-portdecl-resolve-vl-scopestack-equiv-congruence-on-ss

(defthm
      vl-ansi-portdecl-resolve-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
    (vl-ansi-portdecl-resolve
         x
         ports-acc portdecls-acc vardecls-acc ss)
    (vl-ansi-portdecl-resolve x ports-acc
                              portdecls-acc vardecls-acc ss-equiv)))
 :rule-classes :congruence)