• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
        • Typo-detection
        • Vl-wireinfo-alistp
        • Vl-annotate-vardecllist-with-wireinfo
        • Vl-useset-report-entry-p
        • Vl-print-useset-report-entry
        • Vl-mark-wires-for-module
        • Vl-split-useset-report
        • Vl-annotate-vardecl-with-wireinfo
        • Vl-mark-wires-for-modinstlist
        • Vl-mark-wires-for-modinst
        • Vl-mark-wires-for-gateinstlist
        • Vl-mark-wires-for-gateinst
        • Vl-mark-wires-for-plainarg
        • Vl-wireinfo-p
        • Vl-mark-wires-for-modulelist
        • Vl-vardecllist-impexp-names
        • Vl-report-totals
        • Vl-mark-wires-for-plainarglist
        • Vl-collect-unused-or-unset-wires
        • Vl-clean-up-warning-wires
        • Vl-print-useset-report-top
        • Vl-mark-wires-for-arguments
        • Vl-useset-report-p
        • Vl-star-names-of-warning-wires
        • Vl-design-use-set-report
        • Vl-module-impexp-names
        • Vl-make-initial-wireinfo-alist
        • Vl-mark-wire-used
        • Vl-mark-wire-set
        • Vl-mark-wires-used
        • Vl-mark-wires-for-assignment
        • Vl-mark-wires-for-assignlist
        • Vl-mark-wires-set
        • Vl-print-useset-report-full-aux
        • Vl-print-typo-alist
        • Vl-print-typo-possibilities
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • Svl
    • X86isa
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Use-set

Vl-print-useset-report-entry

Print an individual entry in the use-set report.

Signature

(vl-print-useset-report-entry entry include-namep suppress-spuriousp 
                              suppress-unusedp suppress-unsetp 
                              suppress-typosp suppress-linputsp 
                              suppress-warningsp &key (ps 'ps)) 
 
  → 
ps

Arguments

entry — Guard (vl-useset-report-entry-p entry).

In HTML mode, this function is used for two purposes:

• To generate an individual report for a particular module, and
• To generate a full report covering all of the modules.

If we are dealing with a single module, we do not want to include the name of the module and a link to it, because we are already on that page, so we set include-namep to nil. On the other hand, for a full report we do want to go ahead and include the names with links.

Definitions and Theorems

Function: vl-print-useset-report-entry-fn

(defun vl-print-useset-report-entry-fn
       (entry include-namep
              suppress-spuriousp suppress-unusedp
              suppress-unsetp suppress-typosp
              suppress-linputsp suppress-warningsp ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-useset-report-entry-p entry)))
 (let ((__function__ 'vl-print-useset-report-entry))
  (declare (ignorable __function__))
  (b*
   ((htmlp (vl-ps->htmlp))
    (name (vl-useset-report-entry->name entry))
    ((when (equal name "mp_verror"))
     (vl-cw "Skipping mp_verror module~%~%"))
    (spurious (vl-useset-report-entry->spurious entry))
    (unused (vl-useset-report-entry->unused entry))
    (unset (vl-useset-report-entry->unset entry))
    (typos (vl-useset-report-entry->typos entry))
    (linputs (vl-useset-report-entry->lvalue-inputs entry))
    (num-spurious (len spurious))
    (num-unused (len unused))
    (num-unset (len unset))
    (num-linputs (len linputs))
    (warnings (vl-useset-report-entry->warnings entry))
    (warnings (vl-remove-warnings '(:vl-warn-ifxz :vl-warn-noports)
                                  warnings))
    (wwires (vl-useset-report-entry->wwires entry))
    (spurious* (vl-star-names-of-warning-wires spurious wwires))
    (unused* (vl-star-names-of-warning-wires unused wwires))
    (unset* (vl-star-names-of-warning-wires unset wwires))
    (show-linputs (and* linputs (not* suppress-linputsp)))
    (show-spurious (and* spurious (not* suppress-spuriousp)))
    (show-unused (and* unused (not* suppress-unusedp)))
    (show-unset (and* unset (not* suppress-unsetp)))
    (show-typos (and* typos (not* suppress-typosp)))
    (show-warnings (and* warnings (not* suppress-warningsp)))
    (show-anything (or* show-linputs show-spurious show-unused
                        show-unset show-typos show-warnings)))
   (if
    (not htmlp)
    (vl-ps-seq
     (if show-anything
      (vl-cw
       "Module ~s0 -- ~x1 spurious, ~x2 unused and ~x3 unset wires.~%"
       name num-spurious num-unused num-unset)
      ps)
     (if show-linputs
         (vl-ps-seq (vl-print "Inputs used like inouts: (")
                    (vl-print num-linputs)
                    (vl-println "):")
                    (vl-print-strings-with-commas linputs 3)
                    (vl-println ""))
       ps)
     (if show-spurious
         (vl-ps-seq (vl-println " Spurious wires:")
                    (vl-print-strings-with-commas spurious* 3)
                    (vl-println ""))
       ps)
     (if show-unused
         (vl-ps-seq (vl-println " Unused wires:")
                    (vl-print-strings-with-commas unused* 3)
                    (vl-println ""))
       ps)
     (if show-unset
         (vl-ps-seq (vl-println " Unset wires:")
                    (vl-print-strings-with-commas unset* 3)
                    (vl-println ""))
       ps)
     (if show-typos (vl-ps-seq (vl-println " Possible typos:")
                               (vl-print-typo-alist typos)
                               (vl-println ""))
       ps)
     (if show-warnings (vl-ps-seq (vl-println " Warnings:")
                                  (vl-print-warnings warnings)
                                  (vl-println ""))
       ps)
     (if show-anything (vl-println "") ps))
    (vl-ps-seq
     (if (not show-anything)
         ps
      (vl-ps-seq
       (vl-println-markup "<div class=\"vl_use_set_report\">")
       (vl-println-markup "<dl>")
       (if (not* include-namep)
           ps
        (vl-ps-seq
           (vl-println-markup "<dt class=\"vl_useset_report_title\">")
           (vl-print-markup "<a href=\"javascript:showModule('")
           (vl-print-url name)
           (vl-print-markup "')\">")
           (vl-print name)
           (vl-print-markup "</a></dt>")))))
     (if
      (and* show-linputs
            (or* linputs (not* include-namep)))
      (vl-ps-seq
        (vl-println-markup (if linputs "<dt class=\"vl_yes_linputs\">"
                             "<dt class=\"vl_no_linputs\">"))
        (vl-print num-linputs)
        (vl-print (if (= num-linputs 1)
                      " Input used like inout:"
                    " Inputs used like inouts:"))
        (vl-println-markup "</dt>")
        (vl-println-markup "<dd>")
        (vl-print-strings-with-commas linputs 0)
        (vl-println-markup "</dd>"))
      ps)
     (if
       (and* show-spurious
             (or* spurious (not include-namep)))
       (vl-ps-seq (vl-println-markup
                       (if spurious "<dt class=\"vl_yes_spurious\">"
                         "<dt class=\"vl_no_spurious\">"))
                  (vl-print num-spurious)
                  (vl-print " Spurious ")
                  (vl-print (if (= num-spurious 1) "Wire" "Wires"))
                  (vl-println-markup "</dt>")
                  (vl-print-markup "<dd>")
                  (vl-print-strings-with-commas spurious* 0)
                  (vl-println-markup "</dd>"))
       ps)
     (if
      (and* show-unused
            (or* unused (not include-namep)))
      (vl-ps-seq
          (vl-println-markup (if unused "<dt class=\"vl_yes_unused\">"
                               "<dt class=\"vl_no_unused\">"))
          (vl-print num-unused)
          (vl-print " Unused ")
          (vl-print (if (= num-unused 1) "Wire" "Wires"))
          (vl-println-markup "</dt>")
          (vl-print-markup "<dd>")
          (vl-print-strings-with-commas unused* 0)
          (vl-println-markup "</dd>"))
      ps)
     (if
      (and* show-unset
            (or* unset (not include-namep)))
      (vl-ps-seq
           (vl-println-markup (if unset "<dt class=\"vl_yes_unset\">"
                                "<dt class=\"vl_no_unset\">"))
           (vl-print num-unset)
           (vl-print " Unset ")
           (vl-print (if (= num-unset 1) "Wire" "Wires"))
           (vl-println-markup "</dt>")
           (vl-print-markup "<dd>")
           (vl-print-strings-with-commas unset* 0)
           (vl-println-markup "</dd>"))
      ps)
     (if (or* (not show-typos) (not typos))
         ps
       (vl-ps-seq
            (vl-println-markup
                 "<dt class=\"vl_yes_typos\">Possible Typos</dt>")
            (vl-println-markup "<dd><ul class=\"typo_list\">")
            (vl-print-typo-alist typos)
            (vl-println-markup "</ul></dd>")))
     (if (and* show-warnings warnings)
         (vl-print-warnings warnings)
       ps)
     (if show-anything (vl-println-markup "</div>")
       ps))))))