		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-vardecl-atts-end

Signature
(vl-pp-vardecl-atts-end x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-atts-p x).

Definitions and Theorems

Function: vl-pp-vardecl-atts-end-fn

(defun vl-pp-vardecl-atts-end-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-atts-p x)))
  (let ((__function__ 'vl-pp-vardecl-atts-end))
    (declare (ignorable __function__))
    (b* ((x (vl-atts-fix x))
         ((unless x) (vl-println ""))
         (cars (alist-keys x))
         (notes nil)
         (notes (if (member-equal "VL_IMPLICIT" cars)
                    (cons "Implicit" notes)
                  notes))
         (notes (cond ((member-equal "VL_UNUSED" cars)
                       (cons "Unused" notes))
                      ((member-equal "VL_MAYBE_UNUSED" cars)
                       (cons "Unused?" notes))
                      (t notes)))
         (notes (cond ((member-equal "VL_UNSET" cars)
                       (cons "Unset" notes))
                      ((member-equal "VL_MAYBE_UNSET" cars)
                       (cons "Unset?" notes))
                      (t notes)))
         ((unless notes) (vl-println "")))
      (vl-ps-span "vl_cmt" (vl-indent 30)
                  (vl-print "// ")
                  (vl-pp-strings-separated-by-commas notes)
                  (vl-println "")))))

Theorem: vl-pp-vardecl-atts-end-fn-of-vl-atts-fix-x

(defthm vl-pp-vardecl-atts-end-fn-of-vl-atts-fix-x
  (equal (vl-pp-vardecl-atts-end-fn (vl-atts-fix x)
                                    ps)
         (vl-pp-vardecl-atts-end-fn x ps)))

Theorem: vl-pp-vardecl-atts-end-fn-vl-atts-equiv-congruence-on-x

(defthm vl-pp-vardecl-atts-end-fn-vl-atts-equiv-congruence-on-x
  (implies (vl-atts-equiv x x-equiv)
           (equal (vl-pp-vardecl-atts-end-fn x ps)
                  (vl-pp-vardecl-atts-end-fn x-equiv ps)))
  :rule-classes :congruence)