• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
        • Ps
        • Basic-printing
        • Verilog-printing
          • Vl-fmt
          • Vl-ppc-module
          • Vl-pp-expr
          • Vl-maybe-escape-identifier
          • Vl-print-ext-wirename
          • Vl-pp-module
          • Vl-print-wirename
          • Vl-print-loc
          • Vl-print-modname
          • Vl-pp-origexpr
          • Vl-pps-module
          • Vl-pps-expr
          • Vl-ppc-modulelist
          • Vl-ppcs-module
          • Vl-ps-update-show-atts
          • Vl-pps-origexpr
          • Vl-pps-modulelist
          • Vl-ppcs-modulelist
          • Vl-cw-obj
          • Vl-ps->show-atts-p
          • Vl-cw
        • Printing-locally
        • Formatted-printing
        • Accessing-printed-output
        • Vl-printedlist
        • Json-printing
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Verilog-printing

Vl-print-modname

(vl-print-modname x &key (ps 'ps)) prints a module's name.

Signature

(vl-print-modname x &key (ps 'ps)) → ps

Arguments

x — Guard (stringp x).

When we are printing plain-text output, this function behaves the same as vl-print except that we may escape x if necessary; see vl-maybe-escape-identifier.

When we are printing HTML output, we print something like:

<a class="vl_modlink" href="javascript:showModule('foo')">foo</a>

This function is used in various warning messages, reports, and other displays. The module browser's web pages are responsible for defining the showModule function to carry out some sensible behavior.

Definitions and Theorems

Function: vl-print-modname-fn

(defun vl-print-modname-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (stringp x)))
 (let ((__function__ 'vl-print-modname))
  (declare (ignorable __function__))
  (vl-ps-span
   "vl_id"
   (vl-when-html
    (vl-print-markup
     "<a class=\"vl_modlink\" href=\"javascript:void(0);\" onClick=\"showModule('")
    (vl-print-url (string-fix x))
    (vl-print-markup "')\">"))
   (vl-print-str (vl-maybe-escape-identifier x))
   (vl-when-html (vl-print-markup "</a>")))))

Theorem: vl-print-modname-fn-of-str-fix-x

(defthm vl-print-modname-fn-of-str-fix-x
  (equal (vl-print-modname-fn (str-fix x) ps)
         (vl-print-modname-fn x ps)))

Theorem: vl-print-modname-fn-streqv-congruence-on-x

(defthm vl-print-modname-fn-streqv-congruence-on-x
  (implies (streqv x x-equiv)
           (equal (vl-print-modname-fn x ps)
                  (vl-print-modname-fn x-equiv ps)))
  :rule-classes :congruence)