		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-modelement

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

Definitions and Theorems

Function: vl-pp-modelement-fn

(defun vl-pp-modelement-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-modelement-p x)))
 (let ((__function__ 'vl-pp-modelement))
  (declare (ignorable __function__))
  (let ((x (vl-modelement-fix x)))
   (case
       (tag x)
       (:vl-port (vl-pp-port x))
       (:vl-portdecl (vl-pp-portdecl x))
       (:vl-assign (vl-pp-assign x))
       (:vl-alias (vl-pp-alias x))
       (:vl-vardecl (vl-pp-vardecl x))
       (:vl-paramdecl (vl-pp-paramdecl x))
       (:vl-fundecl (vl-pp-fundecl x))
       (:vl-taskdecl (vl-pp-taskdecl x))
       (:vl-modinst (vl-pp-modinst x nil))
       (:vl-gateinst (vl-pp-gateinst x))
       (:vl-always (vl-pp-always x))
       (:vl-initial (vl-pp-initial x))
       (:vl-final (vl-pp-final x))
       (:vl-typedef (vl-pp-typedef x))
       (:vl-import (vl-pp-import x))
       (:vl-fwdtypedef (vl-pp-fwdtypedef x))
       (:vl-modport (vl-pp-modport x))
       (:vl-genvar (vl-pp-genvar x))
       (:vl-property (vl-pp-property x))
       (:vl-sequence (vl-pp-sequence x))
       (:vl-clkdecl (vl-pp-clkdecl x))
       (:vl-gclkdecl (vl-pp-gclkdecl x))
       (:vl-defaultdisable (vl-pp-defaultdisable x))
       (:vl-dpiimport (vl-pp-dpiimport x))
       (:vl-dpiexport (vl-pp-dpiexport x))
       (:vl-bind (vl-pp-bind x nil))
       (:vl-class (vl-pp-class x))
       (:vl-covergroup (vl-pp-covergroup x))
       (:vl-elabtask (vl-pp-elabtask x))
       (:vl-assertion (vl-pp-assertion x :include-name t))
       (:vl-cassertion (vl-pp-cassertion x :include-name t))
       (:vl-letdecl (vl-println "/* Implement LETDECL printing */"))
       (otherwise (progn$ (impossible) ps))))))

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

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

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

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