• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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-portlist-reasonable-p

(vl-portlist-reasonable-p x) determines if a vl-portlist-p is reasonable.

We just require that any externally visible names are unique. A number of additional well-formedness checks are done in argresolve and e-conversion.

Definitions and Theorems

Function: vl-portlist-reasonable-p

(defun vl-portlist-reasonable-p (x)
  (declare (xargs :guard (vl-portlist-p x)))
  (let* ((names (remove nil (vl-portlist->names x)))
         (dupes (duplicated-members names)))
    (if (not dupes) t nil)))

Function: vl-portlist-reasonable-p-warn

(defun vl-portlist-reasonable-p-warn (x warnings)
  (declare (xargs :guard (and (vl-portlist-p x)
                              (vl-warninglist-p warnings)))
           (ignorable warnings))
  (let* ((names (remove nil (vl-portlist->names x)))
         (dupes (duplicated-members names)))
    (if (not dupes)
        (mv t warnings)
      (mv nil
          (cons (make-vl-warning :type :vl-bad-ports
                                 :msg "Duplicate port names: ~&0."
                                 :args (list dupes))
                warnings)))))

Theorem: eliminate-vl-portlist-reasonable-p-warn

(defthm eliminate-vl-portlist-reasonable-p-warn
  (equal (mv-nth 0
                 (vl-portlist-reasonable-p-warn x warnings))
         (vl-portlist-reasonable-p x)))

Theorem: vl-warninglist-p-of-vl-portlist-reasonable-p-warn

(defthm vl-warninglist-p-of-vl-portlist-reasonable-p-warn
  (implies
       (force (vl-warninglist-p warnings))
       (vl-warninglist-p
            (mv-nth 1
                    (vl-portlist-reasonable-p-warn x warnings)))))