(vl-pp-genblob-guts x ss &key (ps 'ps)) → ps
Function:
(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:
(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:
(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:
(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:
(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)