• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
        • Defwellformed
        • Reasonable
          • Vl-modulelist-check-reasonable
          • Vl-vardecl-reasonable-p
          • Vl-portdecl-and-moduleitem-compatible-p
          • Vl-module-reasonable-p
          • Vl-overlap-compatible-p
          • Vl-module-check-reasonable
          • Vl-portlist-reasonable-p
          • Vl-vardecllist-reasonable-p
          • Vl-modulelist-reasonable-p
        • Lvaluecheck
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • Svl
    • X86isa
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Reasonable

Vl-portdecl-and-moduleitem-compatible-p

Main function for checking whether a port declaration, which overlaps with some module item declaration, is a reasonable overlap.

For instance, we might have:

input x;
wire x;

Which is fine, or we might have:

input [3:0] x;
wire [4:0] x;

Which is definitely not okay. See also portdecl-sign. We expect that after parsing, the types will agree exactly.

Definitions and Theorems

Function: vl-portdecl-and-moduleitem-compatible-p

(defun vl-portdecl-and-moduleitem-compatible-p (portdecl item)
  (declare (xargs :guard (and (vl-portdecl-p portdecl)
                              (vl-moditem-p item))))
  (b* (((vl-portdecl portdecl) portdecl)
       ((unless (eq (tag item) :vl-vardecl))
        nil)
       ((vl-vardecl vardecl) item))
    (if (equal portdecl.type vardecl.type)
        t
      nil)))

Function: vl-portdecl-and-moduleitem-compatible-p-warn

(defun vl-portdecl-and-moduleitem-compatible-p-warn
       (portdecl item warnings)
 (declare (xargs :guard (and (and (vl-portdecl-p portdecl)
                                  (vl-moditem-p item))
                             (vl-warninglist-p warnings)))
          (ignorable warnings))
 (b*
  (((vl-portdecl portdecl) portdecl)
   ((unless (eq (tag item) :vl-vardecl))
    (if nil (mv t warnings)
     (mv
       nil
       (cons (make-vl-warning
                  :type :vl-weird-port
                  :msg "~a0: port ~s1 is also declared to be a ~s2."
                  :args (list portdecl portdecl.name (tag item)))
             warnings))))
   ((vl-vardecl vardecl) item))
  (if (equal portdecl.type vardecl.type)
      (mv t warnings)
   (mv
    nil
    (cons
     (make-vl-warning
      :type :vl-incompatible-port
      :msg
      "~a0: the variable declaration for port ~s1 has incompatible
                  type: ~a1 vs. ~a2."
      :args (list portdecl portdecl.type vardecl.type))
     warnings)))))

Theorem: eliminate-vl-portdecl-and-moduleitem-compatible-p-warn

(defthm eliminate-vl-portdecl-and-moduleitem-compatible-p-warn
  (equal (mv-nth 0
                 (vl-portdecl-and-moduleitem-compatible-p-warn
                      portdecl item warnings))
         (vl-portdecl-and-moduleitem-compatible-p portdecl item)))

Theorem: vl-warninglist-p-of-vl-portdecl-and-moduleitem-compatible-p-warn

(defthm
   vl-warninglist-p-of-vl-portdecl-and-moduleitem-compatible-p-warn
 (implies (force (vl-warninglist-p warnings))
          (vl-warninglist-p (mv-nth 1
                                    (vl-portdecl-and-moduleitem-compatible-p-warn
                                         portdecl item warnings)))))