• 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-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

• E-conversion

Vl-modulelist-make-esims

Extend vl-module-make-esim across a list of modules.

Signature

(vl-modulelist-make-esims x mods modalist eal) 
  → 
(mv new-x eal)

Arguments

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

mods — Guard (vl-modulelist-p mods).

modalist — Guard (equal modalist (vl-modalist mods)).

eal — Guard (vl-ealist-p eal).

Returns

new-x — Type (vl-modulelist-p new-x), given (force (vl-modulelist-p x)).

eal — Type (vl-ealist-p eal), given (and (vl-modulelist-p x) (vl-ealist-p eal)).

Definitions and Theorems

Function: vl-modulelist-make-esims

(defun
  vl-modulelist-make-esims
  (x mods modalist eal)
  (declare (xargs :guard (and (vl-modulelist-p x)
                              (vl-modulelist-p mods)
                              (vl-ealist-p eal)
                              (equal modalist (vl-modalist mods)))))
  (let ((__function__ 'vl-modulelist-make-esims))
       (declare (ignorable __function__))
       (b* (((when (atom x)) (mv nil eal))
            ((mv car eal)
             (vl-module-make-esim (car x)
                                  mods modalist eal))
            ((mv cdr eal)
             (vl-modulelist-make-esims (cdr x)
                                       mods modalist eal)))
           (mv (cons car cdr) eal))))

Theorem: vl-modulelist-p-of-vl-modulelist-make-esims.new-x

(defthm
     vl-modulelist-p-of-vl-modulelist-make-esims.new-x
     (implies (force (vl-modulelist-p x))
              (b* (((mv ?new-x ?eal)
                    (vl-modulelist-make-esims x mods modalist eal)))
                  (vl-modulelist-p new-x)))
     :rule-classes :rewrite)

Theorem: vl-ealist-p-of-vl-modulelist-make-esims.eal

(defthm
     vl-ealist-p-of-vl-modulelist-make-esims.eal
     (implies (and (vl-modulelist-p x)
                   (vl-ealist-p eal))
              (b* (((mv ?new-x ?eal)
                    (vl-modulelist-make-esims x mods modalist eal)))
                  (vl-ealist-p eal)))
     :rule-classes :rewrite)

Theorem: vl-modulelist-make-esims-mvtypes-0

(defthm
     vl-modulelist-make-esims-mvtypes-0
     (true-listp
          (mv-nth 0
                  (vl-modulelist-make-esims x mods modalist eal)))
     :rule-classes :type-prescription)

Theorem: vl-modulelist->names-of-vl-modulelist-make-esims

(defthm vl-modulelist->names-of-vl-modulelist-make-esims
        (let ((ret (vl-modulelist-make-esims x mods modalist eal)))
             (equal (vl-modulelist->names (mv-nth 0 ret))
                    (vl-modulelist->names x))))