• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
        • Vl-ealist-p
        • Modinsts-to-eoccs
        • Vl-module-make-esim
        • Exploding-vectors
        • Resolving-multiple-drivers
        • Vl-modulelist-make-esims
        • Vl-module-check-e-ok
        • Vl-collect-design-wires
        • Adding-z-drivers
        • Vl-design-to-e
        • Vl-design-to-e-check-ports
        • Vl-design-to-e-main
        • Port-bit-checking
          • Vl-modulelist-check-port-bits
          • Vl-module-check-port-bits
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Port-bit-checking

Vl-module-check-port-bits

Ensure the port pattern for a module is reasonable.

Signature

(vl-module-check-port-bits x) → new-x

Arguments

x — Guard (vl-module-p x).

Returns

new-x — Type (and (vl-module-p new-x) (equal (vl-module->name new-x) (vl-module->name x))) .

(vl-module-check-port-bits x) separately builds up the bit patterns for ports and the port declarations of the module x, then makes sure that there is exactly one port bit for every port declaration bit and vice versa. We extend X with a fatal warning if this doesn't hold.

Definitions and Theorems

Function: vl-module-check-port-bits

(defun vl-module-check-port-bits (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-module-check-port-bits))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) (vl-module-fix x))
    (warnings x.warnings)
    ((mv successp warnings walist)
     (vl-module-wirealist x warnings))
    ((unless successp)
     (change-vl-module x :warnings warnings))
    ((with-fast walist))
    ((mv okp1 warnings1 port-bits)
     (vl-portlist-msb-bit-pattern x.ports walist))
    ((mv okp2 warnings2 in-wires out-wires)
     (vl-portdecls-to-i/o x.portdecls walist))
    (warnings (append-without-guard warnings1 warnings2 x.warnings))
    ((unless (and okp1 okp2))
     (change-vl-module x :warnings warnings))
    (flat-ports (flatten port-bits))
    (flat-ports-s (mergesort flat-ports))
    (flat-ins (flatten in-wires))
    (flat-outs (flatten out-wires))
    (flat-ins-s (mergesort flat-ins))
    (flat-outs-s (mergesort flat-outs))
    (flat-decls-s (union flat-ins-s flat-outs-s))
    (warnings
     (b*
      (((when
         (mbe
          :logic (uniquep (append flat-ins flat-outs))
          :exec
          (and
           (mbe :logic (uniquep flat-ins)
                :exec (same-lengthp flat-ins-s flat-ins))
           (mbe :logic (uniquep flat-outs)
                :exec (same-lengthp flat-outs-s flat-outs))
           (mbe
            :logic (not (intersectp-equal flat-ins flat-outs))
            :exec (not (set::intersectp flat-ins-s flat-outs-s))))))
        warnings)
       (dupe-names
          (duplicated-members (vl-portdecllist->names x.portdecls)))
       ((when dupe-names)
        (fatal
         :type :vl-bad-portdecls
         :msg
         "The following ports are illegally declared more ~
                           than once: ~&0."
         :args (list dupe-names)))
       (dupe-bits (duplicated-members (append flat-ins flat-outs))))
      (fatal
       :type :vl-programming-error
       :msg
       "Failed to generate unique port bit names even though ~
                       the port decls have unique names.  Jared thinks this ~
                       should be impossible unless the wire alist is invalid. ~
                       Duplicate bits: ~&0."
       :args (list (vl-verilogify-emodwirelist dupe-bits)))))
    (warnings
     (b* (((when (mbe :logic (uniquep flat-ports)
                      :exec (same-lengthp flat-ports-s flat-ports)))
           warnings)
          (dupe-bits (duplicated-members flat-ports)))
      (fatal
       :type :vl-bad-ports
       :msg
       "The following wires are directly connected to multiple ~
                       ports: ~&0."
       :args (list (vl-verilogify-emodwirelist dupe-bits)))))
    (warnings
     (b* (((when (equal flat-decls-s flat-ports-s))
           warnings)
          (extra-port-bits (difference flat-ports-s flat-decls-s))
          (extra-decl-bits (difference flat-decls-s flat-ports-s)))
      (fatal
       :type :vl-bad-ports
       :msg
       "Mismatch between the ports and port declarations:~%  ~
                        - Bits only in ports: ~&0~%  ~
                        - Bits only in port declarations: ~&1"
       :args (list (vl-verilogify-emodwirelist extra-port-bits)
                   (vl-verilogify-emodwirelist extra-decl-bits)))))
    ((when (equal x.warnings warnings)) x))
   (change-vl-module x
                     :warnings warnings))))

Theorem: return-type-of-vl-module-check-port-bits

(defthm return-type-of-vl-module-check-port-bits
  (b* ((new-x (vl-module-check-port-bits x)))
    (and (vl-module-p new-x)
         (equal (vl-module->name new-x)
                (vl-module->name x))))
  :rule-classes :rewrite)