• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
          • Expression-sizing
          • Occform
          • Oprewrite
          • Expand-functions
          • Delayredux
          • Unparameterization
          • Caseelim
          • Split
          • Selresolve
          • Weirdint-elim
          • Vl-delta
          • Replicate-insts
          • Rangeresolve
          • Propagate
          • Clean-selects
          • Clean-params
          • Blankargs
          • Inline-mods
          • Expr-simp
          • Trunc
          • Always-top
          • Gatesplit
          • Gate-elim
          • Expression-optimization
          • Elim-supplies
          • Wildelim
          • Drop-blankports
          • Clean-warnings
          • Addinstnames
          • Custom-transform-hooks
          • Annotate
            • Make-implicit-wires
              • Vl-modulelist-make-implicit-wires
              • Vl-make-implicit-wires-aux
              • Shadowcheck
              • Vl-stmt-check-undeclared
              • Vl-make-implicit-wires-main
              • Vl-fundecl-check-undeclared
              • Vl-warn-about-undeclared-wires
              • Vl-implicitst
              • Vl-blockitem-check-undeclared
              • Vl-taskdecl-check-undeclared
                • Vl-modinst-exprs-for-implicit-wires
                • Vl-blockitemlist-check-undeclared
                • Vl-import-check-undeclared
                • Vl-make-ordinary-implicit-wires
                • Vl-gateinst-exprs-for-implicit-wires
                • Vl-remove-declared-wires
                • Vl-make-port-implicit-wires
                • Vl-module-make-implicit-wires
                • Vl-vardecl-exprs-for-implicit-wires
                • Vl-design-make-implicit-wires
              • Resolve-indexing
              • Origexprs
              • Argresolve
              • Portdecl-sign
              • Designwires
              • Udp-elim
              • Vl-annotate-design
            • Latchcode
            • Elim-unused-vars
            • Problem-modules
          • Lint
          • Mlib
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Make-implicit-wires

    Vl-taskdecl-check-undeclared

    Check an arbitrary vl-taskdecl-p for uses of undeclared names.

    Signature
    (vl-taskdecl-check-undeclared x st warnings) → new-warnings
    Arguments
    x — Guard (vl-taskdecl-p x).
    st — Guard (vl-implicitst-p st).
    warnings — Guard (vl-warninglist-p warnings).
    Returns
    new-warnings — Type (vl-warninglist-p new-warnings).

    This is nearly identical to vl-fundecl-check-undeclared and it has the same problems with parameters.

    Definitions and Theorems

    Function: vl-taskdecl-check-undeclared

    (defun vl-taskdecl-check-undeclared (x st warnings)
     (declare (xargs :guard (and (vl-taskdecl-p x)
                                 (vl-implicitst-p st)
                                 (vl-warninglist-p warnings))))
     (let ((__function__ 'vl-taskdecl-check-undeclared))
      (declare (ignorable __function__))
      (b*
       ((x (vl-taskdecl-fix x))
        ((vl-taskdecl x) x)
        (other-names
          (vl-exprlist-varnames (vl-portdecllist-allexprs x.portdecls)))
        (warnings
             (vl-warn-about-undeclared-wires x other-names st warnings))
        (local-decls (hons-shrink-alist (vl-implicitst->decls st)
                                        nil))
        (local-imports (hons-shrink-alist (vl-implicitst->imports st)
                                          nil))
        (local-st (change-vl-implicitst st
                                        :decls local-decls
                                        :imports local-imports))
        ((mv warnings local-st)
         (vl-blockitemlist-check-undeclared
              x.blockitems local-st warnings))
        (local-decls (vl-implicitst->decls local-st))
        (local-decls
             (make-fal (pairlis$ (vl-portdecllist->names x.portdecls)
                                 nil)
                       local-decls))
        (local-st (change-vl-implicitst local-st
                                        :decls local-decls))
        (warnings
             (vl-stmt-check-undeclared x x.body local-st warnings)))
       (fast-alist-free local-decls)
       warnings)))

    Theorem: vl-warninglist-p-of-vl-taskdecl-check-undeclared

    (defthm vl-warninglist-p-of-vl-taskdecl-check-undeclared
      (b* ((new-warnings (vl-taskdecl-check-undeclared x st warnings)))
        (vl-warninglist-p new-warnings))
      :rule-classes :rewrite)

    Theorem: vl-taskdecl-check-undeclared-of-vl-taskdecl-fix-x

    (defthm vl-taskdecl-check-undeclared-of-vl-taskdecl-fix-x
      (equal (vl-taskdecl-check-undeclared (vl-taskdecl-fix x)
                                           st warnings)
             (vl-taskdecl-check-undeclared x st warnings)))

    Theorem: vl-taskdecl-check-undeclared-vl-taskdecl-equiv-congruence-on-x

    (defthm
         vl-taskdecl-check-undeclared-vl-taskdecl-equiv-congruence-on-x
      (implies
           (vl-taskdecl-equiv x x-equiv)
           (equal (vl-taskdecl-check-undeclared x st warnings)
                  (vl-taskdecl-check-undeclared x-equiv st warnings)))
      :rule-classes :congruence)

    Theorem: vl-taskdecl-check-undeclared-of-vl-implicitst-fix-st

    (defthm vl-taskdecl-check-undeclared-of-vl-implicitst-fix-st
      (equal (vl-taskdecl-check-undeclared x (vl-implicitst-fix st)
                                           warnings)
             (vl-taskdecl-check-undeclared x st warnings)))

    Theorem: vl-taskdecl-check-undeclared-vl-implicitst-equiv-congruence-on-st

    (defthm
      vl-taskdecl-check-undeclared-vl-implicitst-equiv-congruence-on-st
      (implies
           (vl-implicitst-equiv st st-equiv)
           (equal (vl-taskdecl-check-undeclared x st warnings)
                  (vl-taskdecl-check-undeclared x st-equiv warnings)))
      :rule-classes :congruence)

    Theorem: vl-taskdecl-check-undeclared-of-vl-warninglist-fix-warnings

    (defthm vl-taskdecl-check-undeclared-of-vl-warninglist-fix-warnings
     (equal
       (vl-taskdecl-check-undeclared x st (vl-warninglist-fix warnings))
       (vl-taskdecl-check-undeclared x st warnings)))

    Theorem: vl-taskdecl-check-undeclared-vl-warninglist-equiv-congruence-on-warnings

    (defthm
     vl-taskdecl-check-undeclared-vl-warninglist-equiv-congruence-on-warnings
     (implies
          (vl-warninglist-equiv warnings warnings-equiv)
          (equal (vl-taskdecl-check-undeclared x st warnings)
                 (vl-taskdecl-check-undeclared x st warnings-equiv)))
     :rule-classes :congruence)