• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • 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-genblob->interface

    Install fields from a vl-genblob into a interface.

    Signature
    (vl-genblob->interface x orig) → new-mod
    Arguments
    x — Guard (vl-genblob-p x).
    orig — Guard (vl-interface-p orig).
    Returns
    new-mod — Type (vl-interface-p new-mod).

    See vl-interface->genblob. This is the companion operation which takes the fields from the genblob and sticks them back into a interface.

    Certain fields of the interface, like its warnings, name, and location information, aren't affected. But the real fields like modinsts, assigns, etc., are overwritten with whatever is in the genblob.

    Definitions and Theorems

    Function: vl-genblob->interface

    (defun vl-genblob->interface (x orig)
      (declare (xargs :guard (and (vl-genblob-p x)
                                  (vl-interface-p orig))))
      (let ((__function__ 'vl-genblob->interface))
        (declare (ignorable __function__))
        (b* (((vl-genblob x)))
          (change-vl-interface orig
                               :generates x.generates
                               :ports x.ports
                               :portdecls x.portdecls
                               :assigns x.assigns
                               :aliases x.aliases
                               :vardecls x.vardecls
                               :paramdecls x.paramdecls
                               :fundecls x.fundecls
                               :taskdecls x.taskdecls
                               :modinsts x.modinsts
                               :alwayses x.alwayses
                               :initials x.initials
                               :finals x.finals
                               :typedefs x.typedefs
                               :imports x.imports
                               :modports x.modports
                               :genvars x.genvars
                               :assertions x.assertions
                               :cassertions x.cassertions
                               :properties x.properties
                               :sequences x.sequences
                               :clkdecls x.clkdecls
                               :gclkdecls x.gclkdecls
                               :defaultdisables x.defaultdisables
                               :dpiimports x.dpiimports
                               :dpiexports x.dpiexports
                               :binds x.binds
                               :classes x.classes
                               :elabtasks x.elabtasks))))

    Theorem: vl-interface-p-of-vl-genblob->interface

    (defthm vl-interface-p-of-vl-genblob->interface
      (b* ((new-mod (vl-genblob->interface x orig)))
        (vl-interface-p new-mod))
      :rule-classes :rewrite)

    Theorem: vl-genblob->interface-of-vl-genblob-fix-x

    (defthm vl-genblob->interface-of-vl-genblob-fix-x
      (equal (vl-genblob->interface (vl-genblob-fix x)
                                    orig)
             (vl-genblob->interface x orig)))

    Theorem: vl-genblob->interface-vl-genblob-equiv-congruence-on-x

    (defthm vl-genblob->interface-vl-genblob-equiv-congruence-on-x
      (implies (vl-genblob-equiv x x-equiv)
               (equal (vl-genblob->interface x orig)
                      (vl-genblob->interface x-equiv orig)))
      :rule-classes :congruence)

    Theorem: vl-genblob->interface-of-vl-interface-fix-orig

    (defthm vl-genblob->interface-of-vl-interface-fix-orig
      (equal (vl-genblob->interface x (vl-interface-fix orig))
             (vl-genblob->interface x orig)))

    Theorem: vl-genblob->interface-vl-interface-equiv-congruence-on-orig

    (defthm vl-genblob->interface-vl-interface-equiv-congruence-on-orig
      (implies (vl-interface-equiv orig orig-equiv)
               (equal (vl-genblob->interface x orig)
                      (vl-genblob->interface x orig-equiv)))
      :rule-classes :congruence)