• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
          • Vl-module
          • Vl-vardecl
          • Expressions
          • Vl-fundecl
          • Vl-assign
          • Vl-gateinst
          • Vl-modinst
          • Vl-commentmap
          • Vl-portdecl
          • Vl-taskdecl
          • Vl-design
          • Vl-interface
          • Vl-plainarglist->exprs
          • Vl-taskdecllist->names
          • Vl-fundecllist->names
          • Vl-package
          • Vl-port
          • Vl-udp
          • Vl-paramdecl
          • Vl-genelement
          • Vl-cycledelayrange
          • Vl-namedarg
          • Vl-sort-blockitems-aux
          • Vl-distitem
          • Vl-gatedelay
          • Vl-repetition
          • Vl-typedef
          • Vl-range
          • Vl-gatestrength
          • Vl-program
          • Vl-config
          • Vl-always
          • Vl-datatype-update-dims
          • Vl-import
          • Vl-enumbasetype
          • Vl-repeateventcontrol
          • Vl-paramargs
          • Vl-initial
          • Vl-eventcontrol
          • Vl-udpsymbol-p
          • Vl-maybe-range
          • Vl-maybe-nettypename
          • Vl-maybe-gatestrength
          • Vl-maybe-gatedelay
          • Vl-maybe-delayoreventcontrol
          • Vl-alias
          • Maybe-string-fix
          • Vl-maybe-packeddimension
          • Vl-fwdtypedef
          • Vl-evatom
          • Vl-packeddimension-p
          • Vl-maybe-udpsymbol
          • Vl-maybe-module
          • Vl-maybe-direction
          • Vl-maybe-datatype
          • Vl-maybe-cstrength
          • Vl-direction-p
          • Vl-arguments
          • Vl-maybe-design
          • Vl-udpline
          • Vl-exprdist
          • Vl-context1
          • Vl-genvar
          • Vl-enumitem
          • Vl-datatype-update-udims
          • Vl-datatype-update-pdims
          • Vl-modelement
          • Vl-udpedge
          • Vl-delaycontrol
          • Vl-context
          • Vl-sort-blockitems
          • Vl-distweighttype-p
          • Vl-ctxelement->loc
          • Vl-blockitem
            • Vl-blockitem-fix
              • Vl-blockitem-p
              • Vl-blockitem-equiv
            • Vl-vardecllist
            • Vl-module->ifports
            • Vl-modelement->loc
            • Vl-ctxelement
            • Vl-coretypename-p
            • Vl-packeddimensionlist
            • Vl-modelementlist->genelements
            • Vl-gatetype-p
            • Vl-paramdecllist
            • Vl-lifetime-p
            • Vl-datatype->udims
            • Vl-datatype->pdims
            • Vl-timeunit-p
            • Vl-repetitiontype-p
            • Vl-port->name
            • Vl-importlist
            • Vl-genelement->loc
            • Vl-delayoreventcontrol
            • Vl-cstrength-p
            • Statements
            • Vl-udpentry-p
            • Vl-packeddimension-fix
            • Vl-nettypename-p
            • Vl-portdecllist
            • Vl-port->loc
            • Vl-enumbasekind-fix
            • Vl-arguments->args
            • Vl-taskdecllist
            • Vl-portlist
            • Vl-importpart-p
            • Vl-importpart-fix
            • Vl-fundecllist
            • Vl-blockstmt-p
            • Vl-assignlist
            • Vl-alwaystype-p
            • Vl-typedeflist
            • Vl-syntaxversion-p
            • Vl-randomqualifier-p
            • Vl-modinstlist
            • Vl-gateinstlist
            • Vl-blockitemlist
            • Vl-udptable
            • Vl-udplist
            • Vl-udpentrylist
            • Vl-programlist
            • Vl-paramvaluelist
            • Vl-packagelist
            • Vl-namedparamvaluelist
            • Vl-namedarglist
            • Vl-modulelist
            • Vl-modportlist
            • Vl-modport-portlist
            • Vl-interfacelist
            • Vl-initiallist
            • Vl-genvarlist
            • Vl-fwdtypedeflist
            • Vl-evatomlist
            • Vl-enumitemlist
            • Vl-distlist
            • Vl-configlist
            • Vl-alwayslist
            • Vl-aliaslist
            • Vl-regularportlist
            • Vl-rangelist-list
            • Vl-rangelist
            • Vl-paramdecllist-list
            • Vl-modelementlist
            • Vl-maybe-range-list
            • Vl-interfaceportlist
            • Vl-argumentlist
            • Data-types
          • Getting-started
          • Utilities
          • Loader
          • Transforms
          • Lint
          • Mlib
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-blockitem

    Vl-blockitem-fix

    (vl-blockitem-fix x) is a ACL2::fty fixing function.

    Signature
    (vl-blockitem-fix x) → fty::newx
    Arguments
    x — Guard (vl-blockitem-p x).
    Returns
    fty::newx — Type (vl-blockitem-p fty::newx).

    Note that in the execution this is just an inline identity function.

    Definitions and Theorems

    Function: vl-blockitem-fix$inline

    (defun vl-blockitem-fix$inline (x)
      (declare (xargs :guard (vl-blockitem-p x)))
      (let ((__function__ 'vl-blockitem-fix))
        (declare (ignorable __function__))
        (mbe :logic
             (common-lisp::case (tag x)
               ((:vl-vardecl) (vl-vardecl-fix x))
               ((:vl-paramdecl) (vl-paramdecl-fix x))
               (otherwise (vl-import-fix x)))
             :exec x)))

    Theorem: vl-blockitem-p-of-vl-blockitem-fix

    (defthm vl-blockitem-p-of-vl-blockitem-fix
      (b* ((fty::newx (vl-blockitem-fix$inline x)))
        (vl-blockitem-p fty::newx))
      :rule-classes :rewrite)

    Theorem: vl-blockitem-fix-when-vl-blockitem-p

    (defthm vl-blockitem-fix-when-vl-blockitem-p
      (implies (vl-blockitem-p x)
               (equal (vl-blockitem-fix x) x)))

    Function: vl-blockitem-equiv$inline

    (defun vl-blockitem-equiv$inline (acl2::x acl2::y)
      (declare (xargs :guard (and (vl-blockitem-p acl2::x)
                                  (vl-blockitem-p acl2::y))))
      (equal (vl-blockitem-fix acl2::x)
             (vl-blockitem-fix acl2::y)))

    Theorem: vl-blockitem-equiv-is-an-equivalence

    (defthm vl-blockitem-equiv-is-an-equivalence
      (and (booleanp (vl-blockitem-equiv x y))
           (vl-blockitem-equiv x x)
           (implies (vl-blockitem-equiv x y)
                    (vl-blockitem-equiv y x))
           (implies (and (vl-blockitem-equiv x y)
                         (vl-blockitem-equiv y z))
                    (vl-blockitem-equiv x z)))
      :rule-classes (:equivalence))

    Theorem: vl-blockitem-equiv-implies-equal-vl-blockitem-fix-1

    (defthm vl-blockitem-equiv-implies-equal-vl-blockitem-fix-1
      (implies (vl-blockitem-equiv acl2::x x-equiv)
               (equal (vl-blockitem-fix acl2::x)
                      (vl-blockitem-fix x-equiv)))
      :rule-classes (:congruence))

    Theorem: vl-blockitem-fix-under-vl-blockitem-equiv

    (defthm vl-blockitem-fix-under-vl-blockitem-equiv
      (vl-blockitem-equiv (vl-blockitem-fix acl2::x)
                          acl2::x)
      :rule-classes (:rewrite :rewrite-quoted-constant))

    Theorem: equal-of-vl-blockitem-fix-1-forward-to-vl-blockitem-equiv

    (defthm equal-of-vl-blockitem-fix-1-forward-to-vl-blockitem-equiv
      (implies (equal (vl-blockitem-fix acl2::x)
                      acl2::y)
               (vl-blockitem-equiv acl2::x acl2::y))
      :rule-classes :forward-chaining)

    Theorem: equal-of-vl-blockitem-fix-2-forward-to-vl-blockitem-equiv

    (defthm equal-of-vl-blockitem-fix-2-forward-to-vl-blockitem-equiv
      (implies (equal acl2::x (vl-blockitem-fix acl2::y))
               (vl-blockitem-equiv acl2::x acl2::y))
      :rule-classes :forward-chaining)

    Theorem: vl-blockitem-equiv-of-vl-blockitem-fix-1-forward

    (defthm vl-blockitem-equiv-of-vl-blockitem-fix-1-forward
      (implies (vl-blockitem-equiv (vl-blockitem-fix acl2::x)
                                   acl2::y)
               (vl-blockitem-equiv acl2::x acl2::y))
      :rule-classes :forward-chaining)

    Theorem: vl-blockitem-equiv-of-vl-blockitem-fix-2-forward

    (defthm vl-blockitem-equiv-of-vl-blockitem-fix-2-forward
      (implies (vl-blockitem-equiv acl2::x (vl-blockitem-fix acl2::y))
               (vl-blockitem-equiv acl2::x acl2::y))
      :rule-classes :forward-chaining)

    Theorem: tag-of-vl-blockitem-fix-forward

    (defthm tag-of-vl-blockitem-fix-forward
      (or (equal (tag (vl-blockitem-fix x))
                 :vl-vardecl)
          (equal (tag (vl-blockitem-fix x))
                 :vl-paramdecl)
          (equal (tag (vl-blockitem-fix x))
                 :vl-import))
      :rule-classes
      ((:forward-chaining :trigger-terms ((tag (vl-blockitem-fix x))))))