		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-gateinst-atts-begin

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

Definitions and Theorems

Function: vl-pp-gateinst-atts-begin-fn

(defun vl-pp-gateinst-atts-begin-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-atts-p x)))
 (let ((__function__ 'vl-pp-gateinst-atts-begin))
  (declare (ignorable __function__))
  (b*
   ((x (vl-atts-fix x))
    ((unless x) ps)
    ((when (and (tuplep 1 x)
                (equal (caar x) "VL_FOR")))
     (b*
      ((val (cdar x))
       (str
        (and
            val
            (vl-expr-case
                 val
                 :vl-literal (vl-value-case val.val
                                            :vl-string val.val.value
                                            :otherwise nil)
                 :otherwise nil)))
       ((unless str)
        (prog2$ (raise "Expected VL_FOR to contain a string.")
                ps)))
      (vl-ps-span "vl_cmt" (vl-println "")
                  (vl-progindent)
                  (vl-print "/* For ")
                  (vl-print-str str)
                  (vl-println " */")))))
   (vl-ps-seq (vl-println "")
              (vl-progindent)
              (vl-pp-atts x)
              (vl-println "")))))

Theorem: vl-pp-gateinst-atts-begin-fn-of-vl-atts-fix-x

(defthm vl-pp-gateinst-atts-begin-fn-of-vl-atts-fix-x
  (equal (vl-pp-gateinst-atts-begin-fn (vl-atts-fix x)
                                       ps)
         (vl-pp-gateinst-atts-begin-fn x ps)))

Theorem: vl-pp-gateinst-atts-begin-fn-vl-atts-equiv-congruence-on-x

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