• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
          • Vl-genblob
          • Vl-sort-genelements
          • Vl-genblob->interface
          • Vl-genblob->module
          • Vl-genblob->elems
          • Vl-interface->genblob
          • Vl-genblob->package
          • Vl-module->genblob
          • Vl-genblob->class
          • Vl-package->genblob
          • Vl-class->genblob
          • Vl-genelementlist->defaultdisables
          • Vl-genelementlist->properties
          • Vl-genelementlist->paramdecls
          • Vl-genelementlist->fwdtypedefs
          • Vl-genelementlist->dpiimports
          • Vl-genelementlist->dpiexports
          • Vl-genelementlist->covergroups
          • Vl-genelementlist->cassertions
          • Vl-genelementlist->assertions
          • Vl-genelementlist->vardecls
          • Vl-genelementlist->typedefs
          • Vl-genelementlist->taskdecls
          • Vl-genelementlist->sequences
          • Vl-genelementlist->portdecls
          • Vl-genelementlist->modports
          • Vl-genelementlist->modinsts
          • Vl-genelementlist->letdecls
          • Vl-genelementlist->initials
          • Vl-genelementlist->imports
          • Vl-genelementlist->genvars
          • Vl-genelementlist->generates
          • Vl-genelementlist->gclkdecls
          • Vl-genelementlist->gateinsts
          • Vl-genelementlist->fundecls
          • Vl-genelementlist->elabtasks
          • Vl-genelementlist->clkdecls
          • Vl-genelementlist->assigns
          • Vl-genelementlist->alwayses
          • Vl-genelementlist->finals
          • Vl-genelementlist->classes
          • Vl-genelementlist->binds
          • Vl-genelementlist->aliases
          • Vl-genblock->genblob
          • Vl-scopetype-p
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Genblob

Vl-genelementlist->defaultdisables

Signature

(vl-genelementlist->defaultdisables x) → defaultdisables

Arguments

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

Returns

defaultdisables — Type (vl-defaultdisablelist-p defaultdisables).

Definitions and Theorems

Function: vl-genelementlist->defaultdisables

(defun vl-genelementlist->defaultdisables (x)
 (declare (xargs :guard (vl-genelementlist-p x)))
 (let ((__function__ 'vl-genelementlist->defaultdisables))
  (declare (ignorable __function__))
  (b* (((when (atom x)) nil) (x1 (car x)))
    (vl-genelement-case
         x1 :vl-genbase
         (if (eq (tag x1.item) :vl-defaultdisable)
             (cons x1.item
                   (vl-genelementlist->defaultdisables (cdr x)))
           (vl-genelementlist->defaultdisables (cdr x)))
         :otherwise (vl-genelementlist->defaultdisables (cdr x))))))

Theorem: vl-defaultdisablelist-p-of-vl-genelementlist->defaultdisables

(defthm
      vl-defaultdisablelist-p-of-vl-genelementlist->defaultdisables
  (b* ((defaultdisables (vl-genelementlist->defaultdisables x)))
    (vl-defaultdisablelist-p defaultdisables))
  :rule-classes :rewrite)

Theorem: vl-sort-genelements-aux-is-vl-genelementlist->defaultdisables

(defthm
      vl-sort-genelements-aux-is-vl-genelementlist->defaultdisables
 (equal
  (mv-nth
    23
    (vl-sort-genelements-aux x portdecls assigns aliases
                             vardecls paramdecls fundecls taskdecls
                             modinsts gateinsts alwayses initials
                             finals typedefs imports fwdtypedefs
                             modports genvars assertions cassertions
                             properties sequences clkdecls
                             gclkdecls defaultdisables dpiimports
                             dpiexports binds classes covergroups
                             elabtasks letdecls generates))
  (append (rev (vl-defaultdisablelist-fix defaultdisables))
          (vl-genelementlist->defaultdisables x))))

Theorem: vl-genelementlist->defaultdisables-of-vl-genelementlist-fix-x

(defthm
      vl-genelementlist->defaultdisables-of-vl-genelementlist-fix-x
 (equal
      (vl-genelementlist->defaultdisables (vl-genelementlist-fix x))
      (vl-genelementlist->defaultdisables x)))

Theorem: vl-genelementlist->defaultdisables-vl-genelementlist-equiv-congruence-on-x

(defthm
 vl-genelementlist->defaultdisables-vl-genelementlist-equiv-congruence-on-x
 (implies (vl-genelementlist-equiv x x-equiv)
          (equal (vl-genelementlist->defaultdisables x)
                 (vl-genelementlist->defaultdisables x-equiv)))
 :rule-classes :congruence)