		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-modulename-link

Signature
(vl-pp-modulename-link name ss &key (ps 'ps)) → ps
Arguments: name — Guard (stringp name).; ss — Guard (vl-scopestack-p ss).

Definitions and Theorems

Function: vl-pp-modulename-link-fn

(defun vl-pp-modulename-link-fn (name ss ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (and (stringp name)
                             (vl-scopestack-p ss))))
 (let ((__function__ 'vl-pp-modulename-link))
   (declare (ignorable __function__))
   (b*
    ((name (string-fix name))
     (def (vl-scopestack-find-definition name ss))
     ((unless def)
      (prog2$ (cw "Warning: instance of undefined module ~s0?~%"
                  name)
              (vl-print-modname name)))
     ((unless (eq (tag def) :vl-module))
      (prog2$
           (cw "Warning: module instance of non-module ~s0? (~s1)~%"
               name (tag def))
           (vl-print-modname name)))
     (origname (vl-module->origname def)))
    (vl-pp-modulename-link-aux name origname))))

Theorem: vl-pp-modulename-link-fn-of-str-fix-name

(defthm vl-pp-modulename-link-fn-of-str-fix-name
  (equal (vl-pp-modulename-link-fn (str-fix name)
                                   ss ps)
         (vl-pp-modulename-link-fn name ss ps)))

Theorem: vl-pp-modulename-link-fn-streqv-congruence-on-name

(defthm vl-pp-modulename-link-fn-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-pp-modulename-link-fn name ss ps)
                  (vl-pp-modulename-link-fn name-equiv ss ps)))
  :rule-classes :congruence)

Theorem: vl-pp-modulename-link-fn-of-vl-scopestack-fix-ss

(defthm vl-pp-modulename-link-fn-of-vl-scopestack-fix-ss
  (equal (vl-pp-modulename-link-fn name (vl-scopestack-fix ss)
                                   ps)
         (vl-pp-modulename-link-fn name ss ps)))

Theorem: vl-pp-modulename-link-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
      vl-pp-modulename-link-fn-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-pp-modulename-link-fn name ss ps)
                  (vl-pp-modulename-link-fn name ss-equiv ps)))
  :rule-classes :congruence)