		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-genblob-guts

Signature
(vl-pp-genblob-guts x ss &key (ps 'ps)) → ps
Arguments: x — Guard (vl-genblob-p x).; ss — Guard (vl-scopestack-p ss).

Definitions and Theorems

Function: vl-pp-genblob-guts-fn

(defun
    vl-pp-genblob-guts-fn (x ss ps)
    (declare (xargs :stobjs (ps)))
    (declare (xargs :guard (and (vl-genblob-p x)
                                (vl-scopestack-p ss))))
    (let ((__function__ 'vl-pp-genblob-guts))
         (declare (ignorable __function__))
         (b* (((vl-genblob x)))
             (vl-ps-seq (vl-pp-paramdecllist x.paramdecls)
                        (vl-pp-typedeflist x.typedefs)
                        (vl-pp-portdecllist x.portdecls)
                        (vl-pp-vardecllist x.vardecls)
                        (vl-println "")
                        (vl-pp-dpiimportlist x.dpiimports)
                        (vl-pp-dpiexportlist x.dpiexports)
                        (vl-pp-fundecllist x.fundecls)
                        (vl-pp-taskdecllist x.taskdecls)
                        (vl-pp-assignlist x.assigns)
                        (vl-pp-modinstlist x.modinsts ss)
                        (vl-pp-gateinstlist x.gateinsts)
                        (vl-pp-alwayslist x.alwayses)
                        (vl-pp-initiallist x.initials)
                        (vl-pp-finallist x.finals)
                        (vl-pp-genelementlist x.generates)
                        (vl-pp-propertylist x.properties)
                        (vl-pp-sequencelist x.sequences)
                        (vl-pp-clkdecllist x.clkdecls)
                        (vl-pp-gclkdecllist x.gclkdecls)
                        (vl-pp-defaultdisablelist x.defaultdisables)
                        (vl-pp-assertionlist x.assertions)
                        (vl-pp-cassertionlist x.cassertions)
                        (vl-pp-bindlist x.binds ss)
                        (vl-pp-classlist x.classes)
                        (vl-pp-covergrouplist x.covergroups)
                        (vl-pp-elabtasklist x.elabtasks)))))

Theorem: vl-pp-genblob-guts-fn-of-vl-genblob-fix-x

(defthm vl-pp-genblob-guts-fn-of-vl-genblob-fix-x
        (equal (vl-pp-genblob-guts-fn (vl-genblob-fix x)
                                      ss ps)
               (vl-pp-genblob-guts-fn x ss ps)))

Theorem: vl-pp-genblob-guts-fn-vl-genblob-equiv-congruence-on-x

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

Theorem: vl-pp-genblob-guts-fn-of-vl-scopestack-fix-ss

(defthm vl-pp-genblob-guts-fn-of-vl-scopestack-fix-ss
        (equal (vl-pp-genblob-guts-fn x (vl-scopestack-fix ss)
                                      ps)
               (vl-pp-genblob-guts-fn x ss ps)))

Theorem: vl-pp-genblob-guts-fn-vl-scopestack-equiv-congruence-on-ss

(defthm vl-pp-genblob-guts-fn-vl-scopestack-equiv-congruence-on-ss
        (implies (vl-scopestack-equiv ss ss-equiv)
                 (equal (vl-pp-genblob-guts-fn x ss ps)
                        (vl-pp-genblob-guts-fn x ss-equiv ps)))
        :rule-classes :congruence)