• Top
  • Documentation
  • Books
  • 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-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
  • Math
  • Testing-utilities

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