• 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-fundecl-check-undeclared

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

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

    Function declarations are tricky because they can have their own declarations and hence we need to treat them basically like a named block statement.

    BOZO a problem with our approach is that paramterized function inputs won't exactly work, e.g., for

    function foo ;
      parameter p = 4;
      input [p-1:0] in;
      ...
    endfunction

    We will think that p is undeclared when we see in, because we aren't maintaining the mixed order of inputs and parameters.

    Well, this is a pretty obscure, so I don't want to fix it until it becomes a problem.

    Definitions and Theorems

    Function: vl-fundecl-check-undeclared

    (defun vl-fundecl-check-undeclared (x st warnings)
     (declare (xargs :guard (and (vl-fundecl-p x)
                                 (vl-implicitst-p st)
                                 (vl-warninglist-p warnings))))
     (let ((__function__ 'vl-fundecl-check-undeclared))
      (declare (ignorable __function__))
      (b*
       ((x (vl-fundecl-fix x))
        ((vl-fundecl x) x)
        (other-names (vl-exprlist-varnames
                          (append (vl-portdecllist-allexprs x.portdecls)
                                  (vl-datatype-allexprs x.rettype))))
        (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-decls (hons-acons x.name 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-fundecl-check-undeclared

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

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

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

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

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

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

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

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

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

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

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

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

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