• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
      • Transforms
        • Unparameterization
        • Elaborate
        • Addnames
        • Annotate
          • Increment-elim
          • Make-implicit-wires
            • Shadowcheck
            • Implicit-wires-minutia
            • Implicit-wires-generate-scoping
            • Vl-genbase-make-implicit-wires
            • Vl-expr-names-for-implicit
            • Vl-make-implicit-wires-main
            • Vl-implicitst
            • Vl-make-port-implicit-wires
            • Vl-import-update-implicit
            • Vl-blockitemlist-update-implicit
            • Vl-blockitem-update-implicit
            • Vl-make-ordinary-implicit-wires
            • Vl-remove-declared-wires
            • Vl-implicitsts-restore-fast-alists
            • Vl-genblock-under-cond-make-implicit-wires
            • Vl-collect-exprs-for-implicit-wires-from-namedargs
            • Vl-genblock-make-implicit-wires
            • Vl-collect-exprs-for-implicit-wires-from-portargs
            • Vl-collect-exprs-for-implicit-wires-from-namedarg
            • Vl-gateinst-exprs-for-implicit-wires
            • Vl-modinst-exprs-for-implicit-wires
            • Vl-genelementlist-make-implicit-wires
            • Vl-packagemap-find-name
          • Basic-bind-elim
          • Argresolve
          • Basicsanity
          • Portdecl-sign
          • Enum-names
          • Port-resolve
          • Udp-elim
          • Vl-annotate-design
          • Vl-annotate-module
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Make-implicit-wires

Vl-genbase-make-implicit-wires

Make implicit wires for a single modelement.

Signature

(vl-genbase-make-implicit-wires x st impitems warnings) 
  → 
(mv warnings st impitems)

Arguments

x — Base genelement to process.
    Guard (vl-genelement-p x).

st — Current state, so we can tell what is declared.
    Guard (vl-implicitst-p st).

impitems — Accumulator for implicit variable declarations.
    Guard (vl-vardecllist-p impitems).

warnings — Guard (vl-warninglist-p warnings).

Returns

warnings — Type (vl-warninglist-p warnings).

st — Type (vl-implicitst-p st).

impitems — Type (vl-vardecllist-p impitems).

Definitions and Theorems

Function: vl-genbase-make-implicit-wires

(defun vl-genbase-make-implicit-wires (x st impitems warnings)
 (declare (xargs :guard (and (vl-genelement-p x)
                             (vl-implicitst-p st)
                             (vl-vardecllist-p impitems)
                             (vl-warninglist-p warnings))))
 (declare (xargs :guard (vl-genelement-case x :vl-genbase)))
 (let ((__function__ 'vl-genbase-make-implicit-wires))
  (declare (ignorable __function__))
  (b*
   ((x (vl-genelement-fix x))
    (st (vl-implicitst-fix st))
    (impitems (vl-vardecllist-fix impitems))
    (item (vl-genbase->item x))
    (tag (tag item))
    ((when (or (eq tag :vl-interfaceport)
               (eq tag :vl-regularport)))
     (mv (fatal :type :vl-programming-error
                :msg "~a0: unexpected kind of module item."
                :args (list item))
         st impitems))
    ((when (eq tag :vl-portdecl))
     (b*
       ((declname (vl-portdecl->name item))
        (portdecls (hons-acons declname
                               item (vl-implicitst->portdecls st)))
        (st (change-vl-implicitst st
                                  :portdecls portdecls)))
       (mv (ok) st impitems)))
    ((when (or (eq tag :vl-vardecl)
               (eq tag :vl-paramdecl)
               (eq tag :vl-import)))
     (b* (((mv warnings st)
           (vl-blockitem-update-implicit item st warnings)))
       (mv warnings st impitems)))
    ((when (or (eq tag :vl-modinst)
               (eq tag :vl-gateinst)))
     (b* (((mv loc port-exprs maybe-name)
           (if (eq tag :vl-modinst)
               (mv (vl-modinst->loc item)
                   (vl-modinst-exprs-for-implicit-wires item)
                   (vl-modinst->instname item))
             (mv (vl-gateinst->loc item)
                 (vl-gateinst-exprs-for-implicit-wires item)
                 (vl-gateinst->name item))))
          (port-names (vl-exprlist-names-for-implicit port-exprs))
          (imp-names
               (mergesort (vl-remove-declared-wires port-names st)))
          (imp-nets (vl-make-ordinary-implicit-wires loc imp-names))
          (decls (vl-implicitst->decls st))
          (decls (make-fal (pairlis$ imp-names nil)
                           decls))
          (decls (if maybe-name (hons-acons maybe-name nil decls)
                   decls))
          (st (change-vl-implicitst st :decls decls))
          (impitems (append imp-nets impitems)))
       (mv (ok) st impitems)))
    ((when (eq tag :vl-assign))
     (b* (((vl-assign item))
          (lhs-names (vl-expr-names-for-implicit item.lvalue))
          (imp-names
               (mergesort (vl-remove-declared-wires lhs-names st)))
          (imp-nets
               (vl-make-ordinary-implicit-wires item.loc imp-names))
          (decls (vl-implicitst->decls st))
          (decls (make-fal (pairlis$ imp-names nil)
                           decls))
          (st (change-vl-implicitst st :decls decls))
          (impitems (append imp-nets impitems)))
       (mv (ok) st impitems)))
    ((when (eq tag :vl-alias))
     (b*
      (((vl-alias item) item)
       (lhs-names (vl-expr-names-for-implicit item.lhs))
       (rhs-names (vl-expr-names-for-implicit item.rhs))
       (imp-names
         (mergesort
              (vl-remove-declared-wires (append lhs-names rhs-names)
                                        st)))
       (imp-nets
            (vl-make-ordinary-implicit-wires item.loc imp-names))
       (warnings
        (if (not imp-names)
            (ok)
         (warn
          :type :vl-tricky-implicit
          :msg
          "~a0: wire~s1 ~&2 ~s3 implicitly ~
                                      declared by this alias declaration."
          :args (list item (if (vl-plural-p imp-names) "s" "")
                      imp-names
                      (if (vl-plural-p imp-names)
                          "are"
                        "is")))))
       (decls (vl-implicitst->decls st))
       (decls (make-fal (pairlis$ imp-names nil)
                        decls))
       (st (change-vl-implicitst st :decls decls))
       (impitems (append imp-nets impitems)))
      (mv warnings st impitems)))
    ((when (or (eq tag :vl-initial)
               (eq tag :vl-final)
               (eq tag :vl-always)
               (eq tag :vl-dpiexport)
               (eq tag :vl-clkdecl)
               (eq tag :vl-gclkdecl)
               (eq tag :vl-defaultdisable)
               (eq tag :vl-bind)
               (eq tag :vl-class)
               (eq tag :vl-covergroup)
               (eq tag :vl-elabtask)))
     (mv (ok) st impitems))
    ((when (or (eq tag :vl-fundecl)
               (eq tag :vl-taskdecl)
               (eq tag :vl-dpiimport)
               (eq tag :vl-assertion)
               (eq tag :vl-cassertion)
               (eq tag :vl-property)
               (eq tag :vl-sequence)
               (eq tag :vl-typedef)
               (eq tag :vl-fwdtypedef)
               (eq tag :vl-genvar)
               (eq tag :vl-modport)
               (eq tag :vl-letdecl)))
     (b* ((name (case tag
                      (:vl-fundecl (vl-fundecl->name item))
                      (:vl-taskdecl (vl-taskdecl->name item))
                      (:vl-dpiimport (vl-dpiimport->name item))
                      (:vl-assertion (vl-assertion->name item))
                      (:vl-cassertion (vl-cassertion->name item))
                      (:vl-property (vl-property->name item))
                      (:vl-sequence (vl-sequence->name item))
                      (:vl-typedef (vl-typedef->name item))
                      (:vl-fwdtypedef (vl-fwdtypedef->name item))
                      (:vl-genvar (vl-genvar->name item))
                      (:vl-modport (vl-modport->name item))
                      (:vl-letdecl (vl-letdecl->name item))))
          (decls (hons-acons name nil (vl-implicitst->decls st)))
          (st (change-vl-implicitst st :decls decls)))
       (mv (ok) st impitems))))
   (impossible)
   (mv (ok) st impitems))))

Theorem: vl-warninglist-p-of-vl-genbase-make-implicit-wires.warnings

(defthm vl-warninglist-p-of-vl-genbase-make-implicit-wires.warnings
  (b* (((mv ?warnings ?st ?impitems)
        (vl-genbase-make-implicit-wires x st impitems warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-implicitst-p-of-vl-genbase-make-implicit-wires.st

(defthm vl-implicitst-p-of-vl-genbase-make-implicit-wires.st
  (b* (((mv ?warnings ?st ?impitems)
        (vl-genbase-make-implicit-wires x st impitems warnings)))
    (vl-implicitst-p st))
  :rule-classes :rewrite)

Theorem: vl-vardecllist-p-of-vl-genbase-make-implicit-wires.impitems

(defthm vl-vardecllist-p-of-vl-genbase-make-implicit-wires.impitems
  (b* (((mv ?warnings ?st ?impitems)
        (vl-genbase-make-implicit-wires x st impitems warnings)))
    (vl-vardecllist-p impitems))
  :rule-classes :rewrite)

Theorem: vl-genbase-make-implicit-wires-of-vl-genelement-fix-x

(defthm vl-genbase-make-implicit-wires-of-vl-genelement-fix-x
  (equal (vl-genbase-make-implicit-wires (vl-genelement-fix x)
                                         st impitems warnings)
         (vl-genbase-make-implicit-wires x st impitems warnings)))

Theorem: vl-genbase-make-implicit-wires-vl-genelement-equiv-congruence-on-x

(defthm
 vl-genbase-make-implicit-wires-vl-genelement-equiv-congruence-on-x
 (implies
  (vl-genelement-equiv x x-equiv)
  (equal
     (vl-genbase-make-implicit-wires x st impitems warnings)
     (vl-genbase-make-implicit-wires x-equiv st impitems warnings)))
 :rule-classes :congruence)

Theorem: vl-genbase-make-implicit-wires-of-vl-implicitst-fix-st

(defthm vl-genbase-make-implicit-wires-of-vl-implicitst-fix-st
  (equal (vl-genbase-make-implicit-wires x (vl-implicitst-fix st)
                                         impitems warnings)
         (vl-genbase-make-implicit-wires x st impitems warnings)))

Theorem: vl-genbase-make-implicit-wires-vl-implicitst-equiv-congruence-on-st

(defthm
 vl-genbase-make-implicit-wires-vl-implicitst-equiv-congruence-on-st
 (implies
  (vl-implicitst-equiv st st-equiv)
  (equal
     (vl-genbase-make-implicit-wires x st impitems warnings)
     (vl-genbase-make-implicit-wires x st-equiv impitems warnings)))
 :rule-classes :congruence)

Theorem: vl-genbase-make-implicit-wires-of-vl-vardecllist-fix-impitems

(defthm
      vl-genbase-make-implicit-wires-of-vl-vardecllist-fix-impitems
 (equal
  (vl-genbase-make-implicit-wires x st (vl-vardecllist-fix impitems)
                                  warnings)
  (vl-genbase-make-implicit-wires x st impitems warnings)))

Theorem: vl-genbase-make-implicit-wires-vl-vardecllist-equiv-congruence-on-impitems

(defthm
 vl-genbase-make-implicit-wires-vl-vardecllist-equiv-congruence-on-impitems
 (implies
  (vl-vardecllist-equiv impitems impitems-equiv)
  (equal
     (vl-genbase-make-implicit-wires x st impitems warnings)
     (vl-genbase-make-implicit-wires x st impitems-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-genbase-make-implicit-wires-of-vl-warninglist-fix-warnings

(defthm
      vl-genbase-make-implicit-wires-of-vl-warninglist-fix-warnings
  (equal (vl-genbase-make-implicit-wires
              x st
              impitems (vl-warninglist-fix warnings))
         (vl-genbase-make-implicit-wires x st impitems warnings)))

Theorem: vl-genbase-make-implicit-wires-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-genbase-make-implicit-wires-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
     (vl-genbase-make-implicit-wires x st impitems warnings)
     (vl-genbase-make-implicit-wires x st impitems warnings-equiv)))
 :rule-classes :congruence)