• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Modinsts-to-eoccs

Vl-portlist-msb-bit-pattern

Compute the port pattern for a module.

Signature

(vl-portlist-msb-bit-pattern x walist) 
  → 
(mv successp warnings pattern)

Arguments

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

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

Returns

successp — Type (booleanp successp).

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

pattern — Type (vl-emodwirelistlist-p pattern).

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

Definitions and Theorems

Function: vl-portlist-msb-bit-pattern

(defun vl-portlist-msb-bit-pattern (x walist)
       (declare (xargs :guard (and (vl-portlist-p x)
                                   (vl-wirealist-p walist))))
       (let ((__function__ 'vl-portlist-msb-bit-pattern))
            (declare (ignorable __function__))
            (b* (((when (atom x)) (mv t nil nil))
                 ((mv successp1 warnings1 wires1)
                  (vl-port-msb-bits (car x) walist))
                 ((mv successp2 warnings2 wires2)
                  (vl-portlist-msb-bit-pattern (cdr x)
                                               walist)))
                (mv (and successp1 successp2)
                    (append-without-guard warnings1 warnings2)
                    (cons wires1 wires2)))))

Theorem: booleanp-of-vl-portlist-msb-bit-pattern.successp

(defthm booleanp-of-vl-portlist-msb-bit-pattern.successp
        (b* (((mv ?successp ?warnings ?pattern)
              (vl-portlist-msb-bit-pattern x walist)))
            (booleanp successp))
        :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-portlist-msb-bit-pattern.warnings

(defthm vl-warninglist-p-of-vl-portlist-msb-bit-pattern.warnings
        (b* (((mv ?successp ?warnings ?pattern)
              (vl-portlist-msb-bit-pattern x walist)))
            (vl-warninglist-p warnings))
        :rule-classes :rewrite)

Theorem: vl-emodwirelistlist-p-of-vl-portlist-msb-bit-pattern.pattern

(defthm vl-emodwirelistlist-p-of-vl-portlist-msb-bit-pattern.pattern
        (b* (((mv ?successp ?warnings ?pattern)
              (vl-portlist-msb-bit-pattern x walist)))
            (vl-emodwirelistlist-p pattern))
        :rule-classes :rewrite)

Theorem: true-listp-of-vl-portlist-msb-bit-pattern.pattern

(defthm true-listp-of-vl-portlist-msb-bit-pattern.pattern
        (b* (((mv ?successp ?warnings ?pattern)
              (vl-portlist-msb-bit-pattern x walist)))
            (true-listp pattern))
        :rule-classes :type-prescription)

Theorem: true-list-listp-of-vl-portlist-msb-bit-pattern.pattern

(defthm true-list-listp-of-vl-portlist-msb-bit-pattern.pattern
        (b* (((mv ?successp ?warnings ?pattern)
              (vl-portlist-msb-bit-pattern x walist)))
            (true-list-listp pattern))
        :rule-classes :rewrite)