• 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-modinstlist-to-eoccs

Build the preliminary E-language occurrences for a list of module instances.

Signature

(vl-modinstlist-to-eoccs x walist mods modalist eal warnings) 
  → 
(mv successp warnings eoccs)

Arguments

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

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

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

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

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

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

Returns

successp — Type (booleanp successp).

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

We just extend vl-modinst-to-eocc across a list.

Definitions and Theorems

Function: vl-modinstlist-to-eoccs

(defun
 vl-modinstlist-to-eoccs
 (x walist mods modalist eal warnings)
 (declare (xargs :guard (and (vl-modinstlist-p x)
                             (vl-wirealist-p walist)
                             (vl-modulelist-p mods)
                             (vl-ealist-p eal)
                             (vl-warninglist-p warnings)
                             (equal modalist (vl-modalist mods)))))
 (let
  ((__function__ 'vl-modinstlist-to-eoccs))
  (declare (ignorable __function__))
  (b*
     (((when (atom x)) (mv t (ok) nil))
      ((mv car-successp warnings car-eocc)
       (vl-modinst-to-eocc (car x)
                           walist mods modalist eal warnings))
      ((mv cdr-successp warnings cdr-eoccs)
       (vl-modinstlist-to-eoccs (cdr x)
                                walist mods modalist eal warnings)))
     (mv (and car-successp cdr-successp)
         warnings (cons car-eocc cdr-eoccs)))))

Theorem: booleanp-of-vl-modinstlist-to-eoccs.successp

(defthm
 booleanp-of-vl-modinstlist-to-eoccs.successp
 (b*
   (((mv ?successp ?warnings ?eoccs)
     (vl-modinstlist-to-eoccs x walist mods modalist eal warnings)))
   (booleanp successp))
 :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-modinstlist-to-eoccs.warnings

(defthm
 vl-warninglist-p-of-vl-modinstlist-to-eoccs.warnings
 (b*
   (((mv ?successp ?warnings ?eoccs)
     (vl-modinstlist-to-eoccs x walist mods modalist eal warnings)))
   (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: true-listp-of-vl-modinstlist-to-eoccs.eoccs

(defthm
 true-listp-of-vl-modinstlist-to-eoccs.eoccs
 (b*
   (((mv ?successp ?warnings ?eoccs)
     (vl-modinstlist-to-eoccs x walist mods modalist eal warnings)))
   (true-listp eoccs))
 :rule-classes :type-prescription)

Theorem: good-esim-occsp-of-vl-modinstlist-to-eoccs

(defthm
 good-esim-occsp-of-vl-modinstlist-to-eoccs
 (let
  ((ret
     (vl-modinstlist-to-eoccs x walist mods modalist eal warnings)))
  (implies (and (mv-nth 0 ret)
                (force (vl-modinstlist-p x))
                (force (vl-wirealist-p walist))
                (force (vl-modulelist-p mods))
                (force (equal modalist (vl-modalist mods)))
                (force (vl-ealist-p eal)))
           (good-esim-occsp (mv-nth 2 ret)))))