		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-propspec

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

Definitions and Theorems

Function: vl-pp-propspec-fn

(defun vl-pp-propspec-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-propspec-p x)))
 (let ((__function__ 'vl-pp-propspec))
  (declare (ignorable __function__))
  (b* (((vl-propspec x)) (col (vl-ps->col)))
   (vl-ps-seq
      (if (consp x.evatoms)
          (vl-ps-seq (vl-print "@(")
                     (vl-pp-evatomlist x.evatoms)
                     (vl-println ")")
                     (if x.disable (vl-indent col) ps))
        ps)
      (if x.disable
          (vl-ps-seq (vl-ps-span "vl_key" (vl-print "disable iff "))
                     (vl-pp-exprdist x.disable)
                     (vl-println ""))
        ps)
      (if (or x.evatoms x.disable)
          (vl-indent (+ (vl-ps->autowrap-ind) 2))
        ps)
      (vl-pp-propexpr x.prop)))))

Theorem: vl-pp-propspec-fn-of-vl-propspec-fix-x

(defthm vl-pp-propspec-fn-of-vl-propspec-fix-x
  (equal (vl-pp-propspec-fn (vl-propspec-fix x)
                            ps)
         (vl-pp-propspec-fn x ps)))

Theorem: vl-pp-propspec-fn-vl-propspec-equiv-congruence-on-x

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