		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-describe

Prints out the definition of name (wherever it can be found in the scopestack) and uses of it in the current module.

Signature
(vl-pp-describe name x ss &key (ps 'ps)) → ps
Arguments: name — Guard (stringp name).; x — Guard (vl-genblob-p x).; ss — design level.
Guard (vl-scopestack-p ss).

Definitions and Theorems

Function: vl-pp-describe-fn

(defun vl-pp-describe-fn (name x ss ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (and (stringp name)
                             (vl-genblob-p x)
                             (vl-scopestack-p ss))))
 (let ((__function__ 'vl-pp-describe))
  (declare (ignorable __function__))
  (b*
   (((vl-genblob x) x)
    (some-uses-will-not-be-displayed-p
     (b*
      ((x-prime (change-vl-genblob x
                                   :modinsts nil
                                   :assigns nil
                                   :ports nil
                                   :portdecls nil
                                   :gateinsts nil))
       (others (vl-exprlist-descvarnames
                    (with-local-nrev
                         (vl-genblob-allexprs-nrev x-prime nrev)))))
      (member-equal name others)))
    (htmlp (vl-ps->htmlp))
    (ps
      (if some-uses-will-not-be-displayed-p
       (vl-ps-seq (vl-when-html (vl-print-markup "<h4>"))
                  (vl-print "Warning: some uses are not displayed!")
                  (vl-when-html (vl-print-markup "</h4>"))
                  (if (not htmlp)
                      (vl-ps-seq (vl-println "")
                                 (vl-println ""))
                    ps))
       ps))
    (ss (vl-scopestack-push x ss))
    (portdecl (vl-find-portdecl name x.portdecls))
    ((mv item item-ss)
     (vl-scopestack-find-item/ss name ss))
    (ps
     (if item
      (vl-ps-seq
           (vl-when-html (vl-print-markup "<h4>"))
           (vl-basic-cw "Module item for ~s0" name)
           (vl-when-html (vl-println-markup "</h4>"))
           (vl-when-html (vl-println-markup "<div class=\"vl_src\">"))
           (if (and portdecl (not (equal item portdecl)))
               (vl-pp-portdecl portdecl)
             ps)
           (if item (case (tag item)
                          (:vl-typedef (vl-pp-typedef item))
                          (:vl-fundecl (vl-pp-fundecl item))
                          (:vl-paramdecl (vl-pp-paramdecl item))
                          (:vl-vardecl (vl-pp-vardecl item))
                          (otherwise (vl-cw "~a0" item)))
             ps)
           (vl-when-html (vl-println-markup "</div>"))
           (if (not (hons-equal item-ss ss))
               (vl-ps-seq (vl-when-html (vl-print-markup "<h5>"))
                          (vl-print " from ")
                          (vl-pp-scope-summary item-ss)
                          (vl-when-html (vl-print-markup "</h5>")))
             ps))
      (vl-ps-seq (vl-when-html (vl-print-markup "<h4>"))
                 (vl-basic-cw "No module item found for ~s0" name)
                 (vl-when-html (vl-println-markup "</h4>")))))
    (ps (if htmlp ps
          (vl-ps-seq (vl-println "")
                     (vl-println ""))))
    (ps (vl-describe-pp-assignlist name x.assigns))
    (ps (vl-describe-pp-modinsts name x.modinsts))
    (ps (vl-describe-pp-gateinsts name x.gateinsts)))
   ps)))