• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • 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-modinst-to-eocc
          • Vl-modinst-eocc-bindings
          • Vl-portdecls-to-i/o
          • Vl-plainarglist-lsb-pattern
          • Vl-modinstlist-to-eoccs
          • Vl-portlist-msb-bit-pattern
          • Vl-plainarg-lsb-bits
          • Vl-port-msb-bits
        • 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
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Modinsts-to-eoccs

Vl-portdecls-to-i/o

Compute the :i and :o fields for a module.

Signature

(vl-portdecls-to-i/o portdecls walist) 
  → 
(mv successp warnings in-wires out-wires)

Arguments

portdecls — Guard (vl-portdecllist-p portdecls).

walist — Guard (vl-wirealist-p walist).

Returns

successp — Type (booleanp successp).

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

in-wires — Type (vl-emodwirelistlist-p in-wires).

out-wires — Type (vl-emodwirelistlist-p out-wires).

We don't take a warnings accumulator because we memoize this function.

See vl-emodwirelistlist-p for some discussion about the kinds of patterns we generate.

Historic note. We originally tried to base our :i and :o patterns on the order of a module's ports. We now instead use the order of the port declarations. This is particularly nice for ports whose expressions are concatenations such as {foo, bar, baz}, since the individual components might not even have the same direction.

Definitions and Theorems

Function: vl-portdecls-to-i/o

(defun
 vl-portdecls-to-i/o (portdecls walist)
 (declare (xargs :guard (and (vl-portdecllist-p portdecls)
                             (vl-wirealist-p walist))))
 (let
  ((__function__ 'vl-portdecls-to-i/o))
  (declare (ignorable __function__))
  (b*
   (((when (atom portdecls))
     (mv t nil nil nil))
    (warnings nil)
    (decl1 (car portdecls))
    ((vl-portdecl decl1) decl1)
    ((unless (or (eq decl1.dir :vl-input)
                 (eq decl1.dir :vl-output)))
     (mv
      nil
      (fatal
         :type :vl-bad-portdecl
         :msg "~a0: port declaration has unsupported direction ~x1."
         :args (list decl1 decl1.dir))
      nil nil))
    (entry (hons-get decl1.name walist))
    ((unless (and entry
                  (mbt (vl-emodwirelist-p (cdr entry)))))
     (mv nil
         (fatal :type :vl-bad-portdecl
                :msg "~a0: no wire alist entry for ~w1."
                :args (list decl1 decl1.name))
         nil nil))
    (msb-wires (llist-fix (cdr entry)))
    (lsb-wires (reverse msb-wires))
    ((mv successp warnings in-wires out-wires)
     (vl-portdecls-to-i/o (cdr portdecls)
                          walist))
    ((unless successp)
     (mv nil warnings in-wires out-wires))
    ((mv in-wires out-wires)
     (case decl1.dir
           (:vl-input (mv (cons lsb-wires in-wires)
                          out-wires))
           (:vl-output (mv in-wires (cons lsb-wires out-wires)))
           (otherwise (prog2$ (impossible)
                              (mv in-wires out-wires))))))
   (mv t warnings in-wires out-wires))))

Theorem: booleanp-of-vl-portdecls-to-i/o.successp

(defthm booleanp-of-vl-portdecls-to-i/o.successp
        (b* (((mv ?successp
                  ?warnings ?in-wires ?out-wires)
              (vl-portdecls-to-i/o portdecls walist)))
            (booleanp successp))
        :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-portdecls-to-i/o.warnings

(defthm vl-warninglist-p-of-vl-portdecls-to-i/o.warnings
        (b* (((mv ?successp
                  ?warnings ?in-wires ?out-wires)
              (vl-portdecls-to-i/o portdecls walist)))
            (vl-warninglist-p warnings))
        :rule-classes :rewrite)

Theorem: vl-emodwirelistlist-p-of-vl-portdecls-to-i/o.in-wires

(defthm vl-emodwirelistlist-p-of-vl-portdecls-to-i/o.in-wires
        (b* (((mv ?successp
                  ?warnings ?in-wires ?out-wires)
              (vl-portdecls-to-i/o portdecls walist)))
            (vl-emodwirelistlist-p in-wires))
        :rule-classes :rewrite)

Theorem: vl-emodwirelistlist-p-of-vl-portdecls-to-i/o.out-wires

(defthm vl-emodwirelistlist-p-of-vl-portdecls-to-i/o.out-wires
        (b* (((mv ?successp
                  ?warnings ?in-wires ?out-wires)
              (vl-portdecls-to-i/o portdecls walist)))
            (vl-emodwirelistlist-p out-wires))
        :rule-classes :rewrite)

Theorem: true-listp-of-vl-portdecls-to-i/o.warnings

(defthm true-listp-of-vl-portdecls-to-i/o.warnings
        (b* (((mv ?successp
                  ?warnings ?in-wires ?out-wires)
              (vl-portdecls-to-i/o portdecls walist)))
            (true-listp warnings))
        :rule-classes :type-prescription)

Theorem: true-listp-of-vl-portdecls-to-i/o.in-wires

(defthm true-listp-of-vl-portdecls-to-i/o.in-wires
        (b* (((mv ?successp
                  ?warnings ?in-wires ?out-wires)
              (vl-portdecls-to-i/o portdecls walist)))
            (true-listp in-wires))
        :rule-classes :type-prescription)

Theorem: true-listp-of-vl-portdecls-to-i/o.out-wires

(defthm true-listp-of-vl-portdecls-to-i/o.out-wires
        (b* (((mv ?successp
                  ?warnings ?in-wires ?out-wires)
              (vl-portdecls-to-i/o portdecls walist)))
            (true-listp out-wires))
        :rule-classes :type-prescription)