• 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-wirename

(vl-print-wirename x &key (ps 'ps)) prints a wire's name.

Signature

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

Arguments

x — Guard (stringp x).

This is much like vl-print-modname except that we use it for the names of identifiers within a module -- most commonly wire names, but we also use it for the names of blocks, module instances, and so on.

In text mode, we just print x, escaping it if necessary. In HTML mode, we print something like:

<a class="vl_wirelink" href="javascript:showWire('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 showWire function to carry out some sensible behavior.

Definitions and Theorems

Function: vl-print-wirename-fn

(defun vl-print-wirename-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (stringp x)))
 (let ((__function__ 'vl-print-wirename))
  (declare (ignorable __function__))
  (b* ((x (string-fix x)))
   (vl-ps-span
       "vl_id"
       (vl-when-html
            (vl-print-markup "<a class=\"")
            (b* ((misc (vl-ps->misc))
                 (ports (cdr (hons-assoc-equal :portnames misc))))
              (vl-print-markup (if (member-equal x (list-fix ports))
                                   "vl_wirelink_port"
                                 "vl_wirelink")))
            (vl-print-markup
                 "\" href=\"javascript:void(0);\" onClick=\"showWire('")
            (vl-print-url x)
            (vl-print-markup "')\">"))
       (vl-print-str (vl-maybe-escape-identifier x))
       (vl-when-html (vl-print-markup "</a>"))))))

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

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

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

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