• 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-1

Signature

(vl-portdecl-sign-1 port var warnings) 
  → 
(mv successp warnings new-port new-var)

Arguments

port — Guard (vl-portdecl-p port).

var — Corresponding variable declaration.
    Guard (vl-vardecl-p var).

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

Returns

successp — Type (booleanp successp).

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

new-port — Type (vl-portdecl-p new-port).

new-var — Type (vl-vardecl-p new-var).

Definitions and Theorems

Function: vl-portdecl-sign-1

(defun vl-portdecl-sign-1 (port var warnings)
 (declare (xargs :guard (and (vl-portdecl-p port)
                             (vl-vardecl-p var)
                             (vl-warninglist-p warnings))))
 (declare (xargs :guard (equal (vl-portdecl->name port)
                               (vl-vardecl->name var))))
 (let ((__function__ 'vl-portdecl-sign-1))
  (declare (ignorable __function__))
  (b*
   (((vl-portdecl port)
     (vl-portdecl-fix port))
    ((vl-vardecl var) (vl-vardecl-fix var))
    ((unless (assoc-equal "VL_INCOMPLETE_DECLARATION" port.atts))
     (if (and (equal port.type var.type)
              (eq port.nettype var.nettype))
         (mv t (ok) port var)
      (mv
       nil
       (fatal
        :type :vl-programming-error
        :msg
        "~a0: mismatching types between complete port ~
                           declaration and its corresponding variable ~
                           declaration.  Port type: ~a1, variable type: ~a2."
        :args (list port port.type var.type))
       port var)))
    ((unless (eq (vl-datatype-kind port.type)
                 :vl-coretype))
     (mv
      nil
      (fatal
       :type :vl-programming-error
       :msg
       "~a0: expected basic wire types for incomplete ~
                         declaration, but found ~a1."
       :args (list port port.type))
      port var))
    ((vl-coretype port.type))
    ((mv ok warnings1 final-type)
     (if port.type.signedp
         (vl-portdecl-type-set-signed var.type var)
       (mv t nil var.type)))
    (warnings (append-without-guard warnings1
                                    (vl-warninglist-fix warnings)))
    ((unless ok) (mv nil warnings port var))
    (new-port
     (change-vl-portdecl
         port
         :atts
         (remove1-assoc-equal "VL_INCOMPLETE_DECLARATION" port.atts)
         :type final-type))
    (new-var
     (change-vl-vardecl
      var
      :atts
      (acons
         "VL_PORT_IMPLICIT" nil
         (remove1-assoc-equal "VL_INCOMPLETE_DECLARATION" var.atts))
      :type final-type)))
   (mv t (ok) new-port new-var))))

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

(defthm booleanp-of-vl-portdecl-sign-1.successp
  (b* (((mv ?successp ?warnings ?new-port ?new-var)
        (vl-portdecl-sign-1 port var warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

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

(defthm vl-warninglist-p-of-vl-portdecl-sign-1.warnings
  (b* (((mv ?successp ?warnings ?new-port ?new-var)
        (vl-portdecl-sign-1 port var warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-portdecl-p-of-vl-portdecl-sign-1.new-port

(defthm vl-portdecl-p-of-vl-portdecl-sign-1.new-port
  (b* (((mv ?successp ?warnings ?new-port ?new-var)
        (vl-portdecl-sign-1 port var warnings)))
    (vl-portdecl-p new-port))
  :rule-classes :rewrite)

Theorem: vl-vardecl-p-of-vl-portdecl-sign-1.new-var

(defthm vl-vardecl-p-of-vl-portdecl-sign-1.new-var
  (b* (((mv ?successp ?warnings ?new-port ?new-var)
        (vl-portdecl-sign-1 port var warnings)))
    (vl-vardecl-p new-var))
  :rule-classes :rewrite)

Theorem: vl-portdecl-sign-1-of-vl-portdecl-fix-port

(defthm vl-portdecl-sign-1-of-vl-portdecl-fix-port
  (equal (vl-portdecl-sign-1 (vl-portdecl-fix port)
                             var warnings)
         (vl-portdecl-sign-1 port var warnings)))

Theorem: vl-portdecl-sign-1-vl-portdecl-equiv-congruence-on-port

(defthm vl-portdecl-sign-1-vl-portdecl-equiv-congruence-on-port
  (implies (vl-portdecl-equiv port port-equiv)
           (equal (vl-portdecl-sign-1 port var warnings)
                  (vl-portdecl-sign-1 port-equiv var warnings)))
  :rule-classes :congruence)

Theorem: vl-portdecl-sign-1-of-vl-vardecl-fix-var

(defthm vl-portdecl-sign-1-of-vl-vardecl-fix-var
  (equal (vl-portdecl-sign-1 port (vl-vardecl-fix var)
                             warnings)
         (vl-portdecl-sign-1 port var warnings)))

Theorem: vl-portdecl-sign-1-vl-vardecl-equiv-congruence-on-var

(defthm vl-portdecl-sign-1-vl-vardecl-equiv-congruence-on-var
  (implies (vl-vardecl-equiv var var-equiv)
           (equal (vl-portdecl-sign-1 port var warnings)
                  (vl-portdecl-sign-1 port var-equiv warnings)))
  :rule-classes :congruence)

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

(defthm vl-portdecl-sign-1-of-vl-warninglist-fix-warnings
  (equal (vl-portdecl-sign-1 port var (vl-warninglist-fix warnings))
         (vl-portdecl-sign-1 port var warnings)))

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

(defthm
     vl-portdecl-sign-1-vl-warninglist-equiv-congruence-on-warnings
  (implies (vl-warninglist-equiv warnings warnings-equiv)
           (equal (vl-portdecl-sign-1 port var warnings)
                  (vl-portdecl-sign-1 port var warnings-equiv)))
  :rule-classes :congruence)